# Documentation

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

An ๐-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 #

• GradeOrder: Graded order.
• GradeMinOrder: Graded order where minimal elements have minimal grades.
• GradeMaxOrder: Graded order where maximal elements have maximal grades.
• GradeBoundedOrder: 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.

Here are the translations between common references and our GradeOrder:

• [Stanley][stanley2012] 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 GradeBoundedOrder (Fin (n + 1)) ฮฑ.
• [Engel][engel1997]'s ranked orders are somewhere between GradeOrder โ ฮฑ and GradeMinOrder โ ฮฑ, in that he requires โ a, IsMin a โง grade โ a = 0 rather than โ a, IsMin 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 GradeBoundedOrder (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.

## References #

• [Richard Stanley, Enumerative Combinatorics][stanley2012]
class GradeOrder (๐ : 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).

• grade : ฮฑ โ ๐

grade is strictly monotonic.

• covBy_grade : โ โฆa b : ฮฑโฆ, a โ b โ

grade preserves CovBy.

Instances
theorem GradeOrder.grade_strictMono {๐ : Type u_5} {ฮฑ : Type u_6} [Preorder ๐] [Preorder ฮฑ] [self : GradeOrder ๐ ฮฑ] :

grade is strictly monotonic.

theorem GradeOrder.covBy_grade {๐ : Type u_5} {ฮฑ : Type u_6} [Preorder ๐] [Preorder ฮฑ] [self : GradeOrder ๐ ฮฑ] โฆa : ฮฑโฆ โฆb : ฮฑโฆ :
a โ b โ

grade preserves CovBy.

class GradeMinOrder (๐ : Type u_5) (ฮฑ : Type u_6) [Preorder ๐] [Preorder ฮฑ] extends :
Type (max u_5 u_6)

An ๐-graded order where minimal elements have minimal grades.

• grade : ฮฑ โ ๐
• covBy_grade : โ โฆa b : ฮฑโฆ, a โ b โ
• isMin_grade : โ โฆa : ฮฑโฆ, โ

Instances
theorem GradeMinOrder.isMin_grade {๐ : Type u_5} {ฮฑ : Type u_6} [Preorder ๐] [Preorder ฮฑ] [self : GradeMinOrder ๐ ฮฑ] โฆa : ฮฑโฆ :
โ

class GradeMaxOrder (๐ : Type u_5) (ฮฑ : Type u_6) [Preorder ๐] [Preorder ฮฑ] extends :
Type (max u_5 u_6)

An ๐-graded order where maximal elements have maximal grades.

• grade : ฮฑ โ ๐
• covBy_grade : โ โฆa b : ฮฑโฆ, a โ b โ
• isMax_grade : โ โฆa : ฮฑโฆ, โ

Instances
theorem GradeMaxOrder.isMax_grade {๐ : Type u_5} {ฮฑ : Type u_6} [Preorder ๐] [Preorder ฮฑ] [self : GradeMaxOrder ๐ ฮฑ] โฆa : ฮฑโฆ :
โ

class GradeBoundedOrder (๐ : Type u_5) (ฮฑ : Type u_6) [Preorder ๐] [Preorder ฮฑ] extends :
Type (max u_5 u_6)

An ๐-graded order where minimal elements have minimal grades and maximal elements have maximal grades.

• grade : ฮฑ โ ๐
• covBy_grade : โ โฆa b : ฮฑโฆ, a โ b โ
• isMin_grade : โ โฆa : ฮฑโฆ, โ
• isMax_grade : โ โฆa : ฮฑโฆ, โ

