isClopen_iff — Mathlib

English

Clopen subsets of Spec(R) are in bijection with idempotent elements of R via a natural isomorphism.

Русский

Клозованные подмножества спектра равны идемпотентным элементам кольца через естественную изоморфизм.

LaTeX

$$isIdempotentElemEquivClopens : { e : R // IsIdempotentElem e } ≃o Clopens (PrimeSpectrum R)$$

Lean4

theorem isClopen_iff {s : Set (PrimeSpectrum R)} : IsClopen s ↔ ∃ e : R, IsIdempotentElem e ∧ s = basicOpen e :=
  by
  refine ⟨exists_idempotent_basicOpen_eq_of_isClopen, ?_⟩
  rintro ⟨e, he, rfl⟩
  refine ⟨?_, (basicOpen e).2⟩
  rw [PrimeSpectrum.basicOpen_eq_zeroLocus_of_isIdempotentElem e he]
  exact isClosed_zeroLocus _

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