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 R, as a presheaf of abelian groups with additional data.

We also provide two alternative constructors :

• When M : CorePresheafOfModules R consists of a family of unbundled modules over R.obj X for all X, the corresponding presheaf of modules is M.toPresheafOfModules.
• When M : BundledCorePresheafOfModules R consists of a family of objects in ModuleCat (R.obj X) for all X, the corresponding presheaf of modules is M.toPresheafOfModules.

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ᵒᵖ AddCommGrp
• 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

theorem PresheafOfModules.map_smul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (self : PresheafOfModules R) {X : Cᵒᵖ} {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

• P.obj 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) : ↑(P.obj X) →ₛₗ[R.map f] ↑(P.obj 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

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

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 : ↑(P.obj X)) : (P.map f) x = (P.presheaf.map f) x

instance PresheafOfModules.instRingHomIdαRingObjOppositeRingCatMapId {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αRingObjOppositeRingCatMapComp {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ᵒᵖ) : P.map (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) : P.map (CategoryTheory.CategoryStruct.comp f g) = (P.map g).comp (P.map 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

theorem PresheafOfModules.Hom.map_smul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P : PresheafOfModules R} {Q : PresheafOfModules R} (self : P.Hom Q) (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) : P.Hom 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 : P.Hom Q) (g : Q.Hom R) : P.Hom R

Composition of morphisms of presheaves of modules.

Equations

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

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

Equations

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

@[simp]

theorem PresheafOfModules.Hom.id_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (P : PresheafOfModules R) : (CategoryTheory.CategoryStruct.id P).hom = CategoryTheory.CategoryStruct.id P.presheaf

theorem PresheafOfModules.Hom.comp_hom_assoc {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) {Z : CategoryTheory.Functor Cᵒᵖ AddCommGrp} (h : T.presheaf ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h = CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)

@[simp]

theorem PresheafOfModules.Hom.comp_hom {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) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

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

