# 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 :

## 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₁} [] (R : ) :
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 :
• 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
Instances For
theorem PresheafOfModules.map_smul {C : Type u₁} [] {R : } (self : ) {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₁} [] {R : } (P : ) (X : Cᵒᵖ) :
ModuleCat (R.obj X)

The bundled module over an object X.

Equations
Instances For
def PresheafOfModules.map {C : Type u₁} [] {R : } (P : ) {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' := }
Instances For
theorem PresheafOfModules.map_apply {C : Type u₁} [] {R : } (P : ) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) (x : (P.obj X)) :
(P.map f) x = (P.presheaf.map f) x
Equations
• =
instance PresheafOfModules.instRingHomCompTripleαRingObjOppositeRingCatMapComp {C : Type u₁} [] {R : } {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} (f : X Y) (g : Y Z) :
RingHomCompTriple (R.map f) (R.map g) (R.map )
Equations
• =
@[simp]
theorem PresheafOfModules.map_id {C : Type u₁} [] {R : } (P : ) (X : Cᵒᵖ) :
P.map = LinearMap.id'
@[simp]
theorem PresheafOfModules.map_comp {C : Type u₁} [] {R : } (P : ) {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} (f : X Y) (g : Y Z) :
P.map = (P.map g).comp (P.map f)
structure PresheafOfModules.Hom {C : Type u₁} [] {R : } (P : ) (Q : ) :
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
Instances For
theorem PresheafOfModules.Hom.map_smul {C : Type u₁} [] {R : } {P : } {Q : } (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₁} [] {R : } (P : ) :
P.Hom P

The identity morphism on a presheaf of modules.

Equations
Instances For
def PresheafOfModules.Hom.comp {C : Type u₁} [] {R : } {P : } {Q : } {R : } (f : P.Hom Q) (g : Q.Hom R) :
P.Hom R

Composition of morphisms of presheaves of modules.

Equations
Instances For
instance PresheafOfModules.instCategory {C : Type u₁} [] {R : } :
Equations
• PresheafOfModules.instCategory =
@[simp]
theorem PresheafOfModules.Hom.id_hom {C : Type u₁} [] {R : } (P : ) :
theorem PresheafOfModules.Hom.comp_hom_assoc {C : Type u₁} [] {R : } {P : } {Q : } {T : } (f : P Q) (g : Q T) (h : T.presheaf Z) :
@[simp]
theorem PresheafOfModules.Hom.comp_hom {C : Type u₁} [] {R : } {P : } {Q : } {T : } (f : P Q) (g : Q T) :
def PresheafOfModules.Hom.app {C : Type u₁} [] {R : } {P : } {Q : } (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' := }
Instances For
@[simp]
theorem PresheafOfModules.Hom.comp_app {C : Type u₁} [] {R : } {P : } {Q : } {T : } (f : P Q) (g : Q T) (X : Cᵒᵖ) :
theorem PresheafOfModules.Hom.ext {C : Type u₁} [] {R : } {P : } {Q : } {f : P Q} {g : P Q} (w : ∀ (X : Cᵒᵖ), ) :
f = g
instance PresheafOfModules.Hom.instZeroHom {C : Type u₁} [] {R : } {P : } {Q : } :
Zero (P Q)
Equations
• PresheafOfModules.Hom.instZeroHom = { zero := { hom := 0, map_smul := } }
@[simp]
theorem PresheafOfModules.Hom.zero_app {C : Type u₁} [] {R : } (P : ) (Q : ) (X : Cᵒᵖ) :
instance PresheafOfModules.Hom.instAddHom {C : Type u₁} [] {R : } {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₁} [] {R : } {P : } {Q : } (f : P Q) (g : P Q) (X : Cᵒᵖ) :
instance PresheafOfModules.Hom.instSubHom {C : Type u₁} [] {R : } {P : } {Q : } :
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₁} [] {R : } {P : } {Q : } (f : P Q) (g : P Q) (X : Cᵒᵖ) :
instance PresheafOfModules.Hom.instNegHom {C : Type u₁} [] {R : } {P : } {Q : } :
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₁} [] {R : } {P : } {Q : } (f : P Q) (X : Cᵒᵖ) :
instance PresheafOfModules.Hom.instAddCommGroupHom {C : Type u₁} [] {R : } {P : } {Q : } :
Equations
instance PresheafOfModules.Hom.instPreadditive {C : Type u₁} [] {R : } :
Equations
theorem PresheafOfModules.naturality_apply {C : Type u₁} [] {R : } {P : } {Q : } (f : P Q) {X : Cᵒᵖ} {Y : Cᵒᵖ} (g : X Y) (x : (P.obj X)) :
((P.map g) x) = (Q.map g) ( x)
@[simp]
theorem PresheafOfModules.toPresheaf_obj {C : Type u₁} [] (R : ) (P : ) :
.obj P = P.presheaf

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

