mathlib3 documentation

order.grade

Graded orders #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines graded orders, also known as ranked orders.

A 𝕆-graded order is an order α equipped with a distinguished "grade" function α → 𝕆 which should be understood as giving the "height" of the elements. Usual graded orders are ℕ-graded, cograded orders are ℕᵒᵈ-graded, but we can also grade by ℤ, and polytopes are naturally fin n-graded.

Visually, grade ℕ a is the height of a in the Hasse diagram of α.

Main declarations #

grade_order: Graded order.
grade_min_order: Graded order where minimal elements have minimal grades.
grade_max_order: Graded order where maximal elements have maximal grades.
grade_bounded_order: Graded order where minimal elements have minimal grades and maximal elements have maximal grades.
grade: The grade of an element. Because an order can admit several gradings, the first argument is the order we grade by.
grade_max_order: Graded orders with maximal elements. All maximal elements have the same grade.
max_grade: The maximum grade in a grade_max_order.
order_embedding.grade: The grade of an element in a linear order as an order embedding.

How to grade your order #

Here are the translations between common references and our grade_order:

Stanley defines a graded order of rank n as an order where all maximal chains have "length" n (so the number of elements of a chain is n + 1). This corresponds to grade_bounded_order (fin (n + 1)) α.
Engel's ranked orders are somewhere between grade_order ℕ α and grade_min_order ℕ α, in that he requires ∃ a, is_min a ∧ grade ℕ a + 0 rather than ∀ a, is_min a → grade ℕ a = 0. He defines a graded order as an order where all minimal elements have grade 0 and all maximal elements have the same grade. This is roughly a less bundled version of grade_bounded_order (fin n) α, assuming we discard orders with infinite chains.

Implementation notes #

One possible definition of graded orders is as the bounded orders whose flags (maximal chains) all have the same finite length (see Stanley p. 99). However, this means that all graded orders must have minimal and maximal elements and that the grade is not data.

Instead, we define graded orders by their grade function, without talking about flags yet.

References #

@[class]

structure grade_order (𝕆 : Type u_5) (α : Type u_6) [preorder 𝕆] [preorder α] :

Type (max u_5 u_6)

grade : α → 𝕆
grade_strict_mono : strict_mono grade_order.grade
covby_grade : ∀ ⦃a b : α⦄, a ⋖ b → grade_order.grade a ⋖ grade_order.grade b

An 𝕆-graded order is an order α equipped with a strictly monotone function grade 𝕆 : α → 𝕆 which preserves order covering (covby).

Instances of this typeclass

Instances of other typeclasses for grade_order

grade_order.has_sizeof_inst

@[class]

structure grade_min_order (𝕆 : Type u_5) (α : Type u_6) [preorder 𝕆] [preorder α] :

Type (max u_5 u_6)

grade : α → 𝕆
grade_strict_mono : strict_mono grade_min_order.grade
covby_grade : ∀ ⦃a b : α⦄, a ⋖ b → grade_min_order.grade a ⋖ grade_min_order.grade b
is_min_grade : ∀ ⦃a : α⦄, is_min a → is_min (grade_min_order.grade a)

A 𝕆-graded order where minimal elements have minimal grades.

Instances of this typeclass

Instances of other typeclasses for grade_min_order

grade_min_order.has_sizeof_inst

@[instance]

def grade_min_order.to_grade_order (𝕆 : Type u_5) (α : Type u_6) [preorder 𝕆] [preorder α] [self : grade_min_order 𝕆 α] :

grade_order 𝕆 α

@[instance]

def grade_max_order.to_grade_order (𝕆 : Type u_5) (α : Type u_6) [preorder 𝕆] [preorder α] [self : grade_max_order 𝕆 α] :

grade_order 𝕆 α

@[class]

structure grade_max_order (𝕆 : Type u_5) (α : Type u_6) [preorder 𝕆] [preorder α] :

Type (max u_5 u_6)

