Presheaves of modules over a presheaf of rings.

Given a presheaf of rings R : Cᵒᵖ ⥤ RingCat, we define the category PresheafOfModules R. An object M : PresheafOfModules R consists of a family of modules M.obj X : ModuleCat (R.obj X) for all X : Cᵒᵖ, together with the data, for all f : X ⟶ Y, of a functorial linear map M.map f from M.obj X to the restriction of scalars of M.obj Y via R.map f.

Future work

• Compare this to the definition as a presheaf of pairs (R, M) with specified first part.
• Compare this to the definition as a module object of the presheaf of rings thought of as a monoid object.
• Presheaves of modules over a presheaf of commutative rings form a monoidal category.
• Pushforward and pullback.

structure PresheafOfModules {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) : Type (max (max (max u u₁) (v + 1)) v₁)

A presheaf of modules over R : Cᵒᵖ ⥤ RingCat consists of family of objects obj X : ModuleCat (R.obj X) for all X : Cᵒᵖ together with functorial maps obj X ⟶ (ModuleCat.restrictScalars (R.map f)).obj (obj Y) for all f : X ⟶ Y in Cᵒᵖ.

• obj (X : Cᵒᵖ) : ModuleCat ↑(R.obj X)

  a family of modules over R.obj X for all X

• map {X Y : Cᵒᵖ} (f : X ⟶ Y) : self.obj X ⟶ (ModuleCat.restrictScalars (R.map f).hom).obj (self.obj Y)

  the restriction maps of a presheaf of modules

• map_id (X : Cᵒᵖ) : self.map (CategoryTheory.CategoryStruct.id X) = (ModuleCat.restrictScalarsId' (R.map (CategoryTheory.CategoryStruct.id X)).hom ⋯).inv.app (self.obj X)
• map_comp {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) : self.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (self.map f) (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars (R.map f).hom).map (self.map g)) ((ModuleCat.restrictScalarsComp' (R.map f).hom (R.map g).hom (R.map (CategoryTheory.CategoryStruct.comp f g)).hom ⋯).inv.app (self.obj Z)))

theorem PresheafOfModules.map_comp_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (self : PresheafOfModules R) {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : ModuleCat ↑(R.obj X)} (h : (ModuleCat.restrictScalars (R.map (CategoryTheory.CategoryStruct.comp f g)).hom).obj (self.obj Z) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (self.map (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (self.map f) (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars (R.map f).hom).map (self.map g)) (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalarsComp' (R.map f).hom (R.map g).hom (R.map (CategoryTheory.CategoryStruct.comp f g)).hom ⋯).inv.app (self.obj Z)) h))

theorem PresheafOfModules.map_smul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) {X Y : Cᵒᵖ} (f : X ⟶ Y) (r : ↑(R.obj X)) (m : ↑(M.obj X)) : (M.map f).hom (r • m) = (R.map f).hom r • (M.map f).hom m

theorem PresheafOfModules.congr_map_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) {X Y : Cᵒᵖ} {f g : X ⟶ Y} (h : f = g) (m : ↑(M.obj X)) : (M.map f).hom m = (M.map g).hom m

structure PresheafOfModules.Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M₁ M₂ : PresheafOfModules R) : Type (max u₁ v)

A morphism of presheaves of modules consists of a family of linear maps which satisfy the naturality condition.

• app (X : Cᵒᵖ) : M₁.obj X ⟶ M₂.obj X

  a family of linear maps M₁.obj X ⟶ M₂.obj X for all X.

• naturality {X Y : Cᵒᵖ} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (M₁.map f) ((ModuleCat.restrictScalars (R.map f).hom).map (self.app Y)) = CategoryTheory.CategoryStruct.comp (self.app X) (M₂.map f)

theorem PresheafOfModules.Hom.ext {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} {x y : M₁.Hom M₂} (app : x.app = y.app) : x = y

@[simp]

theorem PresheafOfModules.Hom.naturality_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (self : M₁.Hom M₂) {X Y : Cᵒᵖ} (f : X ⟶ Y) {Z : ModuleCat ↑(R.obj X)} (h : (ModuleCat.restrictScalars (R.map f).hom).obj (M₂.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (M₁.map f) (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars (R.map f).hom).map (self.app Y)) h) = CategoryTheory.CategoryStruct.comp (self.app X) (CategoryTheory.CategoryStruct.comp (M₂.map f) h)

instance PresheafOfModules.instCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} : CategoryTheory.Category.{max u₁ v, max (max (max (v + 1) u) u₁) v₁} (PresheafOfModules R)

Equations

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

theorem PresheafOfModules.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} {f g : M₁ ⟶ M₂} (h : ∀ (X : Cᵒᵖ), f.app X = g.app X) : f = g

