Presheafed spaces #
Introduces the category of topological spaces equipped with a presheaf (taking values in an
arbitrary target category
We further describe how to apply functors and natural transformations to the values of the presheaves.
- base : ↑X ⟶ ↑Y
A morphism between presheafed spaces
Y consists of a continuous map
f between the underlying topological spaces, and a (notice contravariant!) map
from the presheaf on
Y to the pushforward of the presheaf on
Composition of morphisms of
The category of PresheafedSpaces. Morphisms are pairs, a continuous map and a presheaf map from the presheaf on the target to the pushforward of the presheaf on the source.
Sometimes rewriting with
comp_c_app doesn't work because of dependent type issues.
In that case,
erw comp_c_app_assoc might make progress.
comp_c_app_assoc is also better suited for rewrites in the opposite direction.
An isomorphism of
PresheafedSpaces is a homeomorphism of the underlying space, and a
natural transformation between the sheaves.
PresheafedSpaces have naturally isomorphic presheaves.
This could be used in conjunction with
The restriction of a presheafed space along an open embedding into the space.
The map from the restriction of a presheafed space.
The map to the restriction of a presheafed space along the canonical inclusion from the top subspace.
The isomorphism from the restriction to the top subspace.
A natural transformation induces a natural transformation between the