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 isn + 1
). This corresponds toGradeBoundedOrder (Fin (n + 1)) ฮฑ
. - [Engel][engel1997]'s ranked orders are somewhere between
GradeOrder โ ฮฑ
andGradeMinOrder โ ฮฑ
, 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 grade0
and all maximal elements have the same grade. This is roughly a less bundled version ofGradeBoundedOrder (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]
The grading function.
grade : ฮฑ โ ๐grade
is strictly monotonic.grade_strictMono : StrictMono grade
An ๐
-graded order is an order ฮฑ
equipped with a strictly monotone function
grade ๐ : ฮฑ โ ๐โ ๐
which preserves order covering (Covby
).
Instances
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
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
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
Instances #
Equations
- Preorder.toGradeBoundedOrder = GradeBoundedOrder.mk (_ : โ (x : ฮฑ), IsMax x โ IsMax x)
Dual #
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Lifting a graded order #
Lifts a graded order along a strictly monotone function.
Equations
- One or more equations did not get rendered due to their size.
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)))
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)))
Lifts a graded order along a strictly monotone function.
Equations
- One or more equations did not get rendered due to their size.
Lifts a graded order along a strictly monotone function.
Equations
- One or more equations did not get rendered due to their size.
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)))
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)))
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 #
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)
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)
Equations
- GradeOrder.natToInt = GradeOrder.liftLeft (fun x => โx) Int.coe_nat_strictMono GradeOrder.natToInt.proof_1