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
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
WantedExt/GroupTheory/BaumslagGroupGermsFaithfulKourovka17Problem99Wanted.lean:51
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
noncomputable def wordFunction (w : FreeGroup (Fin 2)) : ℝ → ℝ :=
(FreeGroup.toWord w).foldr (fun l h => letterFunction l ∘ h) id
WantedExt/GroupTheory/BaumslagGroupGermsFaithfulKourovka17Problem99Wanted.lean:61
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)))
WantedExt/GroupTheory/BaumslagGroupGermsFaithfulKourovka17Problem99Wanted.lean:44
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
def baumslagGroupGermRepresentationFaithful : Prop :=
∀ w : FreeGroup (Fin 2), wordFunction w =ᶠ[Filter.atTop] id →
(PresentedGroup.mk _ w : BaumslagGroup) = 1
WantedExt/GroupTheory/BaumslagGroupGermsFaithfulKourovka17Problem99Wanted.lean:67
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
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.