Pullback of sheaves of modules

Let S and R be sheaves of rings over sites (C, J) and (D, K) respectively. Let F : C ⥤ D be a continuous functor between these sites, and let φ : S ⟶ (F.sheafPushforwardContinuous RingCat.{u} J K).obj R be a morphism of sheaves of rings.

In this file, we define the pullback functor for sheaves of modules pullback.{v} φ : SheafOfModules.{v} S ⥤ SheafOfModules.{v} R that is left adjoint to pushforward.{v} φ. We show that it exists under suitable assumptions, and prove that the pullback of (pre)sheaves of modules commutes with the sheafification.

noncomputable def SheafOfModules.pullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) [(pushforward φ).IsRightAdjoint] : CategoryTheory.Functor (SheafOfModules S) (SheafOfModules R)

The pullback functor SheafOfModules S ⥤ SheafOfModules R induced by a morphism of sheaves of rings S ⟶ (F.sheafPushforwardContinuous RingCat.{u} J K).obj R, defined as the left adjoint functor to the pushforward, when it exists.

noncomputable def SheafOfModules.pullbackPushforwardAdjunction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) [(pushforward φ).IsRightAdjoint] : pullback φ ⊣ pushforward φ

Given a continuous functor between sites F, and a morphism of sheaves of rings S ⟶ (F.sheafPushforwardContinuous RingCat.{u} J K).obj R, this is the adjunction between the corresponding pullback and pushforward functors on the categories of sheaves of modules.

noncomputable def SheafOfModules.PullbackConstruction.adjunction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) [(PresheafOfModules.pushforward φ.val).IsRightAdjoint] [CategoryTheory.HasWeakSheafify K AddCommGrp] [K.WEqualsLocallyBijective AddCommGrp] : (forget S).comp ((PresheafOfModules.pullback φ.val).comp (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.val))) ⊣ pushforward φ

Construction of a left adjoint to the functor pushforward.{v} φ by using the pullback of presheaves of modules and the sheafification.

instance SheafOfModules.instIsRightAdjointPushforward {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) [(PresheafOfModules.pushforward φ.val).IsRightAdjoint] [CategoryTheory.HasWeakSheafify K AddCommGrp] [K.WEqualsLocallyBijective AddCommGrp] : (pushforward φ).IsRightAdjoint

noncomputable def SheafOfModules.pullbackIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) [(PresheafOfModules.pushforward φ.val).IsRightAdjoint] [CategoryTheory.HasWeakSheafify K AddCommGrp] [K.WEqualsLocallyBijective AddCommGrp] : pullback φ ≅ (forget S).comp ((PresheafOfModules.pullback φ.val).comp (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.val)))

The pullback functor on sheaves of modules can be described as a composition of the forget functor to presheaves, the pullback on presheaves of modules, and the sheafification functor.

noncomputable def SheafOfModules.sheafificationCompPullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) [(PresheafOfModules.pushforward φ.val).IsRightAdjoint] [CategoryTheory.HasWeakSheafify K AddCommGrp] [K.WEqualsLocallyBijective AddCommGrp] [CategoryTheory.HasWeakSheafify J AddCommGrp] [J.WEqualsLocallyBijective AddCommGrp] : (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id S.val)).comp (pullback φ) ≅ (PresheafOfModules.pullback φ.val).comp (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.val))

The pullback of (pre)sheaves of modules commutes with the sheafification.