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.
- presheaf : CategoryTheory.Functor Cᵒᵖ AddCommGroupCat
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
The bundled module over an object X
.
Instances For
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
- hom : P.presheaf ⟶ Q.presheaf
A morphism of presheaves of modules.
Instances For
The identity morphism on a presheaf of modules.
Instances For
Composition of morphisms of presheaves of modules.
Instances For
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
The functor from presheaves of modules over a specified presheaf of rings, to presheaves of abelian groups.