mathlib documentation


PresheafedSpace C has colimits.

If C has limits, then the category PresheafedSpace C has colimits, and the forgetful functor to Top preserves these colimits.

When restricted to a diagram where the underlying continuous maps are open embeddings, this says that we can glue presheaved spaces.

Given a diagram F : J ⥤ PresheafedSpace C, we first build the colimit of the underlying topological spaces, as colimit (F ⋙ PresheafedSpace.forget C). Call that colimit space X.

Our strategy is to push each of the presheaves F.obj j forward along the continuous map colimit.ι (F ⋙ PresheafedSpace.forget C) j to X. Since pushforward is functorial, we obtain a diagram J ⥤ (presheaf C X)ᵒᵖ of presheaves on a single space X. (Note that the arrows now point the other direction, because this is the way PresheafedSpace C is set up.)

The limit of this diagram then constitutes the colimit presheaf.

Auxilliary definition for PresheafedSpace.colimit_cocone_is_colimit.


When C has limits, the category of presheaved spaces with values in C itself has colimits.