Motivation

This mission formalizes John Milnor's Growth of finitely generated solvable groups, J. Differential Geometry 2 (1968) 447–449 (doi:10.4310/jdg/1214428659), a three-page addendum to J. A. Wolf's Growth of finitely generated solvable groups and curvature of Riemannian manifolds, which precedes it in the same issue (421–446, doi:10.4310/jdg/1214428658). Milnor's note has one theorem and three lemmas, and "for definitions and explanations the reader is referred to" Wolf.

Wolf proved that a polycyclic group "either has a finitely generated nilpotent subgroup of finite index and thus is of polynomial growth, or has no such subgroup and is of exponential growth" (p. 421). Milnor's Theorem closes the gap between polycyclic and solvable: "Let $\Gamma$ be a solvable group which is not polycyclic, and $S$ a finite set of generators for $\Gamma$. Then there exists an exponential lower bound $g_S(m) \ge (\text{constant})^m > 1$ for the growth function $g_S$ of $\Gamma$." Together the two papers give the Milnor–Wolf theorem, "that a finitely generated solvable group, either is polycyclic and has a nilpotent subgroup of finite index and is thus of polynomial growth, or has no nilpotent subgroup of finite index and is of exponential growth" (Wolf, p. 421). Milnor notes that Wolf's results "provide a partial answer to a problem which was posed by the author in Amer. Math. Monthly 75 (1968) 685–686", and Wolf raises "the question of whether every finitely generated group $\Gamma$, which is not of exponential growth, necessarily has a nilpotent subgroup of finite index" (p. 422); Grigorchuk's groups of intermediate growth (1984) later answered that in the negative, while Gromov (1981) proved that polynomial growth does force a nilpotent subgroup of finite index. Chou's 1980 extension of the Milnor–Wolf theorem to elementary amenable groups, the mission Chou: elementary amenable groups on this platform, cites exactly this theorem. Wolf's paper is the subject of a companion mission.

Setting

Growth. For a finite subset $S$ of a group $\Gamma$, Wolf's growth function $g_S(m)$ (p. 426) is the number of elements expressible as words of length $\le m$ based on $S$, a word $s_1^{a_1} \cdots s_r^{a_r}$ having length $|a_1| + \cdots + |a_r|$. MilnorWolf.growthFunction S m takes $g_S(m)$ as the size of the ball Chou.wordBall S m of the published growth bundle, the set of products of at most $m$ factors from $S \cup S^{-1}$. $\Gamma$ has exponential growth, the published Chou.HasExponentialGrowth, if for some finite generating set $S$ there is $c > 1$ with $g_S(m) \ge c^m$ for all $m$; Wolf shows (p. 434) that this does not depend on $S$.

Polycyclic groups. Wolf's Proposition 4.1 (p. 433) gives eleven equivalent conditions; the definition used here is condition (1): "There is a normal series $\Gamma = A_0 \supset A_1 \supset \cdots \supset A_t = \{1\}$ with every quotient $A_i/A_{i+1}$ finite or infinite cyclic." This is MilnorWolf.IsPolycyclic. A solvable group is Mathlib's Group.IsSolvable: the derived series reaches the trivial subgroup.

Milnor's standing assumptions. The three lemmas concern a group extension $1 \to A \to B \to C \to 1$ where "we will always assume that $A$ is abelian and that $B$ is finitely generated." In the statements, $B$ is a finitely generated group, $A$ an abelian normal subgroup, and $C$ the quotient $B/A$.

Formalization targets

Milnor's Theorem (p. 447)

"Let $\Gamma$ be a solvable group which is not polycyclic, and $S$ a finite set of generators for $\Gamma$. Then there exists an exponential lower bound $g_S(m) \ge (\text{constant})^m > 1$ for the growth function $g_S$ of $\Gamma$." Stated for an arbitrary finite generating set $S$:

$$\exists\, c > 1 \quad \forall\, m \ge 1: \qquad c^m \le g_S(m).$$

This is the goal. The constant is existentially quantified, so a sharper bound does not change the statement. The milestones are Milnor's three lemmas, in order, followed by one published Open theorem of the Chou mission that they prove: Chou's form of Lemmas 1 and 2, where the normal subgroup need not be abelian.

Significance

