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

Equations

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

instance CategoryTheory.Sheaf.createsLimitsOfShape {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {K : Type z} [Category.{z', z} K] [Limits.HasLimitsOfShape K D] : CreatesLimitsOfShape K (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} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {K : Type z} [Category.{z', z} K] [Limits.HasLimitsOfShape K D] : Limits.HasLimitsOfShape K (Sheaf J D)

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

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

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

Equations

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

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

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

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

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

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

def CategoryTheory.Sheaf.createsColimitOfIsSheaf {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{w', w} D] {K : Type z} [Category.{z', z} K] (F : Functor K (Sheaf J D)) (h : ∀ (c : Limits.Cocone (F.comp (sheafToPresheaf J D))) (x : Limits.IsColimit c), Presheaf.IsSheaf J c.pt) : CreatesColimit F (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.lean).

Equations

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