mathlib documentation

algebraic_geometry.presheafed_space.has_colimits

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.

Auxiliary definition for PresheafedSpace.colimit_cocone_is_colimit.

Equations
@[instance]

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