English
For a morphism α: X ⟶ Y of PresheafedSpaces and a germ in the target at a point, the germ composed with the stalk map equals the composition of the target germ with α’s presheaf map; this is a naturality relation of stalk maps with respect to α.
Русский
Для морфизма α: X ⟶ Y между PresheafedSpace стебель/ stalk-map натурализуется так, что germs и stalkMap взаимодействуют натуративно: germ в Y после α сопоставляется с germ в X через α.c.
LaTeX
$$$Y.presheaf.germ(U, αx, hx) \;\circ\; α.stalkMap x = α.c.app(op U) \circ X.presheaf.germ((Opens.map α.base).obj U) x hx$$$
Lean4
@[elementwise, reassoc]
theorem stalkMap_germ {X Y : PresheafedSpace.{_, _, v} C} (α : X ⟶ Y) (U : Opens Y) (x : X) (hx : α x ∈ U) :
Y.presheaf.germ U (α x) hx ≫ α.stalkMap x = α.c.app (op U) ≫ X.presheaf.germ ((Opens.map α.base).obj U) x hx := by
rw [Hom.stalkMap, stalkFunctor_map_germ_assoc, stalkPushforward_germ]
