Presheaves of modules over a presheaf of rings. #
Given a presheaf of rings R : Cᵒᵖ ⥤ RingCat
, we define the category PresheafOfModules R
.
An object M : PresheafOfModules R
consists of a family of modules
M.obj X : ModuleCat (R.obj X)
for all X : Cᵒᵖ
, together with the data, for all f : X ⟶ Y
,
of a functorial linear map M.map f
from M.obj X
to the restriction
of scalars of M.obj Y
via R.map f
.
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.
- Presheaves of modules over a presheaf of commutative rings form a monoidal category.
- Pushforward and pullback.
A presheaf of modules over R : Cᵒᵖ ⥤ RingCat
consists of family of
objects obj X : ModuleCat (R.obj X)
for all X : Cᵒᵖ
together with
functorial maps obj X ⟶ (ModuleCat.restrictScalars (R.map f)).obj (obj Y)
for all f : X ⟶ Y
in Cᵒᵖ
.
a family of modules over
R.obj X
for allX
- map : {X Y : Cᵒᵖ} → (f : X ⟶ Y) → self.obj X ⟶ (ModuleCat.restrictScalars (R.map f)).obj (self.obj Y)
the restriction maps of a presheaf of modules
- map_id : ∀ (X : Cᵒᵖ), self.map (CategoryTheory.CategoryStruct.id X) = (ModuleCat.restrictScalarsId' (R.map (CategoryTheory.CategoryStruct.id X)) ⋯).inv.app (self.obj X)
- 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)))
Instances For
A morphism of presheaves of modules consists of a family of linear maps which satisfy the naturality condition.
- naturality : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (M₁.map f) ((ModuleCat.restrictScalars (R.map f)).map (self.app Y)) = CategoryTheory.CategoryStruct.comp (self.app X) (M₂.map f)
Instances For
Equations
- PresheafOfModules.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯
The underlying presheaf of abelian groups of a presheaf of modules.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- M.instModuleαRingObjOppositeRingCatAddCommGroupAbPresheaf X = inferInstanceAs (Module ↑(R.obj X) ↑(M.obj X))
The forgetful functor PresheafOfModules R ⥤ Cᵒᵖ ⥤ Ab
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
The object in PresheafOfModules R
that is obtained from M : Cᵒᵖ ⥤ Ab.{v}
such
that for all X : Cᵒᵖ
, M.obj X
is a R.obj X
module, in such a way that the
restriction maps are semilinear. (This constructor should be used only in cases
when the preferred constructor PresheafOfModules.mk
is not as convenient as this one.)
Equations
- One or more equations did not get rendered due to their size.
Instances For
The morphism of presheaves of modules M₁ ⟶ M₂
given by a morphism
of abelian presheaves M₁.presheaf ⟶ M₂.presheaf
which satisfy a suitable linearity condition.
Equations
- PresheafOfModules.homMk φ hφ = { app := fun (X : Cᵒᵖ) => { toFun := ⇑(φ.app X), map_add' := ⋯, map_smul' := ⋯ }, naturality := ⋯ }
Instances For
Equations
- PresheafOfModules.instAddCommGroupHom = AddCommGroup.mk ⋯
Equations
- PresheafOfModules.instPreadditive = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }
Equations
- ⋯ = ⋯
Evaluation on an object X
gives a functor
PresheafOfModules R ⥤ ModuleCat (R.obj X)
.
Equations
- PresheafOfModules.evaluation R X = { obj := fun (M : PresheafOfModules R) => M.obj X, map := fun {X_1 Y : PresheafOfModules R} (f : X_1 ⟶ Y) => f.app X, map_id := ⋯, map_comp := ⋯ }
Instances For
Equations
- ⋯ = ⋯
The restriction natural transformation on presheaves of modules, considered as linear maps to restriction of scalars.
Equations
- PresheafOfModules.restriction R f = { app := fun (M : PresheafOfModules R) => M.map f, naturality := ⋯ }
Instances For
The obvious free presheaf of modules of rank 1
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The type of sections of a presheaf of modules.
Equations
- M.sections = ↑(M.presheaf.comp (CategoryTheory.forget Ab)).sections
Instances For
Given a presheaf of modules M
, s : M.sections
and X : Cᵒᵖ
, this is the induced
element in M.obj X
.
Equations
- s.eval X = ↑s X
Instances For
Constructor for sections of a presheaf of modules.
Equations
- PresheafOfModules.sectionsMk s hs = ⟨s, ⋯⟩
Instances For
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ᵒᵖ) => (f.app X) (↑s X)) ⋯
Instances For
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
PresheafOfModules R ⥤ Cᵒᵖ ⥤ ModuleCat (R.obj X)
when X
is initial #
When X
is initial, we have Module (R.obj X) (M.obj c)
for any c : Cᵒᵖ
.
Auxiliary definition for forgetToPresheafModuleCatObj
.
Equations
- PresheafOfModules.forgetToPresheafModuleCatObjObj X hX M Y = (ModuleCat.restrictScalars (R.map (hX.to Y))).obj (M.obj Y)
Instances For
Auxiliary definition for forgetToPresheafModuleCatObj
.
Equations
- PresheafOfModules.forgetToPresheafModuleCatObjMap X hX M f = { toFun := fun (x : ↑(PresheafOfModules.forgetToPresheafModuleCatObjObj X hX M Y)) => (M.map f) x, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Implementation of the functor PresheafOfModules R ⥤ Cᵒᵖ ⥤ ModuleCat (R.obj X)
when X
is initial.
The functor is implemented as, on object level M ↦ (c ↦ M(c))
where the R(X)
-module structure
on M(c)
is given by restriction of scalars along the unique morphism R(c) ⟶ R(X)
; and on
morphism level (f : M ⟶ N) ↦ (c ↦ f(c))
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Implementation of the functor PresheafOfModules R ⥤ Cᵒᵖ ⥤ ModuleCat (R.obj X)
when X
is initial.
The functor is implemented as, on object level M ↦ (c ↦ M(c))
where the R(X)
-module structure
on M(c)
is given by restriction of scalars along the unique morphism R(c) ⟶ R(X)
; and on
morphism level (f : M ⟶ N) ↦ (c ↦ f(c))
.
Equations
- PresheafOfModules.forgetToPresheafModuleCatMap X hX f = { app := fun (Y : Cᵒᵖ) => { toFun := ⇑(f.app Y), map_add' := ⋯, map_smul' := ⋯ }, naturality := ⋯ }
Instances For
The forgetful functor from presheaves of modules over a presheaf of rings R
to presheaves of
R(X)
-modules where X
is an initial object.
The functor is implemented as, on object level M ↦ (c ↦ M(c))
where the R(X)
-module structure
on M(c)
is given by restriction of scalars along the unique morphism R(c) ⟶ R(X)
; and on
morphism level (f : M ⟶ N) ↦ (c ↦ f(c))
.
Equations
- One or more equations did not get rendered due to their size.