Spaces of right orders

DefinitionRight orders of a group (Kourovka 16.51)#✓fully proved

The right orders of a group \(G\) are the linear orders \(\le\) on \(G\) that are invariant under right multiplication: \(a \le b\) implies \(ac \le bc\) for all \(a, b, c \in G\).

def rightOrders (G : Type*) [Group G] : Set (G → G → Prop) :=
  {r | IsLinearOrder G r ∧ ∀ a b c : G, r a b → r (a * c) (b * c)}
Used by 1

DefinitionGroups with countably infinitely many right orders (Kourovka 16.51)#✓fully proved

The statement that some group has a countably infinite set of right orders.

def existsCountablyInfinitelyRightOrderable : Prop :=
  ∃ (G : Type) (_ : Group G), (rightOrders G).Countable ∧ (rightOrders G).Infinite
Uses 1 · Used by 1

TheoremNo group has countably infinitely many right orders#●ready to prove

For every group \(G\), the set of right orders on \(G\) (linear orders \(\le\) on \(G\) such that \(a \le b\) implies \(ac \le bc\) for all \(a, b, c \in G\)) is either finite or uncountable. That is, Kourovka Problem 16.51 has a negative answer.

Linnell proves this for left orders, which correspond to right orders through \(a \le' b \iff b^{-1} \le a^{-1}\).

public theorem_wanted existsCountablyInfinitelyRightOrderable_refuted :
    ¬ existsCountablyInfinitelyRightOrderable
Sources
  • E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 16.51 (V. M. Kopytov, N. Ya. Medvedev); resolution: P. A. Linnell, Bull. London Math. Soc. 43 (2011), 200-202; A. Clay, preprint, arXiv:0909.0273 (2009); A. Navas and C. Rivas, Algebr. Geom. Topol. 9 (2009), 2079-2100, Linnell, Theorem 1.3 (no group can be left-ordered in a countably infinite number of ways), based on A. V. Zenkov (1997, locally indicable groups); Clay, Corollary 3.10 (the set of left orderings of any group is finite or uncountable); the Kourovka Notebook (21st issue) marks 16.51 solved (No, there are no such groups), https://arxiv.org/abs/0909.0273.
Uses 1
2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.