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.

Notes

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?

References

• 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

class Btw (α : Type u_1) : Type u_1

Syntax typeclass for a betweenness relation.

• btw : α → α → α → Prop

  Betweenness for circular orders. btw a b c states that b is between a and c (in that order).

class SBtw (α : Type u_1) : Type u_1

Syntax typeclass for a strict betweenness relation.

• sbtw : α → α → α → Prop

  Strict betweenness for circular orders. sbtw a b c states that b is strictly between a and c (in that order).

class CircularPreorder (α : Type u_1) extends Btw α, SBtw α : Type u_1

A circular preorder is the analogue of a preorder where you can loop around. ≤ and < are replaced by ternary relations btw and sbtw. btw is reflexive and cyclic. sbtw is transitive.

• btw : α → α → α → Prop
• sbtw : α → α → α → Prop
• btw_refl : ∀ (a : α), btw a a a

  a is between a and a.

• btw_cyclic_left : ∀ {a b c : α}, btw a b c → btw b c a

  If b is between a and c, then c is between b and a. This is motivated by imagining three points on a circle.

• sbtw_iff_btw_not_btw : ∀ {a b c : α}, sbtw a b c ↔ btw a b c ∧ ¬btw c b a

  Strict betweenness is given by betweenness in one direction and non-betweenness in the other.

  I.e., if b is between a and c but not between c and a, then we say b is strictly between a and c.

• sbtw_trans_left : ∀ {a b c d : α}, sbtw a b c → sbtw b d c → sbtw a d c

  For any fixed c, fun a b ↦ sbtw a b c is a transitive relation.

  I.e., given a b d c in that "order", if we have b strictly between a and c, and d strictly between b and c, then d is strictly between a and c.

class CircularPartialOrder (α : Type u_1) extends CircularPreorder α : Type u_1

A circular partial order is the analogue of a partial order where you can loop around. ≤ and < are replaced by ternary relations btw and sbtw. btw is reflexive, cyclic and antisymmetric. sbtw is transitive.

• btw : α → α → α → Prop
• sbtw : α → α → α → Prop
• btw_refl : ∀ (a : α), btw a a a
• btw_cyclic_left : ∀ {a b c : α}, btw a b c → btw b c a
• sbtw_iff_btw_not_btw : ∀ {a b c : α}, sbtw a b c ↔ btw a b c ∧ ¬btw c b a
• sbtw_trans_left : ∀ {a b c d : α}, sbtw a b c → sbtw b d c → sbtw a d c
• btw_antisymm : ∀ {a b c : α}, btw a b c → btw c b a → a = b ∨ b = c ∨ c = a

  If b is between a and c and also between c and a, then at least one pair of points among a, b, c are identical.

class CircularOrder (α : Type u_1) extends CircularPartialOrder α : Type u_1

A circular order is the analogue of a linear order where you can loop around. ≤ and < are replaced by ternary relations btw and sbtw. btw is reflexive, cyclic, antisymmetric and total. sbtw is transitive.

• btw : α → α → α → Prop
• sbtw : α → α → α → Prop
• btw_refl : ∀ (a : α), btw a a a
• btw_cyclic_left : ∀ {a b c : α}, btw a b c → btw b c a
• sbtw_iff_btw_not_btw : ∀ {a b c : α}, sbtw a b c ↔ btw a b c ∧ ¬btw c b a
• sbtw_trans_left : ∀ {a b c d : α}, sbtw a b c → sbtw b d c → sbtw a d c
• btw_antisymm : ∀ {a b c : α}, btw a b c → btw c b a → a = b ∨ b = c ∨ c = a
• btw_total : ∀ (a b c : α), btw a b c ∨ btw c b a

  For any triple of points, the second is between the other two one way or another.

Circular preorders

theorem btw_rfl {α : Type u_1} [CircularPreorder α] {a : α} : btw a a a

theorem Btw.btw.cyclic_left {α : Type u_1} [CircularPreorder α] {a b c : α} (h : btw a b c) : btw b c a

theorem btw_cyclic_right {α : Type u_1} [CircularPreorder α] {a b c : α} (h : btw a b c) : btw c a b

theorem Btw.btw.cyclic_right {α : Type u_1} [CircularPreorder α] {a b c : α} (h : btw a b c) : btw c a b

Alias of btw_cyclic_right.

theorem btw_cyclic {α : Type u_1} [CircularPreorder α] {a b c : α} : btw a b c ↔ btw c a b

The order of the ↔ has been chosen so that rw [btw_cyclic] cycles to the right while rw [← btw_cyclic] cycles to the left (thus following the prepended arrow).

