Nilpotence of upper-unitriangular group points

The convolution points of the coordinate Hopf algebra of U_n are naturally equivalent to the ordinary upper-unitriangular matrix group. The matrix group is nilpotent over every commutative ring, so this equivalence makes every value of the represented group functor nilpotent, and hence solvable.

Main declarations

• TauCeti.UpperUnitriangular.isNilpotent_points: every group of algebra-valued points of U_n is nilpotent.
• TauCeti.UpperUnitriangular.isSolvable_points: every such point group is solvable.

References

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

This is the upper-unitriangular case of the solvability target in Layer 5 of the ReductiveGroups roadmap. Once the upper-unitriangular embedding characterization is complete, subgroup closure transfers this result to every smooth connected unipotent affine group.

theorem TauCeti.UpperUnitriangular.isNilpotent_points (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] (A : Type w) [CommRing A] [Algebra R A] : Group.IsNilpotent (WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A))

The group of A-valued points of U_n is nilpotent.

theorem TauCeti.UpperUnitriangular.isSolvable_points (R : Type u) [CommRing R] (m : Type v) [Fintype m] [LinearOrder m] (A : Type w) [CommRing A] [Algebra R A] : Group.IsSolvable (WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A))

The group of A-valued points of U_n is solvable.