Pullback of sheaves

Main definitions

• CategoryTheory.Functor.sheafPullback: when G : C ⥤ D is a continuous functor between sites (for topologies J on C and K on D) such that the functor G.sheafPushforwardContinuous A J K : Sheaf K A ⥤ Sheaf J A has a left adjoint, this is the pullback functor defined as a chosen left adjoint.

• CategoryTheory.Functor.sheafAdjunctionContinuous: the adjunction G.sheafPullback A J K ⊣ G.sheafPushforwardContinuous A J K when the functor G is continuous. In case G is representably flat, the pullback functor on sheaves commutes with finite limits: this is a morphism of sites in the sense of SGA 4 IV 4.9.

noncomputable def CategoryTheory.Functor.sheafPullback {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] (G : Functor C D) (A : Type u₁) [Category.{v₁, u₁} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [G.IsContinuous J K] [(G.sheafPushforwardContinuous A J K).IsRightAdjoint] : Functor (Sheaf J A) (Sheaf K A)

The pullback functor Sheaf J A ⥤ Sheaf K A associated to a functor G : C ⥤ D in the same direction as G.

noncomputable def CategoryTheory.Functor.sheafAdjunctionContinuous {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] (G : Functor C D) (A : Type u₁) [Category.{v₁, u₁} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [G.IsContinuous J K] [(G.sheafPushforwardContinuous A J K).IsRightAdjoint] : G.sheafPullback A J K ⊣ G.sheafPushforwardContinuous A J K

The pullback functor is left adjoint to the pushforward functor.

noncomputable def CategoryTheory.Functor.sheafPullbackConstruction.sheafPullback {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] (G : Functor C D) (A : Type u₁) [Category.{v₁, u₁} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [∀ (F : Functor Cᵒᵖ A), G.op.HasLeftKanExtension F] [HasWeakSheafify K A] : Functor (Sheaf J A) (Sheaf K A)

Construction of the pullback of sheaves using a left Kan extension.

noncomputable def CategoryTheory.Functor.sheafPullbackConstruction.sheafAdjunctionContinuous {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] (G : Functor C D) (A : Type u₁) [Category.{v₁, u₁} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [∀ (F : Functor Cᵒᵖ A), G.op.HasLeftKanExtension F] [G.IsContinuous J K] [HasWeakSheafify K A] : sheafPullback G A J K ⊣ G.sheafPushforwardContinuous A J K

The constructed sheafPullback G A J K is left adjoint to G.sheafPushforwardContinuous A J K.

instance CategoryTheory.Functor.sheafPullbackConstruction.instIsRightAdjointSheafSheafPushforwardContinuousOfHasWeakSheafify {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] (G : Functor C D) (A : Type u₁) [Category.{v₁, u₁} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [G.IsContinuous J K] [∀ (F : Functor Cᵒᵖ A), G.op.HasLeftKanExtension F] [HasWeakSheafify K A] : (G.sheafPushforwardContinuous A J K).IsRightAdjoint

noncomputable def CategoryTheory.Functor.sheafPullbackConstruction.sheafPullbackIso {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] (G : Functor C D) (A : Type u₁) [Category.{v₁, u₁} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [G.IsContinuous J K] [∀ (F : Functor Cᵒᵖ A), G.op.HasLeftKanExtension F] [HasWeakSheafify K A] : G.sheafPullback A J K ≅ sheafPullback G A J K

The constructed pullback of sheaves is isomorphic to the abstract one.

instance CategoryTheory.Functor.sheafPullbackConstruction.instPreservesFiniteLimitsSheafSheafPullback {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] (G : Functor C D) (A : Type u₁) [Category.{v₁, u₁} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [∀ (F : Functor Cᵒᵖ A), G.op.HasLeftKanExtension F] [HasSheafify K A] [HasSheafify J A] [Limits.PreservesFiniteLimits G.op.lan] : Limits.PreservesFiniteLimits (sheafPullback G A J K)

instance CategoryTheory.Functor.sheafPullbackConstruction.preservesFiniteLimits {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] (G : Functor C D) (A : Type u₁) [Category.{v₁, u₁} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) [G.IsContinuous J K] [∀ (F : Functor Cᵒᵖ A), G.op.HasLeftKanExtension F] [HasSheafify K A] [HasSheafify J A] [Limits.PreservesFiniteLimits G.op.lan] : Limits.PreservesFiniteLimits (G.sheafPullback A J K)

instance CategoryTheory.Functor.SmallCategories.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat {C : Type v₁} [SmallCategory C] {D : Type v₁} [SmallCategory D] (G : Functor C D) (A : Type u₁) [Category.{v₁, u₁} A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) {FA : A → A → Type u_1} {CA : A → Type v₁} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [ConcreteCategory A FA] [Limits.PreservesLimits (forget A)] [Limits.HasColimits A] [Limits.HasLimits A] [Limits.PreservesFilteredColimits (forget A)] [(forget A).ReflectsIsomorphisms] [G.IsContinuous J K] [RepresentablyFlat G] : Limits.PreservesFiniteLimits (G.sheafPullback A J K)