isIdempotentElemEquivClopens_symm_inf

English

Let R be a commutative ring and consider the canonical correspondence between clopen subsets of Spec(R) and idempotent elements of R. Then the idempotent corresponding to the intersection of two clopen sets equals the product of the idempotents corresponding to each set.

Русский

Пусть R — коммутативное кольцо. Пусть между замкнутыми и открытыми подмножествами Spec(R) существует каноничное соответствие с идемпотентами кольца. Тогда идемпотент, соответствующий пересечению двух клозопадных множеств, равен произведению идемпотентов, соответствующих каждого множества.

LaTeX

$$$e(s_1 \cap s_2) = e(s_1) \cdot e(s_2)$$$

Lean4

theorem isIdempotentElemEquivClopens_symm_inf (s₁ s₂) :
    letI e := isIdempotentElemEquivClopens (R := R).symm
    e (s₁ ⊓ s₂) = ⟨_, (e s₁).2.mul (e s₂).2⟩ :=
  map_inf ..

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