fromSpecStalk_closedPoint — Mathlib

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⟩]

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