Subgroup separability of Baumslag–Solitar groups

AbbreviationThe Baumslag–Solitar group BS(1, n)#✓fully proved

For a natural number \(n\), \(\mathrm{BS}(1, n)\) is the group with presentation \(\langle a, b \mid b a b^{-1} = a^n \rangle\).

abbrev BS1 (n : ℕ) : Type :=
  PresentedGroup ({FreeGroup.of 1 * FreeGroup.of 0 * (FreeGroup.of 1)⁻¹ * (FreeGroup.of 0 ^ n)⁻¹} :
    Set (FreeGroup (Fin 2)))

Used by 1

Used byKourovka Problem 16.2 (R. C. Alperin)

DefinitionSeparable subgroup#✓fully proved

A subgroup \(H\) of a group \(G\) is separable when for every element \(x \in G\) with \(x \notin H\) there are a finite group \(F\) and a group homomorphism \(f \colon G \to F\) with \(f(x) \notin f(H)\).

def IsSeparableSubgroup {G : Type} [Group G] (H : Subgroup G) : Prop :=
  ∀ x : G, x ∉ H → ∃ (F : Type) (_ : Group F) (_ : Finite F) (f : G →* F), f x ∉ H.map f

Used by 1

Used byLocally subgroup-separable (LERF) group

DefinitionLocally subgroup-separable (LERF) group#✓fully proved

A group \(G\) is locally subgroup-separable, or LERF, when every finitely generated subgroup of \(G\) is separable.

def IsLocallySubgroupSeparable (G : Type) [Group G] : Prop :=
  ∀ H : Subgroup G, H.FG → IsSeparableSubgroup H

Uses 1 · Used by 1

Statement usesSeparable subgroup

Used byKourovka Problem 16.2 (R. C. Alperin)

DefinitionKourovka Problem 16.2 (R. C. Alperin)#✓fully proved

A finitely generated solvable group \(G\) is locally subgroup-separable if and only if there is no \(n > 1\) such that \(G\) has a subgroup isomorphic to the Baumslag–Solitar group \(\mathrm{BS}(1, n)\).

def solvableLERFIffNoBaumslagSolitar : Prop :=
  ∀ (G : Type) [Group G], Group.FG G → Group.IsSolvable G →
    (IsLocallySubgroupSeparable G ↔ ¬ ∃ n : ℕ, 1 < n ∧ ∃ f : BS1 n →* G, Function.Injective f)

Uses 2 · Used by 1

Statement usesThe Baumslag–Solitar group BS(1, n) · Locally subgroup-separable (LERF) group

Used byKourovka Problem 16.2 has a negative answer

TheoremKourovka Problem 16.2 has a negative answer#●ready to prove

There is a finitely generated solvable group \(G\) for which the following two conditions are not equivalent: \(G\) is locally subgroup-separable; there is no \(n > 1\) such that \(G\) has a subgroup isomorphic to the Baumslag–Solitar group \(\mathrm{BS}(1, n)\).

Button's counterexample is the solvable ascending HNN extension of \(\mathbb{Z} \times \mathbb{Z} = \langle u, v \rangle\) by the injective endomorphism \(u \mapsto u^5 v^{-1}\), \(v \mapsto u^2\): it is not locally subgroup-separable but contains no \(\mathrm{BS}(1, m)\) with \(m \ne 0, \pm 1\).

public theorem_wanted solvableLERFIffNoBaumslagSolitar_refuted : ¬ solvableLERFIffNoBaumslagSolitar

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.2 (R. C. Alperin); resolution: J. O. Button, Strictly ascending HNN extensions in soluble groups, Ricerche di Matematica 61 (2012), no. 1, 139-145, arXiv:1004.0197, Theorem 2.1 and the remark after it (the soluble ascending HNN extension G = ⟨t, ℤ × ℤ⟩ with θ(u) = u⁵v⁻¹, θ(v) = u² is not LERF and contains no BS(1, m), m ≠ 0, ±1, so the answer to Problem 16.2 is no); Kourovka Archive, Problem 16.2 (No, it is not), https://arxiv.org/abs/1004.0197.

Uses 1

Statement usesKourovka Problem 16.2 (R. C. Alperin)

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.