English
For a given affine open U of X and a point x ∈ U, the localization of the ring of sections Γ(X,U) at the corresponding prime ideal is realized in the stalk at x.
Русский
Для данного аффинного открытого U схемы X и точки x ∈ U локализация кольца секций Γ(X,U) по соответствующемуprime-идеалу реализуется в stalk в точке x.
LaTeX
$$$IsLocalization.AtPrime (X.presheaf.stalk x) (h_U.primeIdealOf x).asIdeal$$$
Lean4
theorem isLocalization_stalk (x : U) : IsLocalization.AtPrime (X.presheaf.stalk x) (hU.primeIdealOf x).asIdeal :=
by
rcases x with ⟨x, hx⟩
set y := hU.primeIdealOf ⟨x, hx⟩ with hy
have : hU.fromSpec.base y = x := hy ▸ hU.fromSpec_primeIdealOf ⟨x, hx⟩
clear_value y
subst this
exact hU.isLocalization_stalk' y hx