Milnor's Theorem is the half of the Milnor–Wolf theorem that reaches beyond polycyclic groups: with Wolf's polycyclic dichotomy it says that a finitely generated solvable group is either almost nilpotent, of polynomial growth, or of exponential growth, with nothing in between. That statement is what Chou's Theorem 3.2 extends to elementary amenable groups, and it is the reason a group of intermediate growth cannot be solvable or elementary amenable, the fact that placed Grigorchuk's groups outside those classes.

Formalizing it produces, besides the Theorem, the three lemmas as reusable library results: the subgroup spanned by the conjugates $\beta^k \alpha \beta^{-k}$ is finitely generated when $B$ is not of exponential growth; a normal subgroup with finitely presented quotient is normally generated by finitely many elements; and polycyclic-by-abelian without exponential growth is polycyclic. The proof is complete in the paper; nothing here is open mathematics. On this platform the Theorem and the lemmas are stated and unproved; Chou's mission holds the Open non-abelian form of Lemmas 1 and 2 and two Open reductions that resolve once this mission and the Wolf mission close their externals.

Difficulty

The obvious attempt, to bound the growth of $B$ below by the growth of a free subsemigroup found inside it, is not what Milnor does and does not obviously work for an arbitrary abelian-by-solvable extension. Milnor's argument turns the growth hypothesis into finite generation: among the $2^m$ expressions $\beta\alpha^{i_1} \cdots \beta\alpha^{i_m}$ two must coincide, and the resulting relation expresses $\alpha_m = \beta^m \alpha \beta^{-m}$ in terms of $\alpha_1, \ldots, \alpha_{m-1}$. The delicate step is running this over a whole set of normal generators of $A$ and over each of finitely many $\beta$'s in turn, so that $A$ itself comes out finitely generated (Lemma 3), and then up the derived series of $\Gamma$. In Lean the work is in Lemma 2, which needs the finite presentation of $C$ transported to a presentation on the images of chosen generators of $B$, and in Lemma 3, which needs that a polycyclic group is finitely presented and that an extension of polycyclic groups is polycyclic.

Formalization scope

Growth is measured on the closed balls of the published bundle Chou_Growth: Chou.wordBall S m is the set of products of at most $m$ letters from $S \cup S^{-1}$, and $g_S(m)$ is its cardinality (a Nat.card, finite because $S$ is a Finset). "Not of exponential growth" is the negation of the existential definition, so it is a statement about every finite generating set. Polycyclic is Wolf's condition (1); the definition fixes the reading of "normal series". The abelian hypothesis on $A$ is Mathlib's IsMulCommutative on the subgroup; finite generation and finite presentation are Mathlib's Group.FG and Group.IsFinitelyPresented.

The Theorem's hypotheses are satisfiable: the trivial group is polycyclic, so "not polycyclic" excludes it, and a solvable non-polycyclic finitely generated group exists (the lamplighter group $\mathbb Z/2 \wr \mathbb Z$). No hypothesis is vacuous and no definition makes a target trivially true.

The definitions of polycyclic group, polynomial growth and Wolf's growth exponents $E_1, E_2$ are stated in the bundle MilnorWolf_Growth here because Milnor defers all definitions to Wolf; the results of Wolf's paper, in particular the polycyclic dichotomy that combines with this Theorem into the Milnor–Wolf theorem, belong to the companion mission. Nothing of Milnor's note is omitted. Contributions welcome: proofs of the three lemmas and the Theorem, and general library results they need, such as finite presentability of polycyclic groups.

Selected references

• J. Milnor, Growth of finitely generated solvable groups, J. Differential Geometry 2 (1968), 447–449. doi:10.4310/jdg/1214428659
• J. A. Wolf, Growth of finitely generated solvable groups and curvature of Riemannian manifolds, J. Differential Geometry 2 (1968), 421–446. doi:10.4310/jdg/1214428658
• J. Milnor, A note on curvature and fundamental group, J. Differential Geometry 2 (1968), 1–7.
• A. G. Kurosh, Theory of groups, vol. II, Chelsea, 1956.
• R. I. Grigorchuk, Degrees of growth of finitely generated groups, and the theory of invariant means, Math. USSR-Izv. 25 (1985), 259–300 (Russian original 1984). doi:10.1070/IM1985v025n02ABEH001281
• M. Gromov, Groups of polynomial growth and expanding maps, Publ. Math. IHÉS 53 (1981), 53–78. doi:10.1007/BF02698687
• C. Chou, Elementary amenable groups, Illinois J. Math. 24 (1980), 396–407 (p. 400). doi:10.1215/ijm/1256047608