Equations
• = { obj := fun (P : ) => P.presheaf, map := fun {X Y : } (f : X Y) => f.hom, map_id := , map_comp := }
Instances For
@[simp]
theorem PresheafOfModules.toPresheaf_map_app {C : Type u₁} [] {R : } {P : } {Q : } (f : P Q) (X : Cᵒᵖ) :
Equations
• =
Equations
• =
@[simp]
theorem PresheafOfModules.evaluation_map {C : Type u₁} [] (R : ) (X : Cᵒᵖ) :
∀ {X_1 Y : } (f : X_1 Y), .map f =
@[simp]
theorem PresheafOfModules.evaluation_obj {C : Type u₁} [] (R : ) (X : Cᵒᵖ) (M : ) :
.obj M = M.obj X
def PresheafOfModules.evaluation {C : Type u₁} [] (R : ) (X : Cᵒᵖ) :

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.
Instances For
Equations
• =
noncomputable def PresheafOfModules.restrictionApp {C : Type u₁} [] {R : } {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) (M : ) :
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
Instances For
theorem PresheafOfModules.restrictionApp_apply {C : Type u₁} [] {R : } {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) (M : ) (x : (M.obj X)) :
= (M.map f) x
@[simp]
theorem PresheafOfModules.restriction_app {C : Type u₁} [] (R : ) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) (M : ) :
.app M =
noncomputable def PresheafOfModules.restriction {C : Type u₁} [] (R : ) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
.comp (ModuleCat.restrictScalars (R.map f))

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

Equations
• = { app := , naturality := }
Instances For
@[simp]
theorem PresheafOfModules.restrictionApp_naturality_assoc {C : Type u₁} [] {R : } {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) {M : } {N : } (φ : M N) {Z : ModuleCat (R.obj X)} (h : (ModuleCat.restrictScalars (R.map f)).obj (N.obj Y) Z) :
@[simp]
theorem PresheafOfModules.restrictionApp_naturality {C : Type u₁} [] {R : } {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) {M : } {N : } (φ : M N) :
theorem PresheafOfModules.restrictionApp_id {C : Type u₁} [] {R : } (M : ) (X : Cᵒᵖ) :
= ().inv.app (M.obj X)
theorem PresheafOfModules.restrictionApp_comp {C : Type u₁} [] {R : } (M : ) {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} (f : X Y) (g : Y Z) :
def PresheafOfModules.Hom.mk' {C : Type u₁} [] {R : } {P : } {Q : } (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
Instances For
@[simp]
theorem PresheafOfModules.Hom.mk'_app {C : Type u₁} [] {R : } {P : } {Q : } (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)) :
@[reducible, inline]
abbrev PresheafOfModules.Hom.mk'' {C : Type u₁} [] {R : } {P : } {Q : } (app : (X : Cᵒᵖ) → (P.obj X) →ₗ[(R.obj X)] (Q.obj X)) (naturality : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X Y), CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars (R.map f)).map (app Y)) = ) :
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
Instances For
structure CorePresheafOfModules {C : Type u₁} [] (R : ) :
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ᵒᵖ

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 ) 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 ) x = (self.map g) ((self.map f) x)

map is compatible with the composition

Instances For
@[simp]
theorem CorePresheafOfModules.map_id {C : Type u₁} [] {R : } (self : ) (X : Cᵒᵖ) (x : self.obj X) :
(self.map ) x = x

map is compatible with the identities

@[simp]
theorem CorePresheafOfModules.map_comp {C : Type u₁} [] {R : } (self : ) {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} (f : X Y) (g : Y Z) (x : self.obj X) :
(self.map ) x = (self.map g) ((self.map f) x)

map is compatible with the composition

