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.{w', w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] (F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)) (E : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.sheafToPresheaf J D))) (X : C) (W : J.Cover X) (S : CategoryTheory.Limits.Multifork (W.index E.pt)) : CategoryTheory.Limits.Cone (F.comp ((CategoryTheory.sheafToPresheaf J D).comp ((CategoryTheory.evaluation Cᵒᵖ D).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.{w', 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 (F.comp (CategoryTheory.sheafToPresheaf J D))) (hE : CategoryTheory.Limits.IsLimit E) (X : C) (W : J.Cover X) : CategoryTheory.Limits.IsLimit (W.multifork 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.{w', 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 (F.comp (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.instCreatesLimitFunctorOppositeSheafToPresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', 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.{w', 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 = { CreatesLimit := fun {K_1 : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)} => inferInstance }

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

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

instance CategoryTheory.Sheaf.instHasFiniteLimits {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] [CategoryTheory.Limits.HasFiniteLimits D] : CategoryTheory.Limits.HasFiniteLimits (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.{w', w} D] [CategoryTheory.Limits.HasLimitsOfSize.{u₁, u₂, w', w} D] : CategoryTheory.CreatesLimitsOfSize.{u₁, u₂, max u w', max u w', max (max (max u v) w) w', max (max (max u v) w) w'} (CategoryTheory.sheafToPresheaf J D)

Equations

• CategoryTheory.Sheaf.createsLimits = { CreatesLimitsOfShape := fun {J_1 : Type ?u.44} [CategoryTheory.Category.{?u.45, ?u.44} J_1] => CategoryTheory.Sheaf.createsLimitsOfShape }

instance CategoryTheory.Sheaf.hasLimitsOfSize {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] [CategoryTheory.Limits.HasLimitsOfSize.{u₁, u₂, w', w} D] : CategoryTheory.Limits.HasLimitsOfSize.{u₁, u₂, max u w', max (max (max w u) w') v} (CategoryTheory.Sheaf J D)

noncomputable def CategoryTheory.Sheaf.sheafifyCocone {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] [CategoryTheory.HasWeakSheafify J D] {F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)} (E : CategoryTheory.Limits.Cocone (F.comp (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.

noncomputable def CategoryTheory.Sheaf.isColimitSheafifyCocone {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] [CategoryTheory.HasWeakSheafify J D] {F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)} (E : CategoryTheory.Limits.Cocone (F.comp (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.instHasColimitsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.Limits.HasColimitsOfShape K D] : CategoryTheory.Limits.HasColimitsOfShape K (CategoryTheory.Sheaf J D)

instance CategoryTheory.Sheaf.instHasFiniteCoproducts {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.Limits.HasFiniteCoproducts D] : CategoryTheory.Limits.HasFiniteCoproducts (CategoryTheory.Sheaf J D)

instance CategoryTheory.Sheaf.instHasFiniteColimits {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.Limits.HasFiniteColimits D] : CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.Sheaf J D)

instance CategoryTheory.Sheaf.instHasColimitsOfSize {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.Limits.HasColimitsOfSize.{u₁, u₂, w', w} D] : CategoryTheory.Limits.HasColimitsOfSize.{u₁, u₂, max u w', max (max (max w u) w') v} (CategoryTheory.Sheaf J D)

def CategoryTheory.Sheaf.createsColimitOfIsSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] (F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)) (h : ∀ (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.sheafToPresheaf J D))), CategoryTheory.Limits.IsColimit c → CategoryTheory.Presheaf.IsSheaf J c.pt) : CategoryTheory.CreatesColimit F (CategoryTheory.sheafToPresheaf J D)

If every cocone on a diagram of sheaves which is a colimit on the level of presheaves satisfies the condition that the cocone point is a sheaf, then the functor from sheaves to preseheaves creates colimits of the diagram. Note: this almost never holds in sheaf categories in general, but it does for the extensive topology (see Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits).

Equations

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