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 circular_order 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 circular_partial_order drops totality.
• A circular_preorder 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 circular_preorder, circular_partial_order and circular_order are subtler than between preorder, partial_order, linear_order. In particular, one cannot simply extend the btw of a circular_partial_order to make it a circular_order.

One can translate from usual orders to circular ones by "closing the necklace at infinity". See has_le.to_has_btw and has_lt.to_has_sbtw. 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 order_dual α here. The instances has_le α → has_btw αᵒᵈ and has_lt α → has_sbtw αᵒᵈ can each be inferred in two ways:

• has_le αhas_btw αhas_btw αᵒᵈ vs has_le αhas_le αᵒᵈhas_btw αᵒᵈ
• has_lt αhas_sbtw αhas_sbtw αᵒᵈ vs has_lt αhas_lt αᵒᵈhas_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, real.angle, and roots_of_unity 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?

## Tags #

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

@[class]
structure has_btw (α : Type u_1) :
Type u_1
• btw : α → α → α → Prop

Syntax typeclass for a betweenness relation.

Instances of this typeclass
Instances of other typeclasses for has_btw
• has_btw.has_sizeof_inst
@[class]
structure has_sbtw (α : Type u_1) :
Type u_1
• sbtw : α → α → α → Prop

Syntax typeclass for a strict betweenness relation.

Instances of this typeclass
Instances of other typeclasses for has_sbtw
• has_sbtw.has_sizeof_inst
@[class]
structure circular_preorder (α : Type u_1) :
Type u_1
• to_has_btw :
• to_has_sbtw :
• btw_refl : ∀ (a : α), a a
• btw_cyclic_left : ∀ {a b c : α}, b c c a
• sbtw_iff_btw_not_btw : ∀ {a b c : α}, c b c ¬ b a . "order_laws_tac"
• sbtw_trans_left : ∀ {a b c d : α}, c c c

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.

Instances of this typeclass
Instances of other typeclasses for circular_preorder
• circular_preorder.has_sizeof_inst
@[class]
structure circular_partial_order (α : Type u_1) :
Type u_1
• to_circular_preorder :
• btw_antisymm : ∀ {a b c : α}, b c b aa = b b = c c = a

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.

Instances of this typeclass
Instances of other typeclasses for circular_partial_order
• circular_partial_order.has_sizeof_inst
@[class]
structure circular_order (α : Type u_1) :
Type u_1
• to_circular_partial_order :
• btw_total : ∀ (a b c : α), b c b a

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.

Instances of this typeclass
Instances of other typeclasses for circular_order
• circular_order.has_sizeof_inst

### Circular preorders #

theorem btw_rfl {α : Type u_1} {a : α} :
a a
theorem has_btw.btw.cyclic_left {α : Type u_1} {a b c : α} (h : b c) :
c a
theorem btw_cyclic_right {α : Type u_1} {a b c : α} (h : b c) :
a b
theorem has_btw.btw.cyclic_right {α : Type u_1} {a b c : α} (h : b c) :
a b

Alias of btw_cyclic_right.

theorem btw_cyclic {α : Type u_1} {a b c : α} :
b 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} {a b c : α} :
c b c ¬ b a
theorem btw_of_sbtw {α : Type u_1} {a b c : α} (h : c) :
b c
theorem has_sbtw.sbtw.btw {α : Type u_1} {a b c : α} (h : c) :
b c

Alias of btw_of_sbtw.

theorem not_btw_of_sbtw {α : Type u_1} {a b c : α} (h : c) :
¬ b a
theorem has_sbtw.sbtw.not_btw {α : Type u_1} {a b c : α} (h : c) :
¬ b a

Alias of not_btw_of_sbtw.

theorem not_sbtw_of_btw {α : Type u_1} {a b c : α} (h : b c) :
¬ a
theorem has_btw.btw.not_sbtw {α : Type u_1} {a b c : α} (h : b c) :
¬ a

Alias of not_sbtw_of_btw.

theorem sbtw_of_btw_not_btw {α : Type u_1} {a b c : α} (habc : b c) (hcba : ¬ b a) :
c
theorem has_btw.btw.sbtw_of_not_btw {α : Type u_1} {a b c : α} (habc : b c) (hcba : ¬ b a) :
c

Alias of sbtw_of_btw_not_btw.

theorem sbtw_cyclic_left {α : Type u_1} {a b c : α} (h : c) :
a
theorem has_sbtw.sbtw.cyclic_left {α : Type u_1} {a b c : α} (h : c) :
a

