THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file proves additional properties of the prime spectrum a ring is Noetherian.
theorem
prime_spectrum.exists_prime_spectrum_prod_le
(R : Type u)
[comm_ring R]
[is_noetherian_ring R]
(I : ideal R) :
∃ (Z : multiset (prime_spectrum R)), (multiset.map prime_spectrum.as_ideal Z).prod ≤ I
In a noetherian ring, every ideal contains a product of prime ideals ([samuel, § 3.3, Lemma 3])
theorem
prime_spectrum.exists_prime_spectrum_prod_le_and_ne_bot_of_domain
{A : Type u}
[comm_ring A]
[is_domain A]
[is_noetherian_ring A]
(h_fA : ¬is_field A)
{I : ideal A}
(h_nzI : I ≠ ⊥) :
∃ (Z : multiset (prime_spectrum A)), (multiset.map prime_spectrum.as_ideal Z).prod ≤ I ∧ (multiset.map prime_spectrum.as_ideal Z).prod ≠ ⊥
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])
@[protected, instance]