Functions on a faithfully flat quotient

For a faithfully flat morphism f : H ⟶ K of commutative Hopf algebras, the functions on Spec K invariant under its scheme-theoretic kernel are exactly the functions pulled back from Spec H. In coordinates, (kernelHopfIdeal f).coinvariants = f.hom.toAlgHom.range. This is the coordinate exactness statement for a faithfully flat quotient of affine groups. No finite presentation or smoothness hypothesis is needed.

More generally, the equality holds whenever the coordinate map satisfies Algebra.IsEffective. The kernel-invariance characterization identifies invariant functions with functions constant on fibers over every value algebra, connecting the functor-of-points and coordinate-algebra descriptions of affine-group quotients.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §16.3.
• J. S. Milne, Algebraic Groups (2017), §5.c.
• Mathlib's Algebra.IsEffective.eqLocus_includeLeft_includeRight and Algebra.IsEffective.of_faithfullyFlat.

theorem TauCeti.CommHopfAlgCat.ofConv_apply_eq_of_mem_coinvariants_kernelHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) {x : ↑K} (hx : x ∈ (kernelHopfIdeal f).coinvariants) {A : CommAlgCat R} (g g' : ↑(HopfAlgebra.points A)) (hgg' : (CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor f).app A)) g = (CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor f).app A)) g') : g.ofConv x = g'.ofConv x

A function invariant under the kernel takes the same value on points with the same image, over a value algebra in any universe.

theorem TauCeti.CommHopfAlgCat.mem_coinvariants_kernelHopfIdeal_iff {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (x : ↑K) : x ∈ (kernelHopfIdeal f).coinvariants ↔ ∀ (A : CommAlgCat R) (g g' : ↑(HopfAlgebra.points A)), (CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor f).app A)) g = (CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor f).app A)) g' → g.ofConv x = g'.ofConv x

A function is invariant under the kernel exactly when it takes the same value on any two points with the same image, over every value algebra in the coordinate algebras' universe.

theorem TauCeti.CommHopfAlgCat.coinvariants_kernelHopfIdeal_eq_range_of_isEffective {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : Algebra.IsEffective ↑H ↑K) : (kernelHopfIdeal f).coinvariants = (↑(CommHopfAlgCat.Hom.hom f)).range

If the coordinate map is effective, the functions invariant under its kernel are precisely the pullbacks of functions on its target.

@[simp]

theorem TauCeti.CommHopfAlgCat.coinvariants_kernelHopfIdeal_eq_range {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : (↑↑(CommHopfAlgCat.Hom.hom f)).FaithfullyFlat) : (kernelHopfIdeal f).coinvariants = (↑(CommHopfAlgCat.Hom.hom f)).range

The functions invariant under the kernel of a faithfully flat affine-group morphism are precisely the pullbacks of functions on its target.