theorem NoetherianTopological.primeSpectrum_noetherianSpace (R : Type u) [CommSemiring R] [IsNoetherianRing R] : TopologicalSpace.NoetherianSpace (PrimeSpectrum R)

The prime spectrum of a Noetherian ring is a Noetherian topological space: every descending chain of closed subsets stabilises (Corollary 3, Lecture 2).

theorem NoetherianTopological.noetherian_finite_minimalPrimes (R : Type u) [CommSemiring R] [IsNoetherianRing R] : (minimalPrimes R).Finite

A Noetherian ring has only finitely many minimal primes; this is the algebraic counterpart of the finite decomposition into irreducible components (Proposition 5).

theorem NoetherianTopological.sInf_minimalPrimes_eq_nilradical (R : Type u_1) [CommSemiring R] : sInf (minimalPrimes R) = nilradical R

The intersection of all minimal primes of a commutative semiring equals the nilradical.

theorem NoetherianTopological.reduced_sInf_minimalPrimes (R : Type u_1) [CommSemiring R] [IsReduced R] : sInf (minimalPrimes R) = ⊥

For a reduced ring, the intersection of all minimal primes is the zero ideal.

def NoetherianTopological.IsCatenary (α : Type u_1) [Preorder α] : Prop

A preorder is catenary if any two saturated chains with the same endpoints have the same length.

def NoetherianTopological.IsRingCatenary (R : Type u_1) [CommRing R] : Prop

A commutative ring is catenary if its prime spectrum is a catenary poset.

theorem NoetherianTopological.algebraicVariety_isCatenary (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [Algebra k A] [Algebra.FiniteType k A] : IsRingCatenary A

The coordinate ring of an irreducible algebraic variety over a field is catenary: any two maximal chains of primes with the same endpoints have equal length.