@[simp]

theorem PresheafOfModules.id_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) (X : Cᵒᵖ) : (CategoryTheory.CategoryStruct.id M).app X = CategoryTheory.CategoryStruct.id (M.obj X)

@[simp]

theorem PresheafOfModules.comp_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ M₃ : PresheafOfModules R} (f : M₁ ⟶ M₂) (g : M₂ ⟶ M₃) (X : Cᵒᵖ) : (CategoryTheory.CategoryStruct.comp f g).app X = CategoryTheory.CategoryStruct.comp (f.app X) (g.app X)

theorem PresheafOfModules.naturality_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) {X Y : Cᵒᵖ} (g : X ⟶ Y) (x : ↑(M₁.obj X)) : (f.app Y).hom ((M₁.map g).hom x) = (M₂.map g).hom ((f.app X).hom x)

def PresheafOfModules.isoMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (app : (X : Cᵒᵖ) → M₁.obj X ≅ M₂.obj X) (naturality : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (M₁.map f) ((ModuleCat.restrictScalars (R.map f).hom).map (app Y).hom) = CategoryTheory.CategoryStruct.comp (app X).hom (M₂.map f) := by aesop_cat) : M₁ ≅ M₂

Constructor for isomorphisms in the category of presheaves of modules.

Equations

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

@[simp]

theorem PresheafOfModules.isoMk_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (app : (X : Cᵒᵖ) → M₁.obj X ≅ M₂.obj X) (naturality : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (M₁.map f) ((ModuleCat.restrictScalars (R.map f).hom).map (app Y).hom) = CategoryTheory.CategoryStruct.comp (app X).hom (M₂.map f) := by aesop_cat) (X : Cᵒᵖ) : (PresheafOfModules.isoMk app naturality).inv.app X = (app X).inv

@[simp]

theorem PresheafOfModules.isoMk_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (app : (X : Cᵒᵖ) → M₁.obj X ≅ M₂.obj X) (naturality : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (M₁.map f) ((ModuleCat.restrictScalars (R.map f).hom).map (app Y).hom) = CategoryTheory.CategoryStruct.comp (app X).hom (M₂.map f) := by aesop_cat) (X : Cᵒᵖ) : (PresheafOfModules.isoMk app naturality).hom.app X = (app X).hom

def PresheafOfModules.presheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) : CategoryTheory.Functor Cᵒᵖ Ab

The underlying presheaf of abelian groups of a presheaf of modules.

Equations

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

@[simp]

theorem PresheafOfModules.presheaf_obj_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) (X : Cᵒᵖ) : ↑(M.presheaf.obj X) = ↑(M.obj X)

@[simp]

theorem PresheafOfModules.presheaf_map_apply_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) {X Y : Cᵒᵖ} (f : X ⟶ Y) (x : ↑(M.obj X)) : (M.presheaf.map f) x = (M.map f).hom x

instance PresheafOfModules.instModuleCarrierObjOppositeRingCatαAddCommGroupAbPresheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) (X : Cᵒᵖ) : Module ↑(R.obj X) ↑(M.presheaf.obj X)

Equations

• M.instModuleCarrierObjOppositeRingCatαAddCommGroupAbPresheaf X = inferInstanceAs (Module ↑(R.obj X) ↑(M.obj X))

def PresheafOfModules.toPresheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) : CategoryTheory.Functor (PresheafOfModules R) (CategoryTheory.Functor Cᵒᵖ Ab)

The forgetful functor PresheafOfModules R ⥤ Cᵒᵖ ⥤ Ab.

Equations

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

@[simp]

theorem PresheafOfModules.toPresheaf_obj_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) (X : Cᵒᵖ) : ↑(((PresheafOfModules.toPresheaf R).obj M).obj X) = ↑(M.obj X)

@[simp]

