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, and we show that they interact with the composition of morphisms similarly as pseudofunctors.

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

Implementation of pushforward₀.

@[simp]

theorem PresheafOfModules.pushforward₀_obj_map {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) (M : PresheafOfModules R) {X Y : Cᵒᵖ} (f : X ⟶ Y) : (pushforward₀_obj F R M).map f = M.map (F.op.map f)

@[simp]

theorem PresheafOfModules.pushforward₀_obj_obj_isModule {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) (M : PresheafOfModules R) (X : Cᵒᵖ) : ((pushforward₀_obj F R M).obj X).isModule = (M.obj (F.op.obj X)).isModule

@[simp]

theorem PresheafOfModules.pushforward₀_obj_obj_carrier {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) (M : PresheafOfModules R) (X : Cᵒᵖ) : ↑((pushforward₀_obj F R M).obj X) = ↑(M.obj (F.op.obj X))

@[simp]

theorem PresheafOfModules.pushforward₀_obj_obj_isAddCommGroup {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) (M : PresheafOfModules R) (X : Cᵒᵖ) : ((pushforward₀_obj F R M).obj X).isAddCommGroup = (M.obj (F.op.obj X)).isAddCommGroup

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.

noncomputable 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) : (pushforward₀ F R).comp (toPresheaf (F.op.comp R)) ≅ (toPresheaf R).comp ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ Ab).obj F.op)

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

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.

@[simp]

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) (X : PresheafOfModules R) (X✝ : Cᵒᵖ) : ((pushforward φ).obj X).obj X✝ = (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X✝))).obj ((pushforward₀_obj F R X).obj X✝)

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) : (pushforward φ).comp (toPresheaf S) ≅ (toPresheaf R).comp ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ Ab).obj F.op)

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

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 (RingCat.Hom.hom (φ.app X))).obj (M.obj (Opposite.op (F.obj (Opposite.unop X)))))) : (ModuleCat.Hom.hom (((pushforward φ).obj M).map f)) m = (CategoryTheory.ConcreteCategory.hom (M.map (F.map f.unop).op)) 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 (RingCat.Hom.hom (φ.app X))).obj (M.obj (Opposite.op (F.obj (Opposite.unop X)))))) : (ModuleCat.Hom.hom (((pushforward φ).obj M).map f)) m = (CategoryTheory.ConcreteCategory.hom (M.map (F.map f.unop).op)) 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 (RingCat.Hom.hom (φ.app X))).obj (M.obj (Opposite.op (F.obj (Opposite.unop X)))))) : (ModuleCat.Hom.hom (((pushforward φ).map α).app X)) m = (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op (F.obj (Opposite.unop X))))) 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 (RingCat.Hom.hom (φ.app X))).obj (M.obj (Opposite.op (F.obj (Opposite.unop X)))))) : (ModuleCat.Hom.hom (((pushforward φ).map α).app X)) m = (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op (F.obj (Opposite.unop X))))) m

@[simp]-normal form of pushforward_map_app_apply.

noncomputable def PresheafOfModules.pushforwardId {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor Dᵒᵖ RingCat) : pushforward (CategoryTheory.CategoryStruct.id R) ≅ CategoryTheory.Functor.id (PresheafOfModules R)

The pushforward functor by the identity morphism identifies to the identify functor of the category of presheaves of modules.

noncomputable def PresheafOfModules.pushforwardComp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat} (φ : S ⟶ F.op.comp R) {T : CategoryTheory.Functor Eᵒᵖ RingCat} {G : CategoryTheory.Functor D E} (ψ : R ⟶ G.op.comp T) : (pushforward ψ).comp (pushforward φ) ≅ pushforward (CategoryTheory.CategoryStruct.comp φ (F.op.whiskerLeft ψ))

The composition of two pushforward functors on categories of presheaves of modules identify to the pushforward for the composition.

theorem PresheafOfModules.pushforward_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄} [CategoryTheory.Category.{v₄, u₄} E'] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat} (φ : S ⟶ F.op.comp R) {T : CategoryTheory.Functor Eᵒᵖ RingCat} {G : CategoryTheory.Functor D E} (ψ : R ⟶ G.op.comp T) {T' : CategoryTheory.Functor E'ᵒᵖ RingCat} {G' : CategoryTheory.Functor E E'} (ψ' : T ⟶ G'.op.comp T') : (pushforward ψ').isoWhiskerLeft (pushforwardComp φ ψ) ≪≫ pushforwardComp (CategoryTheory.CategoryStruct.comp φ (F.op.whiskerLeft ψ)) ψ' = ((pushforward ψ').associator (pushforward ψ) (pushforward φ)).symm ≪≫ CategoryTheory.Functor.isoWhiskerRight (pushforwardComp ψ ψ') (pushforward φ) ≪≫ pushforwardComp φ (CategoryTheory.CategoryStruct.comp ψ (G.op.whiskerLeft ψ'))

theorem PresheafOfModules.pushforward_comp_id {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) : pushforwardComp (CategoryTheory.CategoryStruct.id S) φ = (pushforward φ).isoWhiskerLeft (pushforwardId S) ≪≫ (pushforward φ).rightUnitor

theorem PresheafOfModules.pushforward_id_comp {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) : pushforwardComp φ (CategoryTheory.CategoryStruct.id R) = CategoryTheory.Functor.isoWhiskerRight (pushforwardId R) (pushforward φ) ≪≫ (pushforward φ).leftUnitor