Solvability of faithful unipotent representations #
Kolchin's common fixed-vector theorem constructs a complete invariant flag for a finite-dimensional representation whose every operator is unipotent. Relative to a basis adapted to this flag, every representing matrix is upper unitriangular. Consequently a group admitting a faithful representation of this kind embeds in an upper-unitriangular matrix group and is solvable.
Main declarations #
Representation.exists_basis_isUpperUnitriangular_of_isUnipotent: simultaneous upper-unitriangularization of a unipotent monoid representation.Representation.isSolvable_of_injective_of_isUnipotent: a group with a faithful finite-dimensional unipotent representation is solvable.
References #
- A. Borel, Linear Algebraic Groups, Proposition 4.8.
- T. A. Springer, Linear Algebraic Groups, Section 2.4.
This supplies the Lie--Kolchin solvability step in Layer 5 of the ReductiveGroups roadmap.
theorem
Representation.exists_basis_isUpperUnitriangular_of_isUnipotent
{K : Type u}
{G : Type w}
{V : Type v}
[Field K]
[AddCommGroup V]
[Module K V]
[Monoid G]
[FiniteDimensional K V]
(rho : Representation K G V)
(hunipotent : ∀ (g : G), IsNilpotent (rho g - 1))
:
∃ (n : ℕ) (b : Module.Basis (Fin n) K V), ∀ (g : G), ((LinearMap.toMatrixAlgEquiv b) (rho g)).IsUpperUnitriangular
A finite-dimensional monoid representation by unipotent operators has a basis in which all representing matrices are upper unitriangular.
theorem
Representation.isSolvable_of_injective_of_isUnipotent
{K : Type u}
{G : Type w}
{V : Type v}
[Field K]
[AddCommGroup V]
[Module K V]
[Group G]
[FiniteDimensional K V]
(rho : Representation K G V)
(hinjective : Function.Injective ⇑rho.asGroupHom)
(hunipotent : ∀ (g : G), IsNilpotent (rho g - 1))
:
A group admitting a faithful finite-dimensional representation by unipotent operators is solvable.