isLocalization_stalk — Mathlib

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

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