The center is commutative

The center of an affine group scheme is a commutative group scheme. On coordinate Hopf algebras, this says that the quotient by centerDefiningIdeal is cocommutative. The result follows from the more general fact that the coordinate Hopf algebra of every central closed subgroup is cocommutative.

The cocommutativity result supplies the commutative-group-object structure on the Hopf spectrum, registered here on the canonical centerGroupScheme and bundled as centerCommGroupScheme.

Main declarations

• TauCeti.CommHopfAlgCat.isCocomm_quotient_centerDefiningIdeal: the coordinate Hopf algebra of the center is cocommutative.
• TauCeti.CommHopfAlgCat.isCommMonObj_centerGroupScheme: the canonical center group scheme is a commutative group object.
• TauCeti.CommHopfAlgCat.centerCommGroupScheme: the center bundled as a commutative group scheme.
• TauCeti.CommHopfAlgCat.centerCommGroupScheme_toGrp: its underlying group scheme is the canonical center group scheme.

References

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

instance TauCeti.CommHopfAlgCat.isCocomm_quotient_centerDefiningIdeal {k : Type u} [Field k] (H : CommHopfAlgCat k) : Coalgebra.IsCocomm k ↑(quotient H (centerDefiningIdeal H))

The coordinate Hopf algebra of the center is cocommutative.

instance TauCeti.CommHopfAlgCat.isCommMonObj_centerGroupScheme {k : Type u} [Field k] (H : CommHopfAlgCat k) : CategoryTheory.IsCommMonObj (centerGroupScheme H).X

The canonical center group scheme is a commutative group object.

noncomputable def TauCeti.CommHopfAlgCat.centerCommGroupScheme {k : Type u} [Field k] (H : CommHopfAlgCat k) : CategoryTheory.CommGrp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))

The center of an affine group scheme, bundled as a commutative group scheme.

Equations

• TauCeti.CommHopfAlgCat.centerCommGroupScheme H = { X := (TauCeti.CommHopfAlgCat.centerGroupScheme H).X, grp := (TauCeti.CommHopfAlgCat.centerGroupScheme H).grp, comm := ⋯ }

@[simp]

theorem TauCeti.CommHopfAlgCat.centerCommGroupScheme_toGrp {k : Type u} [Field k] (H : CommHopfAlgCat k) : (centerCommGroupScheme H).toGrp = centerGroupScheme H

The underlying group scheme of the bundled commutative center is the canonical center.