Simple right-orderable groups

DefinitionRight orders on a group (Kourovka Problem 16.50)#✓fully proved

The right orders of a group \(G\) are the linear orders \(\le\) on \(G\), viewed as relations, 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

Used byKourovka Problem 16.50 (finitely generated simple right-orderable groups)

DefinitionKourovka Problem 16.50 (finitely generated simple right-orderable groups)#✓fully proved

The statement that there exists a finitely generated simple group \(G\) admitting a right order, that is, a linear order \(\le\) on \(G\) such that \(a \le b\) implies \(ac \le bc\) for all \(a, b, c \in G\). The problem is due to V. M. Kopytov and N. Ya. Medvedev.

def existsSimpleFGRightOrderable : Prop :=
  ∃ (G : Type) (_ : Group G), IsSimpleGroup G ∧ Group.FG G ∧ (rightOrders G).Nonempty

Uses 1 · Used by 1

Statement usesRight orders on a group (Kourovka Problem 16.50)

Used byFinitely generated simple right-orderable groups exist

TheoremFinitely generated simple right-orderable groups exist#●ready to prove

There is a finitely generated simple group \(G\) that admits a right order, that is, a linear order \(\le\) on \(G\) such that \(a \le b\) implies \(ac \le bc\) for all \(a, b, c \in G\). This answers Kourovka Problem 16.50 positively.

Hyde and Lodha (Theorem 1.3) construct finitely generated simple groups of orientation-preserving homeomorphisms of the real line, which are finitely generated simple left (or right) orderable groups (Corollary 1.5 and the abstract). The Kourovka Archive answers 16.50 "Yes, such groups do exist".

public theorem_wanted existsSimpleFGRightOrderable_holds : existsSimpleFGRightOrderable

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Archive of Solved Problems, Problem 16.50 (V. M. Kopytov, N. Ya. Medvedev); resolution: J. Hyde and Y. Lodha, Finitely generated infinite simple groups of homeomorphisms of the real line, Invent. Math. 218 (2019), 83-112, arXiv:1807.06478, Theorem 1.3 (G_ρ is a finitely generated simple subgroup of Homeo+(ℝ)) and Corollary 1.5 (finitely generated simple left orderable groups exist; by the abstract, equivalently left or right orderable); Kourovka Archive, Problem 16.50 (Yes, such groups do exist), https://arxiv.org/abs/1807.06478.

Uses 1

Statement usesKourovka Problem 16.50 (finitely generated simple right-orderable groups)

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.