In a group with no free subsemigroup on two generators, the conjugates of one element by the powers of another generate a finitely generated subgroup

Proved

GroupFiniteness.fg_closure_zpow_conj_of_not_hasFreeSubsemigroupOfRankTwo

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

combinatorial-group-theorygroup-growthgroup-theory

Let $B$ be a group with no free subsemigroup on two generators, that is, no pair of elements on which the evaluation map from the free monoid on two letters is injective, 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\}$ is finitely generated.

This is the free-subsemigroup counterpart of Milnor's Lemma 1. If the ordered products of $\beta$ with powers of $\alpha$ were all distinct they would exhibit a free subsemigroup on two generators; two of them therefore coincide, and after cancelling a common prefix and pairing the two words in both orders one gets distinct words of the same length, which is what allows the trailing power of $\beta$ to cancel. The resulting relation among the conjugates, solved at its last and first index of disagreement, expresses one conjugate in terms of the earlier ones.

The hypothesis is weaker than not having exponential growth, since a free subsemigroup on two generators forces exponential growth, so this is the stronger of the two lemmas. Note also that $B$ is not assumed finitely generated.

Preamble

import Definitions.Def_Chou_Growth
import Mathlib

Formal statement

namespace GroupFiniteness

/-- Rosenblatt's Lemma 4.8 (Invariant measures and growth conditions, Trans. Amer. Math. Soc. 193
(1974) 42) with its hypotheses removed: if a group has no free subsemigroup on two generators then
for any two elements the subgroup generated by the two-sided orbit
`{β ^ k * α * β ^ (-k) : k ∈ ℤ}` is finitely generated.

Rosenblatt states it for an exact sequence with abelian kernel and finitely generated middle term,
and concludes finite generation of a subgroup of the kernel; none of that is used, not even finite
generation of the ambient group. This is the free-subsemigroup counterpart of Milnor's Lemma 1: a
free subsemigroup on two generators would make the ordered products of `β` with powers of `α` all
distinct, and their collision is what yields a relation expressing one conjugate in terms of the
earlier ones. -/
theorem fg_closure_zpow_conj_of_not_hasFreeSubsemigroupOfRankTwo {B : Type*} [Group B]
    (h : ¬ Chou.HasFreeSubsemigroupOfRankTwo B) (α β : B) :
    (Subgroup.closure {x : B | ∃ k : ℤ, x = β ^ k * α * β ^ (-k)}).FG := by
  sorry

end GroupFiniteness

Source

Rosenblatt, J. M., Invariant measures and growth conditions, Transactions of the American Mathematical Society 193 (1974) 33-53, https://doi.org/10.1090/S0002-9947-1974-0342955-9, Lemma 4.8 (p. 42), with the abelian hypothesis, the ambient exact sequence and the finite generation of the middle term removed; Rosenblatt states it for a subgroup of an abelian kernel, and the argument uses none of that.

View graph