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.prod (Multiset.map PrimeSpectrum.asIdeal Z) ≤ 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.prod (Multiset.map PrimeSpectrum.asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map PrimeSpectrum.asIdeal Z) ≠ ⊥

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])

instance PrimeSpectrum.instNoetherianSpacePrimeSpectrumToCommSemiringZariskiTopology (R : Type u) [CommRing R] [IsNoetherianRing R] : TopologicalSpace.NoetherianSpace (PrimeSpectrum R)

Equations

• (_ : TopologicalSpace.NoetherianSpace (PrimeSpectrum R)) = (_ : TopologicalSpace.NoetherianSpace (PrimeSpectrum R))

theorem minimalPrimes.finite_of_isNoetherianRing (R : Type u) [CommRing R] [IsNoetherianRing R] : Set.Finite (minimalPrimes R)