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.
The ring-theoretic Krull dimension is the Krull dimension of its spectrum ordered by inclusion.
Equations
Instances For
Type class for rings with krull dimension at most n
.
Equations
- Ring.KrullDimLE n R = Order.KrullDimLE n (PrimeSpectrum R)
Instances For
If f : R →+* S
is surjective, then ringKrullDim S ≤ ringKrullDim R
.
If I
is an ideal of R
, then ringKrullDim (R ⧸ I) ≤ ringKrullDim R
.
If R
and S
are isomorphic, then ringKrullDim R = ringKrullDim S
.
Alias of ringKrullDim_eq_of_ringEquiv
.
If R
and S
are isomorphic, then ringKrullDim R = ringKrullDim S
.
A ring has finite Krull dimension if its PrimeSpectrum
is
finite-dimensional (and non-empty).
Equations
Instances For
Also see Ideal.IsPrime.isMaximal
for the analogous statement for Dedekind domains.
Alternative constructor for Ring.KrullDimLE 1
, convenient for domains.