# Documentation

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 #

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

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 rather than ∀ a, IsMin a → 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.