Stalks for presheaved spaces #
This file lifts constructions of stalks and pushforwards of stalks to work with the category of presheafed spaces. Additionally, we prove that restriction of presheafed spaces does not change the stalks.
The stalk at
x of a
A morphism of presheafed spaces induces a morphism of stalks.
- algebraic_geometry.PresheafedSpace.stalk_map α x = (Top.presheaf.stalk_functor C (⇑(α.base) x)).map α.c ≫ Top.presheaf.stalk_pushforward C α.base X.presheaf x
For an open embedding
f : U ⟶ X and a point
x : U, we get an isomorphism between the stalk
f x and the stalk of the restriction of
f at t
- X.restrict_stalk_iso h x = category_theory.functor.final.colimit_iso (_.functor_nhds x).op ((topological_space.open_nhds.inclusion (⇑f x)).op ⋙ X.presheaf)
α = β and
x = x', we would like to say that
stalk_map α x = stalk_map β x'.
Unfortunately, this equality is not well-formed, as their types are not definitionally the same.
To get a proper congruence lemma, we therefore have to introduce these
eq_to_hom arrows on
either side of the equality.
An isomorphism between presheafed spaces induces an isomorphism of stalks.