Pushforward of presheaves of modules #
If F : C ⥤ D
, the precomposition F.op ⋙ _
induces a functor from presheaves
over D
to presheaves over C
. When R : Dᵒᵖ ⥤ RingCat
, we define the
induced functor pushforward₀ : PresheafOfModules.{v} R ⥤ PresheafOfModules.{v} (F.op ⋙ R)
on presheaves of modules.
In case we have a morphism of presheaves of rings S ⟶ F.op ⋙ R
, we also construct
a functor pushforward : PresheafOfModules.{v} R ⥤ PresheafOfModules.{v} S
.
The pushforward functor on presheaves of modules for a functor F : C ⥤ D
and
R : Dᵒᵖ ⥤ RingCat
. On the underlying presheaves of abelian groups, it is induced
by the precomposition with F.op
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pushforward of presheaves of modules commutes with the forgetful functor to presheaves of abelian groups.
Equations
- PresheafOfModules.pushforward₀CompToPresheaf F R = CategoryTheory.Iso.refl ((PresheafOfModules.pushforward₀ F R).comp (PresheafOfModules.toPresheaf (F.op.comp R)))
Instances For
The pushforward functor PresheafOfModules R ⥤ PresheafOfModules S
induced by
a morphism of presheaves of rings S ⟶ F.op ⋙ R
.
Equations
Instances For
The pushforward of presheaves of modules commutes with the forgetful functor to presheaves of abelian groups.
Equations
Instances For
@[simp]
-normal form of pushforward_obj_map_apply
.
@[simp]
-normal form of pushforward_map_app_apply
.