Presheaves of modules over a presheaf of rings.

We give a hands-on description of a presheaf of modules over a fixed presheaf of rings, as a presheaf of abelian groups with additional data.

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.
• (Pre)sheaves of modules over a given sheaf of rings are an abelian category.
• 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₁)

• presheaf : CategoryTheory.Functor Cᵒᵖ AddCommGroupCat
• module : (X : Cᵒᵖ) → Module ↑(R.obj X) ↑(s.presheaf.obj X)
• map_smul : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (r : ↑(R.obj X)) (x : ↑(s.presheaf.obj X)), ↑(s.presheaf.map f) (r • x) = ↑(R.map f) r • ↑(s.presheaf.map f) x

A presheaf of modules over a given presheaf of rings, described as a presheaf of abelian groups, and the extra data of the action at each object, and a condition relating functoriality and scalar multiplication.

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

The bundled module over an object X.

def PresheafOfModules.map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (P : PresheafOfModules R) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ⟶ Y) : ↑(PresheafOfModules.obj P X) →ₛₗ[R.map f] ↑(PresheafOfModules.obj P Y)

If P is a presheaf of modules over a presheaf of rings R, both over some category C, and f : X ⟶ Y is a morphism in Cᵒᵖ, we construct the R.map f-semilinear map from the R.obj X-module P.presheaf.obj X to the R.obj Y-module P.presheaf.obj Y.

@[simp]

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

instance PresheafOfModules.instRingHomIdαRingObjOppositeToQuiverToCategoryStructOppositeRingCatToQuiverToCategoryStructInstRingCatLargeCategoryToPrefunctorToSemiringStrMapId {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) : RingHomId (R.map (CategoryTheory.CategoryStruct.id X))

instance PresheafOfModules.instRingHomCompTripleαRingObjOppositeToQuiverToCategoryStructOppositeRingCatToQuiverToCategoryStructInstRingCatLargeCategoryToPrefunctorToSemiringStrMapComp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) : RingHomCompTriple (R.map f) (R.map g) (R.map (CategoryTheory.CategoryStruct.comp f g))

@[simp]

theorem PresheafOfModules.map_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (P : PresheafOfModules R) (X : Cᵒᵖ) : PresheafOfModules.map P (CategoryTheory.CategoryStruct.id X) = LinearMap.id'

@[simp]

theorem PresheafOfModules.map_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (P : PresheafOfModules R) {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) : PresheafOfModules.map P (CategoryTheory.CategoryStruct.comp f g) = LinearMap.comp (PresheafOfModules.map P g) (PresheafOfModules.map P f)

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

• hom : P.presheaf ⟶ Q.presheaf
• map_smul : ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(P.presheaf.obj X)), ↑(s.hom.app X) (r • x) = r • ↑(s.hom.app X) x

A morphism of presheaves of modules.

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

The identity morphism on a presheaf of modules.

def PresheafOfModules.Hom.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P : PresheafOfModules R} {Q : PresheafOfModules R} {R : PresheafOfModules R} (f : PresheafOfModules.Hom P Q) (g : PresheafOfModules.Hom Q R) : PresheafOfModules.Hom P R

Composition of morphisms of presheaves of modules.

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

def PresheafOfModules.Hom.app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P : PresheafOfModules R} {Q : PresheafOfModules R} (f : PresheafOfModules.Hom P Q) (X : Cᵒᵖ) : ↑(PresheafOfModules.obj P X) →ₗ[↑(R.obj X)] ↑(PresheafOfModules.obj Q X)

The (X : Cᵒᵖ)-component of morphism between presheaves of modules over a presheaf of rings R, as an R.obj X-linear map.

@[simp]

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

theorem PresheafOfModules.Hom.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P : PresheafOfModules R} {Q : PresheafOfModules R} {f : P ⟶ Q} {g : P ⟶ Q} (w : ∀ (X : Cᵒᵖ), PresheafOfModules.Hom.app f X = PresheafOfModules.Hom.app g X) : f = g

instance PresheafOfModules.Hom.instZeroHomPresheafOfModulesToQuiverToCategoryStructInstCategoryPresheafOfModules {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P : PresheafOfModules R} {Q : PresheafOfModules R} : Zero (P ⟶ Q)

@[simp]

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

instance PresheafOfModules.Hom.instAddHomPresheafOfModulesToQuiverToCategoryStructInstCategoryPresheafOfModules {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P : PresheafOfModules R} {Q : PresheafOfModules R} : Add (P ⟶ Q)

@[simp]

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

instance PresheafOfModules.Hom.instSubHomPresheafOfModulesToQuiverToCategoryStructInstCategoryPresheafOfModules {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P : PresheafOfModules R} {Q : PresheafOfModules R} : Sub (P ⟶ Q)

@[simp]

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

instance PresheafOfModules.Hom.instNegHomPresheafOfModulesToQuiverToCategoryStructInstCategoryPresheafOfModules {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P : PresheafOfModules R} {Q : PresheafOfModules R} : Neg (P ⟶ Q)

@[simp]

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

instance PresheafOfModules.Hom.instAddCommGroupHomPresheafOfModulesToQuiverToCategoryStructInstCategoryPresheafOfModules {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P : PresheafOfModules R} {Q : PresheafOfModules R} : AddCommGroup (P ⟶ Q)

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

@[simp]

theorem PresheafOfModules.toPresheaf_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (P : PresheafOfModules R) : (PresheafOfModules.toPresheaf R).obj P = P.presheaf

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

The functor from presheaves of modules over a specified presheaf of rings, to presheaves of abelian groups.

@[simp]

theorem PresheafOfModules.toPresheaf_map_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P : PresheafOfModules R} {Q : PresheafOfModules R} (f : P ⟶ Q) (X : Cᵒᵖ) : ((PresheafOfModules.toPresheaf R).map f).app X = LinearMap.toAddMonoidHom (PresheafOfModules.Hom.app f X)

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

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