Pullback of presheaves of modules

Let F : C ⥤ D be a functor, R : Dᵒᵖ ⥤ RingCat and S : Cᵒᵖ ⥤ RingCat be presheaves of rings, and φ : S ⟶ F.op ⋙ R be a morphism of presheaves of rings, we introduce the pullback functor pullback : PresheafOfModules S ⥤ PresheafOfModules R as the left adjoint of pushforward : PresheafOfModules R ⥤ PresheafOfModules S. The existence of this left adjoint functor is obtained under suitable universe assumptions.

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

The pullback functor PresheafOfModules S ⥤ PresheafOfModules R induced by a morphism of presheaves of rings S ⟶ F.op ⋙ R, defined as the left adjoint functor to the pushforward, when it exists.

noncomputable def PresheafOfModules.pullbackPushforwardAdjunction {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 φ).IsRightAdjoint] : pullback φ ⊣ pushforward φ

Given a morphism of presheaves of rings S ⟶ F.op ⋙ R, this is the adjunction between associated pullback and pushforward functors on the categories of presheaves of modules.

@[reducible, inline]

abbrev PresheafOfModules.pullbackObjIsDefined {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.ObjectProperty (PresheafOfModules S)

Given a morphism of presheaves of rings φ : S ⟶ F.op ⋙ R, this is the property that the (partial) left adjoint functor of pushforward φ is defined on a certain object M : PresheafOfModules S.

@[deprecated PresheafOfModules.pullbackObjIsDefined (since := "2025-03-06")]

def PresheafOfModules.PullbackObjIsDefined {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.ObjectProperty (PresheafOfModules S)

Alias of PresheafOfModules.pullbackObjIsDefined.

---

Given a morphism of presheaves of rings φ : S ⟶ F.op ⋙ R, this is the property that the (partial) left adjoint functor of pushforward φ is defined on a certain object M : PresheafOfModules S.

noncomputable def PresheafOfModules.pushforwardCompCoyonedaFreeYonedaCorepresentableBy {C D : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.SmallCategory D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat} (φ : S ⟶ F.op.comp R) (X : C) : ((pushforward φ).comp (CategoryTheory.coyoneda.obj (Opposite.op ((free S).obj (CategoryTheory.yoneda.obj X))))).CorepresentableBy ((free R).obj (CategoryTheory.yoneda.obj (F.obj X)))

Given a morphism of presheaves of rings φ : S ⟶ F.op ⋙ R, where F : C ⥤ D, S : Cᵒᵖ ⥤ RingCat, R : Dᵒᵖ ⥤ RingCat and X : C, the (partial) left adjoint functor of pushforward φ is defined on the object (free S).obj (yoneda.obj X): this object shall be mapped to (free R).obj (yoneda.obj (F.obj X)).

theorem PresheafOfModules.pullbackObjIsDefined_free_yoneda {C D : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.SmallCategory D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat} (φ : S ⟶ F.op.comp R) (X : C) : pullbackObjIsDefined φ ((free S).obj (CategoryTheory.yoneda.obj X))

theorem PresheafOfModules.pullbackObjIsDefined_eq_top {C D : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.SmallCategory D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat} (φ : S ⟶ F.op.comp R) : pullbackObjIsDefined φ = ⊤

instance PresheafOfModules.instIsRightAdjointPushforward {C D : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.SmallCategory D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat} (φ : S ⟶ F.op.comp R) : (pushforward φ).IsRightAdjoint