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.

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

structure SheafOfModules.Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (X 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

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} (val : 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

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

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

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

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

@[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

@[simp]

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

theorem SheafOfModules.comp_val_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {X Y 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)

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.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✝) : (forget R).map φ = φ.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) : (forget R).obj F = F.val

def SheafOfModules.fullyFaithfulForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) : (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.

@[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} (φ : (forget R).obj X✝ ⟶ (forget R).obj Y✝) : ((fullyFaithfulForget R).preimage φ).val = φ

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

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

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

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)

noncomputable 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.toSheaf_obj_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) (M : SheafOfModules R) : ((toSheaf R).obj M).val = M.val.presheaf

@[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✝) : ((toSheaf R).map f).val = ((forget R).comp (PresheafOfModules.toPresheaf R.val)).map f

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.

@[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✝ Y✝ : SheafOfModules R} (f : X✝ ⟶ Y✝) : ((forgetToSheafModuleCat R X hX).map f).val = (PresheafOfModules.forgetToPresheafModuleCat X hX).map f.val

@[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) : ((forgetToSheafModuleCat R X hX).obj M).val = (PresheafOfModules.forgetToPresheafModuleCat X hX).obj M.val

noncomputable def SheafOfModules.toSheafCompSheafToPresheafIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) : (toSheaf R).comp (CategoryTheory.sheafToPresheaf J AddCommGrp) ≅ (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) : (toSheaf R).Faithful

instance SheafOfModules.instAddCommGroupHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) (M 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 N : SheafOfModules R} (f 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) : (forget R).Additive

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

@[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 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 N P : SheafOfModules R} (f : M ⟶ N) (g : N ⟶ P) (s : M.sections) : sectionsMap (CategoryTheory.CategoryStruct.comp f g) s = sectionsMap g (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) : sectionsMap (CategoryTheory.CategoryStruct.id M) s = s

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.sectionsFunctor_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) (M : SheafOfModules R) : (sectionsFunctor R).obj M = M.sections

@[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) : (sectionsFunctor R).map f s = sectionsMap f s

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

@[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)] : (unit R).val = PresheafOfModules.unit R.val

noncomputable 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) : (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 : unit R ⟶ M) (X : Cᵒᵖ) : ↑(M.unitHomEquiv f) X = (CategoryTheory.ConcreteCategory.hom (f.val.app 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 N : SheafOfModules R} (f : unit R ⟶ M) (p : M ⟶ N) : N.unitHomEquiv (CategoryTheory.CategoryStruct.comp f p) = 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 N : SheafOfModules R} (s : M.sections) (p : M ⟶ N) : CategoryTheory.CategoryStruct.comp (M.unitHomEquiv.symm s) p = N.unitHomEquiv.symm (sectionsMap p s)

@[reducible, inline]

abbrev PresheafOfModules.IsLocallySurjective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) : Prop

A morphism of presheaves of modules is locally surjective if the underlying morphism of presheaves of abelian groups is.

Equations

• PresheafOfModules.IsLocallySurjective J f = CategoryTheory.Presheaf.IsLocallySurjective J ((PresheafOfModules.toPresheaf R).map f)

@[reducible, inline]

abbrev PresheafOfModules.IsLocallyInjective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) : Prop

A morphism of presheaves of modules is locally injective if the underlying morphism of presheaves of abelian groups is.

Equations

• PresheafOfModules.IsLocallyInjective J f = CategoryTheory.Presheaf.IsLocallyInjective J ((PresheafOfModules.toPresheaf R).map f)

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

@[simp]

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

@[simp]

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