Normal Hopf ideals as categorical normal subgroups #
A commutative Hopf algebra is equivalently a group object in the opposite category of
commutative algebras. Under this equivalence, a Hopf-ideal quotient H ⟶ H/I represents the
closed-subgroup inclusion Spec(H/I) ⟶ Spec H.
This file proves that normality of the Hopf ideal makes this inclusion a normal subgroup object in Mathlib's sense. The proof uses the generalized-point criterion for categorical normality and the existing characterization of normal Hopf ideals by normality of their subgroups of algebra-valued points.
The result is the bridge needed to apply the internal semidirect-product construction to two normal closed affine subgroup schemes. Its multiplication map and scheme-theoretic image are the binary product used in the maximal-dimension construction of the unipotent radical.
The multiplication bridge used here is TauCeti.CommHopfAlgCat.grpObjPointsMulEquiv from
TauCeti.Algebra.AlgebraicGroup.CommHopfAlgCat.Yoneda.
Main declarations #
TauCeti.CommHopfAlgCat.quotientGrpObjInclusion_normal_iff: a Hopf ideal is normal exactly when its categorical inclusion is a normal subgroup object.
References #
- W. C. Waterhouse, Introduction to Affine Group Schemes, §§15–17.
- J. S. Milne, Algebraic Groups (2017), §§6.a and 10.20.
- Mathlib's
commHopfAlgCatEquivCogrpCommAlgCatandCategoryTheory.IsMonHom.normal_iff_normal_monoidHom; the latter follows Görtz–Wedhorn, Algebraic Geometry II, Definition 27.3.
This advances Layer 5, "The unipotent radical", of the ReductiveGroups roadmap. It connects the coordinate normality API to the categorical semidirect-product API used to form the product of two normal unipotent-radical candidates.
A Hopf ideal is normal if and only if its categorical closed-subgroup inclusion is a normal subgroup object in the opposite category of commutative algebras.