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 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 finiteRingKrullDim_iff_ne_bot_and_top {R : Type u_1} [CommSemiring R] : FiniteRingKrullDim R ↔ ringKrullDim R ≠ ⊥ ∧ ringKrullDim R ≠ ⊤

instance instKrullDimLEOfNatNatOfSubsingleton {R : Type u_1} [CommSemiring R] [Subsingleton R] : Ring.KrullDimLE 0 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.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

@[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 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.