Zero-dimensional rings

We provide further API for zero-dimensional rings. Basic definitions and lemmas are provided in Mathlib/RingTheory/KrullDimension/Basic.lean.

theorem Ring.KrullDimLE.mem_minimalPrimes_iff {R : Type u_1} [CommSemiring R] [KrullDimLE 0 R] {I J : Ideal R} : I ∈ J.minimalPrimes ↔ I.IsPrime ∧ J ≤ I

theorem Ring.KrullDimLE.mem_minimalPrimes_iff_le_of_isPrime {R : Type u_1} [CommSemiring R] [KrullDimLE 0 R] {I J : Ideal R} [I.IsPrime] : I ∈ J.minimalPrimes ↔ J ≤ I

theorem Ring.KrullDimLE.minimalPrimes_eq_setOfPred_isPrime (R : Type u_1) [CommSemiring R] [KrullDimLE 0 R] : minimalPrimes R = {I : Ideal R | I.IsPrime}

@[deprecated Ring.KrullDimLE.minimalPrimes_eq_setOfPred_isPrime (since := "2026-07-09")]

theorem Ring.KrullDimLE.minimalPrimes_eq_setOf_isPrime (R : Type u_1) [CommSemiring R] [KrullDimLE 0 R] : minimalPrimes R = {I : Ideal R | I.IsPrime}

Alias of Ring.KrullDimLE.minimalPrimes_eq_setOfPred_isPrime.

theorem Ring.KrullDimLE.minimalPrimes_eq_setOfPred_isMaximal (R : Type u_1) [CommSemiring R] [KrullDimLE 0 R] : minimalPrimes R = {I : Ideal R | I.IsMaximal}

@[deprecated Ring.KrullDimLE.minimalPrimes_eq_setOfPred_isMaximal (since := "2026-07-09")]

theorem Ring.KrullDimLE.minimalPrimes_eq_setOf_isMaximal (R : Type u_1) [CommSemiring R] [KrullDimLE 0 R] : minimalPrimes R = {I : Ideal R | I.IsMaximal}

Alias of Ring.KrullDimLE.minimalPrimes_eq_setOfPred_isMaximal.

theorem Ring.KrullDimLE.isField_of_isDomain {R : Type u_1} [CommSemiring R] [KrullDimLE 0 R] [IsDomain R] : IsField R

theorem ringKrullDimZero_iff_ringKrullDim_eq_zero {R : Type u_1} [CommSemiring R] [Nontrivial R] : Ring.KrullDimLE 0 R ↔ ringKrullDim R = 0

theorem Ideal.krullDimLE_zero_quotient_iff_forall_minimalPrimes_isMaximal {R : Type u_2} [CommRing R] {I : Ideal R} : Ring.KrullDimLE 0 (R ⧸ I) ↔ ∀ J ∈ I.minimalPrimes, J.IsMaximal

A quotient R ⧸ I has krull dimension at most zero if and only if all minimal primes over I are maximal.

theorem Ring.krullDimLE_zero_and_isLocalRing_tfae (R : Type u_1) [CommSemiring R] : [KrullDimLE 0 R ∧ IsLocalRing R, ∃! I : Ideal R, I.IsPrime, ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x, (nilradical R).IsMaximal].TFAE

@[simp]

theorem le_isUnit_iff_zero_notMem {R : Type u_1} [CommSemiring R] [Ring.KrullDimLE 0 R] [IsLocalRing R] {M : Submonoid R} : M ≤ IsUnit.submonoid R ↔ 0 ∉ M

theorem Ring.KrullDimLE.existsUnique_isPrime (R : Type u_1) [CommSemiring R] [KrullDimLE 0 R] [IsLocalRing R] : ∃! I : Ideal R, I.IsPrime

theorem Ring.KrullDimLE.eq_maximalIdeal_of_isPrime {R : Type u_1} [CommSemiring R] [KrullDimLE 0 R] [IsLocalRing R] (J : Ideal R) [J.IsPrime] : J = IsLocalRing.maximalIdeal R

theorem Ring.KrullDimLE.radical_eq_maximalIdeal {R : Type u_1} [CommSemiring R] [KrullDimLE 0 R] [IsLocalRing R] (I : Ideal R) (hI : I ≠ ⊤) : I.radical = IsLocalRing.maximalIdeal R

theorem Ring.KrullDimLE.subsingleton_primeSpectrum (R : Type u_1) [CommSemiring R] [KrullDimLE 0 R] [IsLocalRing R] : Subsingleton (PrimeSpectrum R)

theorem Ring.KrullDimLE.isNilpotent_iff_mem_maximalIdeal {R : Type u_1} [CommSemiring R] [KrullDimLE 0 R] [IsLocalRing R] {x : R} : IsNilpotent x ↔ x ∈ IsLocalRing.maximalIdeal R

theorem Ring.KrullDimLE.isNilpotent_iff_mem_nonunits {R : Type u_1} [CommSemiring R] [KrullDimLE 0 R] [IsLocalRing R] {x : R} : IsNilpotent x ↔ x ∈ nonunits R

theorem Ring.KrullDimLE.nilradical_eq_maximalIdeal (R : Type u_1) [CommSemiring R] [KrullDimLE 0 R] [IsLocalRing R] : nilradical R = IsLocalRing.maximalIdeal R

theorem IsLocalRing.of_isMaximal_nilradical (R : Type u_1) [CommSemiring R] [(nilradical R).IsMaximal] : IsLocalRing R

theorem Ring.KrullDimLE.of_isMaximal_nilradical (R : Type u_1) [CommSemiring R] [(nilradical R).IsMaximal] : KrullDimLE 0 R

theorem Ring.KrullDimLE.of_isLocalization {R : Type u_1} [CommSemiring R] (p : Ideal R) (hp : p ∈ minimalPrimes R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization.AtPrime S p] : KrullDimLE 0 S

theorem Ring.KrullDimLE.isField_of_isReduced {R : Type u_1} [CommSemiring R] [KrullDimLE 0 R] [IsReduced R] [IsLocalRing R] : IsField R

@[instance_reducible]

instance PrimeSpectrum.unique_of_ringKrullDimLE_zero {R : Type u_1} [CommSemiring R] [Ring.KrullDimLE 0 R] [IsLocalRing R] : Unique (PrimeSpectrum R)

Equations

• PrimeSpectrum.unique_of_ringKrullDimLE_zero = { default := IsLocalRing.closedPoint R, uniq := ⋯ }

theorem PrimeSpectrum.subsingleton_iff_isField_of_isReduced {R : Type u_2} [CommRing R] [IsReduced R] [Nontrivial R] : Subsingleton (PrimeSpectrum R) ↔ IsField R

theorem Ideal.jacobson_eq_radical {R : Type u_1} [CommRing R] (I : Ideal R) [Ring.KrullDimLE 0 R] : I.jacobson = I.radical

@[instance 100]

instance instIsJacobsonRingOfKrullDimLEOfNatNat {R : Type u_1} [CommRing R] [Ring.KrullDimLE 0 R] : IsJacobsonRing R