Inverse images of Hopf ideals along a quotient morphism

The quotient morphism H ⟶ H ⧸ I is surjective, so every Hopf ideal J of H ⧸ I has an inverse image HopfIdeal.comapOfSurjective J in H. This file records the resulting reflection principle: J is zero as soon as that inverse image is no larger than the Hopf ideal I quotiented by.

Contravariantly, a closed subgroup scheme of a quotient group scheme is the whole quotient exactly when its preimage in the ambient group scheme is everything; the statement below is the form in which rigidity arguments use it, turning "the preimage is small" into "the ideal is trivial".

Main declarations

• TauCeti.CommHopfAlgCat.eq_bot_of_comapOfSurjective_le: a Hopf ideal of H ⧸ I whose inverse image along the quotient morphism lies inside I is zero.

References

This is the Hopf-ideal form of the usual correspondence between ideals of a quotient and ideals of the ambient object containing the one quotiented by; see Waterhouse, Introduction to Affine Group Schemes, §16. It is a Layer 3 prerequisite for TauCetiRoadmap/ReductiveGroups/README.md, "Hopf ideals ↔ closed subgroup schemes", consumed by the Layer 9 rigidity statements for groups generated by a family of subgroups.

theorem TauCeti.CommHopfAlgCat.eq_bot_of_comapOfSurjective_le {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {I : HopfIdeal R ↑H} (J : HopfIdeal R ↑(quotient H I)) (hJ : J.comapOfSurjective (CommHopfAlgCat.Hom.hom (mkQuotient H I)) ⋯ ≤ I) : J = ⊥

A Hopf ideal of a quotient whose preimage lies back inside the ideal quotiented by is zero.

This is the reflection principle behind the rigidity statements for generated closed subgroup schemes: it turns "the preimage is small" into "the ideal is trivial".