notMem_prime_iff_unit_in_stalk — Mathlib

English

For a LocallyRingedSpace X and r in Γ.obj(op X), r is not in the prime ideal associated to x under the unit if and only if r maps to a unit in the stalk O_{X,x}.

Русский

Для LocallyRingedSpace X и элемента r в Γ(X) не принадлежит соответствующему к x идеалу проживания единицы тогда и только тогда, когда образ этого элемента в локальном стержне O_{X,x} является единицей.

LaTeX

$$$r \notin (X.toΓSpecFun x).asIdeal \iff IsUnit\left(X.presheaf.Γgerm x\, r\right).$$$

Lean4

theorem notMem_prime_iff_unit_in_stalk (r : Γ.obj (op X)) (x : X) :
    r ∉ (X.toΓSpecFun x).asIdeal ↔ IsUnit (X.presheaf.Γgerm x r) := by simp [toΓSpecFun, IsLocalRing.closedPoint]

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