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.instCreatesLimitsSheafInstCategorySheafFunctorOppositeOppositeCategorySheafToPresheaf {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.instCreatesLimitsSheafInstCategorySheafFunctorOppositeOppositeCategorySheafToPresheaf A J = inferInstance

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

Equations

• (_ : CategoryTheory.IsCofiltered (CategoryTheory.GrothendieckTopology.Cover J X)) = (_ : CategoryTheory.IsCofiltered (CategoryTheory.GrothendieckTopology.Cover J X))

@[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.ReflectsIsomorphisms (CategoryTheory.forget A)] : ∀ {X Y : CategoryTheory.Sheaf J A} (f : X ⟶ Y), (CategoryTheory.Functor.sheafPullback G A J K).toPrefunctor.map f = (CategoryTheory.presheafToSheaf K A).toPrefunctor.map ((CategoryTheory.lan G.op).toPrefunctor.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.ReflectsIsomorphisms (CategoryTheory.forget A)] (X : CategoryTheory.Sheaf J A) : (CategoryTheory.Functor.sheafPullback G A J K).toPrefunctor.obj X = (CategoryTheory.presheafToSheaf K A).toPrefunctor.obj ((CategoryTheory.lan G.op).toPrefunctor.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.ReflectsIsomorphisms (CategoryTheory.forget A)] : 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

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

instance CategoryTheory.instPreservesFiniteLimitsSheafInstCategorySheafSheafPullback {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.ReflectsIsomorphisms (CategoryTheory.forget A)] [CategoryTheory.RepresentablyFlat G] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.Functor.sheafPullback G 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.ReflectsIsomorphisms (CategoryTheory.forget A)] [CategoryTheory.Functor.IsContinuous G J K] : CategoryTheory.Functor.sheafPullback G A J K ⊣ CategoryTheory.Functor.sheafPushforwardContinuous G 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.