A separator for sheaves of modules, and the Grothendieck abelian instance

Mathlib proves that Sheaf J A is Grothendieck abelian for a Grothendieck abelian target A (CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean) and that the free presheaves of modules on representables separate presheaves of modules (PresheafOfModules.freeYoneda.isSeparating), but records no separator for SheafOfModules R and hence no IsGrothendieckAbelian instance for it. This file adds both over a small site. The separating family is the sheafification of the free presheaves of modules on representables; the argument is the one for Sheaf.freeYoneda, run through the sheafification adjunction for modules. Its right adjoint is forget R ⋙ PresheafOfModules.restrictScalars (𝟙 R.obj), canonically isomorphic pointwise to forget R via ModuleCat.restrictScalarsId'App.

AB5 for sheaves of modules is SheafOfModules.ab5OfSize in Sheaf/AB.lean, so with a separator the Grothendieck abelian instance is a one-liner, and Mathlib then supplies enough injectives and HasExt. The instance for X.Modules on a scheme is in AlgebraicGeometry/Modules/AB.lean.

Main results

• SheafOfModules.freeYonedaSheaf, SheafOfModules.freeYonedaSheaf_isSeparating.
• SheafOfModules.Elements.freeYonedaSheaf, SheafOfModules.freeYonedaSheafCoproduct, and SheafOfModules.fromFreeYonedaSheafCoproduct_epi give a canonical element-indexed coproduct presentation of any module sheaf.
• SheafOfModules.hasSeparator.
• SheafOfModules.isGrothendieckAbelian.

