Documentation

Mathlib.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 GradeOrder:

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

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

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

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

        Instances
          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
          theorem Covby.grade (๐•† : Type u_2) {ฮฑ : Type u_1} [inst : Preorder ฮฑ] [inst : Preorder ๐•†] [inst : GradeOrder ๐•† ฮฑ] {a : ฮฑ} {b : ฮฑ} (h : a โ‹– b) :
          grade ๐•† a โ‹– grade ๐•† b
          theorem grade_strictMono {๐•† : Type u_2} {ฮฑ : Type u_1} [inst : Preorder ฮฑ] [inst : Preorder ๐•†] [inst : GradeOrder ๐•† ฮฑ] :
          StrictMono (grade ๐•†)
          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
          theorem IsMin.grade (๐•† : Type u_2) {ฮฑ : Type u_1} [inst : Preorder ฮฑ] [inst : Preorder ๐•†] [inst : GradeMinOrder ๐•† ฮฑ] {a : ฮฑ} (h : IsMin a) :
          IsMin (grade ๐•† a)
          @[simp]
          theorem isMin_grade_iff {๐•† : Type u_1} {ฮฑ : Type u_2} [inst : Preorder ฮฑ] [inst : Preorder ๐•†] [inst : GradeMinOrder ๐•† ฮฑ] {a : ฮฑ} :
          IsMin (grade ๐•† a) โ†” IsMin a
          theorem IsMax.grade (๐•† : Type u_2) {ฮฑ : Type u_1} [inst : Preorder ฮฑ] [inst : Preorder ๐•†] [inst : GradeMaxOrder ๐•† ฮฑ] {a : ฮฑ} (h : IsMax a) :
          IsMax (grade ๐•† a)
          @[simp]
          theorem isMax_grade_iff {๐•† : Type u_1} {ฮฑ : Type u_2} [inst : Preorder ฮฑ] [inst : Preorder ๐•†] [inst : GradeMaxOrder ๐•† ฮฑ] {a : ฮฑ} :
          IsMax (grade ๐•† a) โ†” IsMax a
          theorem grade_mono {๐•† : Type u_2} {ฮฑ : Type u_1} [inst : PartialOrder ฮฑ] [inst : Preorder ๐•†] [inst : GradeOrder ๐•† ฮฑ] :
          Monotone (grade ๐•†)
          theorem grade_injective {๐•† : Type u_2} {ฮฑ : Type u_1} [inst : LinearOrder ฮฑ] [inst : Preorder ๐•†] [inst : GradeOrder ๐•† ฮฑ] :
          @[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
          @[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
          @[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
          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
          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
          @[simp]
          theorem grade_bot {๐•† : Type u_1} {ฮฑ : Type u_2} [inst : PartialOrder ๐•†] [inst : Preorder ฮฑ] [inst : OrderBot ๐•†] [inst : OrderBot ฮฑ] [inst : GradeMinOrder ๐•† ฮฑ] :
          @[simp]
          theorem grade_top {๐•† : Type u_1} {ฮฑ : Type u_2} [inst : PartialOrder ๐•†] [inst : Preorder ฮฑ] [inst : OrderTop ๐•†] [inst : OrderTop ฮฑ] [inst : GradeMaxOrder ๐•† ฮฑ] :

          Instances #

          instance Preorder.toGradeBoundedOrder {ฮฑ : Type u_1} [inst : Preorder ฮฑ] :
          GradeBoundedOrder ฮฑ ฮฑ
          Equations
          @[simp]
          theorem grade_self {ฮฑ : Type u_1} [inst : Preorder ฮฑ] (a : ฮฑ) :
          grade ฮฑ a = a

          Dual #

          instance OrderDual.gradeOrder {๐•† : Type u_1} {ฮฑ : Type u_2} [inst : Preorder ๐•†] [inst : Preorder ฮฑ] [inst : GradeOrder ๐•† ฮฑ] :
          Equations
          • One or more equations did not get rendered due to their size.
          instance OrderDual.gradeMinOrder {๐•† : Type u_1} {ฮฑ : Type u_2} [inst : Preorder ๐•†] [inst : Preorder ฮฑ] [inst : GradeMaxOrder ๐•† ฮฑ] :
          Equations
          instance OrderDual.gradeMaxOrder {๐•† : Type u_1} {ฮฑ : Type u_2} [inst : Preorder ๐•†] [inst : Preorder ฮฑ] [inst : GradeMinOrder ๐•† ฮฑ] :
          Equations
          instance instGradeBoundedOrderOrderDualOrderDualPreorderPreorder {๐•† : Type u_1} {ฮฑ : Type u_2} [inst : Preorder ๐•†] [inst : Preorder ฮฑ] [inst : GradeBoundedOrder ๐•† ฮฑ] :
          Equations
          • One or more equations did not get rendered due to their size.
          @[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)
          @[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 #

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

          def GradeOrder.finToNat {ฮฑ : Type u_1} [inst : Preorder ฮฑ] (n : โ„•) [inst : GradeOrder (Fin n) ฮฑ] :

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

          Equations
          def GradeMinOrder.finToNat {ฮฑ : Type u_1} [inst : Preorder ฮฑ] (n : โ„•) [inst : GradeMinOrder (Fin n) ฮฑ] :

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

          Equations
          instance GradeOrder.natToInt {ฮฑ : Type u_1} [inst : Preorder ฮฑ] [inst : GradeOrder โ„• ฮฑ] :
          Equations