Geometric solvability of upper-triangular general linear groups

Over a field, the geometric points of the upper-triangular subgroup scheme are solvable: its points are identified with the abstract upper-triangular matrix group, whose diagonal quotient is abelian and whose upper-unitriangular kernel is nilpotent.

Main declarations

• isSolvable_points: every algebra-valued point group is solvable.
• geometricallySolvablePointsCommHopfAlgProperty_coordinateHopfAlgebra: the upper-triangular affine group has solvable geometric points.

References

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

This advances Layer 5, "Lie--Kolchin; solvable groups", of the ReductiveGroups roadmap.

theorem TauCeti.GeneralLinear.UpperTriangular.isSolvable_points (R : Type u) [CommRing R] (A : Type u_1) [CommRing A] [Algebra R A] (n : ℕ) : Group.IsSolvable ↑(HopfAlgebra.points (CommAlgCat.of R A))

Every algebra-valued point group of the upper-triangular affine group is solvable.

theorem TauCeti.GeneralLinear.UpperTriangular.geometricallySolvablePointsCommHopfAlgProperty_coordinateHopfAlgebra (k : Type u) [Field k] (n : ℕ) : geometricallySolvablePointsCommHopfAlgProperty k (coordinateHopfAlgebra k n)

The upper-triangular affine group has a solvable group of geometric points.