grade : α → 𝕆
grade_strict_mono : strict_mono grade_max_order.grade
covby_grade : ∀ ⦃a b : α⦄, a ⋖ b → grade_max_order.grade a ⋖ grade_max_order.grade b
is_max_grade : ∀ ⦃a : α⦄, is_max a → is_max (grade_max_order.grade a)

A 𝕆-graded order where maximal elements have maximal grades.

Instances of this typeclass

Instances of other typeclasses for grade_max_order

grade_max_order.has_sizeof_inst

@[class]

structure grade_bounded_order (𝕆 : Type u_5) (α : Type u_6) [preorder 𝕆] [preorder α] :

Type (max u_5 u_6)

grade : α → 𝕆
grade_strict_mono : strict_mono grade_bounded_order.grade
covby_grade : ∀ ⦃a b : α⦄, a ⋖ b → grade_bounded_order.grade a ⋖ grade_bounded_order.grade b
is_min_grade : ∀ ⦃a : α⦄, is_min a → is_min (grade_bounded_order.grade a)
is_max_grade : ∀ ⦃a : α⦄, is_max a → is_max (grade_bounded_order.grade a)

A 𝕆-graded order where minimal elements have minimal grades and maximal elements have maximal grades.

Instances of this typeclass

Instances of other typeclasses for grade_bounded_order

grade_bounded_order.has_sizeof_inst

@[instance]

def grade_bounded_order.to_grade_min_order (𝕆 : Type u_5) (α : Type u_6) [preorder 𝕆] [preorder α] [self : grade_bounded_order 𝕆 α] :

grade_min_order 𝕆 α

@[instance]

def grade_bounded_order.to_grade_max_order (𝕆 : Type u_5) (α : Type u_6) [preorder 𝕆] [preorder α] [self : grade_bounded_order 𝕆 α] :

grade_max_order 𝕆 α

def grade (𝕆 : Type u_1) {α : Type u_3} [preorder 𝕆] [preorder α] [grade_order 𝕆 α] :

α → 𝕆

The grade of an element in a graded order. Morally, this is the number of elements you need to go down by to get to ⊥.

Equations

grade 𝕆 = grade_order.grade

@[protected]

theorem covby.grade (𝕆 : Type u_1) {α : Type u_3} [preorder 𝕆] [preorder α] [grade_order 𝕆 α] {a b : α} (h : a ⋖ b) :

grade 𝕆 a ⋖ grade 𝕆 b

theorem grade_strict_mono {𝕆 : Type u_1} {α : Type u_3} [preorder 𝕆] [preorder α] [grade_order 𝕆 α] :

strict_mono (grade 𝕆)

theorem covby_iff_lt_covby_grade {𝕆 : Type u_1} {α : Type u_3} [preorder 𝕆] [preorder α] [grade_order 𝕆 α] {a b : α} :

a ⋖ b ↔ a < b ∧ grade 𝕆 a ⋖ grade 𝕆 b

@[protected]

theorem is_min.grade (𝕆 : Type u_1) {α : Type u_3} [preorder 𝕆] [preorder α] [grade_min_order 𝕆 α] {a : α} (h : is_min a) :

is_min (grade 𝕆 a)

@[simp]

theorem is_min_grade_iff {𝕆 : Type u_1} {α : Type u_3} [preorder 𝕆] [preorder α] [grade_min_order 𝕆 α] {a : α} :

is_min (grade 𝕆 a) ↔ is_min a

@[protected]

theorem is_max.grade (𝕆 : Type u_1) {α : Type u_3} [preorder 𝕆] [preorder α] [grade_max_order 𝕆 α] {a : α} (h : is_max a) :

is_max (grade 𝕆 a)

@[simp]

theorem is_max_grade_iff {𝕆 : Type u_1} {α : Type u_3} [preorder 𝕆] [preorder α] [grade_max_order 𝕆 α] {a : α} :

is_max (grade 𝕆 a) ↔ is_max a

theorem grade_mono {𝕆 : Type u_1} {α : Type u_3} [preorder 𝕆] [partial_order α] [grade_order 𝕆 α] :

monotone (grade 𝕆)

