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.

The block-triangularity of the matrix of an endomorphism in a basis adapted to an invariant submodule is TauCeti.toMatrixAlgEquiv_extensionBasis_isUpperUnitriangular, in TauCeti.LinearAlgebra.ExtensionBasis.

Main declarations

• Representation.isNilpotent_quotient_sub_one: unipotent operators stay unipotent on the quotient by an invariant submodule.
• 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.isNilpotent_quotient_sub_one {R : Type u_1} {G : Type u_2} {V : Type u_3} [Ring R] [Monoid G] [AddCommGroup V] [Module R V] (rho : Representation R G V) (p : Submodule R V) (hp : ∀ (g : G), p ≤ Submodule.comap (rho g) p) {g : G} (hg : IsNilpotent (rho g - 1)) : IsNilpotent ((rho.quotient p hp) g - 1)

If rho g - 1 is nilpotent, then so is the operator rho.quotient p hp g - 1 induced on the quotient of the representation rho by an invariant submodule p.

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)) : Group.IsSolvable G

A group admitting a faithful finite-dimensional representation by unipotent operators is solvable.