Read-back

The single declaration in the artifact

Setting and data

Let $B$ be a group. (In the Lean text $B$ is an arbitrary type in an arbitrary universe, carrying a group structure; nothing about $B$ is assumed beyond the hypotheses listed below — in particular $B$ is not assumed finite, infinite, abelian, or torsion-free.)

The statement takes the following data:

• $B$, a group;
• $A$, a subgroup of $B$;
• $\alpha$, an element of $B$;
• $\beta$, an element of $B$.

Hypotheses

(H1) $B$ is finitely generated. Precisely: there is a finite subset $S \subseteq B$ such that the smallest subgroup of $B$ containing $S$ is all of $B$. ("Smallest subgroup containing a set" means the intersection of all subgroups of $B$ that contain the set.)

(H2) $A$ is a normal subgroup of $B$. Precisely: for every $n \in A$ and every $g \in B$, the element $g n g^{-1}$ lies in $A$.

(H3) $A$ is abelian. Precisely: any two elements of $A$ commute with each other, i.e. $a b = b a$ for all $a, b \in A$. (Only elements of $A$ are required to commute; no commutativity is assumed anywhere else in $B$.)

(H4) $B$ does not have exponential growth. This is the negation of a defined property, which must be unfolded in full.

For a subset $S \subseteq B$ and a natural number $n$, define the word ball of radius $n$

$$\mathcal{B}_S(n) \;=\; \Big\{\, g \in B \;:\; g = g_1 g_2 \cdots g_m \text{ for some } m \le n \text{ and some } g_1,\dots,g_m \text{ each satisfying } g_i \in S \text{ or } g_i^{-1} \in S \,\Big\}.$$

Three points of literal detail about this set.

1. The factors are taken from a finite list of length $m \le n$; the product is formed in the listed order; repetitions among the $g_i$ are allowed. The length bound is $\le n$, not $= n$.
2. The list may be empty ($m = 0$), and the empty product is the identity. Hence $1 \in \mathcal{B}_S(n)$ for every $S$ and every $n$, and in particular $\mathcal{B}_S(0) = \{1\}$, so $\mathcal{B}_S(n)$ is never empty.
3. Each factor is required to satisfy "$g_i \in S$ or $g_i^{-1} \in S$"; that is, the factors are drawn from $S \cup S^{-1}$. $S$ itself is not assumed symmetric.

Now, "$B$ has exponential growth" means:

there exist a finite subset $S \subseteq B$ generating $B$ (the smallest subgroup of $B$ containing $S$ is all of $B$), and a real number $c$ with $1 < c$, such that for every natural number $n$,

$$c^{n} \;\le\; \big|\mathcal{B}_S(n)\big| ,$$

where $|X|$ denotes the cardinality of $X$ as a natural number, with the convention that an infinite set has cardinality $0$, and where this natural number is then regarded as a real number, and $c^n$ is the $n$-th power of the real number $c$ with $n$ a natural-number exponent (so $c^0 = 1$).

Note the quantifier order inside this property: a single constant $c$ must work for all radii $n$ simultaneously, and it suffices that one finite generating set $S$ admits such a $c$; the property says nothing about non-generating finite subsets, and nothing about infinite generating sets.

Hypothesis (H4) is the negation of that property. Unfolded, it says:

for every finite subset $S \subseteq B$ whose generated subgroup is all of $B$, and for every real number $c > 1$, there exists a natural number $n$ with

$$\big|\mathcal{B}_S(n)\big| \;<\; c^{n}.$$

(The cardinality convention matters in principle: if some word ball were infinite, its cardinality would be read as $0$, which is $< c^n$ for every $n$. Here $S$ ranges over finite sets, so each ball is in fact a finite set.)

(H5) $\alpha \in A$.

There is no hypothesis on $\beta$: it is an arbitrary element of $B$, not assumed to lie in $A$, not assumed to commute with $\alpha$, not assumed to be of infinite order, and not assumed distinct from $1$ or from $\alpha$.

Conclusion

Consider the subset of $B$

$$C \;=\; \big\{\, x \in B \;:\; x = \beta^{k}\,\alpha\,\beta^{-k} \text{ for some } k \in \mathbb{Z} \,\big\},$$

that is, the set of all conjugates of $\alpha$ by integer powers of $\beta$. Here $\beta^{k}$ is the integer power of $\beta$ in the group $B$ (so $\beta^{0} = 1$, and negative exponents give inverses of positive powers), $\beta^{-k}$ is the power at the negated integer $-k$, which equals $(\beta^{k})^{-1}$, and the triple product is grouped as $(\beta^{k}\alpha)\,\beta^{-k}$ — the same element either way, by associativity. The index $k$ ranges over all integers, positive, negative and zero.

The conclusion asserts:

the subgroup of $B$ generated by $C$ — the intersection of all subgroups of $B$ containing $C$ — is finitely generated, meaning there exists a finite subset $T \subseteq B$ such that the subgroup generated by $T$ is exactly that subgroup.

($T$ is a finite subset of $B$, not a priori of $C$; but since the subgroup it generates equals the subgroup generated by $C$, $T$ is necessarily contained in that subgroup.)

Degenerate cases silently included

• Taking $k = 0$ gives $\beta^{0}\alpha\beta^{0} = \alpha$, so $\alpha \in C$ and $C$ is never empty; the generated subgroup always contains $\alpha$.
• $\beta = 1$ is allowed, in which case $C = \{\alpha\}$ and the conclusion is that the cyclic subgroup generated by $\alpha$ is finitely generated.
• $\alpha = 1$ is allowed, in which case $C = \{1\}$ and the generated subgroup is trivial.
• $A$ may be the trivial subgroup $\{1\}$ (which is normal and abelian), which forces $\alpha = 1$; and $A$ may be all of $B$, which forces $B$ itself to be abelian by (H3).
• $\beta$ may have finite order, in which case $C$ is a finite set.
• The hypotheses are jointly satisfiable — for instance by the trivial group with $A = B = \{1\}$ — so the statement is not vacuous.

Statement of the quantification, in one sentence

For every group $B$ that is finitely generated and does not have exponential growth in the sense above, every normal abelian subgroup $A$ of $B$, every $\alpha \in A$ and every $\beta \in B$, the subgroup of $B$ generated by $\{\beta^{k}\alpha\beta^{-k} : k \in \mathbb{Z}\}$ is finitely generated.