This mission formalizes A. Garrido, An introduction to amenable groups, lecture notes from four talks at the Oxford Advanced Class in Algebra, Michaelmas 2013 (archived PDF) — its Section 4, the (first) Grigorchuk group and its solution of half of the von Neumann–Day problem.

Motivation

The first two Garrido missions, Amenable Groups I and Amenable Groups II (the Banach–Tarski paradox), established the inclusions $EG \subseteq AG \subseteq NF$ between the elementary amenable groups, the amenable groups, and the groups with no free subgroup of rank two. "The von Neumann–Day problem asks whether these inclusions are strict" (p. 12). Ol'shanskii settled $AG \neq NF$; "The other part of the problem was solved in 1985 by Grigorchuk" (p. 12), with the theorem this mission targets.

Chou's theorem that every torsion group in $EG$ is locally finite "traces a clear route for solving the Day problem. Namely, it suffices to find an amenable torsion group which is not locally finite" (p. 13). The Grigorchuk group is such a group: a finitely generated, infinite group of automorphisms of the binary tree in which every element has order a power of $2$, and whose growth is subexponential, so that it is amenable.

Setting

The infinite rooted binary tree $T$ has as vertices the finite words in $\{0, 1\}$, and its automorphisms are the permutations of the vertices that preserve length and prefixes. The Grigorchuk group $\Gamma$ is generated by four of them: $a$ exchanges the two subtrees below the root, and $b$, $c$, $d$ fix the first level and are defined recursively by $b = (a, c)$, $c = (a, d)$, $d = (1, b)$, meaning that $b$ acts on the subtree below $0$ as $a$ and on the subtree below $1$ as $c$, and so on.

$St(n)$ is the subgroup of $\Gamma$ fixing every vertex of level $n$. An element $g \in St(n)$ acts on each of the $2^n$ subtrees below level $n$ as a tree automorphism, its section there. $\psi_n$ sends $g$ to the tuple of these sections, and for $g \in St(3)$, $g_{ijk}$ is its section below the vertex $ijk$. $l(g)$ is the word length with respect to $\{a, b, c, d\}$.

Formalization targets

Goal — Theorem 4.1

"The (first) Grigorchuk group $\Gamma$ is amenable but not elementary amenable" (p. 12). This is the goal because it is the theorem the section proves and the one that separates $EG$ from $AG$.

The structure of $\Gamma$ — p. 14

Conjugation by $a$ exchanges the two sections of an element of $St(1)$; $\{1, b, c, d\}$ is a Klein four-group and $St(1)$ is generated by $b, c, b^a, c^a$; $\Gamma$ is infinite, since $St(1)$ maps onto it; and the maps $\psi_n : St(n) \to \Gamma^{2^n}$ are monomorphisms.

Not elementary amenable — Proposition 4.7

Every element of $\Gamma$ has order a power of $2$, so $\Gamma$ is an infinite finitely generated torsion group and, by Chou's Theorem 4.2, not in $EG$. The notes omit the proof of Proposition 4.7 and refer to de la Harpe's book; it is a milestone to be proved here.

Amenable — Lemma 4.8 and Theorem 4.9

The length contraction $\sum_{ijk} l(g_{ijk}) \le \frac34 l(g) + 8$ for $g \in St(3)$, the index $|\Gamma : St(3)| = 2^7$, and a general inequality comparing the balls of a group with those of a subgroup of finite index give subexponential growth (Theorem 4.9); Theorem 3.8 of the first Garrido mission then gives amenability.

Significance

The Grigorchuk group is one of the central examples of geometric group theory: the first group of intermediate growth, a finitely generated infinite torsion group, and the separation of amenable from elementary amenable groups. Neither Mathlib nor the platform has it, and a search of Lean Pool, Tau Ceti and the Palomar registry found no formalization; Mathlib's only mention is a bibliography entry in its Schreier-graph file. The tree-automorphism definitions here are reusable for other groups acting on the binary tree. Nothing here is a new mathematical result: all of it is classical, and the work is formalization.

Difficulty

Lemma 4.8 is the hard step: a careful count, over three levels of sections, of how a shortest word shrinks and how many cancellations occur. Proposition 4.7 has no proof in the notes; the standard argument is an induction on word length through the sections. The growth argument of Theorem 4.9 is an estimate on $\lim_k \gamma(k)^{1/k}$ built from Lemma 4.8 and the ball inequality.

Formalization scope

The tree is modelled by its vertices, List Bool, and $\Gamma$ is a subgroup of the group of tree automorphisms, following the notes' "a group of automorphisms of $T$". The generators are defined by Garrido's recursion, and the bundle proves that each is an involutive automorphism; sections are defined for every automorphism and every vertex, with a proof that they are automorphisms. The sections of $St(1)$ and $St(n)$ are shown to lie in $\Gamma$ as part of the $\psi_n$ milestone rather than assumed.

One trivialising formalization is ruled out: $\Gamma$ is not taken to be an abstract group given by a presentation or by fiat, but the concrete group of tree automorphisms the notes define, so that the finiteness, torsion and growth statements are about that group.

What is left out

Definition 4.4 and Lemma 4.5, the ordinal hierarchy $EG_\alpha$, and Theorem 4.3 are covered by the Chou 1980 mission, which proved Theorem 4.3 with an inductive predicate in place of the ordinals; Theorem 4.2 enters as a reference. Ol'shanskii's $AG \neq NF$ is outside the notes' scope ("beyond the scope of these talks", p. 12) and is not formalized.

Selected references

• A. Garrido, An introduction to amenable groups, lecture notes, Oxford Advanced Class in Algebra, Michaelmas 2013. archived PDF
• R. I. Grigorchuk, Degrees of growth of finitely generated groups, and the theory of invariant means, Math. USSR-Izvestiya 25 (1985), 259. DOI
• C. Chou, Elementary amenable groups, Illinois J. Math. 24 (1980), 396–407. DOI
• P. de la Harpe, Topics in Geometric Group Theory, Chicago Lectures in Mathematics, University of Chicago Press, 2000.