Semisimple points and closed subgroups of groups of multiplicative type

A finite-type affine group over a field is of multiplicative type when its coordinate Hopf algebra becomes diagonalizable after extension to an algebraic closure. Every point of a diagonalizable group is semisimple, so the geometric fibre of a group of multiplicative type has only semisimple geometric points. The same is true for every closed subgroup of that geometric fibre, represented contravariantly by a Hopf quotient.

This is the semisimple-point input for comparing groups of multiplicative type with unipotent groups. In particular, a reduced unipotent closed subgroup of the geometric fibre of a group of multiplicative type is trivial.

Main declarations

• TauCeti.multiplicativeTypeCommHopfAlgProperty.geometricFiberSemisimplePoints: the geometric fibre of a group of multiplicative type has only semisimple geometric points.
• TauCeti.multiplicativeTypeCommHopfAlgProperty.geometricFiberQuotientSemisimplePoints: every closed subgroup of the geometric fibre has only semisimple geometric points.
• TauCeti.multiplicativeTypeCommHopfAlgProperty.eq_augmentation_of_geometricallyUnipotent: a reduced unipotent closed subgroup of the geometric fibre is trivial.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 12.40.
• T. A. Springer, Linear Algebraic Groups, §2.4.

This advances Layer 4, "Diagonalizable groups and groups of multiplicative type", and supplies a prerequisite for the torus worked example in Layer 6 of the ReductiveGroups roadmap.

theorem TauCeti.multiplicativeTypeCommHopfAlgProperty.geometricFiberSemisimplePoints (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (hH : multiplicativeTypeCommHopfAlgProperty k H) : geometricallySemisimplePointsCommHopfAlgProperty (AlgebraicClosure k) H.baseChange.obj

The geometric fibre of a finite-type group of multiplicative type has only semisimple geometric points.

theorem TauCeti.multiplicativeTypeCommHopfAlgProperty.geometricFiberQuotientSemisimplePoints (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (hH : multiplicativeTypeCommHopfAlgProperty k H) (I : HopfIdeal (AlgebraicClosure k) ↑H.baseChange.obj) : geometricallySemisimplePointsCommHopfAlgProperty (AlgebraicClosure k) (H.baseChange.quotient I).obj

Every closed subgroup of the geometric fibre of a group of multiplicative type has only semisimple geometric points. The subgroup is represented contravariantly by a Hopf quotient.

theorem TauCeti.multiplicativeTypeCommHopfAlgProperty.eq_augmentation_of_geometricallyUnipotent (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (hH : multiplicativeTypeCommHopfAlgProperty k H) (I : HopfIdeal (AlgebraicClosure k) ↑H.baseChange.obj) [IsReduced ↑(H.baseChange.quotient I).obj] (hI : geometricallyUnipotentPointsCommHopfAlgProperty (AlgebraicClosure k) (H.baseChange.quotient I).obj) : I = HopfIdeal.augmentation (AlgebraicClosure k) ↑H.baseChange.obj

A reduced closed subgroup of the geometric fibre of a group of multiplicative type is trivial if all of its geometric points are unipotent. Equivalently, its defining Hopf ideal is the augmentation ideal.

Reducedness cannot be omitted: nonreduced infinitesimal groups are invisible to geometric points.