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ᵒᵖ 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 u₁) v₁) (u_1 + 1)} (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 := ⋯ }

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 : ↑(PresheafOfModules.obj P X)) : (PresheafOfModules.Hom.app f Y) ((P.presheaf.map g) x) = (Q.presheaf.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ᵒᵖ 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.Functor.Faithful (PresheafOfModules.toPresheaf R)

Equations

• ⋯ = ⋯

@[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 = PresheafOfModules.obj M X

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

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.

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) : PresheafOfModules.obj M X ⟶ (ModuleCat.restrictScalars (R.map f)).obj (PresheafOfModules.obj M 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) (PresheafOfModules.obj M X) (PresheafOfModules.obj M Y)) (PresheafOfModules.map M 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 : ↑(PresheafOfModules.obj M X)) : (PresheafOfModules.restrictionApp f M) x = (PresheafOfModules.map M 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 ⟶ CategoryTheory.Functor.comp (PresheafOfModules.evaluation R Y) (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 (PresheafOfModules.obj N 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 (PresheafOfModules.obj M 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 (PresheafOfModules.obj M 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ᵒᵖ) → ↑(PresheafOfModules.obj P X) →ₗ[↑(R.obj X)] ↑(PresheafOfModules.obj Q X)) (naturality : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) (x : ↑(PresheafOfModules.obj P X)), (app Y) ((PresheafOfModules.map P f) x) = (PresheafOfModules.map Q 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ᵒᵖ) => LinearMap.toAddMonoidHom (app X), 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ᵒᵖ) → ↑(PresheafOfModules.obj P X) →ₗ[↑(R.obj X)] ↑(PresheafOfModules.obj Q X)) (naturality : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) (x : ↑(PresheafOfModules.obj P X)), (app Y) ((PresheafOfModules.map P f) x) = (PresheafOfModules.map Q f) ((app X) x)) : PresheafOfModules.Hom.app (PresheafOfModules.Hom.mk' app naturality) = app

@[inline, reducible]

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ᵒᵖ) → ↑(PresheafOfModules.obj P X) →ₗ[↑(R.obj X)] ↑(PresheafOfModules.obj Q 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.presheaf_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : CorePresheafOfModules R) (X : Cᵒᵖ) : (CorePresheafOfModules.presheaf M).obj X = AddCommGroupCat.of (M.obj X)

@[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), (CorePresheafOfModules.presheaf M).map f = AddCommGroupCat.ofHom (LinearMap.toAddMonoidHom (M.map f))

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

The presheaf of abelian groups attached to a CorePresheafOfModules R.

Equations

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

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

Equations

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

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

• CorePresheafOfModules.toPresheafOfModules M = { presheaf := CorePresheafOfModules.presheaf M, 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ᵒᵖ) : PresheafOfModules.obj (CorePresheafOfModules.toPresheafOfModules M) 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) : ((CorePresheafOfModules.toPresheafOfModules M).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

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

• BundledCorePresheafOfModules.toPresheafOfModules M = CorePresheafOfModules.toPresheafOfModules (BundledCorePresheafOfModules.toCorePresheafOfModules M)

@[simp]

theorem BundledCorePresheafOfModules.toPresheafOfModules_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : BundledCorePresheafOfModules R) (X : Cᵒᵖ) : ↑(PresheafOfModules.obj (BundledCorePresheafOfModules.toPresheafOfModules M) 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)) : ((BundledCorePresheafOfModules.toPresheafOfModules M).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 (BundledCorePresheafOfModules.toPresheafOfModules M) = M.map f