Motivation

Von Neumann introduced amenable groups in 1929 to explain the Hausdorff–Banach–Tarski paradox, and showed that the class $AG$ of amenable groups contains all finite and all abelian groups and is closed under four processes: (I) subgroups, (II) quotients, (III) extensions and (IV) directed unions. Day named the smallest class with these properties $EG$, the elementary amenable groups. For fifty years these were the only amenable groups anyone could exhibit, and von Neumann's question whether every non-amenable group contains a free subgroup on two generators — whether $AG$ equals the class $NF$ of groups without such a subgroup — was open. (It was answered in the negative by Ol'shanskii in 1980, the year of this paper, by different methods.)

Ching Chou's Elementary amenable groups (Illinois J. Math. 24 (1980) 396–407, doi:10.1215/ijm/1256047608) gives the structure theory of $EG$ that everything later relies on. Its central result is that the class can be built from finite and abelian groups by extensions and directed unions alone — subgroups and quotients add nothing (Proposition 2.2). From that description three things follow: periodic elementary amenable groups are locally finite, so the periodic non-locally-finite groups of Golod and Novikov–Adjan show $EG \subsetneq NF$ (Theorem 2.3); a finitely generated simple elementary amenable group is finite (Corollary 2.4); and Wolf's conjecture holds in $EG$: a finitely generated elementary amenable group is almost nilpotent or has exponential growth (Theorem 3.2, extending Milnor and Wolf's theorem for solvable groups). A final section introduces a packing property (P) of groups and proves it for every elementary amenable group (Proposition 4.2) and every residually elementary amenable group (Corollary 4.7).

On this platform the definition of $EG$ is already published (the bundle Chou_ElementaryAmenable, from the mission Cannon–Floyd–Parry: Thompson's group F and the simplicity of its commutator subgroup), together with the theorem that Thompson's group $F$ is not elementary amenable (Theorem 4.10) and, from Brin and Squier, that $F$ has no free subgroup on two generators (CannonFloydParry.no_free_subgroup_of_rank_two). This mission formalizes Chou's paper on top of that definition.

Setting

The class $EG$ and its constructible core. Chou.ElementaryAmenable G is an inductive predicate on groups: finite groups and abelian groups are in the class, and the class is closed under isomorphism, subgroups, quotients, extensions and directed unions of subgroups; each rule is a constructor of the published bundle Chou_ElementaryAmenable, where it is stated precisely. Chou builds the hierarchy $EG_0 \subseteq EG_1 \subseteq \cdots$ by transfinite recursion, applying only extensions and directed unions to the finite and abelian groups, and proves that $\bigcup_\alpha EG_\alpha$ is closed under subgroups and quotients, hence equals $EG$. The union $\bigcup_\alpha EG_\alpha$ is realised here without ordinals, as the inductive predicate Chou.Constructible, whose constructors are of_finite, of_commGroup, of_mulEquiv, extension and directedUnion; Chou's transfinite induction over $\alpha$ becomes structural induction over a derivation, with the same case analysis.

Periodic and locally finite groups. A group is periodic if every element has finite order (Mathlib's IsMulTorsion) and locally finite if every finitely generated subgroup is finite (Chou.IsLocallyFinite). Day's class $NF$ is Chou.NoFreeSubgroupOfRankTwo: no homomorphism from the free group on two generators into $G$ is injective.

Growth. For a finite generating set $S$ of $G$, Chou.wordBall S n is the set of products of at most $n$ factors, each in $S$ or with inverse in $S$. $G$ has exponential growth if for some finite generating set the ball of radius $n$ has at least $c^n$ elements for some $c > 1$ and all $n$; it is exponentially bounded if for some finite generating set and every $c > 1$ the balls are eventually smaller than $c^n$. Chou works with $|F^n|$ for products of exactly $n$ elements of a finite generating set $F$; for $F$ symmetric and containing the identity the two agree, and Wolf's observation that the growth type is independent of the generating set is one of the milestones. "Almost nilpotent" is Mathlib's Group.IsVirtuallyNilpotent: a nilpotent subgroup of finite index. A free subsemigroup on two generators means two elements $a, b$ such that distinct positive words in $a, b$ are distinct in $G$ (Chou.HasFreeSubsemigroupOfRankTwo).

Packings. A pair of subsets $(S, X)$ is a packing of $G$ if $(s, x) \mapsto sx$ is a bijection $S \times X \to G$ (Chou.IsPacking), and $G$ has property (P) if every finite subset lies in a finite $S$ for which some $(S, X)$ is a packing (Chou.HasPackingProperty). $G$ is residually elementary amenable if every $x \neq 1$ survives in some elementary amenable quotient (Chou.ResiduallyElementaryAmenable).

Target

The goal is Chou's description of the class, Proposition 2.2 (b) (p. 397): “$EG$ is the smallest class of groups which contains all finite groups and all abelian groups and is closed under processes (III) and (IV).” It is stated as the equivalence ElementaryAmenable G ↔ Constructible G. The milestones follow the paper's order.

Section 2. Proposition 2.1 in two halves — the constructible groups are closed under subgroups and under quotients — which is the whole proof of the goal. Theorem 2.3: periodic elementary amenable groups are locally finite; and its consequence that $NF \setminus EG$ is nonempty. Corollary 2.4: finitely generated simple elementary amenable groups are finite.

Section 3. Lemma 3.1 (an extension of almost nilpotent by almost nilpotent is almost nilpotent or of exponential growth), Theorem 3.2 and Rosenblatt's sharpening Theorem 3.2′, together with the facts Chou uses on the way: a finite-by-nilpotent group is almost nilpotent; a free subsemigroup forces exponential growth; Wolf's independence of the generating set; and Milnor's existence of the growth rate, in the form "exponentially bounded means not of exponential growth".

Section 4. Property (P) for finite groups, for $\mathbb Z$, for finitely generated abelian groups; Lemma 4.1 (directed unions and extensions preserve (P)); Proposition 4.2 (every elementary amenable group has (P)); Lemma 4.6 (a) and Corollary 4.7 (residually elementary amenable groups have (P)); and the free groups.

External theorems as milestones

Chou's Section 3 rests on results the paper cites rather than proves, none of which is in Mathlib. They are stated here as milestones in their own right, so that the dependence is visible and each is a well-defined target: the Milnor–Wolf theorem (a finitely generated solvable group that is exponentially bounded is almost nilpotent); M. Hall's theorem that a finitely generated group has finitely many subgroups of each finite index; that finitely generated nilpotent groups are finitely presented and that a group with a finitely presented subgroup of finite index is finitely presented; Milnor's Lemmas 1–2 in the form Chou states on p. 400 (in a finitely generated exponentially bounded group, a normal subgroup with finitely presented quotient is finitely generated); and Rosenblatt's variant of Lemma 3.1. Section 4 needs one more: free groups are residually finite. Lemma 3.1 and Theorems 3.2, 3.2′ can be closed only once these are; every other milestone is provable from Mathlib and the published library.

Two remarks on Theorem 2.3. Chou's witness for $NF \setminus EG$ is a periodic group that is not locally finite (Golod; Novikov–Adjan), whose existence is not formalized. The platform already holds a different witness: Thompson's group $F$ is not elementary amenable (Cannon–Floyd–Parry, Theorem 4.10) and has no free subgroup on two generators (Brin–Squier); both are published and proved, and the milestone is proved from them. The inclusion $EG \subseteq NF$ itself is von Neumann's theorem that amenable groups contain no free subgroup of rank two, which passes through the definition of amenability and is not part of this mission.

What is left out

The ordinal-indexed hierarchy $EG_\alpha$ and the remark that it stabilises at some $\alpha_0 + 1$ (Proposition 2.2 (a)) are replaced by the inductive predicate. Chou's two examples of finitely generated groups in $EG$ that are not almost solvable (p. 402), the Golod–Shafarevich discussion, and Lemma 4.6 (b) (ordinal-indexed normal series) are omitted. Propositions 4.3–4.5 on almost convergent sets, and Milnor's remark that exponentially bounded groups are amenable, need invariant means on $\ell^\infty(G)$; amenability itself is the subject of Garrido I.

References

• C. Chou, Elementary amenable groups, Illinois J. Math. 24 (1980), 396–407.
• M. M. Day, Amenable semigroups, Illinois J. Math. 1 (1957), 509–544.
• J. Milnor, Growth of finitely generated solvable groups, J. Differential Geometry 2 (1968), 447–449; J. A. Wolf, Growth of finitely generated solvable groups and curvature of Riemannian manifolds, ibid. 421–446.
• J. M. Rosenblatt, Invariant measures and growth conditions, Trans. Amer. Math. Soc. 193 (1974), 33–53.
• J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Math. 42 (1996), 215–256 (Theorem 4.10); M. G. Brin, C. C. Squier, Groups of piecewise linear homeomorphisms of the real line, Invent. Math. 79 (1985), 485–498.