English
For any specialization h: x ⤳ y in Spec(R), the stalk map toStalk at y composed with stalkSpecializes equals the stalk map at x, up to the structure of isomorphisms of stalks.
Русский
Для любой специализации h: x ⤳ y в Spec(R) композиция toStalk(y)∘stalkSpecializes = toStalk(x) с учётом изоморфизмов стэков.
LaTeX
$$$toStalk(R)\\, y \\;\\gg\\; (structureSheaf\\, R).presheaf.stalkSpecializes(h) = toStalk(R)\\, x$$$
Lean4
@[simp, reassoc, elementwise nosimp]
theorem toStalk_stalkSpecializes {R : Type*} [CommRing R] {x y : PrimeSpectrum R} (h : x ⤳ y) :
toStalk R y ≫ (structureSheaf R).presheaf.stalkSpecializes h = toStalk R x := by dsimp [toStalk];
simp [-toOpen_germ]