theorem PresheafOfModules.toPresheaf_map_app_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) (X : Cᵒᵖ) (x : ↑(M₁.obj X)) : (((PresheafOfModules.toPresheaf R).map f).app X) x = (f.app X).hom x

instance PresheafOfModules.instFaithfulFunctorOppositeAbToPresheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} : (PresheafOfModules.toPresheaf R).Faithful

def PresheafOfModules.ofPresheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : CategoryTheory.Functor Cᵒᵖ Ab) [(X : Cᵒᵖ) → Module ↑(R.obj X) ↑(M.obj X)] (map_smul : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r : ↑(R.obj X)) (m : ↑(M.obj X)), (M.map f) (r • m) = (R.map f).hom r • (M.map f) m) : PresheafOfModules R

The object in PresheafOfModules R that is obtained from M : Cᵒᵖ ⥤ Ab.{v} such that for all X : Cᵒᵖ, M.obj X is a R.obj X module, in such a way that the restriction maps are semilinear. (This constructor should be used only in cases when the preferred constructor PresheafOfModules.mk is not as convenient as this one.)

Equations

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

@[simp]

theorem PresheafOfModules.ofPresheaf_obj_isModule {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : CategoryTheory.Functor Cᵒᵖ Ab) [(X : Cᵒᵖ) → Module ↑(R.obj X) ↑(M.obj X)] (map_smul : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r : ↑(R.obj X)) (m : ↑(M.obj X)), (M.map f) (r • m) = (R.map f).hom r • (M.map f) m) (X : Cᵒᵖ) : ((PresheafOfModules.ofPresheaf M map_smul).obj X).isModule = inst✝ X

@[simp]

theorem PresheafOfModules.ofPresheaf_map_hom_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : CategoryTheory.Functor Cᵒᵖ Ab) [(X : Cᵒᵖ) → Module ↑(R.obj X) ↑(M.obj X)] (map_smul : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r : ↑(R.obj X)) (m : ↑(M.obj X)), (M.map f) (r • m) = (R.map f).hom r • (M.map f) m) {X Y : Cᵒᵖ} (f : X ⟶ Y) (x : ↑(M.obj X)) : ((PresheafOfModules.ofPresheaf M map_smul).map f).hom x = (M.map f) x

@[simp]

theorem PresheafOfModules.ofPresheaf_obj_isAddCommGroup {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : CategoryTheory.Functor Cᵒᵖ Ab) [(X : Cᵒᵖ) → Module ↑(R.obj X) ↑(M.obj X)] (map_smul : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r : ↑(R.obj X)) (m : ↑(M.obj X)), (M.map f) (r • m) = (R.map f).hom r • (M.map f) m) (X : Cᵒᵖ) : ((PresheafOfModules.ofPresheaf M map_smul).obj X).isAddCommGroup = AddCommGrp.addCommGroupInstance (M.obj X)

@[simp]

theorem PresheafOfModules.ofPresheaf_obj_carrier {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : CategoryTheory.Functor Cᵒᵖ Ab) [(X : Cᵒᵖ) → Module ↑(R.obj X) ↑(M.obj X)] (map_smul : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r : ↑(R.obj X)) (m : ↑(M.obj X)), (M.map f) (r • m) = (R.map f).hom r • (M.map f) m) (X : Cᵒᵖ) : ↑((PresheafOfModules.ofPresheaf M map_smul).obj X) = ↑(M.obj X)

@[simp]

theorem PresheafOfModules.ofPresheaf_presheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : CategoryTheory.Functor Cᵒᵖ Ab) [(X : Cᵒᵖ) → Module ↑(R.obj X) ↑(M.obj X)] (map_smul : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r : ↑(R.obj X)) (m : ↑(M.obj X)), (M.map f) (r • m) = (R.map f).hom r • (M.map f) m) : (PresheafOfModules.ofPresheaf M map_smul).presheaf = M

def PresheafOfModules.homMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (φ : M₁.presheaf ⟶ M₂.presheaf) (hφ : ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (m : ↑(M₁.obj X)), (φ.app X) (r • m) = r • (φ.app X) m) : M₁ ⟶ M₂

The morphism of presheaves of modules M₁ ⟶ M₂ given by a morphism of abelian presheaves M₁.presheaf ⟶ M₂.presheaf which satisfy a suitable linearity condition.

