Documentation

Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward

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
    theorem PresheafOfModules.pushforward_obj_map_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat} (φ : S F.op.comp R) (M : PresheafOfModules R) {X Y : Cᵒᵖ} (f : X Y) (m : ((ModuleCat.restrictScalars (φ.app X).hom).obj (M.obj (Opposite.op (F.obj (Opposite.unop X)))))) :
    (((PresheafOfModules.pushforward φ).obj M).map f).hom m = (M.map (F.map f.unop).op).hom m
    @[simp]
    theorem PresheafOfModules.pushforward_obj_map_apply' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat} (φ : S F.op.comp R) (M : PresheafOfModules R) {X Y : Cᵒᵖ} (f : X Y) (m : ((ModuleCat.restrictScalars (φ.app X).hom).obj (M.obj (Opposite.op (F.obj (Opposite.unop X)))))) :
    (((PresheafOfModules.pushforward φ).obj M).map f).hom m = (M.map (F.map f.unop).op).hom m

    @[simp]-normal form of pushforward_obj_map_apply.

    theorem PresheafOfModules.pushforward_map_app_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat} (φ : S F.op.comp R) {M N : PresheafOfModules R} (α : M N) (X : Cᵒᵖ) (m : ((ModuleCat.restrictScalars (φ.app X).hom).obj (M.obj (Opposite.op (F.obj (Opposite.unop X)))))) :
    (((PresheafOfModules.pushforward φ).map α).app X).hom m = (α.app (Opposite.op (F.obj (Opposite.unop X)))).hom m
    @[simp]
    theorem PresheafOfModules.pushforward_map_app_apply' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat} (φ : S F.op.comp R) {M N : PresheafOfModules R} (α : M N) (X : Cᵒᵖ) (m : ((ModuleCat.restrictScalars (φ.app X).hom).obj (M.obj (Opposite.op (F.obj (Opposite.unop X)))))) :
    (((PresheafOfModules.pushforward φ).map α).app X).hom m = (α.app (Opposite.op (F.obj (Opposite.unop X)))).hom m

    @[simp]-normal form of pushforward_map_app_apply.