Fppf quotient sheaves of affine groups

Let H be a commutative Hopf algebra over a commutative ring R, and let I be a normal Hopf ideal. The pointwise quotient A ↦ G(A) / V(I)(A) need not satisfy fppf descent. Its sheafification is the fppf quotient sheaf of G by the closed normal subgroup cut out by I.

Nonabelian groups are handled as group objects in type-valued presheaves and sheaves. This is the natural construction because type-valued sheafification is left exact, hence preserves the finite products used by a group object. It also avoids requiring colimits in GrpCat.

No representability is asserted. Representability of an fppf quotient requires additional hypotheses and is a separate downstream theorem.

Main declarations

• TauCeti.CommHopfAlgCat.pointwiseQuotientPresheaf: the pointwise quotient on the affine fppf site.
• TauCeti.CommHopfAlgCat.fppfQuotientSheaf: its sheafification as a group object.
• TauCeti.CommHopfAlgCat.fppfQuotientProjection: the sheafified quotient projection.
• TauCeti.CommHopfAlgCat.fppfQuotientHomEquiv: the quotient sheaf's universal property.

References

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

Implementation notes

The construction uses Mathlib's sheafificationAdjunction, its lift Adjunction.mapGrp to group objects, and the finite-product-preserving monoidal structure on type-valued sheafification.

