Circular order hierarchy #
This file defines circular preorders, circular partial orders and circular orders.
- A ternary "betweenness" relation
btw : α → α → α → Propforms a
CircularOrderif it is
btw a a a
btw a b c → btw b c a
btw a b c → btw c b a → a = b ∨ b = c ∨ c = a
btw a b c ∨ btw c b aalong with a strict betweenness relation
sbtw : α → α → α → Propwhich respects
sbtw a b c ↔ btw a b c ∧ ¬ btw c b a, analogously to how
≤are related, and is
sbtw a b c → sbtw b d c → sbtw a d c.
CircularPreorderfurther drops antisymmetry.
The intuition is that a circular order is a circle and
btw a b c means that going around
a you reach
b is between
c is meaningless on an
unoriented circle). A circular partial order is several, potentially intersecting, circles. A
circular preorder is like a circular partial order, but several points can coexist.
Note that the relations between
are subtler than between
LinearOrder. In particular, one cannot
simply extend the
btw of a
CircularPartialOrder to make it a
One can translate from usual orders to circular ones by "closing the necklace at infinity". See
LT.toSBtw. Going the other way involves "cutting the necklace" or
"rolling the necklace open".
Some concrete circular orders one encounters in the wild are
ZMod n for
0 < n,
Main definitions #
SBtw αᵒᵈThe fields are propeq, but not defeq. It is temporarily fixed by turning the circularizing instances into definitions.
Antisymmetry is quite weak in the sense that there's no way to discriminate which two points are
equal. This prevents defining closed-open intervals
cIoc in the neat
=-less way. We
currently haven't defined them at all.
What is the correct generality of "rolling the necklace" open? At least, this works for
α × β and
β × α where
α is a circular order and
β is a linear order.
What's next is to define circular groups and provide instances for
ZMod n, the usual circle group
RootsOfUnity M. What conditions do we need on
M for this last one
We should have circular order homomorphisms. The typical example is
days_to_month : days_of_the_year →c months_of_the_year which relates the circular order of days
and the circular order of months. Is
α →c β a good notation?
circular order, cyclic order, circularly ordered set, cyclically ordered set
a. This is motivated by imagining three points on a circle.
Strict betweenness is given by betweenness in one direction and non-betweenness in the other.
cbut not between
a, then we say
bis strictly between
For any fixed
fun a b ↦ sbtw a b cis a transitive relation.
cin that "order", if we have
dis strictly between
cand also between
a, then at least one pair of points among
A circular partial order is the analogue of a partial order where you can loop around.
< are replaced by ternary relations
btw is reflexive, cyclic and
sbtw is transitive.
For any triple of points, the second is between the other two one way or another.
A circular order is the analogue of a linear order where you can loop around.
replaced by ternary relations
btw is reflexive, cyclic, antisymmetric and total.
sbtw is transitive.