Prime spectra of Noetherian and Artinian rings

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

instance PrimeSpectrum.instNoetherianSpace (R : Type u) [CommSemiring R] [IsNoetherianRing R] : TopologicalSpace.NoetherianSpace (PrimeSpectrum R)

theorem PrimeSpectrum.finite_setOfPred_isMin (R : Type u) [CommSemiring R] [IsNoetherianRing R] : {x : PrimeSpectrum R | IsMin x}.Finite

@[deprecated PrimeSpectrum.finite_setOfPred_isMin (since := "2026-07-09")]

theorem PrimeSpectrum.finite_setOf_isMin (R : Type u) [CommSemiring R] [IsNoetherianRing R] : {x : PrimeSpectrum R | IsMin x}.Finite

Alias of PrimeSpectrum.finite_setOfPred_isMin.

instance IsArtinianRing.instKrullDimLEOfNatNat (R : Type u_1) [CommRing R] [IsArtinianRing R] : Ring.KrullDimLE 0 R

instance IsArtinianRing.instDiscreteTopologyPrimeSpectrum (R : Type u_1) [CommRing R] [IsArtinianRing R] : DiscreteTopology (PrimeSpectrum R)

theorem IsArtinianRing.exists_notMem_forall_mem_of_ne {R : Type u_1} [CommRing R] [IsArtinianRing R] (p : Ideal R) [p.IsPrime] : ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q

@[deprecated IsArtinianRing.exists_notMem_forall_mem_of_ne (since := "2026-09-28")]

theorem IsArtinianRing.exists_not_mem_forall_mem_of_ne {R : Type u_1} [CommRing R] [IsArtinianRing R] (p : Ideal R) [p.IsPrime] : ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q

Alias of IsArtinianRing.exists_notMem_forall_mem_of_ne.

theorem IsArtinianRing.finrank_eq_sum_primeSpectrum (R : Type u_1) [CommRing R] [IsArtinianRing R] (F : Type u_2) [Field F] [Algebra F R] [Module.Finite F R] [Fintype (PrimeSpectrum R)] : Module.finrank F R = ∑ p : PrimeSpectrum R, Module.finrank F (Localization.AtPrime p.asIdeal)