Orderability of amalgamated free products

DefinitionRight-orderable group#✓fully proved

A group \(G\) is right-orderable if 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 :=
  ∃ r : LinearOrder G, letI := r; ∀ a b c : G, a ≤ b → a * c ≤ b * c

Used by 1

Used byKourovka Problem 15.34 (statement)

DefinitionKourovka Problem 15.34 (statement)#✓fully proved

The statement that for every family \((G_i)_{i \in I}\) of groups, each with a linear order invariant under multiplication on both sides, every group \(H\) with such a linear order, and all strictly increasing group homomorphisms \(\varphi_i \colon H \to G_i\), the free product of the \(G_i\) with \(H\) amalgamated along the maps \(\varphi_i\) is right-orderable.

The problem was posed by V. V. Bludov.

def amalgamOfOrderedGroupsRightOrderable : Prop :=
  ∀ (ι : Type) (G : ι → Type) [∀ i, Group (G i)] [∀ i, LinearOrder (G i)]
    [∀ i, MulLeftMono (G i)] [∀ i, MulRightMono (G i)] (H : Type) [Group H] [LinearOrder H]
    [MulLeftMono H] [MulRightMono H] (φ : ∀ i, H →* G i),
    (∀ i, StrictMono (φ i)) → IsRightOrderable (Monoid.PushoutI φ)

Uses 1 · Used by 1

Statement usesRight-orderable group

Used byBludov–Glass theorem (Kourovka Problem 15.34)

TheoremBludov–Glass theorem (Kourovka Problem 15.34)#●ready to prove

Let \((G_i)_{i \in I}\) be a family of groups, each with a linear order invariant under multiplication on both sides (\(a \le b\) implies \(ca \le cb\) and \(ac \le bc\)), let \(H\) be a group with such a linear order, and for each \(i\) let \(\varphi_i \colon H \to G_i\) be a strictly increasing group homomorphism. Then the free product of the \(G_i\) with \(H\) amalgamated along the maps \(\varphi_i\) is right-orderable: it admits a linear order such that \(a \le b\) implies \(ac \le bc\) for all \(a, b, c\).

public theorem_wanted amalgamOfOrderedGroupsRightOrderable_holds :
    amalgamOfOrderedGroupsRightOrderable

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 15.34 (V. V. Bludov); resolution: V. V. Bludov and A. M. W. Glass, On free products of right ordered groups with amalgamated subgroups, Math. Proc. Cambridge Philos. Soc. 146 (2009), 591-601, main theorem (the free product of ordered groups G₁, G₂ with subgroups amalgamated via an order-preserving isomorphism is right orderable; extended to arbitrary families); Kourovka Archive, Problem 15.34 (answer: Yes, it is).

Uses 1

Statement usesKourovka Problem 15.34 (statement)

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.