isUnit_toStalk — Mathlib

English

An element f in the stalk at x is a unit if and only if its image in the localization at x is a unit.

Русский

Элемент в локальном кольце локального стекла x является единицей тогда и только тогда, когда его образ в локализации в x — единица.

LaTeX

$$$ IsUnit(toStalk\\_R x (f:R)) \\iff IsUnit( toStalk R x f ) $$$

Lean4

theorem isUnit_toStalk (x : PrimeSpectrum.Top R) (f : x.asIdeal.primeCompl) : IsUnit (toStalk R x (f : R)) :=
  by
  rw [← germ_toOpen R (PrimeSpectrum.basicOpen (f : R)) x f.2 (f : R)]
  exact RingHom.isUnit_map _ (isUnit_to_basicOpen_self R f)

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