The center of an affine group scheme

Let H be a commutative Hopf algebra over a field k. This file constructs the center of Spec H as a closed subgroup scheme. The defining equations are the coefficients, in the second tensor factor, of the cocommutativity defect

  Δ(x) - τ(Δ(x)).

A point kills these coefficients exactly when it commutes universally with every point of the group. Since universally central points contain the identity and are closed under products and inverses, the coefficient ideal is a Hopf ideal. Its quotient therefore represents the center.

The coefficient presentation uses a chosen vector-space basis only inside the construction. The public universal property characterizes the resulting Hopf ideal as the smallest central Hopf ideal, so the represented closed subgroup is canonical.

Main declarations

• TauCeti.CommHopfAlgCat.centerDefiningIdeal: the Hopf ideal cutting out the center.
• TauCeti.CommHopfAlgCat.centerCoordinateHopfAlgebra: the coordinate Hopf algebra of the center.
• TauCeti.CommHopfAlgCat.centerGroupScheme: the center as a closed affine group scheme.
• TauCeti.CommHopfAlgCat.mem_centerPointsSubgroup_iff: its points are exactly the universally central points.
• TauCeti.CommHopfAlgCat.centerDefiningIdeal_eq_augmentation_iff_forall_isCentralPoint_eq_one: the center is trivial exactly when every universally central algebra-valued point is the identity.
• TauCeti.CommHopfAlgCat.centerDefiningIdeal_le_iff: the center contains every central closed subgroup scheme.

References

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

noncomputable def TauCeti.CommHopfAlgCat.centerDefiningIdeal {k : Type u} [Field k] (H : CommHopfAlgCat k) : HopfIdeal k ↑H

The Hopf ideal cutting out the center of an affine group scheme.

Its quotient represents the universally central points of the group functor. The construction uses coefficients in a chosen vector-space basis internally; centerDefiningIdeal_le_iff characterizes it without that choice.

Equations

• TauCeti.CommHopfAlgCat.centerDefiningIdeal H = TauCeti.CommHopfAlgCat.centerCoefficientHopfIdeal✝

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.centerCoordinateHopfAlgebra {k : Type u} [Field k] (H : CommHopfAlgCat k) : CommHopfAlgCat k

The coordinate Hopf algebra of the center of an affine group.

Equations

• TauCeti.CommHopfAlgCat.centerCoordinateHopfAlgebra H = TauCeti.CommHopfAlgCat.quotient H (TauCeti.CommHopfAlgCat.centerDefiningIdeal H)

theorem TauCeti.CommHopfAlgCat.isCentral_centerDefiningIdeal {k : Type u} [Field k] (H : CommHopfAlgCat k) : (centerDefiningIdeal H).IsCentral

The Hopf ideal defining the center is central.

@[simp]

theorem TauCeti.CommHopfAlgCat.centerDefiningIdeal_le_iff {k : Type u} [Field k] (H : CommHopfAlgCat k) (I : HopfIdeal k ↑H) : centerDefiningIdeal H ≤ I ↔ I.IsCentral

The center ideal is the smallest central Hopf ideal. Equivalently, every central closed subgroup scheme of Spec H factors through the center.

@[simp]

theorem TauCeti.CommHopfAlgCat.centerDefiningIdeal_eq_bot_iff_isCocomm {k : Type u} [Field k] (H : CommHopfAlgCat k) : centerDefiningIdeal H = ⊥ ↔ Coalgebra.IsCocomm k ↑H

The center is the whole group exactly when the coordinate Hopf algebra is cocommutative.

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.centerPointsSubgroup {k : Type u} [Field k] (H : CommHopfAlgCat k) (A : CommAlgCat k) : Subgroup ↑(HopfAlgebra.points A)

The subgroup of algebra-valued points cut out by the center ideal.

Equations

• TauCeti.CommHopfAlgCat.centerPointsSubgroup H A = TauCeti.CommHopfAlgCat.quotientPointsSubgroup H (TauCeti.CommHopfAlgCat.centerDefiningIdeal H) A

