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) [(PresheafOfModules.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.

Equations

• PresheafOfModules.pullback φ = (PresheafOfModules.pushforward φ).leftAdjoint

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) [(PresheafOfModules.pushforward φ).IsRightAdjoint] : PresheafOfModules.pullback φ ⊣ PresheafOfModules.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.

Equations

• PresheafOfModules.pullbackPushforwardAdjunction φ = CategoryTheory.Adjunction.ofIsRightAdjoint (PresheafOfModules.pushforward φ)

@[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) : PresheafOfModules S → Prop

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.

Equations

• PresheafOfModules.PullbackObjIsDefined φ = (PresheafOfModules.pushforward φ).LeftAdjointObjIsDefined

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) : ((PresheafOfModules.pushforward φ).comp (CategoryTheory.coyoneda.obj (Opposite.op ((PresheafOfModules.free S).obj (CategoryTheory.yoneda.obj X))))).CorepresentableBy ((PresheafOfModules.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)).

Equations

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

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) : PresheafOfModules.PullbackObjIsDefined φ ((PresheafOfModules.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) : PresheafOfModules.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) : (PresheafOfModules.pushforward φ).IsRightAdjoint