Orthogonal refinement of a finite family of idempotents

In a commutative ring, idempotents e i are the clopen subsets D(e i) of the spectrum. Finitely many of them can be made disjoint without changing their union: order the index set and replace D(e i) by the part of it not covered by the earlier ones. Algebraically, this gives orthogonal idempotents f i with f i * e i = f i and ∑ i, f i = 1 - ∏ i, (1 - e i) (TauCeti.exists_orthogonalIdempotents_sum_eq_one_sub_prod). If the D(e i) cover the spectrum, that is, if ∏ i, (1 - e i) = 0, the refinement is a complete orthogonal family (TauCeti.exists_completeOrthogonalIdempotents_of_prod_one_sub_eq_zero).

The common refinement of the partitions {e i, 1 - e i} consists of the atoms ∏ i, (if σ i then e i else 1 - e i) of the Boolean algebra generated by the e i, one for each σ : ι → Bool. They form a complete orthogonal family (TauCeti.completeOrthogonalIdempotents_prod_ite) whose components are the loci where each D(e i) is either fully present or fully absent: a prime over the component R ⧸ (1 - ∏ i, ...) of an atom avoids e i exactly when the atom uses e i (TauCeti.notMem_iff_of_one_sub_prod_ite_mem).

theorem TauCeti.exists_orthogonalIdempotents_sum_eq_one_sub_prod {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] (e : ι → R) (he : ∀ (i : ι), IsIdempotentElem (e i)) : ∃ (f : ι → R), OrthogonalIdempotents f ∧ (∀ (i : ι), f i * e i = f i) ∧ ∑ i : ι, f i = 1 - ∏ i : ι, (1 - e i)

Finitely many idempotents e i of a commutative ring can be refined to orthogonal idempotents f i with f i * e i = f i and the same union of components, ∑ i, f i = 1 - ∏ i, (1 - e i).

theorem TauCeti.exists_completeOrthogonalIdempotents_of_prod_one_sub_eq_zero {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] (e : ι → R) (he : ∀ (i : ι), IsIdempotentElem (e i)) (hcover : ∏ i : ι, (1 - e i) = 0) : ∃ (f : ι → R), CompleteOrthogonalIdempotents f ∧ ∀ (i : ι), f i * e i = f i

Idempotents e i whose components cover the spectrum, ∏ i, (1 - e i) = 0, can be refined to a complete orthogonal family f i with f i * e i = f i.

theorem TauCeti.completeOrthogonalIdempotents_prod_ite {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {e : ι → R} (he : ∀ (i : ι), IsIdempotentElem (e i)) : CompleteOrthogonalIdempotents fun (σ : ι → Bool) => ∏ i : ι, if σ i = true then e i else 1 - e i

The atoms of the Boolean algebra generated by finitely many idempotents e i: for each choice σ i of e i or 1 - e i, the product ∏ i, (if σ i then e i else 1 - e i). They form a complete orthogonal family, the common refinement of the partitions {e i, 1 - e i}.

theorem TauCeti.ite_mul_prod_ite {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] {e : ι → R} (σ : ι → Bool) {x : ι} (hx : IsIdempotentElem (e x)) : ((if σ x = true then e x else 1 - e x) * ∏ y : ι, if σ y = true then e y else 1 - e y) = ∏ y : ι, if σ y = true then e y else 1 - e y

Each factor of an atom ∏ y, (if σ y then e y else 1 - e y) absorbs it.

theorem TauCeti.notMem_iff_of_one_sub_prod_ite_mem {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] {e : ι → R} (σ : ι → Bool) {p : Ideal R} [p.IsPrime] (hp : (1 - ∏ y : ι, if σ y = true then e y else 1 - e y) ∈ p) {x : ι} (hx : IsIdempotentElem (e x)) : e x ∉ p ↔ σ x = true

A prime ideal over the component R ⧸ (1 - ∏ y, ...) of an atom contains e x exactly when the atom uses 1 - e x.