Group objects on the affine fppf site

This file relates group-valued presheaves and sheaves on the affine fppf site to group objects in type-valued presheaves and sheaves. In particular, it presents the convolution-points sheaf of a commutative Hopf algebra as a group object, functorially in the Hopf algebra through pointsFppfGroupObjectMap, and exposes the group-object sheafification adjunction.

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

theorem GrpCat.uliftFunctor_comp_forget_eq_forget_comp_uliftFunctor : uliftFunctor.comp (CategoryTheory.forget GrpCat) = (CategoryTheory.forget GrpCat).comp CategoryTheory.uliftFunctor.{u + 1, u}

Forgetting a universe-lifted group agrees with universe-lifting its underlying type.

noncomputable def TauCeti.CommHopfAlgCat.groupFunctorGrp {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C GrpCat) : CategoryTheory.Grp (CategoryTheory.Functor C (Type u))

Regard a group-valued functor as a group object in type-valued functors.

Equations

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

noncomputable def TauCeti.CommHopfAlgCat.groupFunctorGrpMap {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C GrpCat} (α : F ⟶ G) : groupFunctorGrp F ⟶ groupFunctorGrp G

A natural transformation of group-valued functors is a morphism of their associated group objects in type-valued functors.

Equations

• TauCeti.CommHopfAlgCat.groupFunctorGrpMap α = CategoryTheory.Grp.homMk'' (CategoryTheory.Functor.whiskerRight α (CategoryTheory.forget GrpCat)) ⋯ ⋯

noncomputable def TauCeti.CommHopfAlgCat.groupFunctorGrpIso {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C GrpCat} (e : F ≅ G) : groupFunctorGrp F ≅ groupFunctorGrp G

A natural isomorphism of group-valued functors induces an isomorphism of their associated group objects in type-valued functors.

Equations

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

@[simp]

theorem TauCeti.CommHopfAlgCat.groupFunctorGrpIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C GrpCat} (e : F ≅ G) : (groupFunctorGrpIso e).hom = groupFunctorGrpMap e.hom

The forward map of the group-object isomorphism induced by a natural isomorphism is the group-object map induced by its forward natural transformation.

