A pointwise criterion for an ideal to be a Hopf ideal

If the points annihilating an ideal form a subgroup over every value algebra, then that ideal is a Hopf ideal. Multiplication can be tested on the two universal quotient-valued points over the tensor square of the quotient. Inversion can be tested on the universal quotient-valued point, and the identity detects the counit condition.

This criterion turns equations representing a subgroup functor into a closed subgroup scheme without separately calculating the comultiplication of each equation.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §3.

noncomputable def TauCeti.HopfIdeal.ofIdealOfPointsSubgroup {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (I : Ideal H) (S : (A : CommAlgCat R) → Subgroup (WithConv (H →ₐ[R] ↑A))) (hS : ∀ (A : CommAlgCat R) (g : WithConv (H →ₐ[R] ↑A)), g ∈ S A ↔ I ≤ RingHom.ker g.ofConv) : HopfIdeal R H

An ideal cutting out subgroups over every value algebra is a Hopf ideal. The subgroup family need not be given separate naturality data: its equations already imply naturality.

@[simp]

theorem TauCeti.HopfIdeal.ofIdealOfPointsSubgroup_toIdeal {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (I : Ideal H) (S : (A : CommAlgCat R) → Subgroup (WithConv (H →ₐ[R] ↑A))) (hS : ∀ (A : CommAlgCat R) (g : WithConv (H →ₐ[R] ↑A)), g ∈ S A ↔ I ≤ RingHom.ker g.ofConv) : (ofIdealOfPointsSubgroup I S hS).toIdeal = I

The pointwise construction leaves the defining ideal unchanged.