English
Let R be a local ring. Then the map on schemes obtained by applying Spec to the inverse of stalkClosedPointIso R coincides with the canonical morphism from Spec R to the target via the closed point stalk construction.
Русский
Пусть R – локальное кольцо. Тогда отображение на схемах, получаемое применением Spec к обратной стороне изоморфизма stalkClosedPointIso R, совпадает с каноническим морфизмом из Spec R к целевому схеме через стоячий точечный конструированный открытый.
LaTeX
$$$ \\mathrm{Spec}.\\mathrm{map}\\big((\\mathrm{stalkClosedPointIso}\\;R)^{-1}\\big) = (\\mathrm{Spec}\\;R).\\mathrm{fromSpecStalk}(\\mathrm{closedPoint}\\;R) $$$
Lean4
theorem Spec_stalkClosedPointIso : Spec.map (stalkClosedPointIso R).inv = (Spec R).fromSpecStalk (closedPoint R) := by
rw [stalkClosedPointIso_inv, Scheme.Spec_fromSpecStalk']