• f.app 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.instZeroHom {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.instZeroHom = { 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.instAddHom {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.instAddHom = { 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.instSubHom {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.instSubHom = { 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.instNegHom {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.instNegHom = { 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.instAddCommGroupHom {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.instAddCommGroupHom = AddCommGroup.mk ⋯

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

Equations

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

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

@[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ᵒᵖ AddCommGrp)

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

Equations

• PresheafOfModules.toPresheaf R = { obj := fun (P : PresheafOfModules R) => P.presheaf, map := fun {X Y : PresheafOfModules R} (f : X ⟶ Y) => f.hom, map_id := ⋯, map_comp := ⋯ }

@[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 = (PresheafOfModules.Hom.app f X).toAddMonoidHom

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

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

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

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

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

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

Equations

• ⋯ = ⋯

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

Given a presheaf of modules M on a category C and f : X ⟶ Y in Cᵒᵖ, this is the restriction map M.obj X ⟶ M.obj Y, considered as a linear map to the restriction of scalars of M.obj Y.

Equations

• PresheafOfModules.restrictionApp f M = (ModuleCat.semilinearMapAddEquiv (R.map f) (M.obj X) (M.obj Y)) (M.map f)

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

@[simp]

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

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

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

Equations

• PresheafOfModules.restriction R f = { app := PresheafOfModules.restrictionApp f, naturality := ⋯ }

@[simp]

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

@[simp]

theorem PresheafOfModules.restrictionApp_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ⟶ Y) {M : PresheafOfModules R} {N : PresheafOfModules R} (φ : M ⟶ N) : CategoryTheory.CategoryStruct.comp (PresheafOfModules.restrictionApp f M) ((ModuleCat.restrictScalars (R.map f)).map (PresheafOfModules.Hom.app φ Y)) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (PresheafOfModules.Hom.app φ X)) (PresheafOfModules.restrictionApp f N)

theorem PresheafOfModules.restrictionApp_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) (X : Cᵒᵖ) : PresheafOfModules.restrictionApp (CategoryTheory.CategoryStruct.id X) M = (ModuleCat.restrictScalarsId' (R.map (CategoryTheory.CategoryStruct.id X)) ⋯).inv.app (M.obj X)

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

def PresheafOfModules.Hom.mk' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P : PresheafOfModules R} {Q : PresheafOfModules R} (app : (X : Cᵒᵖ) → ↑(P.obj X) →ₗ[↑(R.obj X)] ↑(Q.obj X)) (naturality : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) (x : ↑(P.obj X)), (app Y) ((P.map f) x) = (Q.map f) ((app X) x)) : P ⟶ Q

A constructor for morphisms in PresheafOfModules R that is based on the data of a family of linear maps over the various rings R.obj X.

Equations

• PresheafOfModules.Hom.mk' app naturality = { hom := { app := fun (X : Cᵒᵖ) => (app X).toAddMonoidHom, naturality := ⋯ }, map_smul := ⋯ }

@[simp]

theorem PresheafOfModules.Hom.mk'_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P : PresheafOfModules R} {Q : PresheafOfModules R} (app : (X : Cᵒᵖ) → ↑(P.obj X) →ₗ[↑(R.obj X)] ↑(Q.obj X)) (naturality : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) (x : ↑(P.obj X)), (app Y) ((P.map f) x) = (Q.map f) ((app X) x)) : PresheafOfModules.Hom.app (PresheafOfModules.Hom.mk' app naturality) = app

@[reducible, inline]

abbrev PresheafOfModules.Hom.mk'' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P : PresheafOfModules R} {Q : PresheafOfModules R} (app : (X : Cᵒᵖ) → ↑(P.obj X) →ₗ[↑(R.obj X)] ↑(Q.obj X)) (naturality : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (PresheafOfModules.restrictionApp f P) ((ModuleCat.restrictScalars (R.map f)).map (app Y)) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (app X)) (PresheafOfModules.restrictionApp f Q)) : P ⟶ Q

A constructor for morphisms in PresheafOfModules R that is based on the data of a family of linear maps over the various rings R.obj X, and for which the naturality condition is stated using the restriction of scalars.

Equations

• PresheafOfModules.Hom.mk'' app naturality = PresheafOfModules.Hom.mk' app ⋯

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

This structure contains the data and axioms in order to produce a PresheafOfModules R from a collection of types equipped with module structures over the various rings R.obj X. (See the constructor PresheafOfModules.mk'.)

• obj : Cᵒᵖ → Type v

  the datum of a type for each object in Cᵒᵖ

• addCommGroup : (X : Cᵒᵖ) → AddCommGroup (self.obj X)

  the abelian group structure on the types obj X

• module : (X : Cᵒᵖ) → Module (↑(R.obj X)) (self.obj X)

  the module structure on the types obj X over the various rings R.obj X

• map : {X Y : Cᵒᵖ} → (f : X ⟶ Y) → self.obj X →ₛₗ[R.map f] self.obj Y

  the semi-linear restriction maps

• map_id : ∀ (X : Cᵒᵖ) (x : self.obj X), (self.map (CategoryTheory.CategoryStruct.id X)) x = x

  map is compatible with the identities

• map_comp : ∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) (x : self.obj X), (self.map (CategoryTheory.CategoryStruct.comp f g)) x = (self.map g) ((self.map f) x)

  map is compatible with the composition

@[simp]

theorem CorePresheafOfModules.map_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (self : CorePresheafOfModules R) (X : Cᵒᵖ) (x : self.obj X) : (self.map (CategoryTheory.CategoryStruct.id X)) x = x

map is compatible with the identities

@[simp]

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

map is compatible with the composition

@[simp]

theorem CorePresheafOfModules.presheaf_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : CorePresheafOfModules R) : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), M.presheaf.map f = AddCommGrp.ofHom (M.map f).toAddMonoidHom

@[simp]

theorem CorePresheafOfModules.presheaf_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : CorePresheafOfModules R) (X : Cᵒᵖ) : M.presheaf.obj X = AddCommGrp.of (M.obj X)

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

The presheaf of abelian groups attached to a CorePresheafOfModules R.

Equations

• M.presheaf = { obj := fun (X : Cᵒᵖ) => AddCommGrp.of (M.obj X), map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) => AddCommGrp.ofHom (M.map f).toAddMonoidHom, map_id := ⋯, map_comp := ⋯ }

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

Equations

• M.instModuleαRingObjOppositeRingCatAddCommGroupAddCommGrpPresheaf X = M.module X

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

Constructor for PresheafOfModules R based on a collection of types equipped with module structures over the various rings R.obj X, see the structure CorePresheafOfModules.

Equations

• M.toPresheafOfModules = { presheaf := M.presheaf, module := inferInstance, map_smul := ⋯ }

@[simp]

theorem CorePresheafOfModules.toPresheafOfModules_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : CorePresheafOfModules R) (X : Cᵒᵖ) : M.toPresheafOfModules.obj X = ModuleCat.of (↑(R.obj X)) (M.obj X)

