Baumslag–Gersten group

AbbreviationBaumslag's group#✓fully proved

Baumslag's group is the one-relator group \(B = \langle a, b \mid (bab^{-1})\, a\, (bab^{-1})^{-1} = a^2 \rangle\), the quotient of the free group on the two generators \(a\) and \(b\) by the normal subgroup generated by \((bab^{-1})\, a\, (bab^{-1})^{-1} a^{-2}\).

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

DefinitionLetter functions for Baumslag's group#✓fully proved

To each letter of the free group on \(a, b\) attach a function \(\mathbb{R} \to \mathbb{R}\): \(a\) gives \(f(x) = 2x\), \(a^{-1}\) gives \(x/2\), \(b\) gives \(g(x) = 2^x\) and \(b^{-1}\) gives \(\log_2 x\).

On \((0, \infty)\) the function \(\log_2 x\) is the inverse of \(g\), which is all that matters for germs at \(+\infty\).

noncomputable def letterFunction : Fin 2 × Bool → ℝ → ℝ
  | (0, true) => fun x => 2 * x
  | (0, false) => fun x => x / 2
  | (1, true) => fun x => (2 : ℝ) ^ x
  | (1, false) => fun x => Real.logb 2 x
Used by 1

DefinitionWord functions for Baumslag's group#✓fully proved

To an element \(w\) of the free group on \(a, b\) with reduced word \(l_1 l_2 \cdots l_n\) attach the composite \(\varphi_w = \varphi_{l_1} \circ \varphi_{l_2} \circ \cdots \circ \varphi_{l_n}\), where \(\varphi_l\) is the function attached to the letter \(l\); the first letter is applied last, and \(\varphi_1\) is the identity. With this order products of germs are composites, and \(f(x) = 2x\) and \(g(x) = 2^x\) satisfy the defining relation of Baumslag's group as germs at \(+\infty\).

noncomputable def wordFunction (w : FreeGroup (Fin 2)) : ℝ → ℝ :=
  (FreeGroup.toWord w).foldr (fun l h => letterFunction l ∘ h) id
Uses 1 · Used by 1

DefinitionFaithfulness of Baumslag's germ representation (Kourovka 17.99)#✓fully proved

Let \(B\) be Baumslag's group \(\langle a, b \mid (bab^{-1})\, a\, (bab^{-1})^{-1} = a^2 \rangle\), let \(f(x) = 2x\) and \(g(x) = 2^x\), and for \(w\) in the free group on \(a, b\) let \(\varphi_w\) be its word function, the composite of \(f\), \(g\) and their inverses along the reduced word of \(w\). The representation \(a \mapsto f\), \(b \mapsto g\) of \(B\) by germs at \(+\infty\) is faithful when every \(w\) with \(\varphi_w(x) = x\) for all sufficiently large real \(x\) is trivial in \(B\).

This is Olshanskii's question whether the representation of \(B\) in the group of germs at \(+\infty\) of increasing continuous functions on \((0, \infty)\) is faithful.

def baumslagGroupGermRepresentationFaithful : Prop :=
  ∀ w : FreeGroup (Fin 2), wordFunction w =ᶠ[Filter.atTop] id →
    (PresentedGroup.mk _ w : BaumslagGroup) = 1
Uses 1 · Used by 1

TheoremBaumslag's germ representation is not faithful#●ready to prove

Let \(B\) be Baumslag's group \(\langle a, b \mid (bab^{-1})\, a\, (bab^{-1})^{-1} = a^2 \rangle\), let \(f(x) = 2x\) and \(g(x) = 2^x\), and for \(w\) in the free group on \(a, b\) with reduced word \(l_1 l_2 \cdots l_k\) let \(\varphi_w = \varphi_{l_1} \circ \varphi_{l_2} \circ \cdots \circ \varphi_{l_k}\), where \(\varphi_a = f\), \(\varphi_{a^{-1}}(x) = x/2\), \(\varphi_b = g\) and \(\varphi_{b^{-1}}(x) = \log_2 x\). The representation \(a \mapsto f\), \(b \mapsto g\) of \(B\) by germs at \(+\infty\) is not faithful: there is an element \(w\) of the free group on \(a, b\) such that \(\varphi_w(x) = x\) for all sufficiently large real \(x\), but the image of \(w\) in \(B\) is not trivial.

public theorem_wanted baumslagGroupGermRepresentationFaithful_refuted :
    ¬ baumslagGroupGermRepresentationFaithful
Sources
  • E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 17.99 (A. Yu. Olshanskii); resolution: C.-F. Nyberg-Brodda, The Baumslag-Gersten group and a problem of Olshanskii, preprint, arXiv:2606.27408 (2026), abstract (the representation of BG(1, 2) by germs is not faithful: an explicit non-trivial element of its kernel); the Kourovka Notebook (21st issue) marks 17.99 solved (No, it is not), https://arxiv.org/abs/2606.27408.
Uses 1
4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.