theorem sbtw_iff_btw_not_btw {α : Type u_1} [CircularPreorder α] {a b c : α} : sbtw a b c ↔ btw a b c ∧ ¬btw c b a

theorem btw_of_sbtw {α : Type u_1} [CircularPreorder α] {a b c : α} (h : sbtw a b c) : btw a b c

theorem SBtw.sbtw.btw {α : Type u_1} [CircularPreorder α] {a b c : α} (h : sbtw a b c) : btw a b c

Alias of btw_of_sbtw.

theorem not_btw_of_sbtw {α : Type u_1} [CircularPreorder α] {a b c : α} (h : sbtw a b c) : ¬btw c b a

theorem SBtw.sbtw.not_btw {α : Type u_1} [CircularPreorder α] {a b c : α} (h : sbtw a b c) : ¬btw c b a

Alias of not_btw_of_sbtw.

theorem not_sbtw_of_btw {α : Type u_1} [CircularPreorder α] {a b c : α} (h : btw a b c) : ¬sbtw c b a

theorem Btw.btw.not_sbtw {α : Type u_1} [CircularPreorder α] {a b c : α} (h : btw a b c) : ¬sbtw c b a

Alias of not_sbtw_of_btw.

theorem sbtw_of_btw_not_btw {α : Type u_1} [CircularPreorder α] {a b c : α} (habc : btw a b c) (hcba : ¬btw c b a) : sbtw a b c

theorem Btw.btw.sbtw_of_not_btw {α : Type u_1} [CircularPreorder α] {a b c : α} (habc : btw a b c) (hcba : ¬btw c b a) : sbtw a b c

Alias of sbtw_of_btw_not_btw.

theorem sbtw_cyclic_left {α : Type u_1} [CircularPreorder α] {a b c : α} (h : sbtw a b c) : sbtw b c a

theorem SBtw.sbtw.cyclic_left {α : Type u_1} [CircularPreorder α] {a b c : α} (h : sbtw a b c) : sbtw b c a

Alias of sbtw_cyclic_left.

theorem sbtw_cyclic_right {α : Type u_1} [CircularPreorder α] {a b c : α} (h : sbtw a b c) : sbtw c a b

theorem SBtw.sbtw.cyclic_right {α : Type u_1} [CircularPreorder α] {a b c : α} (h : sbtw a b c) : sbtw c a b

Alias of sbtw_cyclic_right.

theorem sbtw_cyclic {α : Type u_1} [CircularPreorder α] {a b c : α} : sbtw a b c ↔ sbtw c a b

The order of the ↔ has been chosen so that rw [sbtw_cyclic] cycles to the right while rw [← sbtw_cyclic] cycles to the left (thus following the prepended arrow).

theorem SBtw.sbtw.trans_left {α : Type u_1} [CircularPreorder α] {a b c d : α} (h : sbtw a b c) : sbtw b d c → sbtw a d c

theorem sbtw_trans_right {α : Type u_1} [CircularPreorder α] {a b c d : α} (hbc : sbtw a b c) (hcd : sbtw a c d) : sbtw a b d

theorem SBtw.sbtw.trans_right {α : Type u_1} [CircularPreorder α] {a b c d : α} (hbc : sbtw a b c) (hcd : sbtw a c d) : sbtw a b d

Alias of sbtw_trans_right.

theorem sbtw_asymm {α : Type u_1} [CircularPreorder α] {a b c : α} (h : sbtw a b c) : ¬sbtw c b a

theorem SBtw.sbtw.not_sbtw {α : Type u_1} [CircularPreorder α] {a b c : α} (h : sbtw a b c) : ¬sbtw c b a

Alias of sbtw_asymm.

theorem sbtw_irrefl_left_right {α : Type u_1} [CircularPreorder α] {a b : α} : ¬sbtw a b a

theorem sbtw_irrefl_left {α : Type u_1} [CircularPreorder α] {a b : α} : ¬sbtw a a b

theorem sbtw_irrefl_right {α : Type u_1} [CircularPreorder α] {a b : α} : ¬sbtw a b b

theorem sbtw_irrefl {α : Type u_1} [CircularPreorder α] (a : α) : ¬sbtw a a a

Circular partial orders

theorem Btw.btw.antisymm {α : Type u_1} [CircularPartialOrder α] {a b c : α} (h : btw a b c) : btw c b a → a = b ∨ b = c ∨ c = a

Circular orders

theorem btw_refl_left_right {α : Type u_1} [CircularOrder α] (a b : α) : btw a b a

theorem btw_rfl_left_right {α : Type u_1} [CircularOrder α] {a b : α} : btw a b a

