[Merged by Bors] - feat(ring_theory/ideal/operations.lean): lemmas about coprime ideals

src/linear_algebra/dfinsupp.lean

@@ -291,6 +291,30 @@ lemma mem_bsupr_iff_exists_dfinsupp (p : ι → Prop) [decidable_pred p] (S : ι
     ∃ f : Π₀ i, S i, dfinsupp.lsum ℕ (λ i, (S i).subtype) (f.filter p) = x :=
 set_like.ext_iff.mp (bsupr_eq_range_dfinsupp_lsum p S) x
 
+open_locale big_operators
+omit dec_ι
+lemma mem_supr_finset_iff_exists_sum {s : finset ι} (p : ι → submodule R N) (a : N) :
+  a ∈ (⨆ i ∈ s, p i) ↔ ∃ μ : Π i, p i, ∑ i in s, (μ i : N) = a :=
+begin
+  classical,
+  rw submodule.mem_supr_iff_exists_dfinsupp',
+  split; rintro ⟨μ, hμ⟩,
+  { use λ i, ⟨μ i, (supr_const_le : _ ≤ p i) (coe_mem $ μ i)⟩,
+    rw ← hμ, symmetry, apply finset.sum_subset,
+    { intro x, contrapose, intro hx,
+      rw [mem_support_iff, not_ne_iff],
+      ext, rw [coe_zero, ← mem_bot R], convert coe_mem (μ x),
+      symmetry, exact supr_neg hx },
+    { intros x _ hx, rw [mem_support_iff, not_ne_iff] at hx, rw hx, refl } },
+  { refine ⟨dfinsupp.mk s _, _⟩,
+    { rintro ⟨i, hi⟩, refine ⟨μ i, _⟩,
+      rw supr_pos, { exact coe_mem _ }, { exact hi } },
+    simp only [dfinsupp.sum],
+    rw [finset.sum_subset support_mk_subset, ← hμ],
+    exact finset.sum_congr rfl (λ x hx, congr_arg coe $ mk_of_mem hx),
+    { intros x _ hx, rw [mem_support_iff, not_ne_iff] at hx, rw hx, refl } }
+end
+
 end submodule
 
 namespace complete_lattice

src/ring_theory/coprime/ideal.lean

@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2022 Pierre-Alexandre Bazin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Pierre-Alexandre Bazin
+-/
+import linear_algebra.dfinsupp
+import ring_theory.ideal.operations
+
+/-!
+# An additional lemma about coprime ideals
+
+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.
+-/
+
+namespace ideal
+variables {ι R : Type*} [comm_semiring R]
+
+/--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.-/
+lemma supr_infi_eq_top_iff_pairwise {t : finset ι} (h : t.nonempty) (I : ι → ideal R) :
+  (⨆ i ∈ t, ⨅ j (hj : j ∈ t) (ij : j ≠ i), I j) = ⊤ ↔
+    (t : set ι).pairwise (λ i j, I i ⊔ I j = ⊤) :=
+begin
+  haveI : decidable_eq ι := classical.dec_eq ι,
+  rw [eq_top_iff_one, submodule.mem_supr_finset_iff_exists_sum],
+  refine h.cons_induction _ _; clear' t h,
+  { simp only [finset.sum_singleton, finset.coe_singleton, set.pairwise_singleton, iff_true],
+    refine λ a, ⟨λ i, if h : i = a then ⟨1, _⟩ else 0, _⟩,
+    { rw h, simp only [finset.mem_singleton, ne.def, infi_infi_eq_left, eq_self_iff_true,
+        not_true, infi_false]},
+    { simp only [dif_pos, dif_ctx_congr, submodule.coe_mk, eq_self_iff_true] } },
+  intros a t hat h ih,
+  rw [finset.coe_cons,
+    set.pairwise_insert_of_symmetric (λ i j (h : I i ⊔ I j = ⊤), sup_comm.trans h)],
+  split,
+  { rintro ⟨μ, hμ⟩, rw finset.sum_cons at hμ,
+    refine ⟨ih.mp ⟨pi.single h.some ⟨μ a, _⟩ + λ i, ⟨μ i, _⟩, _⟩, λ b hb ab, _⟩,
+    { have := submodule.coe_mem (μ a), rw mem_infi at this ⊢,
+      --for some reason `simp only [mem_infi]` times out
+      intro i, specialize this i, rw [mem_infi, mem_infi] at this ⊢,
+      intros hi _, apply this (finset.subset_cons _ hi),
+      rintro rfl, exact hat hi },
+    { have := submodule.coe_mem (μ i), simp only [mem_infi] at this ⊢,
+      intros j hj ij, exact this _ (finset.subset_cons _ hj) ij },
+    { rw [← @if_pos _ _ h.some_spec R (μ a) 0, ← finset.sum_pi_single',
+        ← finset.sum_add_distrib] at hμ,
+      convert hμ, ext i, rw [pi.add_apply, submodule.coe_add, submodule.coe_mk],
+      by_cases hi : i = h.some,
+      { rw [hi, pi.single_eq_same, pi.single_eq_same, submodule.coe_mk] },
+      { rw [pi.single_eq_of_ne hi, pi.single_eq_of_ne hi, submodule.coe_zero] } },
+    { rw [eq_top_iff_one, submodule.mem_sup],
+      rw add_comm at hμ, refine ⟨_, _, _, _, hμ⟩,
+      { refine sum_mem _ (λ x hx, _),
+        have := submodule.coe_mem (μ x), simp only [mem_infi] at this,
+        apply this _ (finset.mem_cons_self _ _), rintro rfl, exact hat hx },
+      { have := submodule.coe_mem (μ a), simp only [mem_infi] at this,
+        exact this _ (finset.subset_cons _ hb) ab.symm } } },
+  { rintro ⟨hs, Hb⟩, obtain ⟨μ, hμ⟩ := ih.mpr hs,
+    obtain ⟨u, hu, v, hv, huv⟩ := submodule.mem_sup.mp
+      ((eq_top_iff_one _).mp $ sup_infi_eq_top $ λ b hb, Hb b hb $ by { rintro rfl, exact hat hb }),
+    refine ⟨λ i, if hi : i = a then ⟨v, _⟩ else ⟨u * μ i, _⟩, _⟩,
+    { simp only [mem_infi] at hv ⊢,
+      intros j hj ij, rw [finset.mem_cons, ← hi] at hj,
+      exact hv _ (hj.resolve_left ij) },
+    { have := submodule.coe_mem (μ i), simp only [mem_infi] at this ⊢,
+      intros j hj ij,
+      rcases finset.mem_cons.mp hj with rfl | hj,
+      { exact mul_mem_right _ _ hu },
+      { exact mul_mem_left _ _ (this _ hj ij) } },
+    { rw [finset.sum_cons, dif_pos rfl, add_comm],
+      rw ← mul_one u at huv, rw [← huv, ← hμ, finset.mul_sum],
+      congr' 1, apply finset.sum_congr rfl, intros j hj,
+      rw dif_neg, refl,
+      rintro rfl, exact hat hj } }
+end
+
+end ideal

src/ring_theory/ideal/operations.lean

@@ -441,6 +441,51 @@ let ⟨s, hsi, t, htj, hst⟩ := submodule.mem_sup.1 ((eq_top_iff_one _).1 h) in
 mul_one r ▸ hst ▸ (mul_add r s t).symm ▸ ideal.add_mem (I * J) (mul_mem_mul_rev hsi hrj)
   (mul_mem_mul hri htj)
 
+lemma sup_mul_eq_of_coprime_left (h : I ⊔ J = ⊤) : I ⊔ (J * K) = I ⊔ K :=
+le_antisymm (sup_le_sup_left mul_le_left _) $ λ i hi,
+begin
+  rw eq_top_iff_one at h, rw submodule.mem_sup at h hi ⊢,
+  obtain ⟨i1, hi1, j, hj, h⟩ := h, obtain ⟨i', hi', k, hk, hi⟩ := hi,
+  refine ⟨_, add_mem hi' (mul_mem_right k _ hi1), _, mul_mem_mul hj hk, _⟩,
+  rw [add_assoc, ← add_mul, h, one_mul, hi]
+end
+
+lemma sup_mul_eq_of_coprime_right (h : I ⊔ K = ⊤) : I ⊔ (J * K) = I ⊔ J :=
+by { rw mul_comm, exact sup_mul_eq_of_coprime_left h }
+
+lemma mul_sup_eq_of_coprime_left (h : I ⊔ J = ⊤) : (I * K) ⊔ J = K ⊔ J :=
+by { rw sup_comm at h, rw [sup_comm, sup_mul_eq_of_coprime_left h, sup_comm] }
+
+lemma mul_sup_eq_of_coprime_right (h : K ⊔ J = ⊤) : (I * K) ⊔ J = I ⊔ J :=
+by { rw sup_comm at h, rw [sup_comm, sup_mul_eq_of_coprime_right h, sup_comm] }
+
+lemma sup_prod_eq_top {s : finset ι} {J : ι → ideal R} (h : ∀ i, i ∈ s → I ⊔ J i = ⊤) :
+  I ⊔ ∏ i in s, J i = ⊤ :=
+finset.prod_induction _ (λ J, I ⊔ J = ⊤) (λ J K hJ hK, (sup_mul_eq_of_coprime_left hJ).trans hK)
+(by rw [one_eq_top, sup_top_eq]) h
+
+lemma sup_infi_eq_top {s : finset ι} {J : ι → ideal R} (h : ∀ i, i ∈ s → I ⊔ J i = ⊤) :
+  I ⊔ (⨅ i ∈ s, J i) = ⊤ :=
+eq_top_iff.mpr $ le_of_eq_of_le (sup_prod_eq_top h).symm $ sup_le_sup_left
+  (le_of_le_of_eq prod_le_inf $ finset.inf_eq_infi _ _) _
+
+lemma prod_sup_eq_top {s : finset ι} {J : ι → ideal R} (h : ∀ i, i ∈ s → J i ⊔ I = ⊤) :
+  (∏ i in s, J i) ⊔ I = ⊤ :=
+sup_comm.trans (sup_prod_eq_top $ λ i hi, sup_comm.trans $ h i hi)
+
+lemma infi_sup_eq_top {s : finset ι} {J : ι → ideal R} (h : ∀ i, i ∈ s → J i ⊔ I = ⊤) :
+  (⨅ i ∈ s, J i) ⊔ I = ⊤ :=
+sup_comm.trans (sup_infi_eq_top $ λ i hi, sup_comm.trans $ h i hi)
+
+lemma sup_pow_eq_top {n : ℕ} (h : I ⊔ J = ⊤) : I ⊔ (J ^ n) = ⊤ :=
+by { rw [← finset.card_range n, ← finset.prod_const], exact sup_prod_eq_top (λ _ _, h) }
+
+lemma pow_sup_eq_top {n : ℕ} (h : I ⊔ J = ⊤) : (I ^ n) ⊔ J = ⊤ :=
+by { rw [← finset.card_range n, ← finset.prod_const], exact prod_sup_eq_top (λ _ _, h) }
+
+lemma pow_sup_pow_eq_top {m n : ℕ} (h : I ⊔ J = ⊤) : (I ^ m) ⊔ (J ^ n) = ⊤ :=
+sup_pow_eq_top (pow_sup_eq_top h)
+
 variables (I)
 @[simp] theorem mul_bot : I * ⊥ = ⊥ :=
 submodule.smul_bot I