toStalk_stalkSpecializes — Mathlib

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]

Похожие утверждения