Krull dimensions of (commutative) rings

Given a commutative ring, its ring-theoretic Krull dimension is the order-theoretic Krull dimension of its prime spectrum. Unfolding this definition, it is the length of the longest sequence(s) of prime ideals ordered by strict inclusion.

noncomputable def ringKrullDim (R : Type u_1) [CommSemiring R] : WithBot ℕ∞

The ring-theoretic Krull dimension is the Krull dimension of its spectrum ordered by inclusion.

Equations

• ringKrullDim R = Order.krullDim (PrimeSpectrum R)

@[reducible, inline]

abbrev Ring.KrullDimLE (n : ℕ) (R : Type u_1) [CommSemiring R] : Prop

Type class for rings with krull dimension at most n.

Equations

• Ring.KrullDimLE n R = Order.KrullDimLE n (PrimeSpectrum R)

theorem Ring.krullDimLE_iff {R : Type u_1} [CommSemiring R] {n : ℕ} : KrullDimLE n R ↔ ringKrullDim R ≤ ↑n

theorem ringKrullDim_eq_bot_of_subsingleton {R : Type u_1} [CommSemiring R] [Subsingleton R] : ringKrullDim R = ⊥

theorem ringKrullDim_nonneg_of_nontrivial {R : Type u_1} [CommSemiring R] [Nontrivial R] : 0 ≤ ringKrullDim R

theorem ringKrullDim_le_of_surjective {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) (hf : Function.Surjective ⇑f) : ringKrullDim S ≤ ringKrullDim R

If f : R →+* S is surjective, then ringKrullDim S ≤ ringKrullDim R.

theorem ringKrullDim_quotient_le {R : Type u_3} [CommRing R] (I : Ideal R) : ringKrullDim (R ⧸ I) ≤ ringKrullDim R

If I is an ideal of R, then ringKrullDim (R ⧸ I) ≤ ringKrullDim R.

theorem ringKrullDim_eq_of_ringEquiv {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) : ringKrullDim R = ringKrullDim S

If R and S are isomorphic, then ringKrullDim R = ringKrullDim S.

theorem RingEquiv.ringKrullDim {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) : _root_.ringKrullDim R = _root_.ringKrullDim S

Alias of ringKrullDim_eq_of_ringEquiv.

---

If R and S are isomorphic, then ringKrullDim R = ringKrullDim S.

@[reducible, inline]

abbrev FiniteRingKrullDim (R : Type u_3) [CommSemiring R] : Prop

A ring has finite Krull dimension if its PrimeSpectrum is finite-dimensional (and non-empty).

Equations

• FiniteRingKrullDim R = FiniteDimensionalOrder (PrimeSpectrum R)

theorem ringKrullDim_ne_top {R : Type u_1} [CommSemiring R] [FiniteRingKrullDim R] : ringKrullDim R ≠ ⊤

theorem ringKrullDim_lt_top {R : Type u_1} [CommSemiring R] [FiniteRingKrullDim R] : ringKrullDim R < ⊤

theorem ringKrullDim_ne_bot {R : Type u_1} [CommSemiring R] [FiniteRingKrullDim R] : ringKrullDim R ≠ ⊥

theorem finiteRingKrullDim_iff_ne_bot_and_top {R : Type u_1} [CommSemiring R] : FiniteRingKrullDim R ↔ ringKrullDim R ≠ ⊥ ∧ ringKrullDim R ≠ ⊤

theorem Nontrivial.of_finiteRingKrullDim {R : Type u_1} [CommSemiring R] [FiniteRingKrullDim R] : Nontrivial R

theorem Ring.krullDimLE_zero_iff {R : Type u_1} [CommSemiring R] : KrullDimLE 0 R ↔ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal

theorem Ring.krullDimLE_zero_iff_forall_minimalPrimes_isMaximal {R : Type u_1} [CommSemiring R] : KrullDimLE 0 R ↔ ∀ I ∈ minimalPrimes R, I.IsMaximal

A ring has krull dimension at most zero if and only if all minimal primes are maximal.

theorem Ring.KrullDimLE.mk₀ {R : Type u_1} [CommSemiring R] (H : ∀ (I : Ideal R), I.IsPrime → I.IsMaximal) : KrullDimLE 0 R

theorem Ideal.isMaximal_of_isPrime {R : Type u_1} [CommSemiring R] [Ring.KrullDimLE 0 R] (I : Ideal R) [I.IsPrime] : I.IsMaximal

theorem Ideal.IsPrime.isMaximal' {R : Type u_1} [CommSemiring R] [Ring.KrullDimLE 0 R] {I : Ideal R} (hI : I.IsPrime) : I.IsMaximal

Also see Ideal.IsPrime.isMaximal for the analogous statement for Dedekind domains.

@[instance 100]

instance instIsMaximalOfIsPrimeOfKrullDimLEOfNatNat {R : Type u_1} [CommSemiring R] (I : Ideal R) [I.IsPrime] [Ring.KrullDimLE 0 R] : I.IsMaximal

theorem Ideal.isMaximal_iff_isPrime {R : Type u_1} [CommSemiring R] [Ring.KrullDimLE 0 R] {I : Ideal R} : I.IsMaximal ↔ I.IsPrime

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

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

theorem nilradical_le_jacobson (R : Type u_3) [CommRing R] : nilradical R ≤ Ring.jacobson R

theorem Ring.jacobson_eq_nilradical_of_krullDimLE_zero (R : Type u_3) [CommRing R] [KrullDimLE 0 R] : jacobson R = nilradical R

instance instKrullDimLEOfNatNat {R : Type u_1} [CommSemiring R] [Ring.KrullDimLE 0 R] : Ring.KrullDimLE 1 R

theorem Ring.krullDimLE_one_iff {R : Type u_1} [CommSemiring R] : KrullDimLE 1 R ↔ ∀ (I : Ideal R), I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal

theorem Ring.KrullDimLE.mk₁ {R : Type u_1} [CommSemiring R] (H : ∀ (I : Ideal R), I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal) : KrullDimLE 1 R

theorem Ring.krullDimLE_one_iff_of_isPrime_bot {R : Type u_1} [CommSemiring R] [⊥.IsPrime] : KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

theorem Ring.krullDimLE_one_iff_of_noZeroDivisors {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] : KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

theorem Ideal.IsPrime.isMaximal_of_ne_bot {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] [Ring.KrullDimLE 1 R] {I : Ideal R} (hI : I.IsPrime) (hI' : I ≠ ⊥) : I.IsMaximal

theorem Ideal.isMaximal_of_isPrime_of_ne_bot {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] [Ring.KrullDimLE 1 R] (I : Ideal R) [I.IsPrime] (hI' : I ≠ ⊥) : I.IsMaximal

theorem Ring.KrullDimLE.mk₁' {R : Type u_1} [CommSemiring R] (H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal) : KrullDimLE 1 R

Alternative constructor for Ring.KrullDimLE 1, convenient for domains.

theorem Prime.isMaximal_span_singleton {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] [Ring.KrullDimLE 1 R] {a : R} (ha : Prime a) : (Ideal.span {a}).IsMaximal

theorem Ideal.liesOver_span_iff {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [NoZeroDivisors R] [Ring.KrullDimLE 1 R] [Algebra R S] {P : Ideal S} {p : R} (hP : P ≠ ⊤) (hp : Prime p) : P.LiesOver (span {p}) ↔ (algebraMap R S) p ∈ P