Residual finiteness growth of free groups
DefinitionLogarithmic-index separation in free groups (Kourovka 15.35)#✓fully proved
The statement, posed by O. V. Bogopolski, that for some integer \(r \ge 2\) there is a real number \(C\) such that every element \(w\) of the free group \(F_r\) of rank \(r\) whose reduced word length \(n\) satisfies \(n > 1\) lies outside some subgroup of \(F_r\) of finite index at most \(C \log n\), where \(\log\) is the natural logarithm.
TheoremBogopolski's logarithmic-index separation fails in free groups of rank at least 2#●ready to prove
For every integer \(r \ge 2\) and every real number \(C\), there is an element \(w\) of the free group \(F_r\) of rank \(r\) whose reduced word length \(n\) satisfies \(n > 1\) and such that every subgroup of finite index in \(F_r\) that does not contain \(w\) has index greater than \(C \log n\), where \(\log\) is the natural logarithm. That is, the logarithmic-index separation property of Kourovka Problem 15.35 holds for no rank \(r \ge 2\).
Bou-Rabee and McReynolds (Theorem 1.4) prove that for every rank \(m > 1\) the maximal divisibility function of \(F_m\) on words of length at most \(n\) is not \(O(\log n)\), which rules out every \(C\); the Kourovka Archive answers 15.35 "No, it is not true".
public theorem_wanted logIndexSeparation_refuted : ¬ logIndexSeparation
def logIndexSeparation : Prop :=
∃ r : ℕ, 2 ≤ r ∧ ∃ C : ℝ, ∀ w : FreeGroup (Fin r), 1 < w.norm →
∃ H : Subgroup (FreeGroup (Fin r)), H.FiniteIndex ∧ w ∉ H ∧
(H.index : ℝ) ≤ C * Real.log w.norm
WantedExt/GroupTheory/FreeGroupLogIndexSeparationKourovka15Problem35Wanted.lean:41
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.35 (O. V. Bogopolski); resolution: K. Bou-Rabee and D. B. McReynolds, Asymptotic growth and least common multiples in groups, Bull. London Math. Soc. 43 (2011), 1059-1068, arXiv:0907.3681, Theorem 1.4 (for m > 1, max D_{F_m}(n) is not bounded by O(log n)), https://arxiv.org/abs/0907.3681.
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.