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.

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

    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

      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.