English
In a Noetherian ring, every nonzero ideal I contains a product of prime ideals; i.e., there exists a multiset Z of prime spectrum elements such that the product of the corresponding asIdeals is ≤ I, and this product is nonzero.
Русский
В кольце Нётерова типа любой непустой идеал I содержит произведение простых идеалов; существует мультисет Z из элементов спектра простых идеалов, такое что произведение соответствующих asIdeal ≤ I и не равно нулю.
LaTeX
$$$\\exists Z : \\mathrm{Multiset}(\\mathrm{PrimeSpectrum}(R)),\\ \\prod (Z.map \\mathrm{asIdeal}) \\le I \\ \\land\\ \\prod (Z.map \\mathrm{asIdeal}) \\neq \\bot.$$$
Lean4
/-- In a Noetherian ring, every ideal contains a product of prime ideals
([samuel1967, § 3.3, Lemma 3]). -/
theorem exists_primeSpectrum_prod_le (I : Ideal R) :
∃ Z : Multiset (PrimeSpectrum R), Multiset.prod (Z.map asIdeal) ≤ I := by
induction I using IsNoetherian.induction with
| hgt M hgt =>
change Ideal R at M
by_cases h_prM : M.IsPrime
· use {⟨M, h_prM⟩}
rw [Multiset.map_singleton, Multiset.prod_singleton]
by_cases htop : M = ⊤
· rw [htop]
exact ⟨0, le_top⟩
have lt_add : ∀ z ∉ M, M < M + span R { z } := by
intro z hz
refine lt_of_le_of_ne le_sup_left fun m_eq => hz ?_
rw [m_eq]
exact Ideal.mem_sup_right (mem_span_singleton_self z)
obtain ⟨x, hx, y, hy, hxy⟩ := (Ideal.not_isPrime_iff.mp h_prM).resolve_left htop
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
rw [Multiset.map_add, Multiset.prod_add]
apply le_trans (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, Set.singleton_mul_singleton, span_singleton_le_iff_mem]
