Representing normal fppf quotients by coinvariants

Let G be a geometrically reduced affine group of finite type over a field, and let N be a normal closed subgroup. The fppf quotient G/N is represented by the affine group whose coordinate Hopf algebra consists of the N-coinvariant functions on G. The subgroup N may be nonreduced, and the field need not be perfect.

The isomorphism coinvariantsFppfQuotientIso identifies the sheaf quotient projection with the morphism induced by the inclusion of coinvariants. The coordinate maps form a short exact sequence, recorded by isShortExact_coinvariantsι_mkQuotient.

This combines faithfullyFlat_coinvariantsι, kernelHopfIdeal_coinvariantsι_eq, and the fppf first isomorphism theorem kernelFppfQuotientIso.

References

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

noncomputable def TauCeti.CommHopfAlgCat.coinvariantsFppfQuotientIso {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] [Algebra.IsGeometricallyReduced k ↑H] {I : HopfIdeal k ↑H} (hI : I.IsNormal) : fppfQuotientSheaf H I hI ≅ pointsFppfGroupObject (coinvariants hI)

The fppf quotient by a normal closed subgroup of a geometrically reduced finite-type affine group is represented by its coinvariant Hopf algebra.

Equations

• TauCeti.CommHopfAlgCat.coinvariantsFppfQuotientIso hI = CategoryTheory.eqToIso ⋯ ≪≫ TauCeti.CommHopfAlgCat.kernelFppfQuotientIso (TauCeti.CommHopfAlgCat.coinvariantsι hI) ⋯ ⋯

@[simp]

theorem TauCeti.CommHopfAlgCat.fppfQuotientProjection_comp_coinvariantsFppfQuotientIso_hom {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] [Algebra.IsGeometricallyReduced k ↑H] {I : HopfIdeal k ↑H} (hI : I.IsNormal) : CategoryTheory.CategoryStruct.comp (fppfQuotientProjection H I hI) (coinvariantsFppfQuotientIso hI).hom = pointsFppfGroupObjectMap (coinvariantsι hI)

The representing isomorphism carries the fppf quotient projection to the affine group morphism defined by the inclusion of coinvariants.

@[simp]

theorem TauCeti.CommHopfAlgCat.fppfQuotientProjection_comp_coinvariantsFppfQuotientIso_hom_assoc {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] [Algebra.IsGeometricallyReduced k ↑H] {I : HopfIdeal k ↑H} (hI : I.IsNormal) {Z : CategoryTheory.Grp (CategoryTheory.Sheaf (CommAlgCat.fppfTopology k) (Type (u + 1)))} (h : pointsFppfGroupObject (coinvariants hI) ⟶ Z) : CategoryTheory.CategoryStruct.comp (fppfQuotientProjection H I hI) (CategoryTheory.CategoryStruct.comp (coinvariantsFppfQuotientIso hI).hom h) = CategoryTheory.CategoryStruct.comp (pointsFppfGroupObjectMap (coinvariantsι hI)) h

The representing isomorphism carries the fppf quotient projection to the affine group morphism defined by the inclusion of coinvariants.