Scheme-theoretic images as fppf quotients

The scheme-theoretic image of a homomorphism from a geometrically reduced finite-type affine group is the fppf quotient of that group by its kernel. This holds over any field; the ambient target can be nonreduced. For finite-type affine groups, geometric reducedness is equivalent to smoothness. The kernel itself may be nonreduced, as with inseparable homomorphisms.

The image factorization has the original scheme-theoretic kernel, so the quotient is by the original subgroup, including its possibly nonreduced scheme structure.

References

• J. S. Milne, Algebraic Groups (2017), §5.a--c and Proposition 1.70.
• W. C. Waterhouse, Introduction to Affine Group Schemes, §§14--16.

theorem TauCeti.CommHopfAlgCat.isIso_kernelFppfQuotientHom_imageι {k : Type u} [Field k] {H K : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] [Algebra.FiniteType k ↑K] [Algebra.IsGeometricallyReduced k ↑K] (f : H ⟶ K) : CategoryTheory.IsIso (kernelFppfQuotientHom (imageι f))

The scheme-theoretic image of a homomorphism from a geometrically reduced finite-type affine group is represented by the fppf quotient by its kernel. The image factor's kernel is the original kernel, by kernelHopfIdeal_imageι.