Stalks are functorial with respect to morphisms of presheaves over a fixed
The stalk of a presheaf
F at a point
x is calculated as the colimit of the functor
nbhds x ⥤ opens F.X ⥤ C
The germ of a section of a presheaf over an open at a point of that open.
- Top.presheaf.stalk_pushforward C f ℱ x = category_theory.limits.colim.map (category_theory.whisker_right (category_theory.nat_trans.op (topological_space.open_nhds.inclusion_map_iso f x).inv) ℱ) ≫ category_theory.limits.colimit.pre (((category_theory.whiskering_left (topological_space.open_nhds x)ᵒᵖ (topological_space.opens ↥X)ᵒᵖ C).obj (topological_space.open_nhds.inclusion x).op).obj ℱ) (topological_space.open_nhds.map f x).op