Commit 2020-09-26 10:16 e3cc06e0
View on Github →feat(algebraic_geometry/presheafed_space): gluing presheaves (#4198)
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.