Theorems · Theorem · commutative algebra

Ideal.iSup_iInf_eq_top_iff_pairwise

∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] {t : Finset ι},
  t.Nonempty → ∀ (I : ι → Ideal R), ⨆ i ∈ t, ⨅ j ∈ t, ⨅ (_ : j ≠ i), I j = ⊤ ↔ (↑t).Pairwise fun 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.

Defined in

Mathlib.RingTheory.Coprime.Ideal

Cited by

1 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiring