Pullback of sheaves

Main definitions

• CategoryTheory.Functor.sheafPullback: the functor Sheaf J A ⥤ Sheaf K A obtained as an extension of a functor G : C ⥤ D between the underlying categories.

• 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.

instance CategoryTheory.instCreatesLimitsSheafFunctorOppositeSheafToPresheafOfHasLimits {C : Type v₁} [CategoryTheory.SmallCategory C] (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.Limits.HasLimits A] : CategoryTheory.CreatesLimits (CategoryTheory.sheafToPresheaf J A)

Equations

• CategoryTheory.instCreatesLimitsSheafFunctorOppositeSheafToPresheafOfHasLimits A J = inferInstance

instance CategoryTheory.instIsCofilteredCover {C : Type v₁} [CategoryTheory.SmallCategory C] (J : CategoryTheory.GrothendieckTopology C) {X : C} : CategoryTheory.IsCofiltered (J.Cover X)

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Functor.sheafPullback_map {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] : ∀ {X Y : CategoryTheory.Sheaf J A} (f : X ⟶ Y), (G.sheafPullback A J K).map f = (CategoryTheory.presheafToSheaf K A).map ((CategoryTheory.lan G.op).map f.val)

@[simp]

theorem CategoryTheory.Functor.sheafPullback_obj {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] (X : CategoryTheory.Sheaf J A) : (G.sheafPullback A J K).obj X = (CategoryTheory.presheafToSheaf K A).obj ((CategoryTheory.lan G.op).obj X.val)

def CategoryTheory.Functor.sheafPullback {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] : 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 = (CategoryTheory.sheafToPresheaf J A).comp ((CategoryTheory.lan G.op).comp (CategoryTheory.presheafToSheaf K A))

instance CategoryTheory.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat {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] [CategoryTheory.RepresentablyFlat G] : CategoryTheory.Limits.PreservesFiniteLimits (G.sheafPullback A J K)

Equations

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

def CategoryTheory.Functor.sheafAdjunctionContinuous {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] : G.sheafPullback A J K ⊣ G.sheafPushforwardContinuous A J K

The pullback functor is left adjoint to the pushforward functor.

Equations

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