Instances
def grade (๐ : Type u_1) {ฮฑ : Type u_3} [Preorder ๐] [Preorder ฮฑ] [GradeOrder ๐ ฮฑ] :
ฮฑ โ ๐

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
Instances For
theorem CovBy.grade (๐ : Type u_1) {ฮฑ : Type u_3} [Preorder ๐] [Preorder ฮฑ] [GradeOrder ๐ ฮฑ] {a : ฮฑ} {b : ฮฑ} (h : a โ b) :
theorem grade_strictMono {๐ : Type u_1} {ฮฑ : Type u_3} [Preorder ๐] [Preorder ฮฑ] [GradeOrder ๐ ฮฑ] :
theorem covBy_iff_lt_covBy_grade {๐ : Type u_1} {ฮฑ : Type u_3} [Preorder ๐] [Preorder ฮฑ] [GradeOrder ๐ ฮฑ] {a : ฮฑ} {b : ฮฑ} :
a โ b โ a < b โง grade ๐ a โ grade ๐ b
theorem IsMin.grade (๐ : Type u_1) {ฮฑ : Type u_3} [Preorder ฮฑ] [Preorder ๐] [GradeMinOrder ๐ ฮฑ] {a : ฮฑ} (h : ) :
@[simp]
theorem isMin_grade_iff {๐ : Type u_1} {ฮฑ : Type u_3} [Preorder ฮฑ] [Preorder ๐] [GradeMinOrder ๐ ฮฑ] {a : ฮฑ} :
theorem IsMax.grade (๐ : Type u_1) {ฮฑ : Type u_3} [Preorder ฮฑ] [Preorder ๐] [GradeMaxOrder ๐ ฮฑ] {a : ฮฑ} (h : ) :
@[simp]
theorem isMax_grade_iff {๐ : Type u_1} {ฮฑ : Type u_3} [Preorder ฮฑ] [Preorder ๐] [GradeMaxOrder ๐ ฮฑ] {a : ฮฑ} :
theorem grade_mono {๐ : Type u_1} {ฮฑ : Type u_3} [] [Preorder ๐] [GradeOrder ๐ ฮฑ] :
theorem grade_injective {๐ : Type u_1} {ฮฑ : Type u_3} [] [Preorder ๐] [GradeOrder ๐ ฮฑ] :
@[simp]
theorem grade_le_grade_iff {๐ : Type u_1} {ฮฑ : Type u_3} [] [Preorder ๐] [GradeOrder ๐ ฮฑ] {a : ฮฑ} {b : ฮฑ} :
@[simp]
theorem grade_lt_grade_iff {๐ : Type u_1} {ฮฑ : Type u_3} [] [Preorder ๐] [GradeOrder ๐ ฮฑ] {a : ฮฑ} {b : ฮฑ} :
@[simp]
theorem grade_eq_grade_iff {๐ : Type u_1} {ฮฑ : Type u_3} [] [Preorder ๐] [GradeOrder ๐ ฮฑ] {a : ฮฑ} {b : ฮฑ} :
theorem grade_ne_grade_iff {๐ : Type u_1} {ฮฑ : Type u_3} [] [Preorder ๐] [GradeOrder ๐ ฮฑ] {a : ฮฑ} {b : ฮฑ} :
theorem grade_covBy_grade_iff {๐ : Type u_1} {ฮฑ : Type u_3} [] [Preorder ๐] [GradeOrder ๐ ฮฑ] {a : ฮฑ} {b : ฮฑ} :
@[simp]
theorem grade_bot {๐ : Type u_1} {ฮฑ : Type u_3} [PartialOrder ๐] [Preorder ฮฑ] [OrderBot ๐] [OrderBot ฮฑ] [GradeMinOrder ๐ ฮฑ] :
@[simp]
theorem grade_top {๐ : Type u_1} {ฮฑ : Type u_3} [PartialOrder ๐] [Preorder ฮฑ] [OrderTop ๐] [OrderTop ฮฑ] [GradeMaxOrder ๐ ฮฑ] :

### Instances #

instance Preorder.toGradeBoundedOrder {ฮฑ : Type u_3} [Preorder ฮฑ] :
Equations
@[simp]
theorem grade_self {ฮฑ : Type u_3} [Preorder ฮฑ] (a : ฮฑ) :

#### Dual #

instance OrderDual.gradeOrder {๐ : Type u_1} {ฮฑ : Type u_3} [Preorder ๐] [Preorder ฮฑ] [GradeOrder ๐ ฮฑ] :
Equations
instance OrderDual.gradeMinOrder {๐ : Type u_1} {ฮฑ : Type u_3} [Preorder ๐] [Preorder ฮฑ] [GradeMaxOrder ๐ ฮฑ] :
Equations
instance OrderDual.gradeMaxOrder {๐ : Type u_1} {ฮฑ : Type u_3} [Preorder ๐] [Preorder ฮฑ] [GradeMinOrder ๐ ฮฑ] :
Equations
instance instGradeBoundedOrderOrderDual {๐ : Type u_1} {ฮฑ : Type u_3} [Preorder ๐] [Preorder ฮฑ] [GradeBoundedOrder ๐ ฮฑ] :
Equations
@[simp]
theorem grade_toDual {๐ : Type u_1} {ฮฑ : Type u_3} [Preorder ๐] [Preorder ฮฑ] [GradeOrder ๐ ฮฑ] (a : ฮฑ) :
@[simp]
theorem grade_ofDual {๐ : Type u_1} {ฮฑ : Type u_3} [Preorder ๐] [Preorder ฮฑ] [GradeOrder ๐ ฮฑ] (a : ฮฑแตแต) :

#### Lifting a graded order #

@[reducible, inline]
abbrev GradeOrder.liftLeft {๐ : Type u_1} {โ : Type u_2} {ฮฑ : Type u_3} [Preorder ๐] [Preorder โ] [Preorder ฮฑ] [GradeOrder ๐ ฮฑ] (f : ๐ โ โ) (hf : ) (hcovBy : โ (a b : ๐), a โ b โ f a โ f b) :

Lifts a graded order along a strictly monotone function.

