Commit 2020-09-26 10:16 e3cc06e0View on Github →
feat(algebraic_geometry/presheafed_space): gluing presheaves (#4198)
PresheafedSpace C has colimits.
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,
colimit (F ⋙ PresheafedSpace.forget C). Call that colimit space
Our strategy is to push each of the presheaves
forward along the continuous map
colimit.ι (F ⋙ PresheafedSpace.forget C) j to
Since pushforward is functorial, we obtain a diagram
J ⥤ (presheaf C X)ᵒᵖ
of presheaves on a single space
(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.