Limits and colimits of sheaves

Limits

We prove that the forgetful functor from Sheaf J D to presheaves creates limits. If the target category D has limits (of a certain shape), this then implies that Sheaf J D has limits of the same shape and that the forgetful functor preserves these limits.

Colimits

Given a diagram F : K ⥤ Sheaf J D of sheaves, and a colimit cocone on the level of presheaves, we show that the cocone obtained by sheafifying the cocone point is a colimit cocone of sheaves.

This allows us to show that Sheaf J D has colimits (of a certain shape) as soon as D does.

def CategoryTheory.Sheaf.multiforkEvaluationCone {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] (F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)) (E : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.sheafToPresheaf J D))) (X : C) (W : CategoryTheory.GrothendieckTopology.Cover J X) (S : CategoryTheory.Limits.Multifork (CategoryTheory.GrothendieckTopology.Cover.index W E.pt)) : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Functor.comp (CategoryTheory.sheafToPresheaf J D) ((CategoryTheory.evaluation Cᵒᵖ D).toPrefunctor.obj (Opposite.op X))))

An auxiliary definition to be used below.

Whenever E is a cone of shape K of sheaves, and S is the multifork associated to a covering W of an object X, with respect to the cone point E.X, this provides a cone of shape K of objects in D, with cone point S.X.

See isLimitMultiforkOfIsLimit for more on how this definition is used.

Equations

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

def CategoryTheory.Sheaf.isLimitMultiforkOfIsLimit {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] [CategoryTheory.Limits.HasLimitsOfShape K D] (F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)) (E : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.sheafToPresheaf J D))) (hE : CategoryTheory.Limits.IsLimit E) (X : C) (W : CategoryTheory.GrothendieckTopology.Cover J X) : CategoryTheory.Limits.IsLimit (CategoryTheory.GrothendieckTopology.Cover.multifork W E.pt)

If E is a cone of shape K of sheaves, which is a limit on the level of presheaves, this definition shows that the limit presheaf satisfies the multifork variant of the sheaf condition, at a given covering W.

This is used below in isSheaf_of_isLimit to show that the limit presheaf is indeed a sheaf.

Equations

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

theorem CategoryTheory.Sheaf.isSheaf_of_isLimit {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] [CategoryTheory.Limits.HasLimitsOfShape K D] (F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)) (E : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.sheafToPresheaf J D))) (hE : CategoryTheory.Limits.IsLimit E) : CategoryTheory.Presheaf.IsSheaf J E.pt

If E is a cone which is a limit on the level of presheaves, then the limit presheaf is again a sheaf.

This is used to show that the forgetful functor from sheaves to presheaves creates limits.

instance CategoryTheory.Sheaf.instCreatesLimitSheafInstCategorySheafFunctorOppositeOppositeCategorySheafToPresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] [CategoryTheory.Limits.HasLimitsOfShape K D] (F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)) : CategoryTheory.CreatesLimit F (CategoryTheory.sheafToPresheaf J D)

Equations

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

instance CategoryTheory.Sheaf.createsLimitsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] [CategoryTheory.Limits.HasLimitsOfShape K D] : CategoryTheory.CreatesLimitsOfShape K (CategoryTheory.sheafToPresheaf J D)

Equations

• CategoryTheory.Sheaf.createsLimitsOfShape = CategoryTheory.CreatesLimitsOfShape.mk

instance CategoryTheory.Sheaf.instHasLimitsOfShapeSheafInstCategorySheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] [CategoryTheory.Limits.HasLimitsOfShape K D] : CategoryTheory.Limits.HasLimitsOfShape K (CategoryTheory.Sheaf J D)

Equations

• (_ : CategoryTheory.Limits.HasLimitsOfShape K (CategoryTheory.Sheaf J D)) = (_ : CategoryTheory.Limits.HasLimitsOfShape K (CategoryTheory.Sheaf J D))

instance CategoryTheory.Sheaf.instHasFiniteProductsSheafInstCategorySheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.Limits.HasFiniteProducts D] : CategoryTheory.Limits.HasFiniteProducts (CategoryTheory.Sheaf J D)

Equations

• (_ : CategoryTheory.Limits.HasFiniteProducts (CategoryTheory.Sheaf J D)) = (_ : CategoryTheory.Limits.HasFiniteProducts (CategoryTheory.Sheaf J D))

