mathlib3 documentation

category_theory.sites.limits

Limits and colimits of sheaves #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 is_limit_multifork_of_is_limit for more on how this definition is used.

Equations

If E is a cone of shape K of sheaves, which is a limit on the level of presheves, 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 is_sheaf_of_is_limit to show that the limit presheaf is indeed a sheaf.

Equations

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.

Construct a cocone by sheafifying a cocone point of a cocone E of presheaves over a functor which factors through sheaves. In is_colimit_sheafify_cocone, we show that this is a colimit cocone when E is a colimit.

Equations