# Documentation

Mathlib.Algebra.Category.ModuleCat.Presheaf

# 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₁} [] (R : ) :
Type (max (max (max u u₁) (v + 1)) v₁)
• presheaf :
• 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.

Instances For
def PresheafOfModules.obj {C : Type u₁} [] {R : } (P : ) (X : Cᵒᵖ) :
ModuleCat ↑(R.obj X)

The bundled module over an object X.

Instances For
def PresheafOfModules.map {C : Type u₁} [] {R : } (P : ) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
↑() →ₛₗ[R.map f] ↑()

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.

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

Instances For
def PresheafOfModules.Hom.id {C : Type u₁} [] {R : } (P : ) :

The identity morphism on a presheaf of modules.

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

Composition of morphisms of presheaves of modules.

Instances For
def PresheafOfModules.Hom.app {C : Type u₁} [] {R : } {P : } {Q : } (f : ) (X : Cᵒᵖ) :
↑() →ₗ[↑(R.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.

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
@[simp]
theorem PresheafOfModules.Hom.zero_app {C : Type u₁} [] {R : } (P : ) (Q : ) (X : Cᵒᵖ) :
@[simp]
theorem PresheafOfModules.Hom.add_app {C : Type u₁} [] {R : } {P : } {Q : } (f : P Q) (g : P Q) (X : Cᵒᵖ) :
@[simp]
theorem PresheafOfModules.Hom.sub_app {C : Type u₁} [] {R : } {P : } {Q : } (f : P Q) (g : P Q) (X : Cᵒᵖ) :
@[simp]
theorem PresheafOfModules.Hom.neg_app {C : Type u₁} [] {R : } {P : } {Q : } (f : P Q) (X : Cᵒᵖ) :
@[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.

Instances For
@[simp]
theorem PresheafOfModules.toPresheaf_map_app {C : Type u₁} [] {R : } {P : } {Q : } (f : P Q) (X : Cᵒᵖ) :
(().map f).app X =