# 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.

noncomputable def krullDim (α : Type u_1) [] :

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.

Equations
• = ⨆ (p : ), p.length
Instances For
noncomputable def height (α : Type u_1) [] (a : α) :

Height of an element a of a preordered set α is the Krull dimension of the subset (-∞, a]

Equations
Instances For
noncomputable def coheight (α : Type u_1) [] (a : α) :

Coheight of an element a of a pre-ordered set α is the Krull dimension of the subset [a, +∞)

Equations
Instances For