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. See coheight_eq for the definition with a series ordered by < and beginning with a.

Equations

• Order.coheight a = Order.height a

Height

@[simp]

theorem Order.height_toDual {α : Type u_1} [Preorder α] (x : α) : Order.height (OrderDual.toDual x) = Order.coheight x

@[simp]

theorem Order.height_ofDual {α : Type u_1} [Preorder α] (x : αᵒᵈ) : Order.height (OrderDual.ofDual x) = Order.coheight x

@[simp]

theorem Order.coheight_toDual {α : Type u_1} [Preorder α] (x : α) : Order.coheight (OrderDual.toDual x) = Order.height x

@[simp]

theorem Order.coheight_ofDual {α : Type u_1} [Preorder α] (x : αᵒᵈ) : Order.coheight (OrderDual.ofDual x) = Order.height x

theorem Order.coheight_eq {α : Type u_1} [Preorder α] (a : α) : Order.coheight a = ⨆ (p : LTSeries α), ⨆ (_ : a ≤ RelSeries.head p), ↑p.length

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.

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

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.coheight_le_iff {α : Type u_1} [Preorder α] {a : α} {n : ℕ∞} : Order.coheight a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, a ≤ RelSeries.head p → ↑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

Variant of height_le_iff ranging only over those series that end exactly on a.

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.coheight_eq_iSup_head_eq {α : Type u_1} [Preorder α] (a : α) : Order.coheight a = ⨆ (p : LTSeries α), ⨆ (_ : RelSeries.head p = a), ↑p.length

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

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

Variant of coheight_le_iff ranging only over those series that begin exactly on a.

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

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_coheight {α : Type u_1} [Preorder α] {x : α} {p : LTSeries α} (hhead : x ≤ RelSeries.head p) : ↑p.length ≤ Order.coheight 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.length_le_coheight_head {α : Type u_1} [Preorder α] {p : LTSeries α} : ↑p.length ≤ Order.coheight (RelSeries.head p)

The coheight of the first 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.rev_index_le_coheight {α : Type u_1} [Preorder α] (p : LTSeries α) (i : Fin (p.length + 1)) : ↑↑i.rev ≤ Order.coheight (p.toFun i)

The coheight of an element in a series is larger or equal to its reverse 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.coheight_eq_index_of_length_eq_head_coheight {α : Type u_1} [Preorder α] {p : LTSeries α} (h : ↑p.length = Order.coheight (RelSeries.head p)) (i : Fin (p.length + 1)) : Order.coheight (p.toFun i) = ↑↑i.rev

In a maximally long series, i.e one as long as the coheight of the first element, the coheight of each element is its reverse 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

theorem Order.coheight_anti {α : Type u_1} [Preorder α] : Antitone Order.coheight

theorem Order.height_strictMono {α : Type u_1} [Preorder α] {x y : α} (hxy : x < y) (hfin : Order.height x < ⊤) : Order.height x < Order.height y

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

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

@[simp]

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

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

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

There exist a series ending in a element for any length up to the element’s height.

theorem Order.exists_series_of_le_coheight {α : Type u_1} [Preorder α] (a : α) {n : ℕ} (h : ↑n ≤ Order.coheight a) : ∃ (p : LTSeries α), RelSeries.head p = a ∧ p.length = n

theorem Order.exists_series_of_height_eq_coe {α : Type u_1} [Preorder α] (a : α) {n : ℕ} (h : Order.height a = ↑n) : ∃ (p : LTSeries α), RelSeries.last p = a ∧ p.length = n

For an element of finite height there exists a series ending in that element of that height.

theorem Order.exists_series_of_coheight_eq_coe {α : Type u_1} [Preorder α] (a : α) {n : ℕ} (h : Order.coheight a = ↑n) : ∃ (p : LTSeries α), RelSeries.head p = a ∧ p.length = n

theorem Order.height_eq_iSup_lt_height {α : Type u_1} [Preorder α] (x : α) : Order.height x = ⨆ (y : α), ⨆ (_ : y < x), Order.height y + 1

Another characterization of height, based on the supremum of the heights of elements below.

theorem Order.coheight_eq_iSup_gt_coheight {α : Type u_1} [Preorder α] (x : α) : Order.coheight x = ⨆ (y : α), ⨆ (_ : y > x), Order.coheight y + 1

Another characterization of coheight, based on the supremum of the coheights of elements above.

theorem Order.height_le_coe_iff {α : Type u_1} [Preorder α] {x : α} {n : ℕ} : Order.height x ≤ ↑n ↔ ∀ y < x, Order.height y < ↑n

theorem Order.coheight_le_coe_iff {α : Type u_1} [Preorder α] {x : α} {n : ℕ} : Order.coheight x ≤ ↑n ↔ ∀ y > x, Order.coheight y < ↑n

theorem Order.height_eq_top_iff {α : Type u_1} [Preorder α] {x : α} : Order.height x = ⊤ ↔ ∀ (n : ℕ), ∃ (p : LTSeries α), RelSeries.last p = x ∧ p.length = n

The height of an element is infinite iff there exist series of arbitrary length ending in that element.

theorem Order.coheight_eq_top_iff {α : Type u_1} [Preorder α] {x : α} : Order.coheight x = ⊤ ↔ ∀ (n : ℕ), ∃ (p : LTSeries α), RelSeries.head p = x ∧ p.length = n

The coheight of an element is infinite iff there exist series of arbitrary length ending in that element.

@[simp]

theorem Order.height_eq_zero {α : Type u_1} [Preorder α] {x : α} : Order.height x = 0 ↔ IsMin x

