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) [CommRing R] : WithBot (WithTop ℕ)

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

Equations

• ringKrullDim R = Order.krullDim (PrimeSpectrum R)

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

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

theorem ringKrullDim_le_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing 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_1} [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} [CommRing R] [CommRing 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} [CommRing R] [CommRing S] (e : R ≃+* S) : ringKrullDim R = ringKrullDim S

Alias of ringKrullDim_eq_of_ringEquiv.

---

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