theorem btw_refl_left {α : Type u_1} [CircularOrder α] (a b : α) : btw a a b

theorem btw_rfl_left {α : Type u_1} [CircularOrder α] {a b : α} : btw a a b

theorem btw_refl_right {α : Type u_1} [CircularOrder α] (a b : α) : btw a b b

theorem btw_rfl_right {α : Type u_1} [CircularOrder α] {a b : α} : btw a b b

theorem sbtw_iff_not_btw {α : Type u_1} [CircularOrder α] {a b c : α} : sbtw a b c ↔ ¬btw c b a

theorem btw_iff_not_sbtw {α : Type u_1} [CircularOrder α] {a b c : α} : btw a b c ↔ ¬sbtw c b a

Circular intervals

def Set.cIcc {α : Type u_1} [CircularPreorder α] (a b : α) : Set α

Closed-closed circular interval

Equations

• Set.cIcc a b = {x : α | btw a x b}

def Set.cIoo {α : Type u_1} [CircularPreorder α] (a b : α) : Set α

Open-open circular interval

Equations

• Set.cIoo a b = {x : α | sbtw a x b}

@[simp]

theorem Set.mem_cIcc {α : Type u_1} [CircularPreorder α] {a b x : α} : x ∈ Set.cIcc a b ↔ btw a x b

@[simp]

theorem Set.mem_cIoo {α : Type u_1} [CircularPreorder α] {a b x : α} : x ∈ Set.cIoo a b ↔ sbtw a x b

theorem Set.left_mem_cIcc {α : Type u_1} [CircularOrder α] (a b : α) : a ∈ Set.cIcc a b

theorem Set.right_mem_cIcc {α : Type u_1} [CircularOrder α] (a b : α) : b ∈ Set.cIcc a b

theorem Set.compl_cIcc {α : Type u_1} [CircularOrder α] {a b : α} : (Set.cIcc a b)ᶜ = Set.cIoo b a

theorem Set.compl_cIoo {α : Type u_1} [CircularOrder α] {a b : α} : (Set.cIoo a b)ᶜ = Set.cIcc b a

Circularizing instances

@[reducible, inline]

abbrev LE.toBtw (α : Type u_1) [LE α] : Btw α

The betweenness relation obtained from "looping around" ≤. See note [reducible non-instances].

Equations

• LE.toBtw α = { btw := fun (a b c : α) => a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b }

@[reducible, inline]

abbrev LT.toSBtw (α : Type u_1) [LT α] : SBtw α

The strict betweenness relation obtained from "looping around" <. See note [reducible non-instances].

Equations

• LT.toSBtw α = { sbtw := fun (a b c : α) => a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b }

@[reducible, inline]

abbrev Preorder.toCircularPreorder (α : Type u_1) [Preorder α] : CircularPreorder α

The circular preorder obtained from "looping around" a preorder. See note [reducible non-instances].

Equations

• Preorder.toCircularPreorder α = CircularPreorder.mk ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev PartialOrder.toCircularPartialOrder (α : Type u_1) [PartialOrder α] : CircularPartialOrder α

The circular partial order obtained from "looping around" a partial order. See note [reducible non-instances].

Equations

• PartialOrder.toCircularPartialOrder α = CircularPartialOrder.mk ⋯

@[reducible, inline]

abbrev LinearOrder.toCircularOrder (α : Type u_1) [LinearOrder α] : CircularOrder α

The circular order obtained from "looping around" a linear order. See note [reducible non-instances].

Equations

• LinearOrder.toCircularOrder α = CircularOrder.mk ⋯

Dual constructions

instance OrderDual.btw (α : Type u_1) [Btw α] : Btw αᵒᵈ

Equations

• OrderDual.btw α = { btw := fun (a b c : α) => btw c b a }

instance OrderDual.sbtw (α : Type u_1) [SBtw α] : SBtw αᵒᵈ

Equations

• OrderDual.sbtw α = { sbtw := fun (a b c : α) => sbtw c b a }

instance OrderDual.circularPreorder (α : Type u_1) [CircularPreorder α] : CircularPreorder αᵒᵈ

Equations

• OrderDual.circularPreorder α = CircularPreorder.mk ⋯ ⋯ ⋯ ⋯

instance OrderDual.circularPartialOrder (α : Type u_1) [CircularPartialOrder α] : CircularPartialOrder αᵒᵈ

Equations

• OrderDual.circularPartialOrder α = CircularPartialOrder.mk ⋯

instance OrderDual.instCircularOrder (α : Type u_1) [CircularOrder α] : CircularOrder αᵒᵈ

Equations

• OrderDual.instCircularOrder α = CircularOrder.mk ⋯