Central closed subgroup schemes

A closed subgroup of the affine group scheme Spec H is cut out by a Hopf ideal I, and it is central when conjugating by its points does nothing. This file states that condition on I, in the same coordinate style as normality: the coordinate morphism of conjugation agrees with the second projection modulo I ⊗ H, the ideal of V(I) × G.

The condition is proved equivalent to the functorial one, that every point of V(I) is a central point of G in the sense of TauCeti.HopfAlgebra.IsCentralPoint. As for normality, one value algebra suffices to detect it, namely (H ⧸ I) ⊗[R] H, which carries the tautological point of the subgroup together with the tautological point of the ambient group.

The main consequences record that the notion behaves as expected. Centrality is preserved by pullback along a bijective bialgebra morphism, a central Hopf ideal is normal, its closed subgroup has commutative point groups and cocommutative coordinate quotient, and the zero Hopf ideal — the one cutting out the whole group — is central exactly when H is cocommutative, that is, exactly when G is commutative.

Centrality is upward closed in the lattice of Hopf ideals, since a larger Hopf ideal cuts out a smaller closed subgroup. It is not closed downwards, so this file does not construct a smallest central Hopf ideal; the center Z(G) as a closed subgroup scheme needs the extra work of producing a Hopf ideal from the cocommutativity defect of H.

Main declarations

• TauCeti.HopfIdeal.IsCentral: centrality of a Hopf ideal, that is, of the closed subgroup scheme it cuts out.

Main results

• TauCeti.CommHopfAlgCat.isCentral_iff_forall_isCentralPoint: a Hopf ideal is central exactly when the points it cuts out are central points over every value algebra.
• TauCeti.HopfIdeal.IsCentral.comapOfSurjective_of_bijective: centrality is preserved by pullback along a bijective bialgebra morphism.
• TauCeti.HopfIdeal.IsCentral.isNormal: a central Hopf ideal is normal.
• TauCeti.HopfIdeal.IsCentral.isCocomm_quotient: the coordinate Hopf algebra of a central closed subgroup is cocommutative.
• TauCeti.HopfIdeal.isCentral_bot_iff_isCocomm: the whole group is central exactly when the coordinate Hopf algebra is cocommutative.
• TauCeti.CommHopfAlgCat.isCentral_augmentation: the trivial subgroup is central.

References

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

The coordinate condition is the conjugation-triviality criterion for a central closed subgroup, and mirrors the normality criterion of TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Normal.Basic. This is a prerequisite for the center Z(G) in Layer 6, "Reductive and semisimple groups", of TauCetiRoadmap/ReductiveGroups/README.md.

def TauCeti.HopfIdeal.IsCentral {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (I : HopfIdeal R H) : Prop

A Hopf ideal is central when the coordinate morphism of conjugation agrees with the inclusion of the acted-on variable modulo I ⊗ H.

The first tensor factor of TauCeti.HopfAlgebra.conjugationAlgHom is the conjugating variable, so the left tensor ideal is the ideal of V(I) × G: the condition says that conjugating an arbitrary point of G by a point of the closed subgroup V(I) leaves it unchanged.

Equations

• I.IsCentral = ∀ (x : H), TauCeti.HopfAlgebra.conjugationAlgHom x - Algebra.TensorProduct.includeRight x ∈ TauCeti.HopfIdeal.leftTensorIdeal R H I.toIdeal

theorem TauCeti.HopfIdeal.IsCentral.mono {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] {I J : HopfIdeal R H} (hI : I.IsCentral) (hIJ : I ≤ J) : J.IsCentral

Centrality passes to larger Hopf ideals, which cut out smaller closed subgroups.

theorem TauCeti.HopfIdeal.isCentral_iSup_of_isCentral {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] {ι : Sort u_1} {I : ι → HopfIdeal R H} {j : ι} (hj : (I j).IsCentral) : (⨆ (i : ι), I i).IsCentral

A supremum of Hopf ideals is central as soon as one of them is; the closed subgroup it cuts out is contained in the central one.

theorem TauCeti.HopfIdeal.isCentral_bot_iff_isCocomm {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] : ⊥.IsCentral ↔ Coalgebra.IsCocomm R H

The whole group is central exactly when its coordinate Hopf algebra is cocommutative. The zero Hopf ideal cuts out all of Spec H, so its centrality says that conjugation is trivial, which for the convolution group of points is commutativity.

theorem TauCeti.CommHopfAlgCat.isCentralPoint_of_mem_quotientPointsSubgroup {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsCentral) (A : CommAlgCat R) {g : ↑(HopfAlgebra.points A)} (hg : g ∈ quotientPointsSubgroup H I A) : HopfAlgebra.IsCentralPoint g

Every point cut out by a central Hopf ideal is a central point of the ambient group, over every value algebra.

theorem TauCeti.CommHopfAlgCat.isCentral_iff_forall_isCentralPoint {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) : I.IsCentral ↔ ∀ (A : CommAlgCat R), ∀ g ∈ quotientPointsSubgroup H I A, HopfAlgebra.IsCentralPoint g

A Hopf ideal is central exactly when it cuts out central points over every value algebra.

theorem TauCeti.CommHopfAlgCat.quotientPointsSubgroup_le_center {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsCentral) (A : CommAlgCat R) : quotientPointsSubgroup H I A ≤ HopfAlgebra.center R ↑H ↑A

The points cut out by a central Hopf ideal lie in the center of the functor of points.

theorem TauCeti.CommHopfAlgCat.isCentral_augmentation {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : (HopfIdeal.augmentation R ↑H).IsCentral

The trivial subgroup is central.

theorem TauCeti.HopfIdeal.IsCentral.comapOfSurjective_of_bijective {R : Type u} [CommRing R] {H K : Type v} [CommRing H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] {I : HopfIdeal R K} (hI : I.IsCentral) (f : H →ₐc[R] K) (hinj : Function.Injective ⇑f) (hsurj : Function.Surjective ⇑f) : (I.comapOfSurjective f hsurj).IsCentral

Pulling a central Hopf ideal back along a bijective bialgebra morphism preserves centrality. Contravariantly, an isomorphism of affine group schemes carries central closed subgroup schemes to central closed subgroup schemes.

theorem TauCeti.HopfIdeal.IsCentral.isNormal {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {I : HopfIdeal R ↑H} (hI : I.IsCentral) : I.IsNormal

A central Hopf ideal is normal. Its points commute with every point of the ambient group over the same value algebra, so they form a normal subgroup there, and normality of a Hopf ideal is detected pointwise.

theorem TauCeti.HopfIdeal.IsCentral.isCocomm_quotient {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {I : HopfIdeal R ↑H} (hI : I.IsCentral) : Coalgebra.IsCocomm R ↑(CommHopfAlgCat.quotient H I)

The coordinate Hopf algebra of a central closed subgroup is cocommutative. Equivalently, every central closed subgroup scheme is a commutative group scheme.