feat(ring_theory/ideal/operations) : add lemma prod_eq_bot (#5795)

Add lemma `prod_eq_bot` showing that a product of ideals in an integral domain is zero if and only if one of the terms
is zero.



Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Filippo A. E. Nuccio <65080144+faenuccio@users.noreply.github.com>
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

src/ring_theory/ideal/basic.lean

@@ -255,6 +255,12 @@ let ⟨m, hm⟩ := (eq_top_or_exists_le_coatom I).resolve_left hI in ⟨m, ⟨
 theorem exists_maximal [nontrivial α] : ∃ M : ideal α, M.is_maximal :=
 let ⟨I, ⟨hI, _⟩⟩ := exists_le_maximal (⊥ : ideal α) submodule.bot_ne_top in ⟨I, hI⟩
 
+instance [nontrivial α] : nontrivial (ideal α) :=
+begin
+  rcases @exists_maximal α _ _ with ⟨M, hM, _⟩,
+  exact nontrivial_of_ne M ⊤ hM
+end
+
 /-- If P is not properly contained in any maximal ideal then it is not properly contained
   in any proper ideal -/
 lemma maximal_of_no_maximal {R : Type u} [comm_semiring R] {P : ideal R}

src/ring_theory/ideal/operations.lean

@@ -3,11 +3,12 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
-import data.nat.choose.sum
-import data.equiv.ring
 import algebra.algebra.operations
-import ring_theory.ideal.basic
 import algebra.algebra.tower
+import data.equiv.ring
+import data.nat.choose.sum
+import ring_theory.ideal.basic
+import ring_theory.non_zero_divisors
 /-!
 # More operations on modules and ideals
 -/
@@ -258,6 +259,11 @@ variables {I J K L: ideal R}
 
 instance : has_mul (ideal R) := ⟨(•)⟩
 
+@[simp] lemma add_eq_sup : I + J = I ⊔ J := rfl
+@[simp] lemma zero_eq_bot : (0 : ideal R) = ⊥ := rfl
+@[simp] lemma one_eq_top : (1 : ideal R) = ⊤ :=
+by erw [submodule.one_eq_map_top, submodule.map_id]
+
 theorem mul_mem_mul {r s} (hr : r ∈ I) (hs : s ∈ J) : r * s ∈ I * J :=
 submodule.smul_mem_smul hr hs
 
@@ -367,6 +373,14 @@ lemma mul_eq_bot {R : Type*} [integral_domain R] {I J : ideal R} :
     or.resolve_left (mul_eq_zero.mp ((I * J).eq_bot_iff.mp hij _ (mul_mem_mul hi hj))) ne0)),
  λ h, by cases h; rw [← ideal.mul_bot, h, ideal.mul_comm]⟩
 
+instance {R : Type*} [integral_domain R] : no_zero_divisors (ideal R) :=
+{ eq_zero_or_eq_zero_of_mul_eq_zero := λ I J, mul_eq_bot.1 }
+
+/-- A product of ideals in an integral domain is zero if and only if one of the terms is zero. -/
+lemma prod_eq_bot {R : Type*} [integral_domain R]
+  {s : multiset (ideal R)} : s.prod = ⊥ ↔ ∃ I ∈ s, I = ⊥ :=
+prod_zero_iff_exists_zero
+
 /-- The radical of an ideal `I` consists of the elements `r` such that `r^n ∈ I` for some `n`. -/
 def radical (I : ideal R) : ideal R :=
 { carrier := { r | ∃ n : ℕ, r ^ n ∈ I },
@@ -450,11 +464,6 @@ eq_bot_iff.2 (λ x hx, hx.rec_on (λ n hn, pow_eq_zero hn))
 
 instance : comm_semiring (ideal R) := submodule.comm_semiring
 
-@[simp] lemma add_eq_sup : I + J = I ⊔ J := rfl
-@[simp] lemma zero_eq_bot : (0 : ideal R) = ⊥ := rfl
-@[simp] lemma one_eq_top : (1 : ideal R) = ⊤ :=
-by erw [submodule.one_eq_map_top, submodule.map_id]
-
 variables (R)
 theorem top_pow (n : ℕ) : (⊤ ^ n : ideal R) = ⊤ :=
 nat.rec_on n one_eq_top $ λ n ih, by rw [pow_succ, ih, top_mul]

src/ring_theory/non_zero_divisors.lean

@@ -73,4 +73,24 @@ lemma map_le_non_zero_divisors_of_injective {B : Type*} [integral_domain B]
 le_non_zero_divisors_of_domain (λ h, let ⟨x, hx, hx0⟩ := h in
   zero_ne_one (hM (hf (trans hx0 (f.map_zero.symm)) ▸ hx : 0 ∈ M) 1 (mul_zero 1)).symm)
 
+lemma prod_zero_iff_exists_zero {R : Type*} [comm_semiring R] [no_zero_divisors R] [nontrivial R]
+  {s : multiset R} : s.prod = 0 ↔ ∃ (r : R) (hr : r ∈ s), r = 0 :=
+begin
+  split, swap,
+  { rintros ⟨r, hrs, rfl⟩,
+    exact multiset.prod_eq_zero hrs, },   
+  refine multiset.induction _ (λ a s ih, _) s,
+  { intro habs,
+    simpa using habs, },
+  { rw multiset.prod_cons,
+    intro hprod,
+    replace hprod := eq_zero_or_eq_zero_of_mul_eq_zero hprod,
+    cases hprod with ha,
+    { exact ⟨a, multiset.mem_cons_self a s, ha⟩ },
+    { apply (ih hprod).imp _,
+      rintros b ⟨hb₁, hb₂⟩,
+      exact ⟨multiset.mem_cons_of_mem hb₁, hb₂⟩, }, },
+end
+
+
 end non_zero_divisors