Basic definitions for sheaves of modules

This file collects the coefficient sheaf obtained by forgetting commutativity, the original commutative-ring actions on its section modules, the counit identifying the sheafification of the underlying presheaf of a sheaf of modules with that sheaf, and the vanishing of every sheaf of modules over a sheaf of rings whose sections are trivial.

Main declarations

• SheafOfModules.ringCatSheaf forgets commutativity in a sheaf of commutative rings;
• SheafOfModules.isZero_of_forall_subsingleton: sheaves of modules over a sheaf of rings all of whose rings of sections are trivial are zero objects;
• SheafOfModules.sheafificationIso identifies a sheaf of modules with the sheafification of its underlying presheaf, naturally (SheafOfModules.sheafificationIso_inv_naturality).

This supports TauCetiRoadmap/JacobianChallenge/README.md, Layer A, item "Invertible sheaves on a scheme; the Picard group Pic X under ⊗".

theorem TauCeti.SheafOfModules.isZero_of_forall_subsingleton {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.Sheaf J RingCat} (hS : ∀ (W : Cᵒᵖ), Subsingleton ↑(S.obj.obj W)) (N : SheafOfModules S) : CategoryTheory.Limits.IsZero N

Every sheaf of modules over a sheaf of rings all of whose rings of sections are trivial is a zero object.

@[reducible, inline]

abbrev TauCeti.SheafOfModules.ringCatSheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J CommRingCat) [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] : CategoryTheory.Sheaf J RingCat

The sheaf of rings underlying a sheaf of commutative rings on a site; the site-level analogue of AlgebraicGeometry.Scheme.ringCatSheaf.

Equations

• TauCeti.SheafOfModules.ringCatSheaf R = (CategoryTheory.sheafCompose J (CategoryTheory.forget₂ CommRingCat RingCat)).obj R

@[instance_reducible]

instance SheafOfModules.sectionModule {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] (P : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) (U : Cᵒᵖ) : Module ↑(R.obj.obj U) ↑(P.val.obj U)

Sections of a sheaf of modules over the underlying ring sheaf retain the module action of the original commutative ring of sections.

Equations

• P.sectionModule U = { toSMul := SheafOfModules.sectionModule._aux_1 P U, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

noncomputable def TauCeti.SheafOfModules.sheafificationIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J RingCat) (M : SheafOfModules R) : (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).obj M.val ≅ M

Sheafifying the underlying presheaf of modules of a sheaf of R-modules M, for a sheaf of rings R, recovers M; this is the counit of the sheafification adjunction.

Equations

• TauCeti.SheafOfModules.sheafificationIso R M = (CategoryTheory.asIso (PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id R.obj)).counit).app M

@[simp]

theorem TauCeti.SheafOfModules.sheafificationIso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J RingCat) (M : SheafOfModules R) : (sheafificationIso R M).hom = (PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id R.obj)).counit.app M

The forward map of sheafificationIso is the counit of the sheafification adjunction.

theorem TauCeti.SheafOfModules.sheafificationIso_inv_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J RingCat} {M N : SheafOfModules R} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp f (sheafificationIso R N).inv = CategoryTheory.CategoryStruct.comp (sheafificationIso R M).inv ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).map f.val)

sheafificationIso is natural: its inverse intertwines a morphism of sheaves of modules with the sheafification of the underlying morphism of presheaves of modules.

theorem TauCeti.SheafOfModules.sheafificationIso_inv_naturality_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J RingCat} {M N : SheafOfModules R} (f : M ⟶ N) {Z : SheafOfModules R} (h : (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).obj N.val ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (sheafificationIso R N).inv h) = CategoryTheory.CategoryStruct.comp (sheafificationIso R M).inv (CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).map f.val) h)

sheafificationIso is natural: its inverse intertwines a morphism of sheaves of modules with the sheafification of the underlying morphism of presheaves of modules.

theorem TauCeti.SheafOfModules.sheafificationIso_hom_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J RingCat} {M N : SheafOfModules R} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).map f.val) (sheafificationIso R N).hom = CategoryTheory.CategoryStruct.comp (sheafificationIso R M).hom f

The inverse direction of sheafificationIso_inv_naturality.

theorem TauCeti.SheafOfModules.sheafificationIso_hom_naturality_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J RingCat} {M N : SheafOfModules R} (f : M ⟶ N) {Z : SheafOfModules R} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).map f.val) (CategoryTheory.CategoryStruct.comp (sheafificationIso R N).hom h) = CategoryTheory.CategoryStruct.comp (sheafificationIso R M).hom (CategoryTheory.CategoryStruct.comp f h)

The inverse direction of sheafificationIso_inv_naturality.