Normality of the identity component

Let H be a commutative Hopf algebra of finite type over an algebraically closed field. The connected component of the counit point is preserved by conjugation, so its defining Hopf ideal is normal.

The proof first constructs the homeomorphism of Spec H induced by conjugation by a rational point, using inversion and right translation. It then tests the universal conjugate of the component idempotent on algebraically closed points of

H ⊗[k] (H / I),

where I cuts out the identity component. Conjugation preserves that component, so every such evaluation is one. The affine Nullstellensatz and idempotence promote this pointwise calculation to membership in H ⊗ I.

Main declaration

• TauCeti.HopfAlgebra.isNormal_identityComponentHopfIdeal: the Hopf ideal defining the identity component is stable under conjugation.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 2.37.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Section 6.7.

This supplies the normal-subgroup input for the component-group quotient in Layer 3, “Identity component G° and component group π₀(G)”, of the ReductiveGroups roadmap.

theorem TauCeti.HopfAlgebra.isNormal_identityComponentHopfIdeal {k : Type u} [Field k] [IsAlgClosed k] {H : Type v} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] : identityComponentHopfIdeal.IsNormal

The Hopf ideal cutting out the identity component is normal: its coordinate ideal is stable under conjugation. Consequently it may be used in the normal fppf quotient construction.