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

    The pushforward of presheaves of modules commutes with the forgetful functor to presheaves of abelian groups.

    Instances For

      The pushforward of presheaves of modules commutes with the forgetful functor to presheaves of abelian groups.

      Instances For
        @[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 : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) (m : ((ModuleCat.restrictScalars (φ.app X)).obj (M.obj (Opposite.op (F.obj (Opposite.unop X)))))) :
        (((PresheafOfModules.pushforward φ).obj M).map f) m = (M.map (F.map f.unop).op) m
        @[simp]