English
The range of the base map of X.fromSpecStalk x equals the set of points y specializing to x. This identifies the image of the stalk map with the specialization relation.
Русский
Область базового отображения X.fromSpecStalk x совпадает с множеством точек y, удовлетворяющих y ⤳ x.
LaTeX
$$Set.range (X.fromSpecStalk x).base = {y | y \;\mathrel{\rhd}\; x}$$
Lean4
theorem fromSpecStalk_closedPoint {U : Opens X} (hU : IsAffineOpen U) {x : X} (hxU : x ∈ U) :
(hU.fromSpecStalk hxU).base (closedPoint (X.presheaf.stalk x)) = x :=
by
rw [IsAffineOpen.fromSpecStalk, Scheme.comp_base_apply]
rw [← hU.primeIdealOf_eq_map_closedPoint ⟨x, hxU⟩, hU.fromSpec_primeIdealOf ⟨x, hxU⟩]