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 := ⋯ }

@[simp]

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

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

The forget functor SheafOfModules R ⥤ PresheafOfModules R.val is fully faithful.

Equations

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

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

• ⋯ = ⋯

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

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)

@[simp]

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

@[simp]

theorem SheafOfModules.toSheaf_obj_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) (M : SheafOfModules R) : ((SheafOfModules.toSheaf R).obj M).val = M.val.presheaf

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

The forget functor SheafOfModules R ⥤ Sheaf J AddCommGrp.

Equations

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

@[simp]

theorem SheafOfModules.forgetToSheafModuleCat_obj_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (M : SheafOfModules R) : ((SheafOfModules.forgetToSheafModuleCat R X hX).obj M).val = (PresheafOfModules.forgetToPresheafModuleCat X hX).obj M.val

@[simp]

theorem SheafOfModules.forgetToSheafModuleCat_map_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) : ∀ {X_1 Y : SheafOfModules R} (f : X_1 ⟶ Y), ((SheafOfModules.forgetToSheafModuleCat R X hX).map f).val = (PresheafOfModules.forgetToPresheafModuleCat X hX).map f.val

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

The forgetful functor from sheaves of modules over sheaf of ring R to sheaves of R(X)-module when X is initial.

Equations

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

def SheafOfModules.toSheafCompSheafToPresheafIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) : (SheafOfModules.toSheaf R).comp (CategoryTheory.sheafToPresheaf J AddCommGrp) ≅ (SheafOfModules.forget R).comp (PresheafOfModules.toPresheaf R.val)

The canonical isomorphism between SheafOfModules.toSheaf R ⋙ sheafToPresheaf J AddCommGrp.{v} and SheafOfModules.forget R ⋙ PresheafOfModules.toPresheaf R.val.

Equations

• SheafOfModules.toSheafCompSheafToPresheafIso R = CategoryTheory.Iso.refl ((SheafOfModules.toSheaf R).comp (CategoryTheory.sheafToPresheaf J AddCommGrp))

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

Equations

• ⋯ = ⋯

instance SheafOfModules.instAddCommGroupHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) (M : SheafOfModules R) (N : SheafOfModules R) : AddCommGroup (M ⟶ N)

Equations

• SheafOfModules.instAddCommGroupHom R M N = (SheafOfModules.fullyFaithfulForget R).homEquiv.addCommGroup

@[simp]

theorem SheafOfModules.add_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) {M : SheafOfModules R} {N : SheafOfModules R} (f : M ⟶ N) (g : M ⟶ N) : (f + g).val = f.val + g.val

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

Equations

• SheafOfModules.instPreadditive R = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }

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

Equations

• ⋯ = ⋯

instance SheafOfModules.instAdditiveSheafAddCommGrpToSheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) : (SheafOfModules.toSheaf R).Additive

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev SheafOfModules.sections {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R) : Type (max u₁ v)

The type of sections of a sheaf of modules.

Equations

• M.sections = M.val.sections

@[reducible, inline]

abbrev SheafOfModules.sectionsMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} {N : SheafOfModules R} (f : M ⟶ N) (s : M.sections) : N.sections

The map M.sections → N.sections induced by a morphisms M ⟶ N of sheaves of modules.

Equations

• SheafOfModules.sectionsMap f s = PresheafOfModules.sectionsMap f.val s

@[simp]

theorem SheafOfModules.sectionsMap_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} {N : SheafOfModules R} {P : SheafOfModules R} (f : M ⟶ N) (g : N ⟶ P) (s : M.sections) : SheafOfModules.sectionsMap (CategoryTheory.CategoryStruct.comp f g) s = SheafOfModules.sectionsMap g (SheafOfModules.sectionsMap f s)

@[simp]

theorem SheafOfModules.sectionsMap_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} (s : M.sections) : SheafOfModules.sectionsMap (CategoryTheory.CategoryStruct.id M) s = s

@[simp]

theorem SheafOfModules.sectionsFunctor_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) : ∀ {X Y : SheafOfModules R} (f : X ⟶ Y) (s : X.sections), (SheafOfModules.sectionsFunctor R).map f s = SheafOfModules.sectionsMap f s

@[simp]

