English
For two affine open neighborhoods U and V of x in X, the morphisms hU.fromSpecStalk hxU and hV.fromSpecStalk hxV are equal. In other words, the canonical morphism from the stalk Spec 𝒪_{X,x} to X does not depend on the chosen affine neighborhood.
Русский
Для двух аффинных открытых окрестностей U и V точки x в X отображения hU.fromSpecStalk hxU и hV.fromSpecStalk hxV совпадают. То есть каноническое отображение из stalk Spec 𝒪_{X,x} в X не зависит от выбора аффинного окрестного множества.
LaTeX
$$$h_U.fromSpecStalk\; hx_U = h_V.fromSpecStalk\; hx_V$$$
Lean4
/-- A morphism from `Spec(O_x)` to `X`, which is defined with the help of an affine open
neighborhood `U` of `x`.
-/
noncomputable def fromSpecStalk {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) {x : X} (hxU : x ∈ U) :
Spec (X.presheaf.stalk x) ⟶ X :=
Spec.map (X.presheaf.germ _ x hxU) ≫ hU.fromSpec
