Solvability of upper-triangular general linear groups

The diagonal quotient of the upper-triangular group is abelian, while its kernel is the nilpotent upper-unitriangular group. Hence every upper-triangular general linear group over a commutative ring is solvable.

This advances the "Lie--Kolchin; solvable groups" milestone in Layer 5 of the ReductiveGroups roadmap. It supplies the abstract solvability input for the upper-triangular subgroup scheme in TauCeti.Algebra.AlgebraicGroup.Solvable.UpperTriangular.

Main declaration

• TauCeti.UpperTriangularGroup.instIsSolvable: upper-triangular general linear groups are solvable.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• T. A. Springer, Linear Algebraic Groups, §2.4.

instance TauCeti.UpperTriangularGroup.instIsSolvable (m : Type u_1) [Fintype m] [LinearOrder m] (R : Type u) [CommRing R] : Group.IsSolvable ↥(upperTriangularGroup m R)

The upper-triangular subgroup of GL_m(R) is solvable over every commutative ring.