Documentation

Mathlib.Order.KrullDimension

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 α] :

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
Instances For
    noncomputable def height (α : Type u_1) [Preorder α] (a : α) :

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

    Equations
    Instances For
      noncomputable def coheight (α : Type u_1) [Preorder α] (a : α) :

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

      Equations
      Instances For
        theorem krullDim_le_of_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : αβ) (hf : StrictMono f) :
        theorem height_mono {α : Type u_1} [Preorder α] {a : α} {b : α} (h : a b) :
        height α a height α b
        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 ba < b) (hf' : Function.Surjective f) :
        theorem krullDim_eq_of_orderIso {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) :
        theorem krullDim_eq_iSup_height {α : Type u_1} [Preorder α] :
        krullDim α = ⨆ (a : α), height α a
        @[simp]
        theorem krullDim_orderDual {α : Type u_1} [Preorder α] :