Alias of sbtw_cyclic_left.

theorem sbtw_cyclic_right {α : Type u_1} {a b c : α} (h : c) :
b
theorem has_sbtw.sbtw.cyclic_right {α : Type u_1} {a b c : α} (h : c) :
b

Alias of sbtw_cyclic_right.

theorem sbtw_cyclic {α : Type u_1} {a b c : α} :
c 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 has_sbtw.sbtw.trans_left {α : Type u_1} {a b c d : α} (h : c) :
c c
theorem sbtw_trans_right {α : Type u_1} {a b c d : α} (hbc : c) (hcd : d) :
d
theorem has_sbtw.sbtw.trans_right {α : Type u_1} {a b c d : α} (hbc : c) (hcd : d) :
d

Alias of sbtw_trans_right.

theorem sbtw_asymm {α : Type u_1} {a b c : α} (h : c) :
¬ a
theorem has_sbtw.sbtw.not_sbtw {α : Type u_1} {a b c : α} (h : c) :
¬ a

Alias of sbtw_asymm.

theorem sbtw_irrefl_left_right {α : Type u_1} {a b : α} :
¬ a
theorem sbtw_irrefl_left {α : Type u_1} {a b : α} :
¬ b
theorem sbtw_irrefl_right {α : Type u_1} {a b : α} :
¬ b
theorem sbtw_irrefl {α : Type u_1} (a : α) :
¬ a

### Circular partial orders #

theorem has_btw.btw.antisymm {α : Type u_1} {a b c : α} (h : b c) :
b aa = b b = c c = a

### Circular orders #

theorem btw_refl_left_right {α : Type u_1} (a b : α) :
b a
theorem btw_rfl_left_right {α : Type u_1} {a b : α} :
b a
theorem btw_refl_left {α : Type u_1} (a b : α) :
a b
theorem btw_rfl_left {α : Type u_1} {a b : α} :
a b
theorem btw_refl_right {α : Type u_1} (a b : α) :
b b
theorem btw_rfl_right {α : Type u_1} {a b : α} :
b b
theorem sbtw_iff_not_btw {α : Type u_1} {a b c : α} :
c ¬ b a
theorem btw_iff_not_sbtw {α : Type u_1} {a b c : α} :
b c ¬ a

### Circular intervals #

def set.cIcc {α : Type u_1} (a b : α) :
set α

Closed-closed circular interval

Equations
• b = {x : α | x b}
def set.cIoo {α : Type u_1} (a b : α) :
set α

Open-open circular interval

Equations
• b = {x : α | b}
@[simp]
theorem set.mem_cIcc {α : Type u_1} {a b x : α} :
x b x b
@[simp]
theorem set.mem_cIoo {α : Type u_1} {a b x : α} :
x b b
theorem set.left_mem_cIcc {α : Type u_1} (a b : α) :
a b
theorem set.right_mem_cIcc {α : Type u_1} (a b : α) :
b b
theorem set.compl_cIcc {α : Type u_1} {a b : α} :
(set.cIcc a b) = a
theorem set.compl_cIoo {α : Type u_1} {a b : α} :
(set.cIoo a b) = a

### Circularizing instances #

@[reducible]
def has_le.to_has_btw (α : Type u_1) [has_le α] :

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

Equations
@[reducible]
def has_lt.to_has_sbtw (α : Type u_1) [has_lt α] :

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

Equations
@[reducible]
def preorder.to_circular_preorder (α : Type u_1) [preorder α] :

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

Equations
@[reducible]
def partial_order.to_circular_partial_order (α : Type u_1)  :

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

Equations
@[reducible]
def linear_order.to_circular_order (α : Type u_1) [linear_order α] :

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

Equations

### Dual constructions #

@[protected, instance]
def order_dual.has_btw (α : Type u_1) [has_btw α] :
Equations
• = {btw := λ (a b c : α), b a}
@[protected, instance]
def order_dual.has_sbtw (α : Type u_1) [has_sbtw α] :
Equations
• = {sbtw := λ (a b c : α), a}
@[protected, instance]
def order_dual.circular_preorder (α : Type u_1) [h : circular_preorder α] :
Equations
@[protected, instance]
def order_dual.circular_partial_order (α : Type u_1)  :
Equations
@[protected, instance]
def order_dual.circular_order (α : Type u_1)  :
Equations