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.

def PresheafOfModules.pushforward₀_obj {C : Type u₁} [CategoryTheory.Category C] {D : Type u₂} [CategoryTheory.Category D] (F : CategoryTheory.Functor C D) (R : CategoryTheory.Functor (Opposite D) RingCat) (M : PresheafOfModules R) : PresheafOfModules (F.op.comp R)

Implementation of pushforward₀.

Equations

• One or more equations did not get rendered due to their size.

theorem PresheafOfModules.pushforward₀_obj_map {C : Type u₁} [CategoryTheory.Category C] {D : Type u₂} [CategoryTheory.Category D] (F : CategoryTheory.Functor C D) (R : CategoryTheory.Functor (Opposite D) RingCat) (M : PresheafOfModules R) {X Y : Opposite C} (f : Quiver.Hom X Y) : Eq ((pushforward₀_obj F R M).map f) (M.map (F.op.map f))

theorem PresheafOfModules.pushforward₀_obj_obj_isModule {C : Type u₁} [CategoryTheory.Category C] {D : Type u₂} [CategoryTheory.Category D] (F : CategoryTheory.Functor C D) (R : CategoryTheory.Functor (Opposite D) RingCat) (M : PresheafOfModules R) (X : Opposite C) : Eq ((pushforward₀_obj F R M).obj X).isModule (M.obj (F.op.obj X)).isModule

theorem PresheafOfModules.pushforward₀_obj_obj_carrier {C : Type u₁} [CategoryTheory.Category C] {D : Type u₂} [CategoryTheory.Category D] (F : CategoryTheory.Functor C D) (R : CategoryTheory.Functor (Opposite D) RingCat) (M : PresheafOfModules R) (X : Opposite C) : Eq ((pushforward₀_obj F R M).obj X).carrier (M.obj (F.op.obj X)).carrier

theorem PresheafOfModules.pushforward₀_obj_obj_isAddCommGroup {C : Type u₁} [CategoryTheory.Category C] {D : Type u₂} [CategoryTheory.Category D] (F : CategoryTheory.Functor C D) (R : CategoryTheory.Functor (Opposite D) RingCat) (M : PresheafOfModules R) (X : Opposite C) : Eq ((pushforward₀_obj F R M).obj X).isAddCommGroup (M.obj (F.op.obj X)).isAddCommGroup

def PresheafOfModules.pushforward₀ {C : Type u₁} [CategoryTheory.Category C] {D : Type u₂} [CategoryTheory.Category D] (F : CategoryTheory.Functor C D) (R : CategoryTheory.Functor (Opposite 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 C] {D : Type u₂} [CategoryTheory.Category D] (F : CategoryTheory.Functor C D) (R : CategoryTheory.Functor (Opposite D) RingCat) : CategoryTheory.Iso ((pushforward₀ F R).comp (toPresheaf (F.op.comp R))) ((toPresheaf R).comp ((CategoryTheory.whiskeringLeft (Opposite C) (Opposite D) Ab).obj F.op))

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

Equations

• Eq (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 C] {D : Type u₂} [CategoryTheory.Category D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor (Opposite D) RingCat} {S : CategoryTheory.Functor (Opposite C) RingCat} (φ : Quiver.Hom 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

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

theorem PresheafOfModules.pushforward_obj_obj {C : Type u₁} [CategoryTheory.Category C] {D : Type u₂} [CategoryTheory.Category D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor (Opposite D) RingCat} {S : CategoryTheory.Functor (Opposite C) RingCat} (φ : Quiver.Hom S (F.op.comp R)) (X : PresheafOfModules R) (X✝ : Opposite C) : Eq (((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 C] {D : Type u₂} [CategoryTheory.Category D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor (Opposite D) RingCat} {S : CategoryTheory.Functor (Opposite C) RingCat} (φ : Quiver.Hom S (F.op.comp R)) : CategoryTheory.Iso ((pushforward φ).comp (toPresheaf S)) ((toPresheaf R).comp ((CategoryTheory.whiskeringLeft (Opposite C) (Opposite D) Ab).obj F.op))

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

Equations

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

theorem PresheafOfModules.pushforward_obj_map_apply {C : Type u₁} [CategoryTheory.Category C] {D : Type u₂} [CategoryTheory.Category D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor (Opposite D) RingCat} {S : CategoryTheory.Functor (Opposite C) RingCat} (φ : Quiver.Hom S (F.op.comp R)) (M : PresheafOfModules R) {X Y : Opposite C} (f : Quiver.Hom X Y) (m : ((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).obj (M.obj { unop := F.obj (Opposite.unop X) })).carrier) : Eq (DFunLike.coe (ModuleCat.Hom.hom (((pushforward φ).obj M).map f)) m) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (M.map (F.map f.unop).op)) m)

theorem PresheafOfModules.pushforward_obj_map_apply' {C : Type u₁} [CategoryTheory.Category C] {D : Type u₂} [CategoryTheory.Category D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor (Opposite D) RingCat} {S : CategoryTheory.Functor (Opposite C) RingCat} (φ : Quiver.Hom S (F.op.comp R)) (M : PresheafOfModules R) {X Y : Opposite C} (f : Quiver.Hom X Y) (m : ((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).obj (M.obj { unop := F.obj (Opposite.unop X) })).carrier) : Eq (DFunLike.coe (ModuleCat.Hom.hom (((pushforward φ).obj M).map f)) m) (DFunLike.coe (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 C] {D : Type u₂} [CategoryTheory.Category D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor (Opposite D) RingCat} {S : CategoryTheory.Functor (Opposite C) RingCat} (φ : Quiver.Hom S (F.op.comp R)) {M N : PresheafOfModules R} (α : Quiver.Hom M N) (X : Opposite C) (m : ((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).obj (M.obj { unop := F.obj (Opposite.unop X) })).carrier) : Eq (DFunLike.coe (ModuleCat.Hom.hom (((pushforward φ).map α).app X)) m) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (α.app { unop := F.obj (Opposite.unop X) })) m)

theorem PresheafOfModules.pushforward_map_app_apply' {C : Type u₁} [CategoryTheory.Category C] {D : Type u₂} [CategoryTheory.Category D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor (Opposite D) RingCat} {S : CategoryTheory.Functor (Opposite C) RingCat} (φ : Quiver.Hom S (F.op.comp R)) {M N : PresheafOfModules R} (α : Quiver.Hom M N) (X : Opposite C) (m : ((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).obj (M.obj { unop := F.obj (Opposite.unop X) })).carrier) : Eq (DFunLike.coe (ModuleCat.Hom.hom (((pushforward φ).map α).app X)) m) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (α.app { unop := F.obj (Opposite.unop X) })) m)

@[simp]-normal form of pushforward_map_app_apply.