The elements of height zero are the minimal elements.

theorem Order.IsMin.height_eq_zero {α : Type u_1} [Preorder α] {x : α} : IsMin x → Order.height x = 0

Alias of the reverse direction of Order.height_eq_zero.

---

The elements of height zero are the minimal elements.

@[simp]

theorem Order.coheight_eq_zero {α : Type u_1} [Preorder α] {x : α} : Order.coheight x = 0 ↔ IsMax x

The elements of coheight zero are the maximal elements.

theorem Order.IsMax.coheight_eq_zero {α : Type u_1} [Preorder α] {x : α} : IsMax x → Order.coheight x = 0

Alias of the reverse direction of Order.coheight_eq_zero.

---

The elements of coheight zero are the maximal elements.

@[simp]

theorem Order.height_bot (α : Type u_3) [Preorder α] [OrderBot α] : Order.height ⊥ = 0

@[simp]

theorem Order.coheight_top (α : Type u_3) [Preorder α] [OrderTop α] : Order.coheight ⊤ = 0

theorem Order.coe_lt_height_iff {α : Type u_1} [Preorder α] {x : α} {n : ℕ} (hfin : Order.height x < ⊤) : ↑n < Order.height x ↔ ∃ y < x, Order.height y = ↑n

theorem Order.coe_lt_coheight_iff {α : Type u_1} [Preorder α] {x : α} {n : ℕ} (hfin : Order.coheight x < ⊤) : ↑n < Order.coheight x ↔ ∃ y > x, Order.coheight y = ↑n

theorem Order.height_eq_coe_add_one_iff {α : Type u_1} [Preorder α] {x : α} {n : ℕ} : Order.height x = ↑n + 1 ↔ Order.height x < ⊤ ∧ (∃ y < x, Order.height y = ↑n) ∧ ∀ y < x, Order.height y ≤ ↑n

theorem Order.coheight_eq_coe_add_one_iff {α : Type u_1} [Preorder α] {x : α} {n : ℕ} : Order.coheight x = ↑n + 1 ↔ Order.coheight x < ⊤ ∧ (∃ y > x, Order.coheight y = ↑n) ∧ ∀ y > x, Order.coheight y ≤ ↑n

theorem Order.height_eq_coe_iff {α : Type u_1} [Preorder α] {x : α} {n : ℕ} : Order.height x = ↑n ↔ Order.height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, Order.height y = ↑n - 1) ∧ ∀ y < x, Order.height y < ↑n

theorem Order.coheight_eq_coe_iff {α : Type u_1} [Preorder α] {x : α} {n : ℕ} : Order.coheight x = ↑n ↔ Order.coheight x < ⊤ ∧ (n = 0 ∨ ∃ y > x, Order.coheight y = ↑n - 1) ∧ ∀ y > x, Order.coheight y < ↑n

theorem Order.height_eq_coe_iff_minimal_le_height {α : Type u_1} [Preorder α] {a : α} {n : ℕ} : Order.height a = ↑n ↔ Minimal (fun (y : α) => ↑n ≤ Order.height y) a

The elements of finite height n are the minimial elements among those of height ≥ n.

theorem Order.coheight_eq_coe_iff_maximal_le_coheight {α : Type u_1} [Preorder α] {a : α} {n : ℕ} : Order.coheight a = ↑n ↔ Maximal (fun (y : α) => ↑n ≤ Order.coheight y) a

The elements of finite coheight n are the maximal elements among those of coheight ≥ n.

Krull dimension

theorem Order.LTSeries.length_le_krullDim {α : Type u_1} [Preorder α] (p : LTSeries α) : ↑p.length ≤ Order.krullDim α

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_nonpos_of_subsingleton {α : Type u_1} [Preorder α] [Subsingleton α] : 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.height_le_krullDim {α : Type u_1} [Preorder α] (a : α) : ↑(Order.height a) ≤ Order.krullDim α

theorem Order.coheight_le_krullDim {α : Type u_1} [Preorder α] (a : α) : ↑(Order.coheight a) ≤ Order.krullDim α

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

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

This version of the lemma assumes that α is nonempty. In this case, the coercion from ℕ∞ to WithBot ℕ∞ is on the outside fo the right-hand side, which is usually more convenient.

If α were empty, then krullDim α = ⊥. See krullDim_eq_iSup_height for the more general version, with the coercion under the supremum.

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

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

This version of the lemma assumes that α is nonempty. In this case, the coercion from ℕ∞ to WithBot ℕ∞ is on the outside of the right-hand side, which is usually more convenient.

If α were empty, then krullDim α = ⊥. See krullDim_eq_iSup_coheight for the more general version, with the coercion under the supremum.

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

The Krull dimension is the supremum of the elements' height plus coheight.

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.

If α is Nonempty, then krullDim_eq_iSup_height_of_nonempty, with the coercion from ℕ∞ to WithBot ℕ∞ outside the supremum, can be more convenient.

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

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

If α is Nonempty, then krullDim_eq_iSup_coheight_of_nonempty, with the coercion from ℕ∞ to WithBot ℕ∞ outside the supremum, can be more convenient.

@[simp]

theorem Order.height_top_eq_krullDim {α : Type u_1} [Preorder α] [OrderTop α] : ↑(Order.height ⊤) = Order.krullDim α

@[simp]

theorem Order.coheight_bot_eq_krullDim {α : Type u_1} [Preorder α] [OrderBot α] : ↑(Order.coheight ⊥) = Order.krullDim α