Right-orderability of residually finite p-groups

DefinitionRight-orderable groups#✓fully proved

A group \(G\) is right-orderable when it admits a linear order \(\le\) that is invariant under right multiplication: \(a \le b\) implies \(ac \le bc\) for all \(a, b, c \in G\).

def IsRightOrderable (G : Type*) [Group G] : Prop :=
  ∃ _ : LinearOrder G, ∀ a b c : G, a ≤ b → a * c ≤ b * c
Used by 2

DefinitionMedvedev's question on right-orderability (Kourovka 10.30)#✓fully proved

The statement that there exist a group \(G\) and distinct primes \(p\) and \(q\) such that \(G\) is residually a finite \(p\)-group and residually a finite \(q\)-group, but \(G\) is not right-orderable.

def residuallyTwoPrimesNotRightOrderable : Prop :=
  ∃ (G : Type) (_ : Group G) (p q : ℕ), p.Prime ∧ q.Prime ∧ p ≠ q ∧
    IsResiduallyFiniteP p G ∧ IsResiduallyFiniteP q G ∧ ¬ IsRightOrderable G
Uses 2 · Used by 1

TheoremA non-right-orderable group that is residually \(p\) for two primes (Linnell)#●ready to prove

There exist a group \(G\) and distinct primes \(p\) and \(q\) such that \(G\) is residually a finite \(p\)-group and residually a finite \(q\)-group but is not right-orderable.

By Rhemtulla, a group that is residually a finite \(p\)-group for infinitely many primes \(p\) is orderable.

public theorem_wanted residuallyTwoPrimesNotRightOrderable_holds :
    residuallyTwoPrimesNotRightOrderable
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 10.30 (N. Ya. Medvedev); resolution: P. A. Linnell, J. Algebra 248 (2002), 605-607, Kourovka Archive, Problem 10.30 ("Yes, there does").
Uses 1
2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.