theorem SheafOfModules.sectionsFunctor_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) (M : SheafOfModules R) : (SheafOfModules.sectionsFunctor R).obj M = M.sections

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

The functor which sends a sheaf of modules to its type of sections.

Equations

• SheafOfModules.sectionsFunctor R = { obj := SheafOfModules.sections, map := fun {X Y : SheafOfModules R} (f : X ⟶ Y) => SheafOfModules.sectionsMap f, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem SheafOfModules.unit_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] : (SheafOfModules.unit R).val = PresheafOfModules.unit R.val

def SheafOfModules.unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] : SheafOfModules R

The obvious free sheaf of modules of rank 1.

Equations

• SheafOfModules.unit R = { val := PresheafOfModules.unit R.val, isSheaf := ⋯ }

def SheafOfModules.unitHomEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] (M : SheafOfModules R) : (SheafOfModules.unit R ⟶ M) ≃ M.sections

The bijection (unit R ⟶ M) ≃ M.sections for M : SheafOfModules R.

Equations

• M.unitHomEquiv = (SheafOfModules.fullyFaithfulForget R).homEquiv.trans M.val.unitHomEquiv

@[simp]

theorem SheafOfModules.unitHomEquiv_apply_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] (M : SheafOfModules R) (f : SheafOfModules.unit R ⟶ M) (X : Cᵒᵖ) : ↑(M.unitHomEquiv f) X = (PresheafOfModules.Hom.app f.val X) 1

theorem SheafOfModules.unitHomEquiv_comp_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] {M : SheafOfModules R} {N : SheafOfModules R} (f : SheafOfModules.unit R ⟶ M) (p : M ⟶ N) : N.unitHomEquiv (CategoryTheory.CategoryStruct.comp f p) = SheafOfModules.sectionsMap p (M.unitHomEquiv f)

theorem SheafOfModules.unitHomEquiv_symm_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] {M : SheafOfModules R} {N : SheafOfModules R} (s : M.sections) (p : M ⟶ N) : CategoryTheory.CategoryStruct.comp (M.unitHomEquiv.symm s) p = N.unitHomEquiv.symm (SheafOfModules.sectionsMap p s)

@[simp]

theorem PresheafOfModules.homEquivOfIsLocallyBijective_symm_apply_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ : PresheafOfModules R} {M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) {N : PresheafOfModules R} (hN : CategoryTheory.Presheaf.IsSheaf J N.presheaf) [J.WEqualsLocallyBijective AddCommGrp] [CategoryTheory.Presheaf.IsLocallySurjective J f.hom] [CategoryTheory.Presheaf.IsLocallyInjective J f.hom] (ψ : M₁ ⟶ N) : ((PresheafOfModules.homEquivOfIsLocallyBijective f hN).symm ψ).hom = (CategoryTheory.Localization.LeftBousfield.W.homEquiv ⋯ N.presheaf hN).symm ψ.hom

@[simp]

theorem PresheafOfModules.homEquivOfIsLocallyBijective_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ : PresheafOfModules R} {M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) {N : PresheafOfModules R} (hN : CategoryTheory.Presheaf.IsSheaf J N.presheaf) [J.WEqualsLocallyBijective AddCommGrp] [CategoryTheory.Presheaf.IsLocallySurjective J f.hom] [CategoryTheory.Presheaf.IsLocallyInjective J f.hom] (φ : M₂ ⟶ N) : (PresheafOfModules.homEquivOfIsLocallyBijective f hN) φ = CategoryTheory.CategoryStruct.comp f φ

noncomputable def PresheafOfModules.homEquivOfIsLocallyBijective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ : PresheafOfModules R} {M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) {N : PresheafOfModules R} (hN : CategoryTheory.Presheaf.IsSheaf J N.presheaf) [J.WEqualsLocallyBijective AddCommGrp] [CategoryTheory.Presheaf.IsLocallySurjective J f.hom] [CategoryTheory.Presheaf.IsLocallyInjective J f.hom] : (M₂ ⟶ N) ≃ (M₁ ⟶ N)

The bijection (M₂ ⟶ N) ≃ (M₁ ⟶ N) induced by a locally bijective morphism f : M₁ ⟶ M₂ of presheaves of modules, when N is a sheaf.

Equations

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