Solvability of geometrically unipotent affine groups

A finite-type affine group admits a faithful finite-dimensional comodule. If all its geometric points are unipotent, their induced operators on this comodule are unipotent. Kolchin's theorem then embeds the geometric point group in an upper-unitriangular matrix group, proving that it is solvable.

Main declaration

• TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.geometricallySolvable: a geometrically unipotent finite-type affine group has a solvable group of geometric points.

References

• A. Borel, Linear Algebraic Groups, §4.8, Theorem, whose "in particular, G is a nilpotent group" is the classical form of what is proved here.
• T. A. Springer, Linear Algebraic Groups, Corollary 2.4.13: a unipotent linear algebraic group is nilpotent, hence solvable.

This completes the point-group solvability implication needed in Layer 5 of the ReductiveGroups roadmap.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.geometricallySolvable {k H : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] (hH : geometricallyUnipotentPointsCommHopfAlgProperty k ↧H) : geometricallySolvablePointsCommHopfAlgProperty k ↧H

A geometrically unipotent finite-type affine group has a solvable group of geometric points.

No reducedness hypothesis is needed: faithfulness is used only to inject the abstract geometric point group into its linear action, while Kolchin's theorem simultaneously upper-unitriangularizes that action.