@[simp]

theorem TauCeti.CommHopfAlgCat.mem_centerPointsSubgroup_iff {k : Type u} [Field k] (H : CommHopfAlgCat k) (A : CommAlgCat k) (g : ↑(HopfAlgebra.points A)) : g ∈ centerPointsSubgroup H A ↔ HopfAlgebra.IsCentralPoint g

Membership in the represented center is universal centrality in the functor of points.

theorem TauCeti.CommHopfAlgCat.centerDefiningIdeal_eq_augmentation_iff_forall_isCentralPoint_eq_one {k : Type u} [Field k] (H : CommHopfAlgCat k) : centerDefiningIdeal H = HopfIdeal.augmentation k ↑H ↔ ∀ (A : CommAlgCat k) (g : ↑(HopfAlgebra.points A)), HopfAlgebra.IsCentralPoint g → g = 1

Triviality of the represented center can be tested on all algebra-valued points.

theorem TauCeti.CommHopfAlgCat.centerPointsSubgroup_eq_center {k : Type u} [Field k] (H : CommHopfAlgCat k) (A : CommAlgCat k) : centerPointsSubgroup H A = HopfAlgebra.center k ↑H ↑A

The represented center agrees with the center previously defined directly on the functor of points.

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.centerGroupScheme {k : Type u} [Field k] (H : CommHopfAlgCat k) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))

The center of an affine group scheme, represented by the quotient by its center ideal.

Equations

• TauCeti.CommHopfAlgCat.centerGroupScheme H = TauCeti.CommHopfAlgCat.quotientSpec H (TauCeti.CommHopfAlgCat.centerDefiningIdeal H)

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.centerGroupSchemeι {k : Type u} [Field k] (H : CommHopfAlgCat k) : centerGroupScheme H ⟶ (AlgebraicGeometry.hopfSpec ↧k).obj (Opposite.op H)

The canonical inclusion of the center into the ambient affine group scheme.

Equations

• TauCeti.CommHopfAlgCat.centerGroupSchemeι H = TauCeti.CommHopfAlgCat.quotientSpecι H (TauCeti.CommHopfAlgCat.centerDefiningIdeal H)

instance TauCeti.CommHopfAlgCat.isClosedImmersion_centerGroupSchemeι {k : Type u} [Field k] (H : CommHopfAlgCat k) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (centerGroupSchemeι H).hom.hom)

The center is a closed subgroup scheme of the ambient affine group scheme.

noncomputable def TauCeti.CommHopfAlgCat.centralSubgroupToCenter {k : Type u} [Field k] (H : CommHopfAlgCat k) (I : HopfIdeal k ↑H) (hI : I.IsCentral) : quotientSpec H I ⟶ centerGroupScheme H

A central closed subgroup scheme cut out by I includes canonically into the center.

Equations

• TauCeti.CommHopfAlgCat.centralSubgroupToCenter H I hI = TauCeti.CommHopfAlgCat.quotientSpecMapOfLe H ⋯

@[simp]

theorem TauCeti.CommHopfAlgCat.centralSubgroupToCenter_comp_centerGroupSchemeι {k : Type u} [Field k] (H : CommHopfAlgCat k) (I : HopfIdeal k ↑H) (hI : I.IsCentral) : CategoryTheory.CategoryStruct.comp (centralSubgroupToCenter H I hI) (centerGroupSchemeι H) = quotientSpecι H I

Including a central subgroup through the center and then into the ambient group recovers its original closed-subgroup inclusion.

instance TauCeti.CommHopfAlgCat.isClosedImmersion_centralSubgroupToCenter {k : Type u} [Field k] (H : CommHopfAlgCat k) (I : HopfIdeal k ↑H) (hI : I.IsCentral) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (centralSubgroupToCenter H I hI).hom.hom)

The inclusion of a central closed subgroup into the center is a closed immersion.