Equations

• PresheafOfModules.homMk φ hφ = { app := fun (X : Cᵒᵖ) => ModuleCat.ofHom { toFun := ⇑(φ.app X), map_add' := ⋯, map_smul' := ⋯ }, naturality := ⋯ }

@[simp]

theorem PresheafOfModules.homMk_app_hom_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (φ : M₁.presheaf ⟶ M₂.presheaf) (hφ : ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (m : ↑(M₁.obj X)), (φ.app X) (r • m) = r • (φ.app X) m) (X : Cᵒᵖ) (a : ↑(M₁.presheaf.obj X)) : ((PresheafOfModules.homMk φ hφ).app X).hom a = (φ.app X) a

instance PresheafOfModules.instZeroHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} : Zero (M₁ ⟶ M₂)

Equations

• PresheafOfModules.instZeroHom = { zero := { app := fun (x : Cᵒᵖ) => 0, naturality := ⋯ } }

@[simp]

theorem PresheafOfModules.zero_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M₁ M₂ : PresheafOfModules R) (X : Cᵒᵖ) : PresheafOfModules.Hom.app 0 X = 0

instance PresheafOfModules.instNegHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} : Neg (M₁ ⟶ M₂)

Equations

• PresheafOfModules.instNegHom = { neg := fun (f : M₁ ⟶ M₂) => { app := fun (X : Cᵒᵖ) => -f.app X, naturality := ⋯ } }

instance PresheafOfModules.instAddHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} : Add (M₁ ⟶ M₂)

Equations

• PresheafOfModules.instAddHom = { add := fun (f g : M₁ ⟶ M₂) => { app := fun (X : Cᵒᵖ) => f.app X + g.app X, naturality := ⋯ } }

instance PresheafOfModules.instSubHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} : Sub (M₁ ⟶ M₂)

Equations

• PresheafOfModules.instSubHom = { sub := fun (f g : M₁ ⟶ M₂) => { app := fun (X : Cᵒᵖ) => f.app X - g.app X, naturality := ⋯ } }

@[simp]

theorem PresheafOfModules.neg_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) (X : Cᵒᵖ) : (-f).app X = -f.app X

@[simp]

theorem PresheafOfModules.add_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f g : M₁ ⟶ M₂) (X : Cᵒᵖ) : (f + g).app X = f.app X + g.app X

@[simp]

theorem PresheafOfModules.sub_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f g : M₁ ⟶ M₂) (X : Cᵒᵖ) : (f - g).app X = f.app X - g.app X

instance PresheafOfModules.instAddCommGroupHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} : AddCommGroup (M₁ ⟶ M₂)

Equations

• PresheafOfModules.instAddCommGroupHom = AddCommGroup.mk ⋯

instance PresheafOfModules.instPreadditive {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} : CategoryTheory.Preadditive (PresheafOfModules R)

Equations

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

instance PresheafOfModules.instAdditiveFunctorOppositeAbToPresheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} : (PresheafOfModules.toPresheaf R).Additive

theorem PresheafOfModules.zsmul_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (n : ℤ) (f : M₁ ⟶ M₂) (X : Cᵒᵖ) : (n • f).app X = n • f.app X

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

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

Equations

• PresheafOfModules.evaluation R X = { obj := fun (M : PresheafOfModules R) => M.obj X, map := fun {X_1 Y : PresheafOfModules R} (f : X_1 ⟶ Y) => f.app X, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem PresheafOfModules.evaluation_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (X : Cᵒᵖ) (M : PresheafOfModules R) : (PresheafOfModules.evaluation R X).obj M = M.obj X

@[simp]

theorem PresheafOfModules.evaluation_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (X : Cᵒᵖ) {X✝ Y✝ : PresheafOfModules R} (f : X✝ ⟶ Y✝) : (PresheafOfModules.evaluation R X).map f = f.app X

instance PresheafOfModules.instAdditiveModuleCatCarrierObjOppositeRingCatEvaluation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (X : Cᵒᵖ) : (PresheafOfModules.evaluation R X).Additive

noncomputable def PresheafOfModules.restriction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) {X Y : Cᵒᵖ} (f : X ⟶ Y) : PresheafOfModules.evaluation R X ⟶ (PresheafOfModules.evaluation R Y).comp (ModuleCat.restrictScalars (R.map f).hom)