instance CategoryTheory.Sheaf.createsLimits {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.Limits.HasLimits D] : CategoryTheory.CreatesLimits (CategoryTheory.sheafToPresheaf J D)

Equations

• CategoryTheory.Sheaf.createsLimits = CategoryTheory.CreatesLimitsOfSize.mk

instance CategoryTheory.Sheaf.instHasLimitsSheafInstCategorySheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.Limits.HasLimits D] : CategoryTheory.Limits.HasLimits (CategoryTheory.Sheaf J D)

Equations

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

@[simp]

theorem CategoryTheory.Sheaf.sheafifyCocone_pt_val {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] [CategoryTheory.ConcreteCategory D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] {F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)} (E : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.sheafToPresheaf J D))) : (CategoryTheory.Sheaf.sheafifyCocone E).pt.val = CategoryTheory.GrothendieckTopology.sheafify J E.pt

@[simp]

theorem CategoryTheory.Sheaf.sheafifyCocone_ι_app_val {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] [CategoryTheory.ConcreteCategory D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] {F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)} (E : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.sheafToPresheaf J D))) (k : K) : ((CategoryTheory.Sheaf.sheafifyCocone E).ι.app k).val = CategoryTheory.CategoryStruct.comp (E.ι.app k) (CategoryTheory.GrothendieckTopology.toSheafify J E.pt)

noncomputable def CategoryTheory.Sheaf.sheafifyCocone {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] [CategoryTheory.ConcreteCategory D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] {F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)} (E : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.sheafToPresheaf J D))) : CategoryTheory.Limits.Cocone F

Construct a cocone by sheafifying a cocone point of a cocone E of presheaves over a functor which factors through sheaves. In isColimitSheafifyCocone, we show that this is a colimit cocone when E is a colimit.

Equations

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

@[simp]

theorem CategoryTheory.Sheaf.isColimitSheafifyCocone_desc_val {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] [CategoryTheory.ConcreteCategory D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] {F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)} (E : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.sheafToPresheaf J D))) (hE : CategoryTheory.Limits.IsColimit E) (S : CategoryTheory.Limits.Cocone F) : ((CategoryTheory.Sheaf.isColimitSheafifyCocone E hE).desc S).val = CategoryTheory.GrothendieckTopology.sheafifyLift J (hE.desc ((CategoryTheory.sheafToPresheaf J D).mapCocone S)) (_ : CategoryTheory.Presheaf.IsSheaf J S.pt.val)

noncomputable def CategoryTheory.Sheaf.isColimitSheafifyCocone {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] [CategoryTheory.ConcreteCategory D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] {F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)} (E : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F (CategoryTheory.sheafToPresheaf J D))) (hE : CategoryTheory.Limits.IsColimit E) : CategoryTheory.Limits.IsColimit (CategoryTheory.Sheaf.sheafifyCocone E)

If E is a colimit cocone of presheaves, over a diagram factoring through sheaves, then sheafifyCocone E is a colimit cocone.

Equations

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

instance CategoryTheory.Sheaf.instHasColimitsOfShapeSheafInstCategorySheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] [CategoryTheory.ConcreteCategory D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] [CategoryTheory.Limits.HasColimitsOfShape K D] : CategoryTheory.Limits.HasColimitsOfShape K (CategoryTheory.Sheaf J D)

Equations

• (_ : CategoryTheory.Limits.HasColimitsOfShape K (CategoryTheory.Sheaf J D)) = (_ : CategoryTheory.Limits.HasColimitsOfShape K (CategoryTheory.Sheaf J D))

instance CategoryTheory.Sheaf.instHasFiniteCoproductsSheafInstCategorySheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] [CategoryTheory.Limits.HasFiniteCoproducts D] : CategoryTheory.Limits.HasFiniteCoproducts (CategoryTheory.Sheaf J D)

Equations

• (_ : CategoryTheory.Limits.HasFiniteCoproducts (CategoryTheory.Sheaf J D)) = (_ : CategoryTheory.Limits.HasFiniteCoproducts (CategoryTheory.Sheaf J D))

instance CategoryTheory.Sheaf.instHasColimitsSheafInstCategorySheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [CategoryTheory.ConcreteCategory D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] [CategoryTheory.Limits.HasColimits D] : CategoryTheory.Limits.HasColimits (CategoryTheory.Sheaf J D)

Equations

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