Documentation

Mathlib.Order.Grade

Graded orders #

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 #

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 #

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

Instances
    source
    theorem GradeOrder.grade_strictMono {๐•† : Type u_5} {ฮฑ : Type u_6} [Preorder ๐•†] [Preorder ฮฑ] [self : GradeOrder ๐•† ฮฑ] :
    StrictMono GradeOrder.grade

    grade is strictly monotonic.

    source
    theorem GradeOrder.covBy_grade {๐•† : Type u_5} {ฮฑ : Type u_6} [Preorder ๐•†] [Preorder ฮฑ] [self : GradeOrder ๐•† ฮฑ] โฆƒa : ฮฑโฆ„ โฆƒb : ฮฑโฆ„ :
    a โ‹– b โ†’ GradeOrder.grade a โ‹– GradeOrder.grade b

    grade preserves CovBy.

    source
    class GradeMinOrder (๐•† : Type u_5) (ฮฑ : Type u_6) [Preorder ๐•†] [Preorder ฮฑ] extends GradeOrder :
    Type (max u_5 u_6)

    An ๐•†-graded order where minimal elements have minimal grades.

    Instances
      source
      theorem GradeMinOrder.isMin_grade {๐•† : Type u_5} {ฮฑ : Type u_6} [Preorder ๐•†] [Preorder ฮฑ] [self : GradeMinOrder ๐•† ฮฑ] โฆƒa : ฮฑโฆ„ :
      IsMin a โ†’ IsMin (GradeOrder.grade a)

      Minimal elements have minimal grades.

      source
      class GradeMaxOrder (๐•† : Type u_5) (ฮฑ : Type u_6) [Preorder ๐•†] [Preorder ฮฑ] extends GradeOrder :
      Type (max u_5 u_6)

      An ๐•†-graded order where maximal elements have maximal grades.

      Instances
        source
        theorem GradeMaxOrder.isMax_grade {๐•† : Type u_5} {ฮฑ : Type u_6} [Preorder ๐•†] [Preorder ฮฑ] [self : GradeMaxOrder ๐•† ฮฑ] โฆƒa : ฮฑโฆ„ :
        IsMax a โ†’ IsMax (GradeOrder.grade a)

        Maximal elements have maximal grades.

        source
        class GradeBoundedOrder (๐•† : Type u_5) (ฮฑ : Type u_6) [Preorder ๐•†] [Preorder ฮฑ] extends GradeMinOrder :
        Type (max u_5 u_6)

        An ๐•†-graded order where minimal elements have minimal grades and maximal elements have maximal grades.

        Instances
          source
          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
          • grade ๐•† = GradeOrder.grade
          Instances For
            source
            theorem CovBy.grade (๐•† : Type u_1) {ฮฑ : Type u_3} [Preorder ๐•†] [Preorder ฮฑ] [GradeOrder ๐•† ฮฑ] {a : ฮฑ} {b : ฮฑ} (h : a โ‹– b) :
            grade ๐•† a โ‹– grade ๐•† b
            source
            theorem grade_strictMono {๐•† : Type u_1} {ฮฑ : Type u_3} [Preorder ๐•†] [Preorder ฮฑ] [GradeOrder ๐•† ฮฑ] :
            StrictMono (grade ๐•†)
            source
            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
            source
            theorem IsMin.grade (๐•† : Type u_1) {ฮฑ : Type u_3} [Preorder ฮฑ] [Preorder ๐•†] [GradeMinOrder ๐•† ฮฑ] {a : ฮฑ} (h : IsMin a) :
            IsMin (grade ๐•† a)
            source
            @[simp]
            theorem isMin_grade_iff {๐•† : Type u_1} {ฮฑ : Type u_3} [Preorder ฮฑ] [Preorder ๐•†] [GradeMinOrder ๐•† ฮฑ] {a : ฮฑ} :
            IsMin (grade ๐•† a) โ†” IsMin a
            source
            theorem IsMax.grade (๐•† : Type u_1) {ฮฑ : Type u_3} [Preorder ฮฑ] [Preorder ๐•†] [GradeMaxOrder ๐•† ฮฑ] {a : ฮฑ} (h : IsMax a) :
            IsMax (grade ๐•† a)
            source
            @[simp]
            theorem isMax_grade_iff {๐•† : Type u_1} {ฮฑ : Type u_3} [Preorder ฮฑ] [Preorder ๐•†] [GradeMaxOrder ๐•† ฮฑ] {a : ฮฑ} :
            IsMax (grade ๐•† a) โ†” IsMax a
            source
            theorem grade_mono {๐•† : Type u_1} {ฮฑ : Type u_3} [PartialOrder ฮฑ] [Preorder ๐•†] [GradeOrder ๐•† ฮฑ] :
            Monotone (grade ๐•†)
            source
            theorem grade_injective {๐•† : Type u_1} {ฮฑ : Type u_3} [LinearOrder ฮฑ] [Preorder ๐•†] [GradeOrder ๐•† ฮฑ] :
            Function.Injective (grade ๐•†)
            source
            @[simp]
            theorem grade_le_grade_iff {๐•† : Type u_1} {ฮฑ : Type u_3} [LinearOrder ฮฑ] [Preorder ๐•†] [GradeOrder ๐•† ฮฑ] {a : ฮฑ} {b : ฮฑ} :
            grade ๐•† a โ‰ค grade ๐•† b โ†” a โ‰ค b
            source
            @[simp]
            theorem grade_lt_grade_iff {๐•† : Type u_1} {ฮฑ : Type u_3} [LinearOrder ฮฑ] [Preorder ๐•†] [GradeOrder ๐•† ฮฑ] {a : ฮฑ} {b : ฮฑ} :
            grade ๐•† a < grade ๐•† b โ†” a < b
            source
            @[simp]
            theorem grade_eq_grade_iff {๐•† : Type u_1} {ฮฑ : Type u_3} [LinearOrder ฮฑ] [Preorder ๐•†] [GradeOrder ๐•† ฮฑ] {a : ฮฑ} {b : ฮฑ} :
            grade ๐•† a = grade ๐•† b โ†” a = b
            source
            theorem grade_ne_grade_iff {๐•† : Type u_1} {ฮฑ : Type u_3} [LinearOrder ฮฑ] [Preorder ๐•†] [GradeOrder ๐•† ฮฑ] {a : ฮฑ} {b : ฮฑ} :
            grade ๐•† a โ‰  grade ๐•† b โ†” a โ‰  b
            source
            theorem grade_covBy_grade_iff {๐•† : Type u_1} {ฮฑ : Type u_3} [LinearOrder ฮฑ] [Preorder ๐•†] [GradeOrder ๐•† ฮฑ] {a : ฮฑ} {b : ฮฑ} :
            grade ๐•† a โ‹– grade ๐•† b โ†” a โ‹– b
            source
            @[simp]
            theorem grade_bot {๐•† : Type u_1} {ฮฑ : Type u_3} [PartialOrder ๐•†] [Preorder ฮฑ] [OrderBot ๐•†] [OrderBot ฮฑ] [GradeMinOrder ๐•† ฮฑ] :
            grade ๐•† โŠฅ = โŠฅ
            source
            @[simp]
            theorem grade_top {๐•† : Type u_1} {ฮฑ : Type u_3} [PartialOrder ๐•†] [Preorder ฮฑ] [OrderTop ๐•†] [OrderTop ฮฑ] [GradeMaxOrder ๐•† ฮฑ] :
            grade ๐•† โŠค = โŠค

            Instances #

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

            Dual #

            source
            instance OrderDual.gradeOrder {๐•† : Type u_1} {ฮฑ : Type u_3} [Preorder ๐•†] [Preorder ฮฑ] [GradeOrder ๐•† ฮฑ] :
            GradeOrder ๐•†แต’แตˆ ฮฑแต’แตˆ
            Equations
            • OrderDual.gradeOrder = { grade := โ‡‘OrderDual.toDual โˆ˜ grade ๐•† โˆ˜ โ‡‘OrderDual.ofDual, grade_strictMono := โ‹ฏ, covBy_grade := โ‹ฏ }
            source
            instance OrderDual.gradeMinOrder {๐•† : Type u_1} {ฮฑ : Type u_3} [Preorder ๐•†] [Preorder ฮฑ] [GradeMaxOrder ๐•† ฮฑ] :
            GradeMinOrder ๐•†แต’แตˆ ฮฑแต’แตˆ
            Equations
            • OrderDual.gradeMinOrder = let __src := OrderDual.gradeOrder; GradeMinOrder.mk โ‹ฏ
            source
            instance OrderDual.gradeMaxOrder {๐•† : Type u_1} {ฮฑ : Type u_3} [Preorder ๐•†] [Preorder ฮฑ] [GradeMinOrder ๐•† ฮฑ] :
            GradeMaxOrder ๐•†แต’แตˆ ฮฑแต’แตˆ
            Equations
            • OrderDual.gradeMaxOrder = let __src := OrderDual.gradeOrder; GradeMaxOrder.mk โ‹ฏ
            source
            instance instGradeBoundedOrderOrderDual {๐•† : Type u_1} {ฮฑ : Type u_3} [Preorder ๐•†] [Preorder ฮฑ] [GradeBoundedOrder ๐•† ฮฑ] :
            GradeBoundedOrder ๐•†แต’แตˆ ฮฑแต’แตˆ
            Equations
            • instGradeBoundedOrderOrderDual = let __src := OrderDual.gradeMinOrder; let __src_1 := OrderDual.gradeMaxOrder; GradeBoundedOrder.mk โ‹ฏ
            source
            @[simp]
            theorem grade_toDual {๐•† : Type u_1} {ฮฑ : Type u_3} [Preorder ๐•†] [Preorder ฮฑ] [GradeOrder ๐•† ฮฑ] (a : ฮฑ) :
            grade ๐•†แต’แตˆ (OrderDual.toDual a) = OrderDual.toDual (grade ๐•† a)
            source
            @[simp]
            theorem grade_ofDual {๐•† : Type u_1} {ฮฑ : Type u_3} [Preorder ๐•†] [Preorder ฮฑ] [GradeOrder ๐•† ฮฑ] (a : ฮฑแต’แตˆ) :
            grade ๐•† (OrderDual.ofDual a) = OrderDual.ofDual (grade ๐•†แต’แตˆ a)

            Lifting a graded order #

            source
            @[reducible, inline]
            abbrev GradeOrder.liftLeft {๐•† : Type u_1} {โ„™ : Type u_2} {ฮฑ : Type u_3} [Preorder ๐•†] [Preorder โ„™] [Preorder ฮฑ] [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
            Instances For
              source
              @[reducible, inline]
              abbrev GradeMinOrder.liftLeft {๐•† : Type u_1} {โ„™ : Type u_2} {ฮฑ : Type u_3} [Preorder ๐•†] [Preorder โ„™] [Preorder ฮฑ] [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
              Instances For
                source
                @[reducible, inline]
                abbrev GradeMaxOrder.liftLeft {๐•† : Type u_1} {โ„™ : Type u_2} {ฮฑ : Type u_3} [Preorder ๐•†] [Preorder โ„™] [Preorder ฮฑ] [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
                Instances For
                  source
                  @[reducible, inline]
                  abbrev GradeBoundedOrder.liftLeft {๐•† : Type u_1} {โ„™ : Type u_2} {ฮฑ : Type u_3} [Preorder ๐•†] [Preorder โ„™] [Preorder ฮฑ] [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
                  Instances For
                    source
                    @[reducible, inline]
                    abbrev GradeOrder.liftRight {๐•† : Type u_1} {ฮฑ : Type u_3} {ฮฒ : Type u_4} [Preorder ๐•†] [Preorder ฮฑ] [Preorder ฮฒ] [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
                    Instances For
                      source
                      @[reducible, inline]
                      abbrev GradeMinOrder.liftRight {๐•† : Type u_1} {ฮฑ : Type u_3} {ฮฒ : Type u_4} [Preorder ๐•†] [Preorder ฮฑ] [Preorder ฮฒ] [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
                      Instances For
                        source
                        @[reducible, inline]
                        abbrev GradeMaxOrder.liftRight {๐•† : Type u_1} {ฮฑ : Type u_3} {ฮฒ : Type u_4} [Preorder ๐•†] [Preorder ฮฑ] [Preorder ฮฒ] [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
                        Instances For
                          source
                          @[reducible, inline]
                          abbrev GradeBoundedOrder.liftRight {๐•† : Type u_1} {ฮฑ : Type u_3} {ฮฒ : Type u_4} [Preorder ๐•†] [Preorder ฮฑ] [Preorder ฮฒ] [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
                          Instances For

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

                            source
                            @[reducible, inline]
                            abbrev GradeOrder.finToNat {ฮฑ : Type u_3} [Preorder ฮฑ] (n : โ„•) [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
                            Instances For
                              source
                              @[reducible, inline]
                              abbrev GradeMinOrder.finToNat {ฮฑ : Type u_3} [Preorder ฮฑ] (n : โ„•) [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
                              Instances For
                                source
                                instance GradeOrder.natToInt {ฮฑ : Type u_3} [Preorder ฮฑ] [GradeOrder โ„• ฮฑ] :
                                GradeOrder โ„ค ฮฑ
                                Equations
                                source
                                theorem GradeOrder.wellFoundedLT {ฮฑ : Type u_3} (๐•† : Type u_5) [Preorder ฮฑ] [Preorder ๐•†] [GradeOrder ๐•† ฮฑ] [WellFoundedLT ๐•†] :
                                WellFoundedLT ฮฑ
                                source
                                theorem GradeOrder.wellFoundedGT {ฮฑ : Type u_3} (๐•† : Type u_5) [Preorder ฮฑ] [Preorder ๐•†] [GradeOrder ๐•† ฮฑ] [WellFoundedGT ๐•†] :
                                WellFoundedGT ฮฑ
                                source
                                instance instWellFoundedLTOfGradeOrderNat {ฮฑ : Type u_3} [Preorder ฮฑ] [GradeOrder โ„• ฮฑ] :
                                WellFoundedLT ฮฑ
                                Equations
                                • โ‹ฏ = โ‹ฏ
                                source
                                instance instWellFoundedGTOfGradeOrderOrderDualNat {ฮฑ : Type u_3} [Preorder ฮฑ] [GradeOrder โ„•แต’แตˆ ฮฑ] :
                                WellFoundedGT ฮฑ
                                Equations
                                • โ‹ฏ = โ‹ฏ