Krull dimension of a preordered set and height of an element

If α is a preordered set, then krullDim α : WithBot ℕ∞ 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 (in ℕ∞) is defined to be sup {n | a₀ < a₁ < ... < aₙ ≤ a} while its coheight is defined to be sup {n | a ≤ a₀ < a₁ < ... < aₙ} .

Main results

• The Krull dimension is the same as that of the dual order (krullDim_orderDual).

• The Krull dimension is the supremum of the heights of the elements (krullDim_eq_iSup_height).

• The height is monotone.

Design notes

Krull dimensions are defined to take value in WithBot ℕ∞ 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.

We could generalize the notion of Krull dimension to an arbitrary binary relation; many results in this file would generalize as well. But we don't think it would be useful, so we only define Krull dimension of a preorder.

noncomputable def Order.krullDim (α : Type u_1) [Preorder α] : WithBot ℕ∞

The Krull dimension of a preorder α is the supremum of the rightmost index of all relation series of α ordered 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

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

noncomputable def Order.height {α : Type u_1} [Preorder α] (a : α) : ℕ∞

The height of an element a in a preorder α is the supremum of the rightmost index of all relation series of α ordered by < and ending below or at a.

Equations

• Order.height a = ⨆ (p : LTSeries α), ⨆ (_ : RelSeries.last p ≤ a), ↑p.length

noncomputable def Order.coheight {α : Type u_1} [Preorder α] (a : α) : ℕ∞

The coheight of an element a in a preorder α is the supremum of the rightmost index of all relation series of α ordered by < and beginning with a.

The definition of coheight is via the height in the dual order, in order to easily transfer theorems between height and coheight.

Equations

• Order.coheight a = Order.height a

Height

theorem Order.height_le_iff {α : Type u_1} [Preorder α] {a : α} {n : ℕ∞} : Order.height a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, RelSeries.last p ≤ a → ↑p.length ≤ n

theorem Order.height_le {α : Type u_1} [Preorder α] {a : α} {n : ℕ∞} (h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n) : Order.height a ≤ n

theorem Order.height_le_iff' {α : Type u_1} [Preorder α] {a : α} {n : ℕ∞} : Order.height a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n

theorem Order.height_eq_iSup_last_eq {α : Type u_1} [Preorder α] (a : α) : Order.height a = ⨆ (p : LTSeries α), ⨆ (_ : RelSeries.last p = a), ↑p.length

Alternative definition of height, with the supremum ranging only over those series that end at a.

theorem Order.length_le_height {α : Type u_1} [Preorder α] {p : LTSeries α} {x : α} (hlast : RelSeries.last p ≤ x) : ↑p.length ≤ Order.height x

theorem Order.length_le_height_last {α : Type u_1} [Preorder α] {p : LTSeries α} : ↑p.length ≤ Order.height (RelSeries.last p)

The height of the last element in a series is larger or equal to the length of the series.

theorem Order.index_le_height {α : Type u_1} [Preorder α] (p : LTSeries α) (i : Fin (p.length + 1)) : ↑↑i ≤ Order.height (p.toFun i)

The height of an element in a series is larger or equal to its index in the series.

theorem Order.height_eq_index_of_length_eq_height_last {α : Type u_1} [Preorder α] {p : LTSeries α} (h : ↑p.length = Order.height (RelSeries.last p)) (i : Fin (p.length + 1)) : Order.height (p.toFun i) = ↑↑i

In a maximally long series, i.e one as long as the height of the last element, the height of each element is its index in the series.

theorem Order.height_mono {α : Type u_1} [Preorder α] : Monotone Order.height

theorem GCongr.height_le_height {α : Type u_1} [Preorder α] (a : α) (b : α) (hab : a ≤ b) : Order.height a ≤ Order.height b

Krull dimension

theorem Order.krullDim_nonneg_of_nonempty {α : Type u_1} [Preorder α] [Nonempty α] : 0 ≤ Order.krullDim α

theorem Order.krullDim_eq_iSup_length {α : Type u_1} [Preorder α] [Nonempty α] : Order.krullDim α = ↑(⨆ (p : LTSeries α), ↑p.length)

A definition of krullDim for nonempty α that avoids WithBot

theorem Order.krullDim_eq_bot_of_isEmpty {α : Type u_1} [Preorder α] [IsEmpty α] : Order.krullDim α = ⊥

theorem Order.krullDim_eq_top_of_infiniteDimensionalOrder {α : Type u_1} [Preorder α] [InfiniteDimensionalOrder α] : Order.krullDim α = ⊤

theorem Order.krullDim_le_of_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α → β) (hf : StrictMono f) : Order.krullDim α ≤ Order.krullDim β

theorem Order.krullDim_eq_length_of_finiteDimensionalOrder {α : Type u_1} [Preorder α] [FiniteDimensionalOrder α] : Order.krullDim α = ↑(LTSeries.longestOf α).length

theorem Order.krullDim_eq_zero_of_unique {α : Type u_1} [Preorder α] [Unique α] : Order.krullDim α = 0

theorem Order.krullDim_le_of_strictComono_and_surj {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α → β) (hf : ∀ ⦃a b : α⦄, f a < f b → a < b) (hf' : Function.Surjective f) : Order.krullDim β ≤ Order.krullDim α

theorem Order.krullDim_eq_of_orderIso {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) : Order.krullDim α = Order.krullDim β

@[simp]

theorem Order.krullDim_orderDual {α : Type u_1} [Preorder α] : Order.krullDim αᵒᵈ = Order.krullDim α

theorem Order.krullDim_eq_iSup_height {α : Type u_1} [Preorder α] : Order.krullDim α = ⨆ (a : α), ↑(Order.height a)

The Krull dimension is the supremum of the elements' heights.