isIdempotentElemEquivClopens — Mathlib

English

There is an order isomorphism between idempotent elements of R and clopen subsets of Spec(R).

Русский

Существует порядковое изоморфизм между идемпотентными элементами кольца и клозованными подмножествами спектра.

LaTeX

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

Lean4

/-- Clopen subsets in the prime spectrum of a commutative ring are in 1-1 correspondence
with idempotent elements in the ring. -/
@[stacks 00EE]
def isIdempotentElemEquivClopens : { e : R // IsIdempotentElem e } ≃o Clopens (PrimeSpectrum R) :=
  .trans .isIdempotentElemMulZeroAddOne mulZeroAddOneEquivClopens

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