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 #
grade_order
: Graded order.grade_min_order
: Graded order where minimal elements have minimal grades.grade_max_order
: Graded order where maximal elements have maximal grades.grade_bounded_order
: 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.grade_max_order
: Graded orders with maximal elements. All maximal elements have the same grade.max_grade
: The maximum grade in agrade_max_order
.order_embedding.grade
: The grade of an element in a linear order as an order embedding.
How to grade your order #
Here are the translations between common references and our grade_order
:
- Stanley 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 isn + 1
). This corresponds tograde_bounded_order (fin (n + 1)) ฮฑ
. - Engel's ranked orders are somewhere between
grade_order โ ฮฑ
andgrade_min_order โ ฮฑ
, in that he requiresโ a, is_min a โง grade โ a + 0
rather thanโ a, is_min a โ grade โ a = 0
. He defines a graded order as an order where all minimal elements have grade0
and all maximal elements have the same grade. This is roughly a less bundled version ofgrade_bounded_order (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 #
- grade : ฮฑ โ ๐
- grade_strict_mono : strict_mono grade_order.grade
- covby_grade : โ โฆa b : ฮฑโฆ, a โ b โ grade_order.grade a โ grade_order.grade b
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
- grade : ฮฑ โ ๐
- grade_strict_mono : strict_mono grade_min_order.grade
- covby_grade : โ โฆa b : ฮฑโฆ, a โ b โ grade_min_order.grade a โ grade_min_order.grade b
- is_min_grade : โ โฆa : ฮฑโฆ, is_min a โ is_min (grade_min_order.grade a)
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
- grade : ฮฑ โ ๐
- grade_strict_mono : strict_mono grade_max_order.grade
- covby_grade : โ โฆa b : ฮฑโฆ, a โ b โ grade_max_order.grade a โ grade_max_order.grade b
- is_max_grade : โ โฆa : ฮฑโฆ, is_max a โ is_max (grade_max_order.grade a)
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
- grade : ฮฑ โ ๐
- grade_strict_mono : strict_mono grade_bounded_order.grade
- covby_grade : โ โฆa b : ฮฑโฆ, a โ b โ grade_bounded_order.grade a โ grade_bounded_order.grade b
- is_min_grade : โ โฆa : ฮฑโฆ, is_min a โ is_min (grade_bounded_order.grade a)
- is_max_grade : โ โฆa : ฮฑโฆ, is_max a โ is_max (grade_bounded_order.grade a)
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
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 ๐ = grade_order.grade
Instances #
Equations
- preorder.to_grade_bounded_order = {grade := id ฮฑ, grade_strict_mono := _, covby_grade := _, is_min_grade := _, is_max_grade := _}
Dual #
Equations
- order_dual.grade_order = {grade := โorder_dual.to_dual โ grade ๐ โ โorder_dual.of_dual, grade_strict_mono := _, covby_grade := _}
Equations
- order_dual.grade_min_order = {grade := grade_order.grade order_dual.grade_order, grade_strict_mono := _, covby_grade := _, is_min_grade := _}
Equations
- order_dual.grade_max_order = {grade := grade_order.grade order_dual.grade_order, grade_strict_mono := _, covby_grade := _, is_max_grade := _}
Equations
- order_dual.grade_bounded_order = {grade := grade_min_order.grade order_dual.grade_min_order, grade_strict_mono := _, covby_grade := _, is_min_grade := _, is_max_grade := _}
Lifting a graded order #
Lifts a graded order along a strictly monotone function.
Equations
- grade_order.lift_left f hf hcovby = {grade := f โ grade ๐, grade_strict_mono := _, covby_grade := _}
Lifts a graded order along a strictly monotone function.
Equations
- grade_min_order.lift_left f hf hcovby hmin = {grade := grade_order.grade (grade_order.lift_left f hf hcovby), grade_strict_mono := _, covby_grade := _, is_min_grade := _}
Lifts a graded order along a strictly monotone function.
Equations
- grade_max_order.lift_left f hf hcovby hmax = {grade := grade_order.grade (grade_order.lift_left f hf hcovby), grade_strict_mono := _, covby_grade := _, is_max_grade := _}
Lifts a graded order along a strictly monotone function.
Equations
- grade_bounded_order.lift_left f hf hcovby hmin hmax = {grade := grade_min_order.grade (grade_min_order.lift_left f hf hcovby hmin), grade_strict_mono := _, covby_grade := _, is_min_grade := _, is_max_grade := _}
Lifts a graded order along a strictly monotone function.
Equations
- grade_order.lift_right f hf hcovby = {grade := grade ๐ โ f, grade_strict_mono := _, covby_grade := _}
Lifts a graded order along a strictly monotone function.
Equations
- grade_min_order.lift_right f hf hcovby hmin = {grade := grade_order.grade (grade_order.lift_right f hf hcovby), grade_strict_mono := _, covby_grade := _, is_min_grade := _}
Lifts a graded order along a strictly monotone function.
Equations
- grade_max_order.lift_right f hf hcovby hmax = {grade := grade_order.grade (grade_order.lift_right f hf hcovby), grade_strict_mono := _, covby_grade := _, is_max_grade := _}
Lifts a graded order along a strictly monotone function.
Equations
- grade_bounded_order.lift_right f hf hcovby hmin hmax = {grade := grade_min_order.grade (grade_min_order.lift_right f hf hcovby hmin), grade_strict_mono := _, covby_grade := _, is_min_grade := _, is_max_grade := _}
A fin n
-graded order is also โ
-graded. We do not mark this an instance because n
is not
inferrable.
Equations
A fin n
-graded order is also โ
-graded. We do not mark this an instance because n
is not
inferrable.
Equations
Equations
- grade_order.nat_to_int = grade_order.lift_left coe int.coe_nat_strict_mono grade_order.nat_to_int._proof_1