In a group without exponential growth, the conjugates of one element by the powers of another generate a finitely generated subgroup

Proved

GroupFiniteness.fg_closure_zpow_conj_of_not_hasExponentialGrowth

by dbenbenn · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatorial-group-theorygroup-growthgroup-theory

Let $B$ be a finitely generated group which does not have exponential growth, and let $\alpha$ and $\beta$ be any two of its elements. Then the subgroup generated by $\{\beta^{k}\alpha\beta^{-k} : k \in \mathbb Z\}$ , the orbit of $\alpha$ under conjugation by the powers of $\beta$ , is finitely generated.

Milnor states this for $\alpha$ an element of an abelian normal subgroup $A$ of $B$ , and concludes finite generation of a subgroup of $A$ . Neither the abelian hypothesis, nor the normality of $A$ , nor the ambient subgroup plays any role: the argument counts the ordered products of $\beta$ with powers of $\alpha$ , finds two that coincide because there are more of them than the ball of the corresponding radius can hold, and reads off from the resulting relation an expression for one conjugate in terms of the earlier ones.

Not having exponential growth is the negation of an existential over finite generating sets, so it is a statement about every finite generating set of $B$ .

Preamble

import Definitions.Def_Chou_Growth
import Mathlib

Formal statement

namespace GroupFiniteness

/-- Milnor's Lemma 1 (Growth of finitely generated solvable groups, J. Differential Geometry 2
(1968) 447–448) with its hypotheses removed: for a finitely generated group without exponential
growth and *any* two elements `α` and `β`, the subgroup generated by the two-sided orbit
`{β ^ k * α * β ^ (-k) : k ∈ ℤ}` is finitely generated.

Milnor states it for `α` in an abelian normal subgroup `A` of `B` and concludes finite generation
of a subgroup of `A`; neither the abelian hypothesis, nor normality, nor the ambient subgroup is
needed. The counting argument is Milnor's: among the ordered products of `β` with powers of `α`
there are more words than the ball of the corresponding radius can hold, so two coincide, and the
resulting relation expresses one conjugate in terms of the earlier ones. -/
theorem fg_closure_zpow_conj_of_not_hasExponentialGrowth {B : Type*} [Group B] [Group.FG B]
    (h : ¬ Chou.HasExponentialGrowth B) (α β : B) :
    (Subgroup.closure {x : B | ∃ k : ℤ, x = β ^ k * α * β ^ (-k)}).FG := by
  sorry

end GroupFiniteness

Source

Milnor, J., Growth of finitely generated solvable groups, Journal of Differential Geometry 2 (1968) 447-449, https://doi.org/10.4310/jdg/1214428659, Lemma 1 (pp. 447-448), with the abelian and normality hypotheses and the ambient subgroup removed; Milnor states it for an element of an abelian normal subgroup, and the counting argument uses none of that.

View graph