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₁)

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.

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

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.

Equations

• PresheafOfModules.obj P X = ModuleCat.of ↑(R.obj X) ↑(P.presheaf.obj 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.

Equations

• PresheafOfModules.map P f = { toAddHom := ↑(P.presheaf.map f), map_smul' := ⋯ }

@[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αRingObjOppositeToQuiverToCategoryStructOppositeRingCatToQuiverToCategoryStructCategoryMapHomTypeSemiringAssocRingHomToSemiringBundledHomOfParentProjectionBundledHomInstParentProjectionTypeSemiringRingToSemiringToPrefunctorStrMapId {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) : RingHomId (R.map (CategoryTheory.CategoryStruct.id X))

Equations

• ⋯ = ⋯

instance PresheafOfModules.instRingHomCompTripleαRingObjOppositeToQuiverToCategoryStructOppositeRingCatToQuiverToCategoryStructCategoryMapHomTypeSemiringAssocRingHomToSemiringBundledHomOfParentProjectionBundledHomInstParentProjectionTypeSemiringRingToSemiringToPrefunctorStrMapComp {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))

Equations

• ⋯ = ⋯

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

A morphism of presheaves of modules.

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

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.

Equations

• PresheafOfModules.Hom.id P = { hom := CategoryTheory.CategoryStruct.id P.presheaf, map_smul := ⋯ }

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.

Equations

• PresheafOfModules.Hom.comp f g = { hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, map_smul := ⋯ }

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)

Equations

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

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.

Equations

• PresheafOfModules.Hom.app f X = { toAddHom := ↑(f.hom.app X), map_smul' := ⋯ }

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

Equations

• PresheafOfModules.Hom.instZeroHomPresheafOfModulesToQuiverToCategoryStructInstCategoryPresheafOfModules = { zero := { hom := 0, map_smul := ⋯ } }

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

Equations

• PresheafOfModules.Hom.instAddHomPresheafOfModulesToQuiverToCategoryStructInstCategoryPresheafOfModules = { add := fun (f g : P ⟶ Q) => { hom := f.hom + g.hom, map_smul := ⋯ } }

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

Equations

• PresheafOfModules.Hom.instSubHomPresheafOfModulesToQuiverToCategoryStructInstCategoryPresheafOfModules = { sub := fun (f g : P ⟶ Q) => { hom := f.hom - g.hom, map_smul := ⋯ } }

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

Equations

• PresheafOfModules.Hom.instNegHomPresheafOfModulesToQuiverToCategoryStructInstCategoryPresheafOfModules = { neg := fun (f : P ⟶ Q) => { hom := -f.hom, map_smul := ⋯ } }

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

Equations

• PresheafOfModules.Hom.instAddCommGroupHomPresheafOfModulesToQuiverToCategoryStructInstCategoryPresheafOfModules = AddCommGroup.mk ⋯

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

Equations

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

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