Solvable reductive groups are tori

A reductive group with solvable geometric points is a torus, over every field and in every characteristic. The torus need not split over the ground field.

Pass to the geometric fibre G over an algebraic closure. It is smooth and connected, and it is commutative by TauCeti.reductiveCommHopfAlgProperty.isCocomm_of_geometricallySolvable. For a reduced connected commutative group, the unipotent radical is the closed unipotent Jordan factor, whose rational points are exactly the unipotent points (TauCeti.HopfAlgebra.Point.mem_quotientPointsSubgroup_unipotentRadical_iff). Reductivity makes this radical trivial, so the unipotent part of every rational point of G is the identity: every point is semisimple. The diagonalization criterion TauCeti.torusCommHopfAlgProperty_of_isSemisimplePoint then identifies G as a split torus.

Consequently such a group is linearly reductive.

Main declarations

• TauCeti.reductiveCommHopfAlgProperty.torus_of_geometricallySolvable: a solvable reductive group is a torus.
• TauCeti.reductiveCommHopfAlgProperty.linearlyReductive_of_geometricallySolvable: a solvable reductive group is linearly reductive.

References

• A. Borel, Linear Algebraic Groups, 2nd ed. (1991), §§4.7, 10.6 and 11.5.
• J. S. Milne, Algebraic Groups (2017), Theorem 16.13 and Chapter 19.

theorem TauCeti.reductiveCommHopfAlgProperty.torus_of_geometricallySolvable {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : reductiveCommHopfAlgProperty k H) (hsolv : geometricallySolvablePointsCommHopfAlgProperty k H.obj) : torusCommHopfAlgProperty k H

A reductive group with solvable geometric points is a torus, over every field and in every characteristic. The torus need not split over the ground field.

theorem TauCeti.reductiveCommHopfAlgProperty.linearlyReductive_of_geometricallySolvable {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : reductiveCommHopfAlgProperty k H) (hsolv : geometricallySolvablePointsCommHopfAlgProperty k H.obj) : linearlyReductiveCommHopfAlgProperty k H.obj

A reductive group with solvable geometric points is linearly reductive, in every characteristic and including when its torus does not split over the ground field.