Faithfully flat homomorphisms as cokernels

A quasi-compact faithfully flat homomorphism of group schemes is the categorical cokernel of its scheme-theoretic kernel. Thus a homomorphism killing that kernel factors uniquely through the quotient. No smoothness or reducedness is required.

The proof uses the kernel-pair translation square and Mathlib's effective-epimorphism theorem for fpqc morphisms, via Grp.isColimitCokernelCoforkOfTorsor.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, §2.4.

noncomputable def TauCeti.GroupScheme.isColimitKernelCofork {S : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over S)} (f : G ⟶ H) [AlgebraicGeometry.QuasiCompact (CategoryTheory.Over.Hom.left f.hom.hom)] [AlgebraicGeometry.Flat (CategoryTheory.Over.Hom.left f.hom.hom)] [AlgebraicGeometry.Surjective (CategoryTheory.Over.Hom.left f.hom.hom)] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ f ⋯)

A quasi-compact faithfully flat homomorphism of group schemes is the cokernel of its kernel inclusion.