Pushforward of sheaves

Main definitions

• CategoryTheory.Sites.Pushforward: the induced functor Sheaf J A ⥤ Sheaf K A for a cover-preserving and compatible-preserving functor G : (C, J) ⥤ (D, K).

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)

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

@[simp]

theorem CategoryTheory.Sites.pushforward_obj_val_obj {C : Type v₁} [CategoryTheory.SmallCategory C] {D : Type v₁} [CategoryTheory.SmallCategory 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)] (G : CategoryTheory.Functor C D) (X : CategoryTheory.Sheaf J A) (X : Dᵒᵖ) : ((CategoryTheory.Sites.pushforward A J K G).obj X).val.obj X = CategoryTheory.Limits.colimit (CategoryTheory.GrothendieckTopology.diagram K (CategoryTheory.GrothendieckTopology.plusObj K ((CategoryTheory.lan G.op).obj X.val)) X.unop)

@[simp]

theorem CategoryTheory.Sites.pushforward_obj_val_map {C : Type v₁} [CategoryTheory.SmallCategory C] {D : Type v₁} [CategoryTheory.SmallCategory 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)] (G : CategoryTheory.Functor C D) (X : CategoryTheory.Sheaf J A) : ∀ {X Y : Dᵒᵖ} (f : X ⟶ Y), ((CategoryTheory.Sites.pushforward A J K G).obj X).val.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimMap (CategoryTheory.GrothendieckTopology.diagramPullback K (CategoryTheory.GrothendieckTopology.plusObj K ((CategoryTheory.lan G.op).obj X.val)) f.unop)) (CategoryTheory.Limits.colimit.pre (CategoryTheory.GrothendieckTopology.diagram K (CategoryTheory.GrothendieckTopology.plusObj K ((CategoryTheory.lan G.op).obj X.val)) Y.unop) (CategoryTheory.GrothendieckTopology.pullback K f.unop).op)

@[simp]

theorem CategoryTheory.Sites.pushforward_map_val_app {C : Type v₁} [CategoryTheory.SmallCategory C] {D : Type v₁} [CategoryTheory.SmallCategory 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)] (G : CategoryTheory.Functor C D) : ∀ {X Y : CategoryTheory.Sheaf J A} (f : X ⟶ Y) (X_1 : Dᵒᵖ), ((CategoryTheory.Sites.pushforward A J K G).map f).val.app X_1 = CategoryTheory.Limits.colimMap (CategoryTheory.GrothendieckTopology.diagramNatTrans K (CategoryTheory.GrothendieckTopology.plusMap K ((CategoryTheory.lan G.op).map f.val)) X_1.unop)

def CategoryTheory.Sites.pushforward {C : Type v₁} [CategoryTheory.SmallCategory C] {D : Type v₁} [CategoryTheory.SmallCategory 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)] (G : CategoryTheory.Functor C D) : CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Sheaf K A)

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

instance CategoryTheory.instPreservesFiniteLimitsSheafInstCategorySheafPushforward {C : Type v₁} [CategoryTheory.SmallCategory C] {D : Type v₁} [CategoryTheory.SmallCategory 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)] (G : CategoryTheory.Functor C D) [CategoryTheory.RepresentablyFlat G] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.Sites.pushforward A J K G)

def CategoryTheory.Sites.pullbackPushforwardAdjunction {C : Type v₁} [CategoryTheory.SmallCategory C] {D : Type v₁} [CategoryTheory.SmallCategory 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)] {G : CategoryTheory.Functor C D} (hG₁ : CategoryTheory.CompatiblePreserving K G) (hG₂ : CategoryTheory.CoverPreserving J K G) : CategoryTheory.Sites.pushforward A J K G ⊣ CategoryTheory.Sites.pullback A hG₁ hG₂

The pushforward functor is left adjoint to the pullback functor.