Equations
Instances For
@[reducible, inline]
abbrev GradeMinOrder.liftLeft {๐ : Type u_1} {โ : Type u_2} {ฮฑ : Type u_3} [Preorder ๐] [Preorder โ] [Preorder ฮฑ] [GradeMinOrder ๐ ฮฑ] (f : ๐ โ โ) (hf : ) (hcovBy : โ (a b : ๐), a โ b โ f a โ f b) (hmin : โ (a : ๐), โ IsMin (f a)) :

Lifts a graded order along a strictly monotone function.

Equations
Instances For
@[reducible, inline]
abbrev GradeMaxOrder.liftLeft {๐ : Type u_1} {โ : Type u_2} {ฮฑ : Type u_3} [Preorder ๐] [Preorder โ] [Preorder ฮฑ] [GradeMaxOrder ๐ ฮฑ] (f : ๐ โ โ) (hf : ) (hcovBy : โ (a b : ๐), a โ b โ f a โ f b) (hmax : โ (a : ๐), โ IsMax (f a)) :

Lifts a graded order along a strictly monotone function.

Equations
Instances For
@[reducible, inline]
abbrev GradeBoundedOrder.liftLeft {๐ : Type u_1} {โ : Type u_2} {ฮฑ : Type u_3} [Preorder ๐] [Preorder โ] [Preorder ฮฑ] [GradeBoundedOrder ๐ ฮฑ] (f : ๐ โ โ) (hf : ) (hcovBy : โ (a b : ๐), a โ b โ f a โ f b) (hmin : โ (a : ๐), โ IsMin (f a)) (hmax : โ (a : ๐), โ IsMax (f a)) :

Lifts a graded order along a strictly monotone function.

Equations
Instances For
@[reducible, inline]
abbrev GradeOrder.liftRight {๐ : Type u_1} {ฮฑ : Type u_3} {ฮฒ : Type u_4} [Preorder ๐] [Preorder ฮฑ] [Preorder ฮฒ] [GradeOrder ๐ ฮฒ] (f : ฮฑ โ ฮฒ) (hf : ) (hcovBy : โ (a b : ฮฑ), a โ b โ f a โ f b) :

Lifts a graded order along a strictly monotone function.

Equations
Instances For
@[reducible, inline]
abbrev GradeMinOrder.liftRight {๐ : Type u_1} {ฮฑ : Type u_3} {ฮฒ : Type u_4} [Preorder ๐] [Preorder ฮฑ] [Preorder ฮฒ] [GradeMinOrder ๐ ฮฒ] (f : ฮฑ โ ฮฒ) (hf : ) (hcovBy : โ (a b : ฮฑ), a โ b โ f a โ f b) (hmin : โ (a : ฮฑ), โ IsMin (f a)) :

Lifts a graded order along a strictly monotone function.

Equations
Instances For
@[reducible, inline]
abbrev GradeMaxOrder.liftRight {๐ : Type u_1} {ฮฑ : Type u_3} {ฮฒ : Type u_4} [Preorder ๐] [Preorder ฮฑ] [Preorder ฮฒ] [GradeMaxOrder ๐ ฮฒ] (f : ฮฑ โ ฮฒ) (hf : ) (hcovBy : โ (a b : ฮฑ), a โ b โ f a โ f b) (hmax : โ (a : ฮฑ), โ IsMax (f a)) :

Lifts a graded order along a strictly monotone function.

Equations
Instances For
@[reducible, inline]
abbrev GradeBoundedOrder.liftRight {๐ : Type u_1} {ฮฑ : Type u_3} {ฮฒ : Type u_4} [Preorder ๐] [Preorder ฮฑ] [Preorder ฮฒ] [GradeBoundedOrder ๐ ฮฒ] (f : ฮฑ โ ฮฒ) (hf : ) (hcovBy : โ (a b : ฮฑ), a โ b โ f a โ f b) (hmin : โ (a : ฮฑ), โ IsMin (f a)) (hmax : โ (a : ฮฑ), โ IsMax (f a)) :

Lifts a graded order along a strictly monotone function.

Equations
Instances For

#### Fin n-graded to โ-graded to โค-graded #

@[reducible, inline]
abbrev GradeOrder.finToNat {ฮฑ : Type u_3} [Preorder ฮฑ] (n : โ) [GradeOrder (Fin n) ฮฑ] :

A Fin n-graded order is also โ-graded. We do not mark this an instance because n is not inferrable.

Equations
Instances For
@[reducible, inline]
abbrev GradeMinOrder.finToNat {ฮฑ : Type u_3} [Preorder ฮฑ] (n : โ) [GradeMinOrder (Fin n) ฮฑ] :

A Fin n-graded order is also โ-graded. We do not mark this an instance because n is not inferrable.

Equations
Instances For
instance GradeOrder.natToInt {ฮฑ : Type u_3} [Preorder ฮฑ] [] :
Equations