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
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
def IsResiduallyFiniteP (p : ℕ) (G : Type*) [Group G] : Prop :=
∀ g : G, g ≠ 1 → ∃ N : Subgroup G, N.Normal ∧ (∃ k : ℕ, N.index = p ^ k) ∧ g ∉ N
WantedExt/GroupTheory/KourovkaNotebookShared.lean:63
def IsRightOrderable (G : Type*) [Group G] : Prop :=
∃ _ : LinearOrder G, ∀ a b c : G, a ≤ b → a * c ≤ b * c
WantedExt/GroupTheory/ResiduallyTwoPrimesNotRightOrderableKourovka10Problem30Wanted.lean:42
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
def residuallyTwoPrimesNotRightOrderable : Prop :=
∃ (G : Type) (_ : Group G) (p q : ℕ), p.Prime ∧ q.Prime ∧ p ≠ q ∧
IsResiduallyFiniteP p G ∧ IsResiduallyFiniteP q G ∧ ¬ IsRightOrderable G
WantedExt/GroupTheory/ResiduallyTwoPrimesNotRightOrderableKourovka10Problem30Wanted.lean:47
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
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.