theorem grade_injective {𝕆 : Type u_1} {α : Type u_3} [preorder 𝕆] [linear_order α] [grade_order 𝕆 α] :

function.injective (grade 𝕆)

@[simp]

theorem grade_le_grade_iff {𝕆 : Type u_1} {α : Type u_3} [preorder 𝕆] [linear_order α] [grade_order 𝕆 α] {a b : α} :

grade 𝕆 a ≤ grade 𝕆 b ↔ a ≤ b

@[simp]

theorem grade_lt_grade_iff {𝕆 : Type u_1} {α : Type u_3} [preorder 𝕆] [linear_order α] [grade_order 𝕆 α] {a b : α} :

grade 𝕆 a < grade 𝕆 b ↔ a < b

@[simp]

theorem grade_eq_grade_iff {𝕆 : Type u_1} {α : Type u_3} [preorder 𝕆] [linear_order α] [grade_order 𝕆 α] {a b : α} :

grade 𝕆 a = grade 𝕆 b ↔ a = b

theorem grade_ne_grade_iff {𝕆 : Type u_1} {α : Type u_3} [preorder 𝕆] [linear_order α] [grade_order 𝕆 α] {a b : α} :

grade 𝕆 a ≠ grade 𝕆 b ↔ a ≠ b

theorem grade_covby_grade_iff {𝕆 : Type u_1} {α : Type u_3} [preorder 𝕆] [linear_order α] [grade_order 𝕆 α] {a b : α} :

grade 𝕆 a ⋖ grade 𝕆 b ↔ a ⋖ b

@[simp]

theorem grade_bot {𝕆 : Type u_1} {α : Type u_3} [partial_order 𝕆] [preorder α] [order_bot 𝕆] [order_bot α] [grade_min_order 𝕆 α] :

grade 𝕆 ⊥ = ⊥

@[simp]

theorem grade_top {𝕆 : Type u_1} {α : Type u_3} [partial_order 𝕆] [preorder α] [order_top 𝕆] [order_top α] [grade_max_order 𝕆 α] :

grade 𝕆 ⊤ = ⊤

Instances #

@[protected, instance]

def preorder.to_grade_bounded_order {α : Type u_3} [preorder α] :

grade_bounded_order α α

Equations

preorder.to_grade_bounded_order = {grade := id α, grade_strict_mono := _, covby_grade := _, is_min_grade := _, is_max_grade := _}

@[simp]

theorem grade_self {α : Type u_3} [preorder α] (a : α) :

grade α a = a

Dual #

@[protected, instance]

def order_dual.grade_order {𝕆 : Type u_1} {α : Type u_3} [preorder 𝕆] [preorder α] [grade_order 𝕆 α] :

grade_order 𝕆ᵒᵈ αᵒᵈ

Equations

order_dual.grade_order = {grade := ⇑order_dual.to_dual ∘ grade 𝕆 ∘ ⇑order_dual.of_dual, grade_strict_mono := _, covby_grade := _}

@[protected, instance]

def order_dual.grade_min_order {𝕆 : Type u_1} {α : Type u_3} [preorder 𝕆] [preorder α] [grade_max_order 𝕆 α] :

grade_min_order 𝕆ᵒᵈ αᵒᵈ

Equations

order_dual.grade_min_order = {grade := grade_order.grade order_dual.grade_order, grade_strict_mono := _, covby_grade := _, is_min_grade := _}

@[protected, instance]

def order_dual.grade_max_order {𝕆 : Type u_1} {α : Type u_3} [preorder 𝕆] [preorder α] [grade_min_order 𝕆 α] :

grade_max_order 𝕆ᵒᵈ αᵒᵈ

Equations

order_dual.grade_max_order = {grade := grade_order.grade order_dual.grade_order, grade_strict_mono := _, covby_grade := _, is_max_grade := _}

@[protected, instance]

def order_dual.grade_bounded_order {𝕆 : Type u_1} {α : Type u_3} [preorder 𝕆] [preorder α] [grade_bounded_order 𝕆 α] :

