Cyclically ordered group

Stream: maths

[Yaël Dillies]

Are people interested in those definitions? Are they general enough?

class circular_order (α : Type*) :=
(Ico : α → α → set α)
(cyclic : ∀ a b c : α, c ∈ Ico a b → c ≠ a → a ∈ Ico b c)
(Ico_subset_Ico : ∀ a b c d : α, c ∈ Ico a b → Ico a c ⊆ Ico a b) -- transitivity
(compl_Ico : ∀ a b : α, (Ico a b)ᶜ = Ico b a) -- asymmetry and totality

class cyclically_ordered_group (α : Type*) extends group α, circular_order α :=
(Ico_mul_left : ∀ a b c g : α, c ∈ Ico a b → g * c ∈ Ico (g * a) (g * b))
(Ico_mul_right : ∀ a b c g : α, c ∈ Ico a b → c * g ∈ Ico (a * g) (b * g))

class add_cyclically_ordered_group (α : Type*) extends add_group α, circular_order α :=
(Ico_mul_left : ∀ a b c g : α, c ∈ Ico a b → g + c ∈ Ico (g + a) (g + b))
(Ico_mul_right : ∀ a b c g : α, c ∈ Ico a b → c + g ∈ Ico (a + g) (b + g))

I'm not (yet) planning on adding those to mathlib, but @Kendall Frey is interested in related stuff.

@Yury G. Kudryashov, can your rotation number be generalized to such groups?

[Yury G. Kudryashov]

AFAIR, there is a generalization of the rotation number construction to cyclically ordered sets. I don't remember all the details.