The restriction natural transformation on presheaves of modules, considered as linear maps to restriction of scalars.

Equations

• PresheafOfModules.restriction R f = { app := fun (M : PresheafOfModules R) => M.map f, naturality := ⋯ }

@[simp]

theorem PresheafOfModules.restriction_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) {X Y : Cᵒᵖ} (f : X ⟶ Y) (M : PresheafOfModules R) : (PresheafOfModules.restriction R f).app M = M.map f

def PresheafOfModules.unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) : PresheafOfModules R

The obvious free presheaf of modules of rank 1.

Equations

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

theorem PresheafOfModules.unit_map_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) {X Y : Cᵒᵖ} (f : X ⟶ Y) : ((PresheafOfModules.unit R).map f).hom 1 = 1

def PresheafOfModules.sections {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) : Type (max u₁ v)

The type of sections of a presheaf of modules.

Equations

• M.sections = ↑(M.presheaf.comp (CategoryTheory.forget Ab)).sections

@[reducible, inline]

abbrev PresheafOfModules.sections.eval {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (s : M.sections) (X : Cᵒᵖ) : ↑(M.obj X)

Given a presheaf of modules M, s : M.sections and X : Cᵒᵖ, this is the induced element in M.obj X.

Equations

• s.eval X = ↑s X

@[simp]

theorem PresheafOfModules.sections_property {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (s : M.sections) {X Y : Cᵒᵖ} (f : X ⟶ Y) : (M.map f).hom (↑s X) = ↑s Y

def PresheafOfModules.sectionsMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (s : (X : Cᵒᵖ) → ↑(M.obj X)) (hs : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y), (M.map f).hom (s X) = s Y) : M.sections

Constructor for sections of a presheaf of modules.

Equations

• PresheafOfModules.sectionsMk s hs = ⟨s, ⋯⟩

@[simp]

theorem PresheafOfModules.sectionsMk_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (s : (X : Cᵒᵖ) → ↑(M.obj X)) (hs : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y), (M.map f).hom (s X) = s Y) (X : Cᵒᵖ) : ↑(PresheafOfModules.sectionsMk s hs) X = s X

theorem PresheafOfModules.sections_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (s t : M.sections) (h : ∀ (X : Cᵒᵖ), ↑s X = ↑t X) : s = t

def PresheafOfModules.sectionsMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M N : PresheafOfModules R} (f : M ⟶ N) (s : M.sections) : N.sections

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

Equations

• PresheafOfModules.sectionsMap f s = PresheafOfModules.sectionsMk (fun (X : Cᵒᵖ) => (f.app X).hom (↑s X)) ⋯

@[simp]

theorem PresheafOfModules.sectionsMap_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M N : PresheafOfModules R} (f : M ⟶ N) (s : M.sections) (X : Cᵒᵖ) : ↑(PresheafOfModules.sectionsMap f s) X = (f.app X).hom (↑s X)

@[simp]

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

@[simp]

theorem PresheafOfModules.sectionsMap_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (s : M.sections) : PresheafOfModules.sectionsMap (CategoryTheory.CategoryStruct.id M) s = s

def PresheafOfModules.unitHomEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) : (PresheafOfModules.unit R ⟶ M) ≃ M.sections

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

Equations

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

@[simp]

theorem PresheafOfModules.unitHomEquiv_apply_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) (f : PresheafOfModules.unit R ⟶ M) (X : Cᵒᵖ) : ↑(M.unitHomEquiv f) X = (f.app X).hom 1

PresheafOfModules R ⥤ Cᵒᵖ ⥤ ModuleCat (R.obj X) when X is initial

When X is initial, we have Module (R.obj X) (M.obj c) for any c : Cᵒᵖ.

@[reducible, inline]

noncomputable abbrev PresheafOfModules.forgetToPresheafModuleCatObjObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) (Y : Cᵒᵖ) : ModuleCat ↑(R.obj X)

Auxiliary definition for forgetToPresheafModuleCatObj.

Equations

• PresheafOfModules.forgetToPresheafModuleCatObjObj X hX M Y = (ModuleCat.restrictScalars (R.map (hX.to Y)).hom).obj (M.obj Y)