noncomputable def SheafOfModules.freeYonedaSheaf {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (X : C) : SheafOfModules R

The sheaf of modules freely generated by one section over X: the sheafification of the free presheaf of modules on the representable presheaf of X.

Equations

• SheafOfModules.freeYonedaSheaf R X = (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).obj ((PresheafOfModules.free R.obj).obj (CategoryTheory.yoneda.obj X))

theorem SheafOfModules.freeYonedaSheaf_isSeparating {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] : (CategoryTheory.ObjectProperty.ofObj (freeYonedaSheaf R)).IsSeparating

The free sheaves of modules on representables separate sheaves of modules.

Element-indexed presentations

@[reducible, inline]

noncomputable abbrev SheafOfModules.Elements.freeYonedaSheaf {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (m : M.val.Elements) : SheafOfModules R

The canonical free-Yoneda module sheaf associated to a section of a sheaf of modules.

Equations

• SheafOfModules.Elements.freeYonedaSheaf R m = SheafOfModules.freeYonedaSheaf R (Opposite.unop m.fst)

noncomputable def SheafOfModules.Elements.fromFreeYonedaSheaf {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (m : M.val.Elements) : freeYonedaSheaf R m ⟶ M

The map from the free-Yoneda sheaf indexed by a section to the sheaf containing it.

Equations

• SheafOfModules.Elements.fromFreeYonedaSheaf R m = (SheafOfModules.freeYonedaSheafHomEquiv✝ R (Opposite.unop m.fst) M).symm m.snd

@[reducible, inline]

noncomputable abbrev SheafOfModules.freeYonedaSheafCoproduct {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) : SheafOfModules R

The coproduct of the free-Yoneda module sheaves indexed by all sections of M.

Equations

• SheafOfModules.freeYonedaSheafCoproduct R M = ∐ fun (m : M.val.Elements) => SheafOfModules.Elements.freeYonedaSheaf R m

@[reducible, inline]

noncomputable abbrev SheafOfModules.ιFreeYonedaSheafCoproduct {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) (m : M.val.Elements) : Elements.freeYonedaSheaf R m ⟶ freeYonedaSheafCoproduct R M

The inclusion of the summand indexed by a section of M.

Equations

• SheafOfModules.ιFreeYonedaSheafCoproduct R M m = CategoryTheory.Limits.Sigma.ι (SheafOfModules.Elements.freeYonedaSheaf R) m

noncomputable def SheafOfModules.fromFreeYonedaSheafCoproduct {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) : freeYonedaSheafCoproduct R M ⟶ M

The canonical map from the element-indexed free-Yoneda coproduct to M.

Equations

• SheafOfModules.fromFreeYonedaSheafCoproduct R M = CategoryTheory.Limits.Sigma.desc fun (m : M.val.Elements) => SheafOfModules.Elements.fromFreeYonedaSheaf R m

@[simp]

theorem SheafOfModules.ι_fromFreeYonedaSheafCoproduct {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) (m : M.val.Elements) : CategoryTheory.CategoryStruct.comp (ιFreeYonedaSheafCoproduct R M m) (fromFreeYonedaSheafCoproduct R M) = Elements.fromFreeYonedaSheaf R m

@[simp]

theorem SheafOfModules.ι_fromFreeYonedaSheafCoproduct_assoc {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) (m : M.val.Elements) {Z : SheafOfModules R} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (ιFreeYonedaSheafCoproduct R M m) (CategoryTheory.CategoryStruct.comp (fromFreeYonedaSheafCoproduct R M) h) = CategoryTheory.CategoryStruct.comp (Elements.fromFreeYonedaSheaf R m) h

instance SheafOfModules.fromFreeYonedaSheafCoproduct_epi {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) : CategoryTheory.Epi (fromFreeYonedaSheafCoproduct R M)

The element-indexed coproduct map is epi: every map from a free-Yoneda sheaf factors through the summand indexed by the image of its distinguished section.

@[reducible, inline]

noncomputable abbrev SheafOfModules.Elements.map {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) {M N : SheafOfModules R} (f : M ⟶ N) (m : M.val.Elements) : N.val.Elements

The element of the target sheaf obtained by applying a morphism to a section.

Equations

• SheafOfModules.Elements.map R f m = N.val.elementsMk m.fst ((CategoryTheory.ConcreteCategory.hom (f.val.app m.fst)) m.snd)

@[simp]

theorem SheafOfModules.Elements.map_id {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) {M : SheafOfModules R} (m : M.val.Elements) : map R (CategoryTheory.CategoryStruct.id M) m = m

@[simp]

theorem SheafOfModules.Elements.map_comp {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) {M N P : SheafOfModules R} (f : M ⟶ N) (g : N ⟶ P) (m : M.val.Elements) : map R (CategoryTheory.CategoryStruct.comp f g) m = map R g (map R f m)

noncomputable def SheafOfModules.freeYonedaSheafCoproductMap {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N) : freeYonedaSheafCoproduct R M ⟶ freeYonedaSheafCoproduct R N

The map on element-indexed coproducts induced by a morphism of module sheaves.

Equations

• SheafOfModules.freeYonedaSheafCoproductMap R f = CategoryTheory.Limits.Sigma.desc fun (m : M.val.Elements) => SheafOfModules.ιFreeYonedaSheafCoproduct R N (SheafOfModules.Elements.map R f m)

noncomputable def SheafOfModules.freeYonedaSheafCoproductFunctor {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules R)

The functor assigning to a sheaf its free-Yoneda coproduct indexed by its sections.

For M : SheafOfModules.{u} R, the index M.val.Elements is in Type u: it is the sigma type of an object of the small site and a section over that object.

Equations

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

theorem SheafOfModules.fromFreeYonedaSheafCoproduct_natural {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (freeYonedaSheafCoproductMap R f) (fromFreeYonedaSheafCoproduct R N) = CategoryTheory.CategoryStruct.comp (fromFreeYonedaSheafCoproduct R M) f

The coproduct presentation commutes with every morphism of sheaves of modules.

noncomputable def SheafOfModules.freeYonedaSheafCoproductToIdentity {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] : freeYonedaSheafCoproductFunctor R ⟶ CategoryTheory.Functor.id (SheafOfModules R)

The natural transformation from the element-indexed coproduct functor to the identity.

Equations

• SheafOfModules.freeYonedaSheafCoproductToIdentity R = { app := fun (M : SheafOfModules R) => SheafOfModules.fromFreeYonedaSheafCoproduct R M, naturality := ⋯ }

instance SheafOfModules.hasSeparator {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] : CategoryTheory.HasSeparator (SheafOfModules R)

Sheaves of modules on a small site have a separator: the coproduct of the free sheaves on representables.

instance SheafOfModules.isGrothendieckAbelian {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] : CategoryTheory.IsGrothendieckAbelian.{u, u, u + 1} (SheafOfModules R)

Sheaves of modules on a small site form a Grothendieck abelian category.