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.

From the compatibility of pushforward with respect to composition, we deduce similar pseudofunctor-like properties of the pullback functors.

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.

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

instance PresheafOfModules.instIsRightAdjointPushforwardIdFunctorOppositeRingCat {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {S : CategoryTheory.Functor Cᵒᵖ RingCat} : (pushforward (CategoryTheory.CategoryStruct.id S)).IsRightAdjoint

noncomputable def PresheafOfModules.pullbackId {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (S : CategoryTheory.Functor Cᵒᵖ RingCat) : pullback (CategoryTheory.CategoryStruct.id S) ≅ CategoryTheory.Functor.id (PresheafOfModules S)

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

instance PresheafOfModules.instIsRightAdjointPushforwardCompFunctorOppositeRingCatWhiskerLeftOp {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) {G : CategoryTheory.Functor D E} {T : CategoryTheory.Functor Eᵒᵖ RingCat} (ψ : R ⟶ G.op.comp T) [(pushforward φ).IsRightAdjoint] [(pushforward ψ).IsRightAdjoint] : (pushforward (CategoryTheory.CategoryStruct.comp φ (F.op.whiskerLeft ψ))).IsRightAdjoint

noncomputable def PresheafOfModules.pullbackComp {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) {G : CategoryTheory.Functor D E} {T : CategoryTheory.Functor Eᵒᵖ RingCat} (ψ : R ⟶ G.op.comp T) [(pushforward φ).IsRightAdjoint] [(pushforward ψ).IsRightAdjoint] : (pullback φ).comp (pullback ψ) ≅ pullback (CategoryTheory.CategoryStruct.comp φ (F.op.whiskerLeft ψ))

The composition of two pullback functors on presheaves of modules identifies to the pullback for the composition.

theorem PresheafOfModules.pullback_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) {G : CategoryTheory.Functor D E} {T : CategoryTheory.Functor Eᵒᵖ RingCat} (ψ : R ⟶ G.op.comp T) [(pushforward φ).IsRightAdjoint] [(pushforward ψ).IsRightAdjoint] {T' : CategoryTheory.Functor E'ᵒᵖ RingCat} {G' : CategoryTheory.Functor E E'} (ψ' : T ⟶ G'.op.comp T') [(pushforward ψ').IsRightAdjoint] : (pullback φ).isoWhiskerLeft (pullbackComp ψ ψ') ≪≫ pullbackComp φ (CategoryTheory.CategoryStruct.comp ψ (G.op.whiskerLeft ψ')) = ((pullback φ).associator (pullback ψ) (pullback ψ')).symm ≪≫ CategoryTheory.Functor.isoWhiskerRight (pullbackComp φ ψ) (pullback ψ') ≪≫ pullbackComp (CategoryTheory.CategoryStruct.comp φ (F.op.whiskerLeft ψ)) ψ'

theorem PresheafOfModules.pullback_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) [(pushforward φ).IsRightAdjoint] : pullbackComp (CategoryTheory.CategoryStruct.id S) φ = CategoryTheory.Functor.isoWhiskerRight (pullbackId S) (pullback φ) ≪≫ (pullback φ).leftUnitor

theorem PresheafOfModules.pullback_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) [(pushforward φ).IsRightAdjoint] : pullbackComp φ (CategoryTheory.CategoryStruct.id R) = (pullback φ).isoWhiskerLeft (pullbackId R) ≪≫ (pullback φ).rightUnitor