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.

instance PresheafOfModules.instModuleαRingObjOppositeRingCatCompOpAddCommGroupAddCommGrpPresheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor Dᵒᵖ RingCat} (P : PresheafOfModules R) (F : CategoryTheory.Functor C D) (X : Cᵒᵖ) : Module ↑((F.op.comp R).obj X) ↑((F.op.comp P.presheaf).obj X)

Equations

• P.instModuleαRingObjOppositeRingCatCompOpAddCommGroupAddCommGrpPresheaf F X = inferInstanceAs (Module ↑(R.obj (F.op.obj X)) ↑(P.presheaf.obj (F.op.obj X)))

def PresheafOfModules.pushforward₀ {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) : CategoryTheory.Functor (PresheafOfModules R) (PresheafOfModules (F.op.comp R))

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.

def PresheafOfModules.pushforward₀CompToPresheaf {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) : (PresheafOfModules.pushforward₀ F R).comp (PresheafOfModules.toPresheaf (F.op.comp R)) ≅ (PresheafOfModules.toPresheaf R).comp ((CategoryTheory.whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrp).obj F.op)

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)))

noncomputable def PresheafOfModules.pushforward {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) : CategoryTheory.Functor (PresheafOfModules R) (PresheafOfModules S)

The pushforward functor PresheafOfModules R ⥤ PresheafOfModules S induced by a morphism of presheaves of rings S ⟶ F.op ⋙ R.

Equations

• PresheafOfModules.pushforward φ = (PresheafOfModules.pushforward₀ F R).comp (PresheafOfModules.restrictScalars φ)

noncomputable def PresheafOfModules.pushforwardCompToPresheaf {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) : (PresheafOfModules.pushforward φ).comp (PresheafOfModules.toPresheaf S) ≅ (PresheafOfModules.toPresheaf R).comp ((CategoryTheory.whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrp).obj F.op)

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

Equations

• PresheafOfModules.pushforwardCompToPresheaf φ = CategoryTheory.Iso.refl ((PresheafOfModules.pushforward φ).comp (PresheafOfModules.toPresheaf S))

theorem PresheafOfModules.pushforward_obj_obj {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ᵒᵖ) : ((PresheafOfModules.pushforward φ).obj M).obj X = (ModuleCat.restrictScalars (φ.app X)).obj (M.obj { unop := F.obj X.unop })

@[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 { unop := F.obj X.unop }))) : (((PresheafOfModules.pushforward φ).obj M).map f) m = (M.map (F.map f.unop).op) 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 : PresheafOfModules R} {N : PresheafOfModules R} (α : M ⟶ N) (X : Cᵒᵖ) (m : ↑((ModuleCat.restrictScalars (φ.app X)).obj (M.obj { unop := F.obj X.unop }))) : (PresheafOfModules.Hom.app ((PresheafOfModules.pushforward φ).map α) X) m = (PresheafOfModules.Hom.app α { unop := F.obj X.unop }) m