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

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

• krullDim α = ⨆ (p : LTSeries α), ↑p.length

noncomputable def height (α : Type u_1) [Preorder α] (a : α) : WithBot (WithTop ℕ)

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

Equations

• height α a = krullDim ↑(Set.Iic a)

noncomputable def coheight (α : Type u_1) [Preorder α] (a : α) : WithBot (WithTop ℕ)

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

Equations

• coheight α a = krullDim ↑(Set.Ici a)