Geometric group theory · The Lumenary

MotivationH

What does a group look like from far away?

In 1911 and 1912 Max Dehn posed three questions about a group given by generators and relations: can we decide whether a word in the generators equals the identity (the word problem), whether two words are conjugate, and whether two presentations give isomorphic groups? For the fundamental groups of closed surfaces of genus $g \ge 2$ he solved the first two — and his solution was geometric. Such a group acts on the hyperbolic plane, tiling it by $4g$ -gons, and a word that represents the identity traces a closed path in that tiling; negative curvature forces any such path to contain more than half of the boundary of some tile, which can then be shortcut. This is "Dehn's algorithm".

Geometric group theory takes Dehn's idea as a programme. A finitely generated group $G$ becomes a metric space, its Cayley graph, and we ask what the large-scale shape of that space says about the algebra of $G$ :

$\Z^2$ looks like the Euclidean plane, the free group $F_2$ like a tree branching four ways, and the fundamental group of a genus-2 surface like the hyperbolic plane.
How fast balls grow — polynomially or exponentially — detects whether $G$ is virtually nilpotent (Gromov's theorem).
Whether triangles are thin detects hyperbolic groups, for which the word problem is solvable by Dehn's algorithm.
Whether $G$ can be cut into pieces that reassemble into two copies of itself — the phenomenon behind the Banach–Tarski paradox — is a property of the group, non-amenability, and random walks on $G$ can detect it.

The key move is to forget small-scale detail: two spaces that agree "up to bounded distortion" are treated as the same. This lesson builds that language — word metrics, quasi-isometries, growth, hyperbolicity and amenability — and proves its first theorems: the Švarc–Milnor lemma, Sanov's free subgroup of $\mathrm{SL}(2, \Z)$ and the paradoxical decomposition of $F_2$ .

IntuitionH

Zooming out

Draw $\Z^2$ with generators $(1,0)$ and $(0,1)$ : the Cayley graph is the square grid. Walk to a point $(m, n)$ and the shortest path has length $|m| + |n|$ ; the ball of radius $r$ is a diamond with $2r^2 + 2r + 1$ points. Now zoom out by a factor of a thousand: the grid becomes a plane with the $\ell^1$ metric. Change the generators to $(1,0), (0,1), (1,1)$ and the diamond becomes a hexagon — a different metric, but only by a bounded factor, and from far away still a plane.

Draw $F_2 = \langle a, b \rangle$ instead: every vertex has four edges ( $a^{\pm1}, b^{\pm1}$ ) and there are no cycles, because no non-trivial reduced word is the identity. The Cayley graph is the 4-regular tree, and the ball of radius $r$ has $2 \cdot 3^r - 1$ elements: exponential growth, like area in the hyperbolic plane.

Balls of radius 3 in two Cayley graphs, centred at the identity (gold). Left: the free group $F_2$ with generators $a^{\pm 1}, b^{\pm 1}$ — a tree, with $1 + 4 + 12 + 36 = 53$ elements. Right: $\Z^2$ with the standard generators — a grid, with $25 = 2 \cdot 3^2 + 2 \cdot 3 + 1$ elements. Edge lengths in the tree are drawn halving at each step only to fit it on the page; every edge has length 1.

The guiding questions are coarse ones. Which properties survive replacing a space by one at bounded distortion from it? A quasi-isometry allows a multiplicative error and an additive error in distances; it can crush a finite group to a point and inflate $\Z$ to $\R$ . What survives is exactly the large-scale geometry: the number of ends, growth type, hyperbolicity, amenability, and (for finitely generated groups) finite presentability. What does not survive is local algebra such as torsion or commutativity: $\Z$ and $\Z \times S_3$ are quasi-isometric.

DefinitionsH

Word metrics, quasi-isometries, growth, hyperbolicity, amenability

Throughout, $G$ is a group with a finite generating set $S$ , which we may assume symmetric ( $S = S^{-1}$ ) and not containing $1$ .

Definition— Cayley graph and word metric

The Cayley graph $\mathrm{Cay}(G, S)$ has vertex set $G$ and an edge from $g$ to $gs$ for each $g \in G$ and $s \in S$ . The word length $|g|_S$ is the length of a shortest word in $S$ representing $g$ , and the word metric is $d_S(g, h) = |g^{-1} h|_S$ , the path metric of the Cayley graph restricted to its vertices. The group acts on its Cayley graph by left multiplication, by isometries: $d_S(kg, kh) = d_S(g, h)$ .

Definition— quasi-isometry

A map $f : X \to Y$ of metric spaces is an $(L, C)$ -quasi-isometric embedding ( $L \ge 1$ , $C \ge 0$ ) if

\tfrac{1}{L}\, d(x, x') - C \;\le\; d(f(x), f(x')) \;\le\; L\, d(x, x') + C \quad \text{for all } x, x' \in X.

It is a quasi-isometry if moreover every point of $Y$ lies within $C$ of $f(X)$ . Being quasi-isometric is an equivalence relation (a quasi-isometry has a quasi-inverse, and quasi-isometries compose).

Definition— growth function

The growth function of $(G, S)$ is $\beta_S(r) = |B_S(r)|$ , the number of elements of word length at most $r$ . Write $\beta \preceq \gamma$ if $\beta(r) \le C\gamma(Cr + C) + C$ for some $C$ , and $\beta \sim \gamma$ if $\beta \preceq \gamma \preceq \beta$ . The growth type of $G$ is the $\sim$ -class of $\beta_S$ ; it does not depend on $S$ and is a quasi-isometry invariant. $G$ has polynomial growth if $\beta_S(r) \le C r^d$ , exponential growth if $\beta_S(r) \ge c^r$ for some $c > 1$ , and intermediate growth otherwise.

Definition— δ-hyperbolic space and hyperbolic group

A geodesic metric space is $\delta$ -hyperbolic (in the sense of Rips) if every geodesic triangle is $\delta$ -slim: each side lies in the closed $\delta$ -neighbourhood of the union of the other two. A finitely generated group is hyperbolic (word-hyperbolic, Gromov-hyperbolic) if its Cayley graph, with edges of length 1, is $\delta$ -hyperbolic for some $\delta \ge 0$ .

Definition— amenable group

A group $G$ is amenable if there is a finitely additive, left-invariant probability measure $\mu$ defined on all subsets of $G$ : $\mu(G) = 1$ , $\mu(A \sqcup B) = \mu(A) + \mu(B)$ and $\mu(gA) = \mu(A)$ . For finitely generated $G$ this is equivalent to the Følner condition (Følner, 1955): for every $\varepsilon > 0$ there is a finite non-empty $F \subseteq G$ with $|Fs \,\triangle\, F| \le \varepsilon |F|$ for all $s \in S$ — sets whose boundary is small compared with their size.

A group action $G \curvearrowright X$ on a metric space is proper if for every compact $K \subseteq X$ the set $\{g \in G : gK \cap K \ne \varnothing\}$ is finite, and cocompact if $X = GK$ for some compact $K$ . A metric space is proper if its closed balls are compact, and geodesic if any two points are joined by a path whose length is their distance.

Worked examplesH

Examples and non-examples

Example— Finite groups, and $\Z$ with different generators

A finite group is quasi-isometric to a point: the map to a point is a $(1, \operatorname{diam})$ -quasi-isometry. For $G = \Z$ and $S = \{\pm 1\}$ the Cayley graph is a line; for $S' = \{\pm 2, \pm 3\}$ it is a "thick" line with $|n|_{S'} = \lceil |n|/3 \rceil$ for $|n| \ge 2$ (and $|1|_{S'} = 2$ , since $1 = 3 - 2$ ). The two word metrics satisfy $\tfrac13 |n|_S \le |n|_{S'} \le 2|n|_S$ , as Theorem 1 below predicts, and both are quasi-isometric to $\R$ .

Example— Fundamental groups and universal covers

$\Z^n$ acts on $\R^n$ by translations, properly and cocompactly, so by the Švarc–Milnor lemma $\Z^n$ is quasi-isometric to $\R^n$ . The fundamental group $\pi_1(\Sigma_g)$ of a closed surface of genus $g \ge 2$ acts by deck transformations on the universal cover, the hyperbolic plane $\mathbb{H}^2$ with a metric of curvature $-1$ , so $\pi_1(\Sigma_g)$ is quasi-isometric to $\mathbb{H}^2$ ; all these surface groups are quasi-isometric to one another. $\mathrm{SL}(2, \Z)$ contains a free subgroup of index 12 — the subgroup generated by Sanov's matrices in Theorem 4 below, which together with $-I$ generate the congruence subgroup of matrices congruent to $I$ modulo 2 — so $\mathrm{SL}(2, \Z)$ is quasi-isometric to a tree (a finite-index subgroup is always quasi-isometric to the whole group).

Example— Distinguishing groups up to quasi-isometry

$\Z^2$ and $\Z^3$ are not quasi-isometric: their growth functions are $\sim r^2$ and $\sim r^3$ , and growth type is a quasi-isometry invariant. $\Z^2$ and $F_2$ are not quasi-isometric: polynomial versus exponential growth. $F_2$ and $F_3$ are quasi-isometric (all regular trees of degree at least 3 are quasi-isometric to one another), although they are not isomorphic. $F_2$ and $\pi_1(\Sigma_2)$ both have exponential growth and are hyperbolic, yet they are not quasi-isometric: the tree has infinitely many ends, the hyperbolic plane only one.

Example— The Heisenberg group: polynomial growth of degree 4

The integer Heisenberg group $H_3(\Z)$ of upper unitriangular $3 \times 3$ integer matrices, written as triples with $(a, b, c)(a', b', c') = (a + a', b + b', c + c' + ab')$ , is generated by $x = (1, 0, 0)$ and $y = (0, 1, 0)$ , with central commutator $[x, y] = (0, 0, 1)$ . Since $[x^n, y^n] = (0, 0, n^2)$ , the central coordinate grows quadratically along words of linear length, and $|B(r)| \sim r^4$ , not $r^3$ . The Bass–Guivarc'h formula gives the degree $d = \sum_k k \cdot \operatorname{rank}(G_k / G_{k+1})$ for the lower central series of a nilpotent group: here $1 \cdot 2 + 2 \cdot 1 = 4$ . The experiment below estimates it.

Example— A non-example of hyperbolicity: the grid

In $\mathrm{Cay}(\Z^2, \{(\pm1, 0), (0, \pm1)\})$ take the geodesic triangle with vertices $(0,0)$ , $(n,0)$ , $(n,n)$ : sides along the $x$ -axis and the line $x = n$ , and as third side the staircase path $(0,0) \to (0, n) \to (n, n)$ , which has length $2n$ and is a geodesic. The point $(0, n)$ on the third side has distance $n$ from the union of the other two. So no $\delta$ works: $\Z^2$ is not hyperbolic. By contrast, a tree is $0$ -hyperbolic (every geodesic triangle is a tripod), and $\mathbb{H}^2$ is $\delta$ -hyperbolic with $\delta = \log(1 + \sqrt2)$ .

ProofH

Central theorems

Theorem— Theorem 1 (the word metric is well defined up to bi-Lipschitz maps)

Let $S$ and $S'$ be finite generating sets of $G$ , and let $L = \max_{s \in S} |s|_{S'}$ . Then $|g|_{S'} \le L\, |g|_S$ for all $g \in G$ . Consequently the identity map $(G, d_S) \to (G, d_{S'})$ is bi-Lipschitz, and $\mathrm{Cay}(G, S)$ and $\mathrm{Cay}(G, S')$ are quasi-isometric.

Proof

Write $g = s_1^{\varepsilon_1} \cdots s_n^{\varepsilon_n}$ with $n = |g|_S$ , $s_i \in S$ , $\varepsilon_i = \pm 1$ . Each $s_i^{\pm1}$ is a product of at most $L$ letters of $S'$ (inverting a word does not change its length). Concatenating gives a word in $S'$ of length at most $Ln$ representing $g$ . Applying this to $g^{-1}h$ gives $d_{S'}(g, h) \le L\, d_S(g, h)$ , and exchanging the roles of $S$ and $S'$ gives the reverse inequality with $L' = \max_{s' \in S'} |s'|_S$ . Every point of the Cayley graph lies within $\tfrac12$ of a vertex, so each Cayley graph is quasi-isometric to its vertex set.

∎

Theorem— Theorem 2 (Švarc–Milnor lemma; Švarc 1955, Milnor 1968)

Let a group $G$ act properly and cocompactly by isometries on a proper geodesic metric space $X$ . Then $G$ is finitely generated, and for every $x_0 \in X$ the orbit map $G \to X$ , $g \mapsto g x_0$ , is a quasi-isometry (for any word metric on $G$ ).

Proof

By cocompactness $X = GK$ for a compact $K$ ; choose $R$ with $K \subseteq \bar B(x_0, R)$ , so the translates $g\,\bar B(x_0, R)$ cover $X$ . Let

S = \{ s \in G : d(x_0, s x_0) \le 2R + 1 \}.

$S$ is finite and symmetric. The ball $K' = \bar B(x_0, 2R + 1)$ is compact because $X$ is proper, and $s x_0 \in sK' \cap K'$ for every $s \in S$ , so $S$ is finite by properness. It is symmetric because $d(x_0, s^{-1} x_0) = d(s x_0, x_0)$ .

$S$ generates $G$ , and $|g|_S \le d(x_0, g x_0) + 1$ . Let $g \in G$ , $D = d(x_0, g x_0)$ and $n = \lfloor D \rfloor + 1$ . Choose a geodesic from $x_0$ to $g x_0$ and points $x_0 = y_0, y_1, \dots, y_n = g x_0$ on it with $d(y_i, y_{i+1}) = D/n < 1$ . For each $i$ choose $h_i \in G$ with $d(y_i, h_i x_0) \le R$ , taking $h_0 = 1$ and $h_n = g$ . Then

d(x_0, h_i^{-1} h_{i+1} x_0) = d(h_i x_0, h_{i+1} x_0) \le R + 1 + R,

so $s_i := h_i^{-1} h_{i+1} \in S$ , and $g = h_n = s_0 s_1 \cdots s_{n-1}$ by telescoping. Hence $|g|_S \le n \le D + 1$ .

$d(x_0, g x_0) \le \lambda |g|_S$ , where $\lambda = \max_{s \in S} d(x_0, s x_0)$ . If $g = t_1 \cdots t_k$ with $t_j \in S$ , then by the triangle inequality and because $G$ acts by isometries,

d(x_0, g x_0) \le \sum_{j=1}^{k} d(t_1 \cdots t_{j-1} x_0,\, t_1 \cdots t_j x_0) = \sum_{j=1}^{k} d(x_0, t_j x_0) \le \lambda k.

Apply both bounds to $g^{-1}h$ , using $d(g x_0, h x_0) = d(x_0, g^{-1} h x_0)$ and $d_S(g, h) = |g^{-1}h|_S$ :

d_S(g, h) - 1 \;\le\; d(g x_0, h x_0) \;\le\; \lambda\, d_S(g, h).

So the orbit map is a quasi-isometric embedding with $L = \max(\lambda, 1)$ and $C = 1$ , and every point of $X$ lies within $R$ of the orbit. By Theorem 1 the conclusion holds for every finite generating set.

∎

Theorem— Corollary

If $M$ is a closed Riemannian manifold, then $\pi_1(M)$ is finitely generated and quasi-isometric to the universal cover $\tilde M$ with the lifted metric. In particular, closed manifolds with quasi-isometrically different universal covers have non-isomorphic fundamental groups.

Proof

$\tilde M$ with the pulled-back metric is complete, hence proper and geodesic by the Hopf–Rinow theorem; deck transformations act by isometries, properly (the action is a covering action) and cocompactly ( $\tilde M = \pi_1(M) \cdot K$ for a compact $K$ mapping onto $M$ , such as the closure of a lift of a fundamental domain). Apply Theorem 2.

∎

Theorem— Theorem 3 (ping-pong lemma, two players)

Let $G$ act on a set $X$ , and let $a, b \in G$ . Suppose $X_1, X_2 \subseteq X$ are disjoint and non-empty, and for every integer $n \ne 0$

a^n(X_2) \subseteq X_1 \qquad\text{and}\qquad b^n(X_1) \subseteq X_2.

Then $a$ and $b$ generate a free group of rank 2: no non-trivial reduced word in $a^{\pm1}, b^{\pm1}$ is the identity.

Proof

A non-trivial reduced word is a product of non-zero powers of $a$ and $b$ that alternate. First let $w = a^{n_1} b^{m_1} a^{n_2} \cdots b^{m_{k-1}} a^{n_k}$ begin and end with a power of $a$ . Reading right to left, $a^{n_k}$ sends $X_2$ into $X_1$ , then $b^{m_{k-1}}$ sends that into $X_2$ , and so on, until $a^{n_1}$ lands in $X_1$ . So $w(X_2) \subseteq X_1$ . Since $X_2$ is non-empty and disjoint from $X_1$ , $w$ moves some point, so $w \ne 1$ . Any other non-trivial reduced word $w$ can be conjugated into this form: if $w = b^{m_1} \cdots b^{m_k}$ , then $a w a^{-1}$ has it; if $w$ begins with $a^{n_1}$ and ends with a power of $b$ , choose $n \ne 0, -n_1$ and use $a^{n} w a^{-n}$ ; if it begins with a power of $b$ and ends with $a^{n_k}$ , use $a^{-n} w a^{n}$ with $n \ne 0, -n_k$ . A conjugate of $w$ is $\ne 1$ only if $w \ne 1$ .

∎

Theorem— Theorem 4 (Sanov, 1947)

The matrices $A = \begin{pmatrix} 1 & 2 \\ 0 & 1 \end{pmatrix}$ and $B = \begin{pmatrix} 1 & 0 \\ 2 & 1 \end{pmatrix}$ generate a free subgroup of rank 2 of $\mathrm{SL}(2, \Z)$ .

Proof

Let $\mathrm{SL}(2, \Z)$ act on $\Z^2$ and put $X_1 = \{(x, y) : |x| > |y|\}$ , $X_2 = \{(x, y) : |x| < |y|\}$ : disjoint, non-empty. For $n \ne 0$ , $A^n(x, y) = (x + 2ny, y)$ . If $|x| < |y|$ then

|x + 2ny| \ge 2|n|\,|y| - |x| \ge 2|y| - |x| > |y|,

so $A^n(X_2) \subseteq X_1$ . Symmetrically $B^n(x, y) = (x, y + 2nx)$ and $B^n(X_1) \subseteq X_2$ . Apply Theorem 3.

∎

The same strategy, with rotations of $\mathbb{R}^3$ acting on the sphere, produces a free subgroup of $\mathrm{SO}(3)$ — for example the rotations through $\arccos \tfrac13$ about two perpendicular axes — which is the group-theoretic heart of the Banach–Tarski paradox. More generally, Tits' alternative (1972) says that a finitely generated linear group over a field is either virtually solvable or contains a free subgroup of rank 2.

Theorem— Theorem 5 (free groups are paradoxical, hence not amenable)

For $x \in \{a^{\pm1}, b^{\pm1}\}$ let $W(x) \subseteq F_2$ be the set of reduced words beginning with $x$ . Then

F_2 = \{1\} \sqcup W(a) \sqcup W(a^{-1}) \sqcup W(b) \sqcup W(b^{-1}), \qquad F_2 = W(a) \sqcup a W(a^{-1}) = W(b) \sqcup b W(b^{-1}).

Consequently $F_2$ , and every group containing $F_2$ , is not amenable.

Proof

The first decomposition sorts reduced words by their first letter. For the second: if $w \notin W(a)$ , then $a^{-1}w$ is reduced (no cancellation, since $w$ does not begin with $a$ ) and begins with $a^{-1}$ , so $w = a(a^{-1}w) \in aW(a^{-1})$ . Conversely, if $u = a^{-1}u' \in W(a^{-1})$ is reduced, then $u'$ does not begin with $a$ , so $au = u' \notin W(a)$ . Thus $F_2 = W(a) \sqcup aW(a^{-1})$ , and likewise for $b$ .

Suppose $\mu$ is a finitely additive left-invariant probability measure on all subsets of $F_2$ . Then $1 = \mu(W(a)) + \mu(aW(a^{-1})) = \mu(W(a)) + \mu(W(a^{-1}))$ and likewise $1 = \mu(W(b)) + \mu(W(b^{-1}))$ , so the four disjoint sets $W(a^{\pm1}), W(b^{\pm1})$ have total measure $2 > 1 = \mu(F_2)$ , a contradiction. If $F_2 \le G$ and $\mu$ were an invariant mean on $G$ , choose a set $T$ of representatives of the right cosets $F_2 g$ ; then $\nu(A) = \mu(A T)$ is an invariant mean on $F_2$ (the sets $AT$ , $A \subseteq F_2$ , are disjoint for disjoint $A$ and $(hA)T = h(AT)$ ), which is impossible.

∎

Theorem— Banach–Tarski paradox (1924), statement

Assuming the axiom of choice, a solid ball in $\R^3$ can be partitioned into finitely many pieces (five suffice, and fewer do not — Robinson, 1947) which can be moved by rigid motions to form two balls of the same radius.

The proof combines Theorem 5 for a free subgroup of $\mathrm{SO}(3)$ with the axiom of choice: choose one point in each orbit of the free group on the sphere (minus the countably many fixed points of its non-trivial elements), and transport the decomposition of $F_2$ to the sphere and then to the ball. The pieces are not Lebesgue measurable, so there is no conflict with measure theory: the paradox shows that no finitely additive, rotation-invariant measure can be defined on all subsets of $\R^3$ (von Neumann's insight was that this is a property of the group of motions; in the plane the motion group is amenable, and no such paradox with rigid motions exists). See the axiom of choice and measure theory.

Theorem— Theorem 6 (growth: Gromov 1981; Milnor–Wolf 1968; Grigorchuk 1984), statements

Gromov's polynomial growth theorem. A finitely generated group has polynomial growth if and only if it has a nilpotent subgroup of finite index. The easy direction: a finitely generated nilpotent group has growth $\sim r^d$ with $d = \sum_k k \cdot \operatorname{rank}(G_k/G_{k+1})$ (Bass 1972, Guivarc'h 1973). The hard direction is Gromov's; a proof using harmonic functions was given by Kleiner (2010).
Milnor–Wolf. A finitely generated solvable group has either polynomial or exponential growth.
Milnor (1968). The fundamental group of a closed Riemannian manifold of negative sectional curvature has exponential growth.
Grigorchuk (1984). There are finitely generated groups of intermediate growth, answering a question of Milnor.

Theorem— Theorem 7 (hyperbolic groups; Gromov 1987), statements

Hyperbolicity of geodesic spaces is invariant under quasi-isometry (by the Morse lemma: quasi-geodesics stay close to geodesics). Hence hyperbolicity of a group does not depend on the generating set.
Free groups, finite groups, surface groups $\pi_1(\Sigma_g)$ with $g \ge 2$ , and fundamental groups of closed manifolds of negative sectional curvature are hyperbolic (the last by the Švarc–Milnor lemma, since the universal cover is $\mathrm{CAT}(-1)$ after rescaling, hence $\delta$ -hyperbolic).
A finitely presented group is hyperbolic if and only if it satisfies a linear isoperimetric inequality; then it has a Dehn presentation, and its word problem is solved by Dehn's algorithm in linear time. Hyperbolic groups are finitely presented and contain no subgroup isomorphic to $\Z^2$ .

ExplanationH

The landscape: what is known and what is open

Established. Beyond the theorems above: Stallings' theorem (1968–71) that a finitely generated group has more than one end exactly when it splits over a finite subgroup; quasi-isometric rigidity results such as "every finitely generated group quasi-isometric to $\Z^n$ is virtually $\Z^n$ " (from Gromov's theorem) and "every finitely generated group quasi-isometric to $\mathbb{H}^2$ is virtually a closed surface group" (Tukia 1988, Gabai 1992, Casson–Jungreis 1994); Kesten's criterion (1959) that a finitely generated group is amenable exactly when the return probability of simple random walk does not decay exponentially; Ol'shanskii's counterexample (1980) to von Neumann's conjecture — a non-amenable group with no free subgroup; and the theory of special cube complexes of Haglund and Wise, which Agol used to prove the virtual Haken conjecture for hyperbolic 3-manifolds (2013).

Open problems.

Is every hyperbolic group residually finite?
Gromov's surface subgroup question: does every one-ended hyperbolic group contain a subgroup isomorphic to the fundamental group of a closed surface of genus at least 2? (Yes for fundamental groups of closed hyperbolic 3-manifolds, by Kahn and Markovic, 2012.)
Cannon's conjecture: a hyperbolic group whose Gromov boundary is a 2-sphere acts properly and cocompactly by isometries on $\mathbb{H}^3$ .
Is Richard Thompson's group $F$ amenable?
Grigorchuk's gap conjecture: is there a gap between polynomial growth and growth $e^{\sqrt r}$ ? (Shalom and Tao proved a smaller gap, 2010.)

Formal mathematicsF

What Lean can say: word metrics, quasi-isometries and ping-pong

Mathlib has recently gained a geometric group theory folder: generating families (Group.Generators), the word length and word metric, and the linear lower bound on growth. It also has the ping-pong lemma for free products. We use all three.

The word metric is a metric because word length is subadditive, and Theorem 1 — the reason the subject is about groups and not about generating sets — is proved here by induction on a shortest word:

word_length_mul_leLean 4Applies a library theoremFormally verified

/-- The word length is subadditive: `|gh|_S ≤ |g|_S + |h|_S`. Concatenating a shortest word for
`g` with one for `h` spells `gh`. This is Mathlib's `Group.Generators.wordLength_mul_le`; it makes
`d_S(g, h) = |g⁻¹h|_S` a metric, the **word metric**. -/
theorem word_length_mul_le (P : Group.Generators G ι) (g h : G) :
    P.wordLength (g * h) ≤ P.wordLength g + P.wordLength h :=
  P.wordLength_mul_le g h