feat(ring_theory/noetherian): add two lemmas on products of prime ide…

…als (#5013)

Add two lemmas saying that in a noetherian ring (resp. _integral domain)_ every (_nonzero_) ideal contains a (_nonzero_) product of prime ideals.



Co-authored-by: faenuccio <65080144+faenuccio@users.noreply.github.com>

src/ring_theory/ideal/basic.lean

@@ -178,6 +178,13 @@ begin
   exact or.cases_on (hI.mem_or_mem H) id ih
 end
 
+lemma not_is_prime_iff {I : ideal α} : ¬ I.is_prime ↔ I = ⊤ ∨ ∃ (x ∉ I) (y ∉ I), x * y ∈ I :=
+begin
+  simp_rw [ideal.is_prime, not_and_distrib, ne.def, not_not, not_forall, not_or_distrib],
+  exact or_congr iff.rfl
+    ⟨λ ⟨x, y, hxy, hx, hy⟩, ⟨x, hx, y, hy, hxy⟩, λ ⟨x, hx, y, hy, hxy⟩, ⟨x, y, hxy, hx, hy⟩⟩
+end
+
 theorem zero_ne_one_of_proper {I : ideal α} (h : I ≠ ⊤) : (0:α) ≠ 1 :=
 λ hz, I.ne_top_iff_one.1 h $ hz ▸ I.zero_mem
 

src/ring_theory/noetherian.lean

@@ -3,9 +3,11 @@ Copyright (c) 2018 Mario Carneiro and Kevin Buzzard. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Kevin Buzzard
 -/
-import ring_theory.ideal.operations
+import algebraic_geometry.prime_spectrum
+import data.multiset.finset_ops
 import linear_algebra.linear_independent
 import order.order_iso_nat
+import ring_theory.ideal.operations
 
 /-!
 # Noetherian rings and modules
@@ -41,6 +43,7 @@ is proved in `ring_theory.polynomial`.
 ## References
 
 * [M. F. Atiyah and I. G. Macdonald, *Introduction to commutative algebra*][atiyah-macdonald]
+* [samuel]
 
 ## Tags
 
@@ -391,6 +394,12 @@ theorem set_has_maximal_iff_noetherian {R M} [ring R] [add_comm_group M] [module
   (∀ a : set $ submodule R M, a.nonempty → ∃ M' ∈ a, ∀ I ∈ a, M' ≤ I → I = M') ↔ is_noetherian R M :=
 by rw [is_noetherian_iff_well_founded, well_founded.well_founded_iff_has_max']
 
+/-- If `∀ I > J, P I` implies `P J`, then `P` holds for all submodules. -/
+lemma is_noetherian.induction {R M} [ring R] [add_comm_group M] [module R M] [is_noetherian R M]
+  {P : submodule R M → Prop} (hgt : ∀ I, (∀ J > I, P J) → P I)
+  (I : submodule R M) : P I :=
+well_founded.recursion (well_founded_submodule_gt R M) I hgt
+
 /--
 A ring is Noetherian if it is Noetherian as a module over itself,
 i.e. all its ideals are finitely generated.
@@ -508,3 +517,92 @@ nat.rec_on n
 (λ n ih, by simpa [pow_succ] using fg_mul _ _ h ih)
 
 end submodule
+
+section primes
+
+variables {R : Type*} [comm_ring R] [is_noetherian_ring R]
+
+/--In a noetherian ring, every ideal contains a product of prime ideals
+([samuel, § 3.3, Lemma 3])-/
+
+lemma exists_prime_spectrum_prod_le (I : ideal R) :
+  ∃ (Z : multiset (prime_spectrum R)), multiset.prod (Z.map (coe : subtype _ → ideal R)) ≤ I :=
+begin
+  refine is_noetherian.induction (λ (M : ideal R) hgt, _) I,
+  by_cases h_prM : M.is_prime,
+  { use {⟨M, h_prM⟩},
+    rw [multiset.map_singleton, multiset.singleton_eq_singleton, multiset.prod_singleton,
+        subtype.coe_mk],
+    exact le_rfl },
+  by_cases htop : M = ⊤,
+  { rw htop,
+    exact ⟨0, le_top⟩ },
+  have lt_add : ∀ z ∉ M, M < M + span R {z},
+  { intros z hz,
+    refine lt_of_le_of_ne le_sup_left (λ m_eq, hz _),
+    rw m_eq,
+    exact mem_sup_right (mem_span_singleton_self z) },
+  obtain ⟨x, hx, y, hy, hxy⟩ := (ideal.not_is_prime_iff.mp h_prM).resolve_left htop,
+  let Jx := M + span R {x},
+  let Jy := M + span R {y},
+  obtain ⟨Wx, h_Wx⟩ := hgt (M + span R {x}) (lt_add _ hx),
+  obtain ⟨Wy, h_Wy⟩ := hgt (M + span R {y}) (lt_add _ hy),
+  use Wx + Wy,
+  let W := Wx + Wy,
+  rw [multiset.map_add, multiset.prod_add],
+  apply le_trans (submodule.mul_le_mul h_Wx h_Wy),
+  rw add_mul,
+  apply sup_le (show M * (M + span R {y}) ≤ M, from ideal.mul_le_right),
+  rw mul_add,
+  apply sup_le (show span R {x} * M ≤ M, from ideal.mul_le_left),
+  rwa [span_mul_span, singleton_mul_singleton, span_singleton_le_iff_mem],
+end
+
+variables {A : Type*} [integral_domain A] [is_noetherian_ring A]
+
+/--In a noetherian integral domain which is not a field, every non-zero ideal contains a non-zero
+  product of prime ideals; in a field, the whole ring is a non-zero ideal containing only 0 as product
+  or prime ideals ([samuel, § 3.3, Lemma 3])
+-/
+
+lemma exists_prime_spectrum_prod_le_and_ne_bot_of_domain (h_fA : ¬ is_field A) {I : ideal A} (h_nzI: I ≠ ⊥) :
+  ∃ (Z : multiset (prime_spectrum A)), multiset.prod (Z.map (coe : subtype _ → ideal A)) ≤ I ∧
+    multiset.prod (Z.map (coe : subtype _ → ideal A)) ≠ ⊥ :=
+begin
+  revert h_nzI,
+  refine is_noetherian.induction (λ (M : ideal A) hgt, _) I,
+  intro h_nzM,
+  have hA_nont : nontrivial A,
+  apply is_integral_domain.to_nontrivial (integral_domain.to_is_integral_domain A),
+  by_cases h_topM : M = ⊤,
+  { rcases h_topM with rfl,
+    obtain ⟨p_id, h_nzp, h_pp⟩ : ∃ (p : ideal A), p ≠ ⊥ ∧ p.is_prime,
+    { apply ring.not_is_field_iff_exists_prime.mp h_fA },
+    use [({⟨p_id, h_pp⟩} : multiset (prime_spectrum A)), le_top],
+    rwa [multiset.map_singleton, multiset.singleton_eq_singleton, multiset.prod_singleton,
+         subtype.coe_mk] },
+  by_cases h_prM : M.is_prime,
+  { use ({⟨M, h_prM⟩} : multiset (prime_spectrum A)),
+    rw [multiset.map_singleton, multiset.singleton_eq_singleton, multiset.prod_singleton,
+         subtype.coe_mk],
+    exact ⟨le_rfl, h_nzM⟩ },
+  obtain ⟨x, hx, y, hy, h_xy⟩ := (ideal.not_is_prime_iff.mp h_prM).resolve_left h_topM,
+  have lt_add : ∀ z ∉ M, M < M + span A {z},
+  { intros z hz,
+    refine lt_of_le_of_ne le_sup_left (λ m_eq, hz _),
+    rw m_eq,
+    exact mem_sup_right (mem_span_singleton_self z) },
+  obtain ⟨Wx, h_Wx_le, h_Wx_ne⟩ := hgt (M + span A {x}) (lt_add _ hx) (ne_bot_of_gt (lt_add _ hx)),
+  obtain ⟨Wy, h_Wy_le, h_Wx_ne⟩ := hgt (M + span A {y}) (lt_add _ hy) (ne_bot_of_gt (lt_add _ hy)),
+  use Wx + Wy,
+  rw [multiset.map_add, multiset.prod_add],
+  refine ⟨le_trans (submodule.mul_le_mul h_Wx_le h_Wy_le) _, mt ideal.mul_eq_bot.mp _⟩,
+  { rw add_mul,
+    apply sup_le (show M * (M + span A {y}) ≤ M, from ideal.mul_le_right),
+    rw mul_add,
+    apply sup_le (show span A {x} * M ≤ M, from ideal.mul_le_left),
+    rwa [span_mul_span, singleton_mul_singleton, span_singleton_le_iff_mem] },
+  { rintro (hx | hy); contradiction },
+end
+
+end primes