grade_bounded_order 𝕆ᵒᵈ αᵒᵈ

Equations

order_dual.grade_bounded_order = {grade := grade_min_order.grade order_dual.grade_min_order, grade_strict_mono := _, covby_grade := _, is_min_grade := _, is_max_grade := _}

@[simp]

theorem grade_to_dual {𝕆 : Type u_1} {α : Type u_3} [preorder 𝕆] [preorder α] [grade_order 𝕆 α] (a : α) :

grade 𝕆ᵒᵈ (⇑order_dual.to_dual a) = ⇑order_dual.to_dual (grade 𝕆 a)

@[simp]

theorem grade_of_dual {𝕆 : Type u_1} {α : Type u_3} [preorder 𝕆] [preorder α] [grade_order 𝕆 α] (a : αᵒᵈ) :

grade 𝕆 (⇑order_dual.of_dual a) = ⇑order_dual.of_dual (grade 𝕆ᵒᵈ a)

Lifting a graded order #

@[reducible]

def grade_order.lift_left {𝕆 : Type u_1} {ℙ : Type u_2} {α : Type u_3} [preorder 𝕆] [preorder «ℙ»] [preorder α] [grade_order 𝕆 α] (f : 𝕆 → «ℙ») (hf : strict_mono f) (hcovby : ∀ (a b : 𝕆), a ⋖ b → f a ⋖ f b) :

grade_order «ℙ» α

Lifts a graded order along a strictly monotone function.

Equations

grade_order.lift_left f hf hcovby = {grade := f ∘ grade 𝕆, grade_strict_mono := _, covby_grade := _}

@[reducible]

def grade_min_order.lift_left {𝕆 : Type u_1} {ℙ : Type u_2} {α : Type u_3} [preorder 𝕆] [preorder «ℙ»] [preorder α] [grade_min_order 𝕆 α] (f : 𝕆 → «ℙ») (hf : strict_mono f) (hcovby : ∀ (a b : 𝕆), a ⋖ b → f a ⋖ f b) (hmin : ∀ (a : 𝕆), is_min a → is_min (f a)) :

grade_min_order «ℙ» α

Lifts a graded order along a strictly monotone function.

Equations

grade_min_order.lift_left f hf hcovby hmin = {grade := grade_order.grade (grade_order.lift_left f hf hcovby), grade_strict_mono := _, covby_grade := _, is_min_grade := _}

@[reducible]

def grade_max_order.lift_left {𝕆 : Type u_1} {ℙ : Type u_2} {α : Type u_3} [preorder 𝕆] [preorder «ℙ»] [preorder α] [grade_max_order 𝕆 α] (f : 𝕆 → «ℙ») (hf : strict_mono f) (hcovby : ∀ (a b : 𝕆), a ⋖ b → f a ⋖ f b) (hmax : ∀ (a : 𝕆), is_max a → is_max (f a)) :

grade_max_order «ℙ» α

Lifts a graded order along a strictly monotone function.

Equations

grade_max_order.lift_left f hf hcovby hmax = {grade := grade_order.grade (grade_order.lift_left f hf hcovby), grade_strict_mono := _, covby_grade := _, is_max_grade := _}

@[reducible]

def grade_bounded_order.lift_left {𝕆 : Type u_1} {ℙ : Type u_2} {α : Type u_3} [preorder 𝕆] [preorder «ℙ»] [preorder α] [grade_bounded_order 𝕆 α] (f : 𝕆 → «ℙ») (hf : strict_mono f) (hcovby : ∀ (a b : 𝕆), a ⋖ b → f a ⋖ f b) (hmin : ∀ (a : 𝕆), is_min a → is_min (f a)) (hmax : ∀ (a : 𝕆), is_max a → is_max (f a)) :

grade_bounded_order «ℙ» α

Lifts a graded order along a strictly monotone function.

Equations

grade_bounded_order.lift_left f hf hcovby hmin hmax = {grade := grade_min_order.grade (grade_min_order.lift_left f hf hcovby hmin), grade_strict_mono := _, covby_grade := _, is_min_grade := _, is_max_grade := _}

