Sheafed spaces #
Introduces the category of topological spaces equipped with a sheaf (taking values in an
arbitrary target category
We further describe how to apply functors and natural transformations to the values of the presheaves.
- carrier : TopCat
- presheaf : TopCat.Presheaf C ↑s.toPresheafedSpace
- IsSheaf : TopCat.Presheaf.IsSheaf s.presheaf
A sheafed space is presheafed space which happens to be sheaf.
SheafedSpace C is a topological space equipped with a sheaf of
Forgetting the sheaf condition is a functor from
SheafedSpace C to
The restriction of a sheafed space along an open embedding into the space.
The restriction of a sheafed space
X to the top subspace is isomorphic to