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.

def CategoryTheory.Functor.sheafPullback {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (G : CategoryTheory.Functor C D) (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsContinuous J K] [(G.sheafPushforwardContinuous A J K).IsRightAdjoint] : CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.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.

Equations

• G.sheafPullback A J K = (G.sheafPushforwardContinuous A J K).leftAdjoint

def CategoryTheory.Functor.sheafAdjunctionContinuous {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (G : CategoryTheory.Functor C D) (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.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.

Equations

• G.sheafAdjunctionContinuous A J K = CategoryTheory.Adjunction.ofIsRightAdjoint (G.sheafPushforwardContinuous A J K)

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

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

Equations

• CategoryTheory.Functor.sheafPullbackConstruction.sheafPullback G A J K = (CategoryTheory.sheafToPresheaf J A).comp (G.op.lan.comp (CategoryTheory.presheafToSheaf K A))

def CategoryTheory.Functor.sheafPullbackConstruction.sheafAdjunctionContinuous {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (G : CategoryTheory.Functor C D) (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasLeftKanExtension F] [G.IsContinuous J K] [CategoryTheory.HasWeakSheafify K A] : CategoryTheory.Functor.sheafPullbackConstruction.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.

Equations

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

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

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

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

Equations

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

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

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

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