Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes