Central closed subgroup schemes are commutative

A central Hopf ideal cuts out a commutative closed subgroup scheme. The coordinate quotient is cocommutative by HopfIdeal.IsCentral.isCocomm_quotient, so its Hopf spectrum carries a commutative group-object structure on the canonical Hopf-ideal quotient spectrum.

Main declarations

• TauCeti.HopfIdeal.IsCentral.isCommMonObj_quotientSpec: the canonical quotient group scheme of a central Hopf ideal is a commutative group object.

References

• J. S. Milne, Algebraic Groups (2017), Sections 1.k and 2.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapter 2.

This supplies a structural property of central closed subgroups used by the center in Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap.

theorem TauCeti.HopfIdeal.IsCentral.isCommMonObj_quotientSpec {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {I : HopfIdeal R ↑H} (hI : I.IsCentral) : CategoryTheory.IsCommMonObj (CommHopfAlgCat.quotientSpec H I).X

The canonical quotient group scheme of a central Hopf ideal is a commutative group object.