Module structures on restrictions to slice sites

Restricting a sheaf of modules to the slice over an object preserves its section modules. For a commutative coefficient sheaf, these sections retain the action of the original commutative ring of sections after forgetting commutativity in the coefficient sheaf.

Since 𝟙 X is a terminal object of the slice over X, a global section of the restriction M.over X is the same as a section of M over X.

Main declarations

• SheafOfModules.overSectionModule: the original commutative-ring action on sections of a sheaf of modules restricted to a slice site;
• SheafOfModules.overSectionsEquiv: global sections of M.over X are sections of M over X.

@[instance_reducible]

instance SheafOfModules.overSectionModule {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 V : C) (g : V ⟶ U) : Module ↑(R.obj.obj (Opposite.op V)) ↑((P.over U).val.obj (Opposite.op (CategoryTheory.Over.mk g)))

Restriction to a slice uses the original commutative-ring action on each section module.

Equations

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

noncomputable def SheafOfModules.overSectionsEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R) (X : C) : (M.over X).sections ≃ ↑(M.val.obj (Opposite.op X))

Global sections of the restriction M.over X are the sections of M over X: a global section is determined by its value over the terminal object 𝟙 X, and a section s over X gives the global section whose value over f : Y ⟶ X is the restriction of s along f.

Equations

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

@[simp]

theorem SheafOfModules.overSectionsEquiv_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R) (X : C) (s : (M.over X).sections) : (M.overSectionsEquiv X) s = PresheafOfModules.sections.eval s (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id X)))

The section of M over X attached to a global section of M.over X is its value over the terminal object 𝟙 X.

@[simp]

theorem SheafOfModules.overSectionsEquiv_symm_apply_eval {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R) (X : C) (s : ↑(M.val.obj (Opposite.op X))) (Y : CategoryTheory.Over X) : PresheafOfModules.sections.eval ((M.overSectionsEquiv X).symm s) (Opposite.op Y) = (CategoryTheory.ConcreteCategory.hom (M.val.map Y.hom.op)) s

The global section of M.over X attached to a section s of M over X takes the value M.val.map f.op s over f : Y ⟶ X.