theorem TauCeti.CommHopfAlgCat.pointsGroupPresheaf_ulift_forget_eq_pointsPresheaf_ulift {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : (HopfAlgebra.pointsGroupPresheaf H).comp (GrpCat.uliftFunctor.comp (CategoryTheory.forget GrpCat)) = (HopfAlgebra.pointsPresheaf H).comp CategoryTheory.uliftFunctor.{u + 1, u}

Forgetting the universe lift of the group-valued points presheaf agrees with universe-lifting its underlying type-valued points presheaf.

noncomputable def TauCeti.CommHopfAlgCat.pointsPresheafGrp {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : CategoryTheory.Grp (CategoryTheory.Functor (CommAlgCat R)ᵒᵖᵒᵖ (Type (u + 1)))

The convolution-points presheaf as a group object in type-valued presheaves, with values lifted to the universe in which the affine-site sheafification lives.

Equations

• TauCeti.CommHopfAlgCat.pointsPresheafGrp H = TauCeti.CommHopfAlgCat.groupFunctorGrp ((TauCeti.HopfAlgebra.pointsGroupPresheaf H).comp GrpCat.uliftFunctor)

theorem TauCeti.CommHopfAlgCat.pointsPresheafGrp_X_eq {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : (pointsPresheafGrp H).X = (HopfAlgebra.pointsGroupPresheaf H).comp (GrpCat.uliftFunctor.comp (CategoryTheory.forget GrpCat))

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

noncomputable def TauCeti.CommHopfAlgCat.pointsPresheafGrpXIsoSchemePointsPresheaf {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : (pointsPresheafGrp H).X ≅ (schemePointsPresheaf H).comp CategoryTheory.uliftFunctor.{u + 1, u}

The carrier of the group-valued points presheaf is naturally isomorphic to the universe lift of the scheme-valued points presheaf.

Equations

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

noncomputable def TauCeti.CommHopfAlgCat.pointsFppfGroupObject {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : CategoryTheory.Grp (CategoryTheory.Sheaf (CommAlgCat.fppfTopology R) (Type (u + 1)))

The fppf sheaf of points, regarded as a group object in type-valued sheaves.

This form is canonically the sheafification of the group-valued points presheaf. Since that presheaf is already an fppf sheaf, its underlying type-valued sheaf is canonically isomorphic to HopfAlgebra.pointsFppfSheaf H after forgetting the group structure.

Equations

• TauCeti.CommHopfAlgCat.pointsFppfGroupObject H = (CategoryTheory.presheafToSheaf (TauCeti.CommAlgCat.fppfTopology R) (Type (?u.1 + 1))).mapGrp.obj (TauCeti.CommHopfAlgCat.pointsPresheafGrp H)

theorem TauCeti.CommHopfAlgCat.pointsFppfGroupObject_X_eq {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : (pointsFppfGroupObject H).X = (CategoryTheory.presheafToSheaf (CommAlgCat.fppfTopology R) (Type (u + 1))).obj (pointsPresheafGrp H).X

The carrier of the fppf points group object is the sheafification of the carrier of its presheaf group object.

noncomputable def TauCeti.CommHopfAlgCat.schemePointsFppfSheaf {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : CategoryTheory.Sheaf (CommAlgCat.fppfTopology R) (Type (u + 1))

The fppf sheafification of the universe-lifted scheme-valued points presheaf.

Equations

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

noncomputable def TauCeti.CommHopfAlgCat.pointsFppfGroupObjectXIsoSchemePointsFppfSheaf {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : (pointsFppfGroupObject H).X ≅ schemePointsFppfSheaf H

The carrier of the fppf points group object is naturally isomorphic to the sheafification of the universe-lifted scheme-valued points presheaf.

Equations

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

noncomputable def TauCeti.CommHopfAlgCat.pointsFppfGroupObjectIso {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : (pointsFppfGroupObject H).X ≅ (CategoryTheory.sheafCompose (CommAlgCat.fppfTopology R) ((CategoryTheory.forget GrpCat).comp CategoryTheory.uliftFunctor.{u + 1, u})).obj (HopfAlgebra.pointsFppfSheaf H)

The underlying sheaf of pointsFppfGroupObject is canonically the universe lift of the existing group-valued points sheaf HopfAlgebra.pointsFppfSheaf.

Equations

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

noncomputable def TauCeti.CommHopfAlgCat.pointsPresheafGrpMap {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) : pointsPresheafGrp K ⟶ pointsPresheafGrp H

Precomposition with a morphism f : H ⟶ K of commutative Hopf algebras, as a morphism of the points presheaves regarded as group objects in type-valued presheaves.

Equations

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

@[simp]

theorem TauCeti.CommHopfAlgCat.pointsPresheafGrpMap_id {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : pointsPresheafGrpMap (CategoryTheory.CategoryStruct.id H) = CategoryTheory.CategoryStruct.id (pointsPresheafGrp H)

The identity Hopf algebra morphism induces the identity on points presheaves.

@[simp]

theorem TauCeti.CommHopfAlgCat.pointsPresheafGrpMap_comp {R : Type u} [CommRing R] {H K L : CommHopfAlgCat R} (f : H ⟶ K) (g : K ⟶ L) : pointsPresheafGrpMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (pointsPresheafGrpMap g) (pointsPresheafGrpMap f)

Formation of the induced morphism on points presheaves reverses composition.

noncomputable def TauCeti.CommHopfAlgCat.pointsFppfGroupObjectMap {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) : pointsFppfGroupObject K ⟶ pointsFppfGroupObject H

The morphism of fppf points group objects induced by a morphism f : H ⟶ K of commutative Hopf algebras: the sheafification of precomposition with f on points.

Equations

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

@[simp]

theorem TauCeti.CommHopfAlgCat.pointsFppfGroupObjectMap_id {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : pointsFppfGroupObjectMap (CategoryTheory.CategoryStruct.id H) = CategoryTheory.CategoryStruct.id (pointsFppfGroupObject H)

The identity Hopf algebra morphism induces the identity on fppf points.

@[simp]

theorem TauCeti.CommHopfAlgCat.pointsFppfGroupObjectMap_comp {R : Type u} [CommRing R] {H K L : CommHopfAlgCat R} (f : H ⟶ K) (g : K ⟶ L) : pointsFppfGroupObjectMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (pointsFppfGroupObjectMap g) (pointsFppfGroupObjectMap f)

Formation of the induced morphism on fppf points reverses composition.

noncomputable def TauCeti.CommHopfAlgCat.fppfGroupObjectToPresheaf {R : Type u} [CommRing R] (F : CategoryTheory.Grp (CategoryTheory.Sheaf (CommAlgCat.fppfTopology R) (Type (u + 1)))) : CategoryTheory.Grp (CategoryTheory.Functor (CommAlgCat R)ᵒᵖᵒᵖ (Type (u + 1)))

The group object in type-valued presheaves underlying a group object in fppf sheaves.

Equations

• TauCeti.CommHopfAlgCat.fppfGroupObjectToPresheaf F = (CategoryTheory.sheafToPresheaf (TauCeti.CommAlgCat.fppfTopology R) (Type (?u.1 + 1))).mapGrp.obj F

noncomputable def TauCeti.CommHopfAlgCat.pointsFppfHomEquiv {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (F : CategoryTheory.Grp (CategoryTheory.Sheaf (CommAlgCat.fppfTopology R) (Type (u + 1)))) : (pointsFppfGroupObject H ⟶ F) ≃ (pointsPresheafGrp H ⟶ fppfGroupObjectToPresheaf F)

Maps from the sheafified points group object to a group object in fppf sheaves are naturally equivalent to maps from the points presheaf to its underlying presheaf.

Equations

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