The cokernel property of fppf quotient projections

The projection from an affine group to its fppf quotient by a closed normal subgroup is the categorical cokernel of the subgroup inclusion. Thus every group-sheaf morphism annihilating the subgroup descends uniquely to the quotient, even when the quotient is not representable.

This is a universal property in group objects in fppf sheaves, with arbitrary group-sheaf targets. It does not require the source to be of finite type or smooth.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §14.
• J. S. Milne, Algebraic Groups (2017), §5.

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.fppfQuotientCokernelCofork {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : CategoryTheory.Limits.CokernelCofork (quotientSubgroupPointsFppfGrpInclusion H I)

The subgroup inclusion and quotient projection form a cokernel cofork.

Equations

• TauCeti.CommHopfAlgCat.fppfQuotientCokernelCofork H I hI = CategoryTheory.Limits.CokernelCofork.ofπ (TauCeti.CommHopfAlgCat.fppfQuotientProjection H I hI) ⋯

@[simp]

theorem TauCeti.CommHopfAlgCat.fppfQuotientCokernelCofork_π {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : CategoryTheory.Limits.Cofork.π (fppfQuotientCokernelCofork H I hI) = fppfQuotientProjection H I hI

The projection of the cokernel cofork is the canonical fppf quotient projection.

noncomputable def TauCeti.CommHopfAlgCat.isColimitFppfQuotientCokernel {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : CategoryTheory.Limits.IsColimit (fppfQuotientCokernelCofork H I hI)

The fppf quotient projection is the categorical cokernel of the closed normal subgroup inclusion. In particular, homomorphisms annihilating that subgroup descend uniquely.

Equations

• One or more equations did not get rendered due to their size.