Sheaves of modules over a sheaf of rings

In this file, we define the category SheafOfModules R when R : Sheaf J RingCat is a sheaf of rings on a category C equipped with a Grothendieck topology J.

TODO

• construct the associated sheaf: more precisely, given a morphism of α : P ⟶ R.val where P is a presheaf of rings and R a sheaf of rings such that α identifies R to the associated sheaf of P, then construct a sheafification functor PresheafOfModules P ⥤ SheafOfModules R.

structure SheafOfModules {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) : Type (max (max (max u u₁) (v + 1)) v₁)

A sheaf of modules is a presheaf of modules such that the underlying presheaf of abelian groups is a sheaf.

• val : PresheafOfModules R.val

  the underlying presheaf of modules of a sheaf of modules

• isSheaf : CategoryTheory.Presheaf.IsSheaf J self.val.presheaf

theorem SheafOfModules.isSheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (self : SheafOfModules R) : CategoryTheory.Presheaf.IsSheaf J self.val.presheaf

theorem SheafOfModules.Hom.ext {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {X Y : SheafOfModules R} (x y : X.Hom Y), x.val = y.val → x = y

theorem SheafOfModules.Hom.ext_iff {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {X Y : SheafOfModules R} (x y : X.Hom Y), x = y ↔ x.val = y.val

structure SheafOfModules.Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (X : SheafOfModules R) (Y : SheafOfModules R) : Type (max u₁ v)

A morphism between sheaves of modules is a morphism between the underlying presheaves of modules.

• val : X.val ⟶ Y.val

  a morphism between the underlying presheaves of modules

instance SheafOfModules.instCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} : CategoryTheory.Category.{max u₁ v, max (max (max (v + 1) u) u₁) v₁} (SheafOfModules R)

Equations

• SheafOfModules.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯

theorem SheafOfModules.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {X : SheafOfModules R} {Y : SheafOfModules R} {f : X ⟶ Y} {g : X ⟶ Y} (h : f.val = g.val) : f = g

@[simp]

theorem SheafOfModules.id_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (X : SheafOfModules R) : (CategoryTheory.CategoryStruct.id X).val = CategoryTheory.CategoryStruct.id X.val

theorem SheafOfModules.comp_val_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {X : SheafOfModules R} {Y : SheafOfModules R} {Z : SheafOfModules R} (f : X ⟶ Y) (g : Y ⟶ Z✝) {Z : PresheafOfModules R.val} (h : Z✝.val ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).val h = CategoryTheory.CategoryStruct.comp f.val (CategoryTheory.CategoryStruct.comp g.val h)

@[simp]

theorem SheafOfModules.comp_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {X : SheafOfModules R} {Y : SheafOfModules R} {Z : SheafOfModules R} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).val = CategoryTheory.CategoryStruct.comp f.val g.val

@[simp]

theorem SheafOfModules.forget_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) (F : SheafOfModules R) : (SheafOfModules.forget R).obj F = F.val

@[simp]

theorem SheafOfModules.forget_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) : ∀ {X Y : SheafOfModules R} (φ : X ⟶ Y), (SheafOfModules.forget R).map φ = φ.val

def SheafOfModules.forget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) : CategoryTheory.Functor (SheafOfModules R) (PresheafOfModules R.val)

The forgetful functor SheafOfModules.{v} R ⥤ PresheafOfModules R.val.

Equations

• SheafOfModules.forget R = { obj := fun (F : SheafOfModules R) => F.val, map := fun {X Y : SheafOfModules R} (φ : X ⟶ Y) => φ.val, map_id := ⋯, map_comp := ⋯ }

instance SheafOfModules.instFaithfulPresheafOfModulesValRingCatForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) : (SheafOfModules.forget R).Faithful

Equations

• ⋯ = ⋯

instance SheafOfModules.instFullPresheafOfModulesValRingCatForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) : (SheafOfModules.forget R).Full

Equations

• ⋯ = ⋯

def SheafOfModules.evaluation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) (X : Cᵒᵖ) : CategoryTheory.Functor (SheafOfModules R) (ModuleCat ↑(R.val.obj X))

Evaluation on an object X gives a functor SheafOfModules R ⥤ ModuleCat (R.val.obj X).

Equations

• SheafOfModules.evaluation R X = (SheafOfModules.forget R).comp (PresheafOfModules.evaluation R.val X)