@[reducible]

def grade_order.lift_right {𝕆 : Type u_1} {α : Type u_3} {β : Type u_4} [preorder 𝕆] [preorder α] [preorder β] [grade_order 𝕆 β] (f : α → β) (hf : strict_mono f) (hcovby : ∀ (a b : α), a ⋖ b → f a ⋖ f b) :

grade_order 𝕆 α

Lifts a graded order along a strictly monotone function.

Equations

grade_order.lift_right f hf hcovby = {grade := grade 𝕆 ∘ f, grade_strict_mono := _, covby_grade := _}

@[reducible]

def grade_min_order.lift_right {𝕆 : Type u_1} {α : Type u_3} {β : Type u_4} [preorder 𝕆] [preorder α] [preorder β] [grade_min_order 𝕆 β] (f : α → β) (hf : strict_mono f) (hcovby : ∀ (a b : α), a ⋖ b → f a ⋖ f b) (hmin : ∀ (a : α), is_min a → is_min (f a)) :

grade_min_order 𝕆 α

Lifts a graded order along a strictly monotone function.

Equations

grade_min_order.lift_right f hf hcovby hmin = {grade := grade_order.grade (grade_order.lift_right f hf hcovby), grade_strict_mono := _, covby_grade := _, is_min_grade := _}

@[reducible]

def grade_max_order.lift_right {𝕆 : Type u_1} {α : Type u_3} {β : Type u_4} [preorder 𝕆] [preorder α] [preorder β] [grade_max_order 𝕆 β] (f : α → β) (hf : strict_mono f) (hcovby : ∀ (a b : α), a ⋖ b → f a ⋖ f b) (hmax : ∀ (a : α), is_max a → is_max (f a)) :

grade_max_order 𝕆 α

Lifts a graded order along a strictly monotone function.

Equations

grade_max_order.lift_right f hf hcovby hmax = {grade := grade_order.grade (grade_order.lift_right f hf hcovby), grade_strict_mono := _, covby_grade := _, is_max_grade := _}

@[reducible]

def grade_bounded_order.lift_right {𝕆 : Type u_1} {α : Type u_3} {β : Type u_4} [preorder 𝕆] [preorder α] [preorder β] [grade_bounded_order 𝕆 β] (f : α → β) (hf : strict_mono f) (hcovby : ∀ (a b : α), a ⋖ b → f a ⋖ f b) (hmin : ∀ (a : α), is_min a → is_min (f a)) (hmax : ∀ (a : α), is_max a → is_max (f a)) :

grade_bounded_order 𝕆 α

Lifts a graded order along a strictly monotone function.

Equations

grade_bounded_order.lift_right f hf hcovby hmin hmax = {grade := grade_min_order.grade (grade_min_order.lift_right f hf hcovby hmin), grade_strict_mono := _, covby_grade := _, is_min_grade := _, is_max_grade := _}

`fin n`-graded to `ℕ`-graded to `ℤ`-graded #

@[reducible]

def grade_order.fin_to_nat {α : Type u_3} [preorder α] (n : ℕ) [grade_order (fin n) α] :

grade_order ℕ α

A fin n-graded order is also ℕ-graded. We do not mark this an instance because n is not inferrable.

Equations

grade_order.fin_to_nat n = grade_order.lift_left coe fin.coe_strict_mono _

@[reducible]

def grade_min_order.fin_to_nat {α : Type u_3} [preorder α] (n : ℕ) [grade_min_order (fin n) α] :

grade_min_order ℕ α

A fin n-graded order is also ℕ-graded. We do not mark this an instance because n is not inferrable.

Equations

grade_min_order.fin_to_nat n = grade_min_order.lift_left coe fin.coe_strict_mono _ _

@[protected, instance]

def grade_order.nat_to_int {α : Type u_3} [preorder α] [grade_order ℕ α] :

grade_order ℤ α

Equations

grade_order.nat_to_int = grade_order.lift_left coe int.coe_nat_strict_mono grade_order.nat_to_int._proof_1