# 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} {D : Type w} {K : Type z} (F : ) (E : CategoryTheory.Limits.Cone (F.comp )) (X : C) (W : J.Cover X) (S : CategoryTheory.Limits.Multifork (W.index E.pt)) :
CategoryTheory.Limits.Cone (F.comp (.comp (.obj { unop := 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.
Instances For
def CategoryTheory.Sheaf.isLimitMultiforkOfIsLimit {C : Type u} {D : Type w} {K : Type z} (F : ) (E : CategoryTheory.Limits.Cone (F.comp )) (hE : ) (X : C) (W : J.Cover X) :

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.
Instances For
theorem CategoryTheory.Sheaf.isSheaf_of_isLimit {C : Type u} {D : Type w} {K : Type z} (F : ) (E : CategoryTheory.Limits.Cone (F.comp )) (hE : ) :

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.

Equations
• One or more equations did not get rendered due to their size.
instance CategoryTheory.Sheaf.createsLimitsOfShape {C : Type u} {D : Type w} {K : Type z} :
Equations
• CategoryTheory.Sheaf.createsLimitsOfShape = { CreatesLimit := fun {K_1 : } => inferInstance }
instance CategoryTheory.Sheaf.instHasLimitsOfShape {C : Type u} {D : Type w} {K : Type z} :
Equations
• =
Equations
• =
Equations
• =
instance CategoryTheory.Sheaf.createsLimits {C : Type u} {D : Type w} [] :
Equations
• CategoryTheory.Sheaf.createsLimits = { CreatesLimitsOfShape := fun {J_1 : Type u₂} [] => CategoryTheory.Sheaf.createsLimitsOfShape }
instance CategoryTheory.Sheaf.hasLimitsOfSize {C : Type u} {D : Type w} [] :
Equations
• =
noncomputable def CategoryTheory.Sheaf.sheafifyCocone {C : Type u} {D : Type w} {K : Type z} {F : } (E : CategoryTheory.Limits.Cocone (F.comp )) :

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.
Instances For
noncomputable def CategoryTheory.Sheaf.isColimitSheafifyCocone {C : Type u} {D : Type w} {K : Type z} {F : } (E : CategoryTheory.Limits.Cocone (F.comp )) (hE : ) :

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.
Instances For
instance CategoryTheory.Sheaf.instHasColimitsOfShape {C : Type u} {D : Type w} {K : Type z} :
Equations
• =
Equations
• =
Equations
• =
Equations
• =