theorem PresheafOfModules.forgetToPresheafModuleCatObjObj_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) (Y : Cᵒᵖ) : ↑(PresheafOfModules.forgetToPresheafModuleCatObjObj X hX M Y) = ↑(M.obj Y)

def PresheafOfModules.forgetToPresheafModuleCatObjMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) {Y Z : Cᵒᵖ} (f : Y ⟶ Z) : PresheafOfModules.forgetToPresheafModuleCatObjObj X hX M Y ⟶ PresheafOfModules.forgetToPresheafModuleCatObjObj X hX M Z

Auxiliary definition for forgetToPresheafModuleCatObj.

Equations

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

@[simp]

theorem PresheafOfModules.forgetToPresheafModuleCatObjMap_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) {Y Z : Cᵒᵖ} (f : Y ⟶ Z) (m : ↑(M.obj Y)) : (PresheafOfModules.forgetToPresheafModuleCatObjMap X hX M f).hom m = (M.map f).hom m

noncomputable def PresheafOfModules.forgetToPresheafModuleCatObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) : CategoryTheory.Functor Cᵒᵖ (ModuleCat ↑(R.obj X))

Implementation of the functor PresheafOfModules R ⥤ Cᵒᵖ ⥤ ModuleCat (R.obj X) when X is initial.

The functor is implemented as, on object level M ↦ (c ↦ M(c)) where the R(X)-module structure on M(c) is given by restriction of scalars along the unique morphism R(c) ⟶ R(X); and on morphism level (f : M ⟶ N) ↦ (c ↦ f(c)).

Equations

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

@[simp]

theorem PresheafOfModules.forgetToPresheafModuleCatObj_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : (PresheafOfModules.forgetToPresheafModuleCatObj X hX M).map f = PresheafOfModules.forgetToPresheafModuleCatObjMap X hX M f

@[simp]

theorem PresheafOfModules.forgetToPresheafModuleCatObj_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) (Y : Cᵒᵖ) : (PresheafOfModules.forgetToPresheafModuleCatObj X hX M).obj Y = PresheafOfModules.forgetToPresheafModuleCatObjObj X hX M Y

noncomputable def PresheafOfModules.forgetToPresheafModuleCatMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) {M N : PresheafOfModules R} (f : M ⟶ N) : PresheafOfModules.forgetToPresheafModuleCatObj X hX M ⟶ PresheafOfModules.forgetToPresheafModuleCatObj X hX N

Implementation of the functor PresheafOfModules R ⥤ Cᵒᵖ ⥤ ModuleCat (R.obj X) when X is initial.

The functor is implemented as, on object level M ↦ (c ↦ M(c)) where the R(X)-module structure on M(c) is given by restriction of scalars along the unique morphism R(c) ⟶ R(X); and on morphism level (f : M ⟶ N) ↦ (c ↦ f(c)).

Equations

• PresheafOfModules.forgetToPresheafModuleCatMap X hX f = { app := fun (Y : Cᵒᵖ) => ModuleCat.ofHom { toFun := ⇑(f.app Y).hom, map_add' := ⋯, map_smul' := ⋯ }, naturality := ⋯ }

noncomputable def PresheafOfModules.forgetToPresheafModuleCat {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) : CategoryTheory.Functor (PresheafOfModules R) (CategoryTheory.Functor Cᵒᵖ (ModuleCat ↑(R.obj X)))

The forgetful functor from presheaves of modules over a presheaf of rings R to presheaves of R(X)-modules where X is an initial object.

The functor is implemented as, on object level M ↦ (c ↦ M(c)) where the R(X)-module structure on M(c) is given by restriction of scalars along the unique morphism R(c) ⟶ R(X); and on morphism level (f : M ⟶ N) ↦ (c ↦ f(c)).

Equations

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

@[simp]

theorem PresheafOfModules.forgetToPresheafModuleCat_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) {X✝ Y✝ : PresheafOfModules R} (f : X✝ ⟶ Y✝) : (PresheafOfModules.forgetToPresheafModuleCat X hX).map f = PresheafOfModules.forgetToPresheafModuleCatMap X hX f

@[simp]

theorem PresheafOfModules.forgetToPresheafModuleCat_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) : (PresheafOfModules.forgetToPresheafModuleCat X hX).obj M = PresheafOfModules.forgetToPresheafModuleCatObj X hX M