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.

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

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.

Equations

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

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.

Equations

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

instance SheafOfModules.instIsLeftAdjointPullback {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 φ).IsLeftAdjoint

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 AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] : (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.

Equations

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

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 AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] : (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 AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] : 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.

Equations

• SheafOfModules.pullbackIso φ = (SheafOfModules.pullbackPushforwardAdjunction φ).leftAdjointUniq (SheafOfModules.PullbackConstruction.adjunction φ)

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 AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] : (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.

Equations

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

instance SheafOfModules.instIsRightAdjointPushforwardIdSheafRingCat {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.Sheaf J RingCat} : (pushforward (CategoryTheory.CategoryStruct.id S)).IsRightAdjoint

noncomputable def SheafOfModules.pullbackId {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (S : CategoryTheory.Sheaf J RingCat) : pullback (CategoryTheory.CategoryStruct.id S) ≅ CategoryTheory.Functor.id (SheafOfModules S)

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

Equations

• SheafOfModules.pullbackId S = (SheafOfModules.pullbackPushforwardAdjunction (CategoryTheory.CategoryStruct.id S)).leftAdjointIdIso (SheafOfModules.pushforwardId S)

instance SheafOfModules.instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {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] {K' : CategoryTheory.GrothendieckTopology D'} {G : CategoryTheory.Functor D D'} {R' : CategoryTheory.Sheaf K' RingCat} [G.IsContinuous K K'] [G.IsContinuous K K'] [(F.comp G).IsContinuous J K'] [(F.comp G).IsContinuous J K'] (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K K').obj R') [(pushforward ψ).IsRightAdjoint] : (pushforward (CategoryTheory.CategoryStruct.comp φ ((F.sheafPushforwardContinuous RingCat J K).map ψ))).IsRightAdjoint

noncomputable def SheafOfModules.pullbackComp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {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] {K' : CategoryTheory.GrothendieckTopology D'} {G : CategoryTheory.Functor D D'} {R' : CategoryTheory.Sheaf K' RingCat} [G.IsContinuous K K'] [G.IsContinuous K K'] [(F.comp G).IsContinuous J K'] [(F.comp G).IsContinuous J K'] (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K K').obj R') [(pushforward ψ).IsRightAdjoint] : (pullback φ).comp (pullback ψ) ≅ pullback (CategoryTheory.CategoryStruct.comp φ ((F.sheafPushforwardContinuous RingCat J K).map ψ))

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

Equations

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

theorem SheafOfModules.pullback_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {D' : Type u₃} [CategoryTheory.Category.{v₃, u₃} D'] {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] {K' : CategoryTheory.GrothendieckTopology D'} {K'' : CategoryTheory.GrothendieckTopology D''} {G : CategoryTheory.Functor D D'} {R' : CategoryTheory.Sheaf K' RingCat} [G.IsContinuous K K'] [G.IsContinuous K K'] [(F.comp G).IsContinuous J K'] [(F.comp G).IsContinuous J K'] (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K K').obj R') [(pushforward ψ).IsRightAdjoint] {G' : CategoryTheory.Functor D' D''} {R'' : CategoryTheory.Sheaf K'' RingCat} [G'.IsContinuous K' K''] [G'.IsContinuous K' K''] [(G.comp G').IsContinuous K K''] [(G.comp G').IsContinuous K K''] [((F.comp G).comp G').IsContinuous J K''] [((F.comp G).comp G').IsContinuous J K''] [(F.comp (G.comp G')).IsContinuous J K''] [(F.comp (G.comp G')).IsContinuous J K''] (ψ' : R' ⟶ (G'.sheafPushforwardContinuous RingCat K' K'').obj R'') [(pushforward ψ').IsRightAdjoint] : (pullback φ).isoWhiskerLeft (pullbackComp ψ ψ') ≪≫ pullbackComp φ (CategoryTheory.CategoryStruct.comp ψ ((G.sheafPushforwardContinuous RingCat K K').map ψ')) = ((pullback φ).associator (pullback ψ) (pullback ψ')).symm ≪≫ CategoryTheory.Functor.isoWhiskerRight (pullbackComp φ ψ) (pullback ψ') ≪≫ pullbackComp (CategoryTheory.CategoryStruct.comp φ ((F.sheafPushforwardContinuous RingCat J K).map ψ)) ψ'

theorem SheafOfModules.pullback_id_comp {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] : pullbackComp (CategoryTheory.CategoryStruct.id S) φ = CategoryTheory.Functor.isoWhiskerRight (pullbackId S) (pullback φ) ≪≫ (pullback φ).leftUnitor

theorem SheafOfModules.pullback_comp_id {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] : pullbackComp φ (CategoryTheory.CategoryStruct.id R) = (pullback φ).isoWhiskerLeft (pullbackId R) ≪≫ (pullback φ).rightUnitor