@[simp]

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

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

This structure contains the data and axioms in order to produce a PresheafOfModules R from a collection of objects of type ModuleCat (R.obj X) for all X, and restriction maps expressed as linear maps to restriction of scalars. (See the constructor PresheafOfModules.mk''.)

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

  the datum of a ModuleCat (R.obj X) for each object in Cᵒᵖ

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

  the restriction maps as linear maps to restriction of scalars

• map_id : ∀ (X : Cᵒᵖ), self.map (CategoryTheory.CategoryStruct.id X) = (ModuleCat.restrictScalarsId' (R.map (CategoryTheory.CategoryStruct.id X)) ⋯).inv.app (self.obj X)

  map is compatible with the identities

• 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)).map (self.map g)) ((ModuleCat.restrictScalarsComp' (R.map f) (R.map g) (R.map (CategoryTheory.CategoryStruct.comp f g)) ⋯).inv.app (self.obj Z)))

  map is compatible with the composition

theorem BundledCorePresheafOfModules.map_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (self : BundledCorePresheafOfModules R) (X : Cᵒᵖ) : self.map (CategoryTheory.CategoryStruct.id X) = (ModuleCat.restrictScalarsId' (R.map (CategoryTheory.CategoryStruct.id X)) ⋯).inv.app (self.obj X)

map is compatible with the identities

theorem BundledCorePresheafOfModules.map_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (self : BundledCorePresheafOfModules R) {X : Cᵒᵖ} {Y : Cᵒᵖ} {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)).map (self.map g)) ((ModuleCat.restrictScalarsComp' (R.map f) (R.map g) (R.map (CategoryTheory.CategoryStruct.comp f g)) ⋯).inv.app (self.obj Z)))

map is compatible with the composition

noncomputable def BundledCorePresheafOfModules.toCorePresheafOfModules {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : BundledCorePresheafOfModules R) : CorePresheafOfModules R

The obvious map BundledCorePresheafOfModules R → CorePresheafOfModules R.

Equations

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

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

Constructor for PresheafOfModules R based on a collection of objects of type ModuleCat (R.obj X) for all X, and restriction maps expressed as linear maps to restriction of scalars, see the structure BundledCorePresheafOfModules.

Equations

• M.toPresheafOfModules = M.toCorePresheafOfModules.toPresheafOfModules

@[simp]

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

@[simp]

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

@[simp]

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

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

Auxiliary definition for unit.

Equations

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

@[reducible, inline]

abbrev 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

• PresheafOfModules.unit R = (PresheafOfModules.unitCore R).toPresheafOfModules

theorem PresheafOfModules.unit_map_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ⟶ Y) : ((PresheafOfModules.unit R).map f) 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 AddCommGrp)).sections

@[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 : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ⟶ Y) : (M.map f) (↑s X) = ↑s Y

@[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) (s X) = s Y) (X : Cᵒᵖ) : ↑(PresheafOfModules.sectionsMk s hs) X = s X

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) (s X) = s Y) : M.sections

Constructor for sections of a presheaf of modules.

Equations

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

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

@[simp]

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

def PresheafOfModules.sectionsMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} {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ᵒᵖ) => (PresheafOfModules.Hom.app f X) (↑s X)) ⋯

@[simp]

theorem PresheafOfModules.sectionsMap_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} {N : PresheafOfModules R} {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

@[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 = (PresheafOfModules.Hom.app f X) 1

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.