Height of an element in a partial order

This module contains a definition for the height of an element in a partial order.

All definitions in this file should likely be upstreamed to mathlib. Hence, this file isn't as polished as one would expect (docstrings etc.), as the polishing will happen during the upstream PR review process.

This height definition could replace the height definition in mathlib. I think it is preferrable, due to the simpler construction and more precise type (the height cannot be -∞, even though the krullDim can).

Some results found here:

• An element of finite height n has a LTSeries ending in it of length n
• For an element of finite height n there exists a series of length n ending in it
• A series of length n ends in an element of height at least n
• The element at position i of a series has height at least i
• Every series of length n ending in the element has at position i an element of height i
• The elements of height n are the minimal elements among those of height ≥n. This lemma proves the recursive equation in the blueprint.

theorem ENat.iSup_eq_coe_iff' {α : Type u_1} [Nonempty α] (f : α → ℕ∞) (n : ℕ) : ⨆ (x : α), f x = ↑n ↔ (∃ (x : α), f x = ↑n) ∧ ∀ (y : α), f y ≤ ↑n

theorem ENat.iSup_eq_coe_iff {α : Type u_1} [Nonempty α] (f : α → ℕ) (n : ℕ) : ⨆ (x : α), ↑(f x) = ↑n ↔ (∃ (x : α), f x = n) ∧ ∀ (y : α), f y ≤ n

theorem ENat.isup_add (ι : Type u_1) [Nonempty ι] (f : ι → ℕ∞) (n : ℕ∞) : (⨆ (x : ι), f x) + n = ⨆ (x : ι), f x + n

def LTSeries.replaceLast {α : Type u_1} [Preorder α] (p : LTSeries α) (x : α) (h : RelSeries.last p ≤ x) : LTSeries α

Replaces the last element in a series. Essentially p.eraseLast.snoc x, but also works when p is a singleton.

Equations

• p.replaceLast x h = if hlen : p.length = 0 then RelSeries.singleton (fun (x1 x2 : α) => x1 < x2) x else (RelSeries.eraseLast p).snoc x ⋯

@[simp]

theorem LTSeries.last_replaceLast {α : Type u_1} [Preorder α] (p : LTSeries α) (x : α) (h : RelSeries.last p ≤ x) : RelSeries.last (p.replaceLast x h) = x

@[simp]

theorem LTSeries.length_replaceLast {α : Type u_1} [Preorder α] (p : LTSeries α) (x : α) (h : RelSeries.last p ≤ x) : (p.replaceLast x h).length = p.length

theorem LTSeries.int_head_add_le_toFun (p : LTSeries ℤ) (i : Fin (p.length + 1)) : RelSeries.head p + ↑↑i ≤ p.toFun i

theorem LTSeries.int_head_add_len_le_last (p : LTSeries ℤ) : RelSeries.head p + ↑p.length ≤ RelSeries.last p

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

Equations

• height a = ⨆ (p : { p : LTSeries α // RelSeries.last p = a }), ↑(↑p).length

instance instNonemptySubtypeLTSeriesEqLastLt_carleson {α : Type u_1} [Preorder α] (a : α) : Nonempty { p : LTSeries α // RelSeries.last p = a }

Equations

• ⋯ = ⋯

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

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

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

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

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

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

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

theorem exists_series_of_height_eq_coe {α : Type u_1} [Preorder α] (a : α) {n : ℕ} (h : 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 height_eq_top_iff {α : Type u_1} [Preorder α] (x : α) : height x = ⊤ ↔ ∀ (n : ℕ), ∃ (p : LTSeries α), RelSeries.last p = x ∧ p.length = n

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

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

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

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

theorem height_eq_zero_iff {α : Type u_1} [Preorder α] (x : α) : height x = 0 ↔ ∀ (y : α), ¬y < x

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

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

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

theorem minimal_iff_height_eq_zero {α : Type u_1} [Preorder α] (a : α) : Minimal (fun (x : α) => True) a ↔ height a = 0

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

theorem subtype_mk_minimal_iff (α : Type u_2) [Preorder α] (s : Set α) (t : Set ↑s) (x : α) (hx : x ∈ s) : Minimal (fun (x : ↑s) => x ∈ t) ⟨x, hx⟩ ↔ Minimal (fun (y : α) => ∃ (h : y ∈ s), y ∈ s ∧ ⟨y, h⟩ ∈ t) x