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.

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

The 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)

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

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

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

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

theorem height_mono {α : Type u_1} [Preorder α] {a : α} {b : α} (h : a ≤ b) : height α a ≤ height α b

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

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

theorem 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) : krullDim β ≤ krullDim α

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

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

@[simp]

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