# Documentation

Mathlib.Order.Circular

# Circular order hierarchy #

This file defines circular preorders, circular partial orders and circular orders.

## Hierarchy #

• A ternary "betweenness" relation btw : α → α → α → Prop forms a CircularOrder if it is
• reflexive: btw a a a
• cyclic: btw a b c → btw b c a
• antisymmetric: btw a b c → btw c b a → a = b ∨ b = c ∨ c = a
• total: btw a b c ∨ btw c b a along with a strict betweenness relation sbtw : α → α → α → Prop which respects sbtw a b c ↔ btw a b c ∧ ¬ btw c b a, analogously to how < and ≤ are related, and is
• transitive: sbtw a b c → sbtw b d c → sbtw a d c.
• A CircularPartialOrder drops totality.
• A CircularPreorder further drops antisymmetry.

The intuition is that a circular order is a circle and btw a b c means that going around clockwise from a you reach b before c (b is between a and 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 CircularPreorder, CircularPartialOrder and CircularOrder are subtler than between Preorder, PartialOrder, LinearOrder. In particular, one cannot simply extend the btw of a CircularPartialOrder to make it a CircularOrder.

One can translate from usual orders to circular ones by "closing the necklace at infinity". See LE.toBtw and LT.toSBtw. Going the other way involves "cutting the necklace" or "rolling the necklace open".

## Examples #

Some concrete circular orders one encounters in the wild are ZMod n for 0 < n, Circle, Real.Angle...

## Main definitions #

• Set.cIcc: Closed-closed circular interval.
• Set.cIoo: Open-open circular interval.

There's an unsolved diamond on OrderDual α here. The instances LE α → Btw αᵒᵈ and LT α → SBtw αᵒᵈ can each be inferred in two ways:

• LE αBtw αBtw αᵒᵈ vs LE αLE αᵒᵈBtw αᵒᵈ
• LT αSBtw αSBtw αᵒᵈ vs LT αLT αᵒᵈSBtw αᵒᵈ The fields are propeq, but not defeq. It is temporarily fixed by turning the circularizing instances into definitions.

## TODO #

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 cIco and 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 Circle, and RootsOfUnity M. What conditions do we need on M for this last one to work?

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?

• https://en.wikipedia.org/wiki/Cyclic_order
• https://en.wikipedia.org/wiki/Partial_cyclic_order

## Tags #

circular order, cyclic order, circularly ordered set, cyclically ordered set