mathlib documentation

order.grade

Graded orders #

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 #

How to grade your order #

Here are the translations between common references and our grade_order:

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)

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)

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)

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)

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
@[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 ๐•† ฮฑ] :
@[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 ๐•† ฮฑ] :
@[simp]
theorem grade_top {๐•† : Type u_1} {ฮฑ : Type u_3} [partial_order ๐•†] [preorder ฮฑ] [order_top ๐•†] [order_top ฮฑ] [grade_max_order ๐•† ฮฑ] :

Instances #

@[protected, instance]
def preorder.to_grade_bounded_order {ฮฑ : Type u_3} [preorder ฮฑ] :
grade_bounded_order ฮฑ ฮฑ
Equations
@[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 ๐•† ฮฑ] :
Equations
@[protected, instance]
def order_dual.grade_min_order {๐•† : Type u_1} {ฮฑ : Type u_3} [preorder ๐•†] [preorder ฮฑ] [grade_max_order ๐•† ฮฑ] :
Equations
@[protected, instance]
def order_dual.grade_max_order {๐•† : Type u_1} {ฮฑ : Type u_3} [preorder ๐•†] [preorder ฮฑ] [grade_min_order ๐•† ฮฑ] :
Equations
@[protected, instance]
def order_dual.grade_bounded_order {๐•† : Type u_1} {ฮฑ : Type u_3} [preorder ๐•†] [preorder ฮฑ] [grade_bounded_order ๐•† ฮฑ] :
Equations
@[simp]
theorem grade_to_dual {๐•† : Type u_1} {ฮฑ : Type u_3} [preorder ๐•†] [preorder ฮฑ] [grade_order ๐•† ฮฑ] (a : ฮฑ) :
@[simp]
theorem grade_of_dual {๐•† : Type u_1} {ฮฑ : Type u_3} [preorder ๐•†] [preorder ฮฑ] [grade_order ๐•† ฮฑ] (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
@[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
@[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
@[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
@[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
@[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
@[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
@[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

fin n-graded to โ„•-graded to โ„ค-graded #

@[reducible]
def grade_order.fin_to_nat {ฮฑ : Type u_3} [preorder ฮฑ] (n : โ„•) [grade_order (fin n) ฮฑ] :

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

Equations
@[reducible]
def grade_min_order.fin_to_nat {ฮฑ : Type u_3} [preorder ฮฑ] (n : โ„•) [grade_min_order (fin n) ฮฑ] :

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

Equations
@[protected, instance]
def grade_order.nat_to_int {ฮฑ : Type u_3} [preorder ฮฑ] [grade_order โ„• ฮฑ] :
Equations