This is the fppf-sheaf-quotient step of Layer 3, "Normality and quotients", in the ReductiveGroups roadmap.

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.pointwiseQuotientPresheaf {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : CategoryTheory.Functor (CommAlgCat R)ᵒᵖᵒᵖ GrpCat

The pointwise quotient group functor, presented as a presheaf on the affine fppf site.

Equations

• TauCeti.CommHopfAlgCat.pointwiseQuotientPresheaf H I hI = (CategoryTheory.unopUnop (CommAlgCat R)).comp (TauCeti.CommHopfAlgCat.pointwiseQuotientFunctor H I hI)

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.pointwiseQuotientPresheafProjection {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : HopfAlgebra.pointsGroupPresheaf H ⟶ pointwiseQuotientPresheaf H I hI

The quotient projection, presented as a morphism of presheaves on the affine fppf site.

Equations

• TauCeti.CommHopfAlgCat.pointwiseQuotientPresheafProjection H I hI = (CategoryTheory.unopUnop (CommAlgCat R)).whiskerLeft (TauCeti.CommHopfAlgCat.pointwiseQuotientProjection H I hI)

noncomputable def TauCeti.CommHopfAlgCat.pointwiseQuotientPresheafGrp {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : CategoryTheory.Grp (CategoryTheory.Functor (CommAlgCat R)ᵒᵖᵒᵖ (Type (u + 1)))

The pointwise quotient presheaf as a group object in type-valued presheaves. Values are lifted by one universe because the category of commutative R-algebras itself lives in Type (u + 1), the universe in which type-valued sheafification is available.

Equations

• TauCeti.CommHopfAlgCat.pointwiseQuotientPresheafGrp H I hI = TauCeti.CommHopfAlgCat.groupFunctorGrp ((TauCeti.CommHopfAlgCat.pointwiseQuotientPresheaf H I hI).comp GrpCat.uliftFunctor)

theorem TauCeti.CommHopfAlgCat.pointwiseQuotientPresheafGrp_def {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : pointwiseQuotientPresheafGrp H I hI = groupFunctorGrp ((pointwiseQuotientPresheaf H I hI).comp GrpCat.uliftFunctor)

Unfold the pointwise quotient presheaf group object to the group object associated to its group-valued functor.

noncomputable def TauCeti.CommHopfAlgCat.pointwiseQuotientPresheafGrpProjection {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : pointsPresheafGrp H ⟶ pointwiseQuotientPresheafGrp H I hI

The quotient projection as a morphism of group objects in type-valued presheaves.

Equations

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

theorem TauCeti.CommHopfAlgCat.pointwiseQuotientPresheafGrp_X_eq {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : (pointwiseQuotientPresheafGrp H I hI).X = (pointwiseQuotientPresheaf H I hI).comp (GrpCat.uliftFunctor.comp (CategoryTheory.forget GrpCat))

The carrier of the pointwise quotient presheaf group object is the universe lift of the underlying group-valued quotient presheaf.

theorem TauCeti.CommHopfAlgCat.pointwiseQuotientPresheafGrpProjection_hom_hom {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : (pointwiseQuotientPresheafGrpProjection H I hI).hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Functor.whiskerRight (pointwiseQuotientPresheafProjection H I hI) GrpCat.uliftFunctor) (CategoryTheory.forget GrpCat)) (CategoryTheory.eqToHom ⋯))

On underlying presheaves, the group-object quotient projection is the universe lift of the pointwise quotient projection.

theorem TauCeti.CommHopfAlgCat.pointwiseQuotientPresheafProjection_ulift_app_apply {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) (A : (CommAlgCat R)ᵒᵖᵒᵖ) (x : ULift.{u + 1, u} ↑(HopfAlgebra.points (Opposite.unop (Opposite.unop A)))) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Functor.whiskerRight (CategoryTheory.Functor.whiskerRight (pointwiseQuotientPresheafProjection H I hI) GrpCat.uliftFunctor) (CategoryTheory.forget GrpCat)).app A)) x = { down := (CategoryTheory.ConcreteCategory.hom ((pointwiseQuotientPresheafProjection H I hI).app A)) x.down }

Evaluating the universe-lifted pointwise quotient projection amounts to applying the pointwise projection and then lifting its value.

noncomputable def TauCeti.CommHopfAlgCat.fppfQuotientSheaf {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : CategoryTheory.Grp (CategoryTheory.Sheaf (CommAlgCat.fppfTopology R) (Type (u + 1)))

The fppf quotient sheaf associated to a normal Hopf ideal, as a group object in type-valued fppf sheaves.

Its underlying sheaf is the sheafification of A ↦ G(A) / V(I)(A). This definition makes no representability claim.

Equations

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

theorem TauCeti.CommHopfAlgCat.fppfQuotientSheaf_def {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : fppfQuotientSheaf H I hI = let F := CategoryTheory.presheafToSheaf (CommAlgCat.fppfTopology R) (Type (u + 1)); have x := CategoryTheory.Functor.Monoidal.ofChosenFiniteProducts F; F.mapGrp.obj (pointwiseQuotientPresheafGrp H I hI)

Unfold the fppf quotient group object to the image of its pointwise presheaf group object under sheafification.

noncomputable def TauCeti.CommHopfAlgCat.fppfQuotientProjection {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : pointsFppfGroupObject H ⟶ fppfQuotientSheaf H I hI

The canonical morphism from the fppf sheaf of points of G to the fppf quotient sheaf G / V(I).

Equations

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

theorem TauCeti.CommHopfAlgCat.fppfQuotientSheaf_X_eq {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : (fppfQuotientSheaf H I hI).X = (CategoryTheory.presheafToSheaf (CommAlgCat.fppfTopology R) (Type (u + 1))).obj (pointwiseQuotientPresheafGrp H I hI).X

The carrier of the fppf quotient group object is the sheafification of the pointwise quotient presheaf's carrier.

theorem TauCeti.CommHopfAlgCat.fppfQuotientProjection_hom {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : (fppfQuotientProjection H I hI).hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.presheafToSheaf (CommAlgCat.fppfTopology R) (Type (u + 1))).map (pointwiseQuotientPresheafGrpProjection H I hI).hom.hom) (CategoryTheory.eqToHom ⋯))

On underlying sheaves, the fppf quotient projection is the sheafification of the pointwise quotient projection.

noncomputable def TauCeti.CommHopfAlgCat.fppfQuotientHomEquiv {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) (F : CategoryTheory.Grp (CategoryTheory.Sheaf (CommAlgCat.fppfTopology R) (Type (u + 1)))) : (fppfQuotientSheaf H I hI ⟶ F) ≃ (pointwiseQuotientPresheafGrp H I hI ⟶ fppfGroupObjectToPresheaf F)

Maps from the fppf quotient sheaf to a group object in fppf sheaves are naturally equivalent to group-object maps from the pointwise quotient presheaf to its underlying presheaf.

Equations

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

@[simp]

theorem TauCeti.CommHopfAlgCat.pointsFppfHomEquiv_apply_fppfQuotientProjection {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : (pointsFppfHomEquiv H (fppfQuotientSheaf H I hI)) (fppfQuotientProjection H I hI) = CategoryTheory.CategoryStruct.comp (pointwiseQuotientPresheafGrpProjection H I hI) ((fppfQuotientHomEquiv H I hI (fppfQuotientSheaf H I hI)) (CategoryTheory.CategoryStruct.id (fppfQuotientSheaf H I hI)))

Under the sheafification adjunction, the quotient projection restricts to the pointwise quotient projection followed by the sheafification unit.

noncomputable def TauCeti.CommHopfAlgCat.fppfQuotientLift {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) (F : CategoryTheory.Grp (CategoryTheory.Sheaf (CommAlgCat.fppfTopology R) (Type (u + 1)))) (f : pointwiseQuotientPresheafGrp H I hI ⟶ fppfGroupObjectToPresheaf F) : fppfQuotientSheaf H I hI ⟶ F

A group-object morphism from the pointwise quotient presheaf into the underlying presheaf of an fppf sheaf extends uniquely to the fppf quotient sheaf.

Equations

• TauCeti.CommHopfAlgCat.fppfQuotientLift H I hI F f = (TauCeti.CommHopfAlgCat.fppfQuotientHomEquiv H I hI F).symm f