Homogeneous quotient projections are torsors

For an affine group G and any closed subgroup N, the fppf homogeneous quotient projection has kernel pair G × N, with maps (g, n) ↦ g and (g, n) ↦ gn. Together with local surjectivity, this says that G → G/N is an N-torsor. Normality is unnecessary: the quotient is a sheaf of sets, and need not be a group.

This identifies the fibers needed when realizing a homogeneous quotient as the orbit of a line with stabilizer N. It does not assert representability of that orbit. The base ring, ambient group, subgroup, and value algebras may all be nonreduced.

The action and product comparisons are those of TauCeti.CommHopfAlgCat.pointwiseQuotientTorsorAction and TauCeti.CommHopfAlgCat.fppfQuotientTorsorProductIso.

References

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

theorem CommHopfAlgCat.isPullback_homogeneousQuotientPresheafTorsor {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : TauCeti.HopfIdeal R ↑H) : CategoryTheory.IsPullback (CategoryTheory.SemiCartesianMonoidalCategory.fst (TauCeti.CommHopfAlgCat.pointsPresheafGrp H).X (TauCeti.CommHopfAlgCat.pointsPresheafGrp (TauCeti.CommHopfAlgCat.quotient H I)).X) (TauCeti.CommHopfAlgCat.pointwiseQuotientTorsorAction H I) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (H.homogeneousQuotientPresheafProjection I)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (H.homogeneousQuotientPresheafProjection I))

The coset projection has kernel pair G × N, even for a nonnormal subgroup.

noncomputable def CommHopfAlgCat.fppfHomogeneousQuotientSheafProjection {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : TauCeti.HopfIdeal R ↑H) : (TauCeti.CommHopfAlgCat.pointsFppfGroupObject H).X ⟶ H.fppfHomogeneousQuotient I

The morphism of fppf sheaves from ambient group points to the homogeneous quotient.

Equations

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

@[simp]

theorem CommHopfAlgCat.toSheafify_comp_fppfHomogeneousQuotientSheafProjection {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : TauCeti.HopfIdeal R ↑H) : CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify (TauCeti.CommAlgCat.fppfTopology R) (TauCeti.CommHopfAlgCat.pointsPresheafGrp H).X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (H.fppfHomogeneousQuotientSheafProjection I).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (H.fppfHomogeneousQuotientProjection I)

On ambient points, the sheaf morphism agrees with the original projection to the sheafification of the coset presheaf.

@[simp]

theorem CommHopfAlgCat.toSheafify_comp_fppfHomogeneousQuotientSheafProjection_assoc {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : TauCeti.HopfIdeal R ↑H) {Z : CategoryTheory.Functor (CommAlgCat R)ᵒᵖᵒᵖ (Type (u + 1))} (h : (H.fppfHomogeneousQuotient I).obj ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify (TauCeti.CommAlgCat.fppfTopology R) (TauCeti.CommHopfAlgCat.pointsPresheafGrp H).X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (H.fppfHomogeneousQuotientSheafProjection I).hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (H.fppfHomogeneousQuotientProjection I) h)

On ambient points, the sheaf morphism agrees with the original projection to the sheafification of the coset presheaf.

instance CommHopfAlgCat.epi_fppfHomogeneousQuotientSheafProjection {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : TauCeti.HopfIdeal R ↑H) : CategoryTheory.Epi (H.fppfHomogeneousQuotientSheafProjection I)

The projection to the fppf homogeneous quotient is an epimorphism of sheaves.

theorem CommHopfAlgCat.isLocallySurjective_fppfHomogeneousQuotientSheafProjection {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : TauCeti.HopfIdeal R ↑H) : CategoryTheory.Sheaf.IsLocallySurjective (H.fppfHomogeneousQuotientSheafProjection I)

Every section of G/N lifts fppf locally to a section of the ambient group sheaf.

theorem CommHopfAlgCat.isPullback_fppfHomogeneousQuotientTorsor {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : TauCeti.HopfIdeal R ↑H) : CategoryTheory.IsPullback (CategoryTheory.SemiCartesianMonoidalCategory.fst (TauCeti.CommHopfAlgCat.pointsFppfGroupObject H).X (TauCeti.CommHopfAlgCat.pointsFppfGroupObject (TauCeti.CommHopfAlgCat.quotient H I)).X) (TauCeti.CommHopfAlgCat.fppfQuotientTorsorAction H I) (H.fppfHomogeneousQuotientSheafProjection I) (H.fppfHomogeneousQuotientSheafProjection I)

The homogeneous quotient projection has torsor kernel pair G × N in fppf sheaves.