An additional lemma about coprime ideals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This lemma generalises exists_sum_eq_one_iff_pairwise_coprime to the case of non-principal ideals. It is on a separate file due to import requirements.

source

theorem ideal.supr_infi_eq_top_iff_pairwise {ι : Type u_1} {R : Type u_2} [comm_semiring R] {t : finset ι} (h : t.nonempty) (I : ι → ideal R) :

(⨆ (i : ι) (H : i ∈ t), ⨅ (j : ι) (hj : j ∈ t) (ij : j ≠ i), I j) = ⊤ ↔ ↑t.pairwise (λ (i j : ι), I i ⊔ I j = ⊤)

A finite family of ideals is pairwise coprime (that is, any two of them generate the whole ring) iff when taking all the possible intersections of all but one of these ideals, the resulting family of ideals still generate the whole ring.

For example with three ideals : I ⊔ J = I ⊔ K = J ⊔ K = ⊤ ↔ (I ⊓ J) ⊔ (I ⊓ K) ⊔ (J ⊓ K) = ⊤.

When ideals are all of the form I i = R ∙ s i, this is equivalent to the exists_sum_eq_one_iff_pairwise_coprime lemma.