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
@[protected, instance]

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

Given a diagram of PresheafedSpace Cs, its colimit is computed by pushing the sheaves onto the colimit of the underlying spaces, and taking componentwise limit. This is the componentwise diagram for an open set U of the colimit of the underlying spaces.

Equations

The components of the colimit of a diagram of PresheafedSpace C is obtained via taking componentwise limits.

Equations