Isolated orders on free groups

DefinitionBi-invariant strict total orders on a group#✓fully proved

A relation \(r\) on a group \(G\) is a bi-invariant order if \(r\) is a strict total order on \(G\) (irreflexive, transitive and trichotomous) and \(r(a, b)\) implies \(r(cad, cbd)\) for all \(a, b, c, d \in G\).

def IsBiOrder {G : Type*} [Group G] (r : G → G → Prop) : Prop :=
  IsStrictTotalOrder G r ∧ ∀ a b c d : G, r a b → r (c * a * d) (c * b * d)

Used by 1

Used byKourovka Problem 12.51 (isolated bi-orders of free groups)

DefinitionKourovka Problem 12.51 (isolated bi-orders of free groups)#✓fully proved

The statement that for some natural number \(n \ge 2\) there is a finite subset \(S\) of the free group \(F_n\) on \(n\) generators such that exactly one bi-invariant strict total order \(<\) on \(F_n\) (a strict total order such that \(a < b\) implies \(cad < cbd\) for all \(a, b, c, d \in F_n\)) makes every element of \(S\) positive, that is, satisfies \(1 < s\) for all \(s \in S\). Such an order is an isolated point of the space of bi-orders of \(F_n\).

def freeGroupHasIsolatedBiOrder : Prop :=
  ∃ n : ℕ, 2 ≤ n ∧ ∃ S : Finset (FreeGroup (Fin n)),
    ∃! r : FreeGroup (Fin n) → FreeGroup (Fin n) → Prop, IsBiOrder r ∧ ∀ s ∈ S, r 1 s

Uses 1 · Used by 1

Statement usesBi-invariant strict total orders on a group

Used byNo free group of finite rank at least 2 has an isolated bi-order

TheoremNo free group of finite rank at least 2 has an isolated bi-order#●ready to prove

For every natural number \(n \ge 2\) and every finite subset \(S\) of the free group \(F_n\) on \(n\) generators, it is not the case that exactly one bi-invariant strict total order \(<\) on \(F_n\) (a strict total order such that \(a < b\) implies \(cad < cbd\) for all \(a, b, c, d \in F_n\)) satisfies \(1 < s\) for every \(s \in S\).

Resolved false: the Kourovka Notebook (21st issue) marks 12.51 solved, "No, it does not". Muliarchyk (arXiv:2403.14779) proves that a free product of bi-ordered groups admits no isolated bi-ordering; \(F_n\) is the free product of \(n \ge 2\) copies of \(\mathbb{Z}\) (see also Dovhyi and Muliarchyk, Groups Geom. Dyn. 17 (2023)).

public theorem_wanted freeGroupHasIsolatedBiOrder_refuted : ¬ freeGroupHasIsolatedBiOrder

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 12.51 (S. McCleary); resolution: K. Muliarchyk, Free products of bi-orderable groups, preprint (2024), arXiv:2403.14779; S. Dovhyi and K. Muliarchyk, Groups Geom. Dyn. 17 (2023), 613-632, Muliarchyk, main theorem: a free product of bi-ordered groups admits no isolated bi-ordering; the Kourovka Notebook (21st issue) marks 12.51 solved, https://arxiv.org/abs/2403.14779.

Uses 1

Statement usesKourovka Problem 12.51 (isolated bi-orders of free groups)

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.