# Documentation

Mathlib.CategoryTheory.Sites.Limits

# 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.

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.

Instances For
def CategoryTheory.Sheaf.isLimitMultiforkOfIsLimit {C : Type u} {D : Type w} [] {K : Type z} (F : ) (hE : ) (X : C) :

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.

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

instance CategoryTheory.Sheaf.createsLimitsOfShape {C : Type u} {D : Type w} [] {K : Type z} :
instance CategoryTheory.Sheaf.createsLimits {C : Type u} {D : Type w} [] :
@[simp]
theorem CategoryTheory.Sheaf.sheafifyCocone_pt_val {C : Type u} {D : Type w} [] {K : Type (max v u)} [] [] [] {F : } :
@[simp]
theorem CategoryTheory.Sheaf.sheafifyCocone_ι_app_val {C : Type u} {D : Type w} [] {K : Type (max v u)} [] [] [] {F : } (k : K) :
(.app k).val = CategoryTheory.CategoryStruct.comp (E.app k) ()
noncomputable def CategoryTheory.Sheaf.sheafifyCocone {C : Type u} {D : Type w} [] {K : Type (max v u)} [] [] [] {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.

Instances For
@[simp]
theorem CategoryTheory.Sheaf.isColimitSheafifyCocone_desc_val {C : Type u} {D : Type w} [] {K : Type (max v u)} [] [] [] {F : } (hE : ) (S : ) :
noncomputable def CategoryTheory.Sheaf.isColimitSheafifyCocone {C : Type u} {D : Type w} [] {K : Type (max v u)} [] [] [] {F : } (hE : ) :

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

Instances For
instance CategoryTheory.Sheaf.instHasColimitsOfShapeSheafInstCategorySheaf {C : Type u} {D : Type w} [] {K : Type (max v u)} [] [] [] :