Documentation

Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian

This file proves additional properties of the prime spectrum a ring is Noetherian.

theorem PrimeSpectrum.exists_primeSpectrum_prod_le (R : Type u) [CommRing R] [IsNoetherianRing R] (I : Ideal R) :
∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map PrimeSpectrum.asIdeal Z).prod I

In a noetherian ring, every ideal contains a product of prime ideals ([samuel, § 3.3, Lemma 3])

theorem PrimeSpectrum.exists_primeSpectrum_prod_le_and_ne_bot_of_domain {A : Type u} [CommRing A] [IsDomain A] [IsNoetherianRing A] (h_fA : ¬IsField A) {I : Ideal A} (h_nzI : I ) :
∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map PrimeSpectrum.asIdeal Z).prod I (Multiset.map PrimeSpectrum.asIdeal 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])