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]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[(pushforward φ).IsRightAdjoint]
:
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.
Instances For
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]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[(pushforward φ).IsRightAdjoint]
:
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.
Instances For
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]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[(pushforward φ).IsRightAdjoint]
:
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]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[(PresheafOfModules.pushforward φ.hom).IsRightAdjoint]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
:
Construction of a left adjoint to the functor pushforward.{v} φ by using the
pullback of presheaves of modules and the sheafification.
Instances For
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]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[(PresheafOfModules.pushforward φ.hom).IsRightAdjoint]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
:
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]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[(PresheafOfModules.pushforward φ.hom).IsRightAdjoint]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
:
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.
Instances For
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]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[(PresheafOfModules.pushforward φ.hom).IsRightAdjoint]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
:
The pullback of (pre)sheaves of modules commutes with the sheafification.
Instances For
noncomputable def
SheafOfModules.pullbackId
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(S : CategoryTheory.Sheaf J RingCat)
:
The pullback by the identity morphism identifies to the identity functor of the category of sheaves of modules.
Instances For
@[simp]
theorem
SheafOfModules.conjugateEquiv_pullbackId_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
(S : CategoryTheory.Sheaf J RingCat)
:
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]
(φ : 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']
[(F.comp G).IsContinuous J K']
(ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K K').obj R')
[(pushforward ψ).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]
(φ : 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']
[(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.
Instances For
@[simp]
theorem
SheafOfModules.conjugateEquiv_pullbackComp_inv
{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]
(φ : 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']
[(F.comp G).IsContinuous J K']
(ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K K').obj R')
[(pushforward ψ).IsRightAdjoint]
:
(CategoryTheory.conjugateEquiv ((pullbackPushforwardAdjunction φ).comp (pullbackPushforwardAdjunction ψ))
(pullbackPushforwardAdjunction
(CategoryTheory.CategoryStruct.comp φ ((F.sheafPushforwardContinuous RingCat J K).map ψ))))
(pullbackComp φ ψ).inv = (pushforwardComp φ ψ).hom
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]
(φ : 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']
[(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.comp G').IsContinuous K 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]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[(pushforward φ).IsRightAdjoint]
:
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]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
[(pushforward φ).IsRightAdjoint]
:
pullbackComp φ (CategoryTheory.CategoryStruct.id R) = (pullback φ).isoWhiskerLeft (pullbackId R) ≪≫ (pullback φ).rightUnitor