The kernel of the fppf quotient projection

For a normal closed subgroup N = Spec (H / I) of G = Spec H, the sequence 1 ⟶ N ⟶ G ⟶ G/N ⟶ 1 is exact as a sequence of fppf group sheaves: the subgroup inclusion is the categorical kernel of the quotient projection, and the projection is locally surjective by isLocallySurjective_fppfQuotientProjection.

The kernel universal property supplies unique factorizations of group-sheaf morphisms annihilated by the quotient projection. It needs neither representability of G/N nor smoothness, finiteness, or field assumptions.

References

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

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientSubgroupPointsFppfGrpInclusion_comp_fppfQuotientProjection {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : CategoryTheory.CategoryStruct.comp (quotientSubgroupPointsFppfGrpInclusion H I) (fppfQuotientProjection H I hI) = 0

The inclusion of a normal closed subgroup followed by the fppf quotient projection is the trivial group-sheaf morphism.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientSubgroupPointsFppfGrpInclusion_comp_fppfQuotientProjection_assoc {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) {Z : CategoryTheory.Grp (CategoryTheory.Sheaf (CommAlgCat.fppfTopology R) (Type (u + 1)))} (h : fppfQuotientSheaf H I hI ⟶ Z) : CategoryTheory.CategoryStruct.comp (quotientSubgroupPointsFppfGrpInclusion H I) (CategoryTheory.CategoryStruct.comp (fppfQuotientProjection H I hI) h) = CategoryTheory.CategoryStruct.comp 0 h

The inclusion of a normal closed subgroup followed by the fppf quotient projection is the trivial group-sheaf morphism.

noncomputable def TauCeti.CommHopfAlgCat.isLimitFppfQuotientKernel {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (quotientSubgroupPointsFppfGrpInclusion H I) ⋯)

The original closed subgroup is the categorical kernel of the fppf quotient projection, as a group object in fppf sheaves.

Equations

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