# Krull dimension of a preordered set #

If `α`

is a preordered set, then `krullDim α`

is defined to be `sup {n | a₀ < a₁ < ... < aₙ}`

.
In case that `α`

is empty, then its Krull dimension is defined to be negative infinity; if the
length of all series `a₀ < a₁ < ... < aₙ`

is unbounded, then its Krull dimension is defined to
be positive infinity.

For `a : α`

, its height is defined to be the krull dimension of the subset `(-∞, a]`

while its
coheight is defined to be the krull dimension of `[a, +∞)`

.

## Implementation notes #

Krull dimensions are defined to take value in `WithBot (WithTop ℕ)`

so that `(-∞) + (+∞)`

is
also negative infinity. This is because we want Krull dimensions to be additive with respect
to product of varieties so that `-∞`

being the Krull dimension of empty variety is equal to
sum of `-∞`

and the Krull dimension of any other varieties.

Krull dimension of a preorder `α`

is the supremum of the rightmost index of all relation
series of `α`

order by `<`

. If there is no series `a₀ < a₁ < ... < aₙ`

in `α`

, then its Krull
dimension is defined to be negative infinity; if the length of all series `a₀ < a₁ < ... < aₙ`

is
unbounded, its Krull dimension is defined to be positive infinity.