Closed subgroups of diagonalizable affine groups

A finite-type commutative Hopf algebra over a field is the coordinate algebra of a diagonalizable group exactly when its group-like elements span it. This condition passes to a Hopf quotient: the quotient morphism is surjective and sends every group-like element to a group-like element, so the images of the original spanning family span the quotient.

Contravariantly, a Hopf ideal cuts out a closed subgroup of the represented affine group. Thus the main result is the coordinate-algebra form of the fact that every closed subgroup of a diagonalizable affine group is diagonalizable.

Main declarations

• TauCeti.DiagonalizableGroup.groupLikeSpannedProperty.of_surjective: a surjective morphism of finite-type commutative Hopf algebras preserves the diagonalizable coordinate property.
• TauCeti.DiagonalizableGroup.groupLikeSpannedProperty.quotient: every Hopf quotient of a diagonalizable coordinate algebra is again diagonalizable.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 12.9.

This advances Layer 4, "Diagonalizable groups and groups of multiplicative type", of the ReductiveGroups roadmap. It also supplies the closed-subgroup classification used in Layer 6 to show that smooth unipotent closed subgroups of tori are trivial, on the way to proving that tori are reductive.

theorem TauCeti.DiagonalizableGroup.groupLikeSpannedProperty.of_surjective (k : Type u) [Field k] (H K : FiniteTypeCommHopfAlgCat k) (f : H ⟶ K) (hf : Function.Surjective ⇑(FiniteTypeCommHopfAlgCat.toBialgHom f)) (hH : groupLikeSpannedProperty k H) : groupLikeSpannedProperty k K

A surjective morphism of finite-type commutative Hopf algebras preserves spanning by group-like elements. Contravariantly, this is closure of diagonalizable affine groups under closed subgroups presented by a surjective coordinate morphism.

theorem TauCeti.DiagonalizableGroup.groupLikeSpannedProperty.quotient (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (I : HopfIdeal k ↑H.obj) (hH : groupLikeSpannedProperty k H) : groupLikeSpannedProperty k (H.quotient I)

Every Hopf quotient of a finite-type diagonalizable coordinate algebra is again a diagonalizable coordinate algebra. Contravariantly, every closed subgroup cut out by a Hopf ideal in a diagonalizable affine group is diagonalizable.