English
If A is a Noetherian domain that is not a field, then for every nonzero ideal I there exists a multiset Z of PrimeSpectrum(A) such that the product of the corresponding asIdeals ≤ I and this product is nonzero.
Русский
Если A — Нётерово доменное кольцо, не являющееся полем, то для любого ненулевого идеала I существует мультисет Z из PrimeSpectrum(A), такое что произведение соответствующих asIdeal ≤ I и это произведение не равно нулю.
LaTeX
$$$\\text{Not Field } A \\;\\Rightarrow\\; \\forall I \\neq \\bot, \\exists Z : Multiset(PrimeSpectrum A), \\prod(Z.map asIdeal) \\le I \\land \\prod(Z.map asIdeal) \\neq \\bot.$$$
Lean4
/-- 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 ([samuel1967, § 3.3, Lemma 3]) -/
theorem exists_primeSpectrum_prod_le_and_ne_bot_of_domain (h_fA : ¬IsField A) {I : Ideal A} (h_nzI : I ≠ ⊥) :
∃ Z : Multiset (PrimeSpectrum A), Multiset.prod (Z.map asIdeal) ≤ I ∧ Multiset.prod (Z.map asIdeal) ≠ ⊥ := by
induction I using IsNoetherian.induction with
| hgt M hgt =>
change Ideal A at M
have hA_nont : Nontrivial A := IsDomain.toNontrivial
by_cases h_topM : M = ⊤
· rcases h_topM with rfl
obtain ⟨p_id, h_nzp, h_pp⟩ : ∃ p : Ideal A, p ≠ ⊥ ∧ p.IsPrime := by
apply Ring.not_isField_iff_exists_prime.mp h_fA
use ({⟨p_id, h_pp⟩} : Multiset (PrimeSpectrum A)), le_top
rwa [Multiset.map_singleton, Multiset.prod_singleton]
by_cases h_prM : M.IsPrime
· use ({⟨M, h_prM⟩} : Multiset (PrimeSpectrum A))
rw [Multiset.map_singleton, Multiset.prod_singleton]
exact ⟨le_rfl, h_nzI⟩
obtain ⟨x, hx, y, hy, h_xy⟩ := (Ideal.not_isPrime_iff.mp h_prM).resolve_left h_topM
have lt_add : ∀ z ∉ M, M < M + span A { z } := by
intro z hz
refine lt_of_le_of_ne le_sup_left fun 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 (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, Set.singleton_mul_singleton, span_singleton_le_iff_mem]
· rintro (hx | hy) <;> contradiction