@[simp]
theorem CorePresheafOfModules.presheaf_obj {C : Type u₁} [] {R : } (M : ) (X : Cᵒᵖ) :
M.presheaf.obj X = AddCommGroupCat.of (M.obj X)
@[simp]
theorem CorePresheafOfModules.presheaf_map {C : Type u₁} [] {R : } (M : ) :
∀ {X Y : Cᵒᵖ} (f : X Y), M.presheaf.map f = AddCommGroupCat.ofHom (M.map f).toAddMonoidHom
def CorePresheafOfModules.presheaf {C : Type u₁} [] {R : } (M : ) :

The presheaf of abelian groups attached to a CorePresheafOfModules R.

Equations
Instances For
instance CorePresheafOfModules.instModuleαRingObjOppositeRingCatAddCommGroupAddCommGroupCatPresheaf {C : Type u₁} [] {R : } (M : ) (X : Cᵒᵖ) :
Module (R.obj X) (M.presheaf.obj X)
Equations
def CorePresheafOfModules.toPresheafOfModules {C : Type u₁} [] {R : } (M : ) :

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 := }
Instances For
@[simp]
theorem CorePresheafOfModules.toPresheafOfModules_obj {C : Type u₁} [] {R : } (M : ) (X : Cᵒᵖ) :
M.toPresheafOfModules.obj X = ModuleCat.of ((R.obj X)) (M.obj X)
@[simp]
theorem CorePresheafOfModules.toPresheafOfModules_presheaf_map_apply {C : Type u₁} [] {R : } (M : ) {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₁} [] (R : ) :
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''.)

Instances For
theorem BundledCorePresheafOfModules.map_id {C : Type u₁} [] {R : } (self : ) (X : Cᵒᵖ) :
self.map = ().inv.app (self.obj X)

map is compatible with the identities

theorem BundledCorePresheafOfModules.map_comp {C : Type u₁} [] {R : } (self : ) {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} (f : X Y) (g : Y Z) :
self.map = 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 ) ).inv.app (self.obj Z)))

map is compatible with the composition

noncomputable def BundledCorePresheafOfModules.toCorePresheafOfModules {C : Type u₁} [] {R : } (M : ) :

The obvious map BundledCorePresheafOfModules R → CorePresheafOfModules R.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def BundledCorePresheafOfModules.toPresheafOfModules {C : Type u₁} [] {R : } (M : ) :

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
Instances For
@[simp]
theorem BundledCorePresheafOfModules.toPresheafOfModules_obj {C : Type u₁} [] {R : } (M : ) (X : Cᵒᵖ) :
(M.toPresheafOfModules.obj X) = (M.obj X)
@[simp]
theorem BundledCorePresheafOfModules.toPresheafOfModules_presheaf_map_apply {C : Type u₁} [] {R : } (M : ) {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₁} [] {R : } (M : ) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
PresheafOfModules.restrictionApp f M.toPresheafOfModules = M.map f
def PresheafOfModules.unitCore {C : Type u₁} [] (R : ) :

Auxiliary definition for unit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev PresheafOfModules.unit {C : Type u₁} [] (R : ) :

The obvious free presheaf of modules of rank 1.

Equations
• = .toPresheafOfModules
Instances For
theorem PresheafOfModules.unit_map_one {C : Type u₁} [] (R : ) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
(.map f) 1 = 1
def PresheafOfModules.sections {C : Type u₁} [] {R : } (M : ) :
Type (max u₁ v)

The type of sections of a presheaf of modules.

Equations
• M.sections = (M.presheaf.comp ).sections
Instances For
@[simp]
theorem PresheafOfModules.sectionsMk_coe {C : Type u₁} [] {R : } {M : } (s : (X : Cᵒᵖ) → (M.obj X)) (hs : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X Y), (M.map f) (s X) = s Y) (X : Cᵒᵖ) :
() X = s X
def PresheafOfModules.sectionsMk {C : Type u₁} [] {R : } {M : } (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
• = s,
Instances For
theorem PresheafOfModules.sections_ext {C : Type u₁} [] {R : } {M : } (s : M.sections) (t : M.sections) (h : ∀ (X : Cᵒᵖ), s X = t X) :
s = t
@[simp]
theorem PresheafOfModules.unitHomEquiv_apply_coe {C : Type u₁} [] {R : } (M : ) (f : ) (X : Cᵒᵖ) :
(M.unitHomEquiv f) X = 1
def PresheafOfModules.unitHomEquiv {C : Type u₁} [] {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.
Instances For