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₀.
Instances For
@[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ᵒᵖ)
:
@[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.
Instances For
@[reducible, inline]
abbrev
PresheafOfModules.pushforward₀OfCommRingCat
{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ᵒᵖ CommRingCat)
:
If F : C ⥤ D if a functor and R : Dᵒᵖ ⥤ CommRingCat is a presheaf
of commutative rings, this is the pushforward functor from the category
of presheaves of modules on R to the category of presheaves of
modules on F.op ⋙ R.
Instances For
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.
Instances For
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)
:
The pushforward functor PresheafOfModules R ⥤ PresheafOfModules S induced by
a morphism of presheaves of rings S ⟶ F.op ⋙ R.
Instances For
@[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.
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 (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)
:
The pushforward functor by the identity morphism identifies to the identify functor of the category of presheaves of modules.
Instances For
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.
Instances For
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)
:
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)
: