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

• 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.

How to grade your order

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∃ a, IsMin a ∧ grade ℕ a = 0∧ grade ℕ a = 0 rather than ∀ a, IsMin a → grade ℕ a = 0∀ a, IsMin a → grade ℕ a = 0→ 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.

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

References

• [Konrad Engel, Sperner Theory][engel1997]
• [Richard Stanley, Enumerative Combinatorics][stanley2012]

ink

class GradeOrder (𝕆 : Type u_1) (α : Type u_2) [inst : Preorder 𝕆] [inst : Preorder α] : Type (maxu_1u_2)

• The grading function.

  grade : α → 𝕆

• grade is strictly monotonic.

  grade_strictMono : StrictMono grade

• grade preserves Covby.

  covby_grade : ∀ ⦃a b : α⦄, a ⋖ b → grade a ⋖ grade b

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

ink

class GradeMinOrder (𝕆 : Type u_1) (α : Type u_2) [inst : Preorder 𝕆] [inst : Preorder α] extends GradeOrder : Type (maxu_1u_2)

• Minimal elements have minimal grades.

  is_min_grade : ∀ ⦃a : α⦄, IsMin a → IsMin (GradeOrder.grade a)

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

ink

class GradeMaxOrder (𝕆 : Type u_1) (α : Type u_2) [inst : Preorder 𝕆] [inst : Preorder α] extends GradeOrder : Type (maxu_1u_2)

• Maximal elements have maximal grades.

  is_max_grade : ∀ ⦃a : α⦄, IsMax a → IsMax (GradeOrder.grade a)

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

ink

class GradeBoundedOrder (𝕆 : Type u_1) (α : Type u_2) [inst : Preorder 𝕆] [inst : Preorder α] extends GradeMinOrder : Type (maxu_1u_2)

• Maximal elements have maximal grades.

  is_max_grade : ∀ ⦃a : α⦄, IsMax a → IsMax (GradeOrder.grade a)

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

ink

def grade (𝕆 : Type u_1) {α : Type u_2} [inst : Preorder α] [inst : Preorder 𝕆] [inst : 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

• grade 𝕆 = GradeOrder.grade

ink

theorem Covby.grade (𝕆 : Type u_2) {α : Type u_1} [inst : Preorder α] [inst : Preorder 𝕆] [inst : GradeOrder 𝕆 α] {a : α} {b : α} (h : a ⋖ b) : grade 𝕆 a ⋖ grade 𝕆 b

ink

theorem grade_strictMono {𝕆 : Type u_2} {α : Type u_1} [inst : Preorder α] [inst : Preorder 𝕆] [inst : GradeOrder 𝕆 α] : StrictMono (grade 𝕆)

ink

theorem covby_iff_lt_covby_grade {𝕆 : Type u_2} {α : Type u_1} [inst : Preorder α] [inst : Preorder 𝕆] [inst : GradeOrder 𝕆 α] {a : α} {b : α} : a ⋖ b ↔ a < b ∧ grade 𝕆 a ⋖ grade 𝕆 b

ink

theorem IsMin.grade (𝕆 : Type u_2) {α : Type u_1} [inst : Preorder α] [inst : Preorder 𝕆] [inst : GradeMinOrder 𝕆 α] {a : α} (h : IsMin a) : IsMin (grade 𝕆 a)

ink

@[simp]

theorem isMin_grade_iff {𝕆 : Type u_1} {α : Type u_2} [inst : Preorder α] [inst : Preorder 𝕆] [inst : GradeMinOrder 𝕆 α] {a : α} : IsMin (grade 𝕆 a) ↔ IsMin a

ink

theorem IsMax.grade (𝕆 : Type u_2) {α : Type u_1} [inst : Preorder α] [inst : Preorder 𝕆] [inst : GradeMaxOrder 𝕆 α] {a : α} (h : IsMax a) : IsMax (grade 𝕆 a)

ink

@[simp]

theorem isMax_grade_iff {𝕆 : Type u_1} {α : Type u_2} [inst : Preorder α] [inst : Preorder 𝕆] [inst : GradeMaxOrder 𝕆 α] {a : α} : IsMax (grade 𝕆 a) ↔ IsMax a

ink

theorem grade_mono {𝕆 : Type u_2} {α : Type u_1} [inst : PartialOrder α] [inst : Preorder 𝕆] [inst : GradeOrder 𝕆 α] : Monotone (grade 𝕆)

ink

theorem grade_injective {𝕆 : Type u_2} {α : Type u_1} [inst : LinearOrder α] [inst : Preorder 𝕆] [inst : GradeOrder 𝕆 α] : Function.Injective (grade 𝕆)

ink

@[simp]

theorem grade_le_grade_iff {𝕆 : Type u_1} {α : Type u_2} [inst : LinearOrder α] [inst : Preorder 𝕆] [inst : GradeOrder 𝕆 α] {a : α} {b : α} : grade 𝕆 a ≤ grade 𝕆 b ↔ a ≤ b

ink

@[simp]

theorem grade_lt_grade_iff {𝕆 : Type u_1} {α : Type u_2} [inst : LinearOrder α] [inst : Preorder 𝕆] [inst : GradeOrder 𝕆 α] {a : α} {b : α} : grade 𝕆 a < grade 𝕆 b ↔ a < b

ink

@[simp]

theorem grade_eq_grade_iff {𝕆 : Type u_1} {α : Type u_2} [inst : LinearOrder α] [inst : Preorder 𝕆] [inst : GradeOrder 𝕆 α] {a : α} {b : α} : grade 𝕆 a = grade 𝕆 b ↔ a = b

ink

theorem grade_ne_grade_iff {𝕆 : Type u_1} {α : Type u_2} [inst : LinearOrder α] [inst : Preorder 𝕆] [inst : GradeOrder 𝕆 α] {a : α} {b : α} : grade 𝕆 a ≠ grade 𝕆 b ↔ a ≠ b

ink

theorem grade_covby_grade_iff {𝕆 : Type u_1} {α : Type u_2} [inst : LinearOrder α] [inst : Preorder 𝕆] [inst : GradeOrder 𝕆 α] {a : α} {b : α} : grade 𝕆 a ⋖ grade 𝕆 b ↔ a ⋖ b

ink

@[simp]

theorem grade_bot {𝕆 : Type u_1} {α : Type u_2} [inst : PartialOrder 𝕆] [inst : Preorder α] [inst : OrderBot 𝕆] [inst : OrderBot α] [inst : GradeMinOrder 𝕆 α] : grade 𝕆 ⊥ = ⊥

ink

@[simp]

theorem grade_top {𝕆 : Type u_1} {α : Type u_2} [inst : PartialOrder 𝕆] [inst : Preorder α] [inst : OrderTop 𝕆] [inst : OrderTop α] [inst : GradeMaxOrder 𝕆 α] : grade 𝕆 ⊤ = ⊤

Instances

ink

instance Preorder.toGradeBoundedOrder {α : Type u_1} [inst : Preorder α] : GradeBoundedOrder α α

Equations

• Preorder.toGradeBoundedOrder = GradeBoundedOrder.mk (_ : ∀ (x : α), IsMax x → IsMax x)

ink

@[simp]

theorem grade_self {α : Type u_1} [inst : Preorder α] (a : α) : grade α a = a

Dual

ink

instance OrderDual.gradeOrder {𝕆 : Type u_1} {α : Type u_2} [inst : Preorder 𝕆] [inst : Preorder α] [inst : GradeOrder 𝕆 α] : GradeOrder 𝕆ᵒᵈ αᵒᵈ

Equations

• One or more equations did not get rendered due to their size.

ink

instance OrderDual.gradeMinOrder {𝕆 : Type u_1} {α : Type u_2} [inst : Preorder 𝕆] [inst : Preorder α] [inst : GradeMaxOrder 𝕆 α] : GradeMinOrder 𝕆ᵒᵈ αᵒᵈ

Equations

• OrderDual.gradeMinOrder = let src := OrderDual.gradeOrder; GradeMinOrder.mk (_ : ∀ (x : αᵒᵈ), IsMax x → IsMax (grade 𝕆 x))

ink

instance OrderDual.gradeMaxOrder {𝕆 : Type u_1} {α : Type u_2} [inst : Preorder 𝕆] [inst : Preorder α] [inst : GradeMinOrder 𝕆 α] : GradeMaxOrder 𝕆ᵒᵈ αᵒᵈ

Equations

• OrderDual.gradeMaxOrder = let src := OrderDual.gradeOrder; GradeMaxOrder.mk (_ : ∀ (x : αᵒᵈ), IsMin x → IsMin (grade 𝕆 x))

ink

instance instGradeBoundedOrderOrderDualOrderDualPreorderPreorder {𝕆 : Type u_1} {α : Type u_2} [inst : Preorder 𝕆] [inst : Preorder α] [inst : GradeBoundedOrder 𝕆 α] : GradeBoundedOrder 𝕆ᵒᵈ αᵒᵈ

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem grade_toDual {𝕆 : Type u_1} {α : Type u_2} [inst : Preorder 𝕆] [inst : Preorder α] [inst : GradeOrder 𝕆 α] (a : α) : grade 𝕆ᵒᵈ (↑OrderDual.toDual a) = ↑OrderDual.toDual (grade 𝕆 a)

ink

@[simp]

theorem grade_ofDual {𝕆 : Type u_1} {α : Type u_2} [inst : Preorder 𝕆] [inst : Preorder α] [inst : GradeOrder 𝕆 α] (a : αᵒᵈ) : grade 𝕆 (↑OrderDual.ofDual a) = ↑OrderDual.ofDual (grade 𝕆ᵒᵈ a)

Lifting a graded order

ink

def GradeOrder.liftLeft {𝕆 : Type u_1} {ℙ : Type u_2} {α : Type u_3} [inst : Preorder 𝕆] [inst : Preorder ℙ] [inst : Preorder α] [inst : GradeOrder 𝕆 α] (f : 𝕆 → ℙ) (hf : StrictMono f) (hcovby : ∀ (a b : 𝕆), a ⋖ b → f a ⋖ f b) : GradeOrder ℙ α

Lifts a graded order along a strictly monotone function.

Equations

• One or more equations did not get rendered due to their size.

ink

def GradeMinOrder.liftLeft {𝕆 : Type u_1} {ℙ : Type u_2} {α : Type u_3} [inst : Preorder 𝕆] [inst : Preorder ℙ] [inst : Preorder α] [inst : GradeMinOrder 𝕆 α] (f : 𝕆 → ℙ) (hf : StrictMono f) (hcovby : ∀ (a b : 𝕆), a ⋖ b → f a ⋖ f b) (hmin : ∀ (a : 𝕆), IsMin a → IsMin (f a)) : GradeMinOrder ℙ α

Lifts a graded order along a strictly monotone function.

Equations

• GradeMinOrder.liftLeft f hf hcovby hmin = let src := GradeOrder.liftLeft f hf hcovby; GradeMinOrder.mk (_ : ∀ (x : α), IsMin x → IsMin (f (GradeOrder.grade x)))

ink

def GradeMaxOrder.liftLeft {𝕆 : Type u_1} {ℙ : Type u_2} {α : Type u_3} [inst : Preorder 𝕆] [inst : Preorder ℙ] [inst : Preorder α] [inst : GradeMaxOrder 𝕆 α] (f : 𝕆 → ℙ) (hf : StrictMono f) (hcovby : ∀ (a b : 𝕆), a ⋖ b → f a ⋖ f b) (hmax : ∀ (a : 𝕆), IsMax a → IsMax (f a)) : GradeMaxOrder ℙ α

Lifts a graded order along a strictly monotone function.

Equations

• GradeMaxOrder.liftLeft f hf hcovby hmax = let src := GradeOrder.liftLeft f hf hcovby; GradeMaxOrder.mk (_ : ∀ (x : α), IsMax x → IsMax (f (GradeOrder.grade x)))

ink

def GradeBoundedOrder.liftLeft {𝕆 : Type u_1} {ℙ : Type u_2} {α : Type u_3} [inst : Preorder 𝕆] [inst : Preorder ℙ] [inst : Preorder α] [inst : GradeBoundedOrder 𝕆 α] (f : 𝕆 → ℙ) (hf : StrictMono f) (hcovby : ∀ (a b : 𝕆), a ⋖ b → f a ⋖ f b) (hmin : ∀ (a : 𝕆), IsMin a → IsMin (f a)) (hmax : ∀ (a : 𝕆), IsMax a → IsMax (f a)) : GradeBoundedOrder ℙ α

Lifts a graded order along a strictly monotone function.

Equations

• One or more equations did not get rendered due to their size.

ink

def GradeOrder.liftRight {𝕆 : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder 𝕆] [inst : Preorder α] [inst : Preorder β] [inst : GradeOrder 𝕆 β] (f : α → β) (hf : StrictMono f) (hcovby : ∀ (a b : α), a ⋖ b → f a ⋖ f b) : GradeOrder 𝕆 α

Lifts a graded order along a strictly monotone function.

Equations

• One or more equations did not get rendered due to their size.

ink

def GradeMinOrder.liftRight {𝕆 : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder 𝕆] [inst : Preorder α] [inst : Preorder β] [inst : GradeMinOrder 𝕆 β] (f : α → β) (hf : StrictMono f) (hcovby : ∀ (a b : α), a ⋖ b → f a ⋖ f b) (hmin : ∀ (a : α), IsMin a → IsMin (f a)) : GradeMinOrder 𝕆 α

Lifts a graded order along a strictly monotone function.

Equations

• GradeMinOrder.liftRight f hf hcovby hmin = let src := GradeOrder.liftRight f hf hcovby; GradeMinOrder.mk (_ : ∀ (x : α), IsMin x → IsMin (grade 𝕆 (f x)))

ink

def GradeMaxOrder.liftRight {𝕆 : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder 𝕆] [inst : Preorder α] [inst : Preorder β] [inst : GradeMaxOrder 𝕆 β] (f : α → β) (hf : StrictMono f) (hcovby : ∀ (a b : α), a ⋖ b → f a ⋖ f b) (hmax : ∀ (a : α), IsMax a → IsMax (f a)) : GradeMaxOrder 𝕆 α

Lifts a graded order along a strictly monotone function.

Equations

• GradeMaxOrder.liftRight f hf hcovby hmax = let src := GradeOrder.liftRight f hf hcovby; GradeMaxOrder.mk (_ : ∀ (x : α), IsMax x → IsMax (grade 𝕆 (f x)))

ink

def GradeBoundedOrder.liftRight {𝕆 : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder 𝕆] [inst : Preorder α] [inst : Preorder β] [inst : GradeBoundedOrder 𝕆 β] (f : α → β) (hf : StrictMono f) (hcovby : ∀ (a b : α), a ⋖ b → f a ⋖ f b) (hmin : ∀ (a : α), IsMin a → IsMin (f a)) (hmax : ∀ (a : α), IsMax a → IsMax (f a)) : GradeBoundedOrder 𝕆 α

Lifts a graded order along a strictly monotone function.

Equations

• One or more equations did not get rendered due to their size.

fin n-graded to ℕ-graded to ℤ-graded

ink

def GradeOrder.finToNat {α : Type u_1} [inst : Preorder α] (n : ℕ) [inst : GradeOrder (Fin n) α] : GradeOrder ℕ α

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

Equations

• GradeOrder.finToNat n = GradeOrder.liftLeft Fin.val (_ : StrictMono Fin.val) (_ : ∀ (x x_1 : Fin n), x ⋖ x_1 → ↑x ⋖ ↑x_1)

ink

def GradeMinOrder.finToNat {α : Type u_1} [inst : Preorder α] (n : ℕ) [inst : GradeMinOrder (Fin n) α] : GradeMinOrder ℕ α

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

Equations

• GradeMinOrder.finToNat n = GradeMinOrder.liftLeft Fin.val (_ : StrictMono Fin.val) (_ : ∀ (x x_1 : Fin n), x ⋖ x_1 → ↑x ⋖ ↑x_1) (_ : ∀ (a : Fin n), IsMin a → IsMin ↑a)

ink

instance GradeOrder.natToInt {α : Type u_1} [inst : Preorder α] [inst : GradeOrder ℕ α] : GradeOrder ℤ α

Equations

• GradeOrder.natToInt = GradeOrder.liftLeft (fun x => ↑x) Int.coe_nat_strictMono GradeOrder.natToInt.proof_1