Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Lemma 3: if B/AB/AB/A is polycyclic and BBB is not of exponential growth, then BBB is polycyclic

Proved
Milnor.isPolycyclic_of_isPolycyclic_quotient_of_not_hasExponentialGrowth

by dbenbenn · Sep 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

group-growthgroup-theorypolycyclic-groupssolvable-groups

Let BBB be a finitely generated group and AAA an abelian normal subgroup. If B/AB/AB/A is polycyclic and BBB does not have exponential growth, then BBB is polycyclic.

Preamble
import Definitions.Def_Chou_Growth
import Definitions.Def_MilnorWolf_Growth
import Mathlib
Formal statement
namespace Milnor

/-- Milnor, Lemma 3 (p. 448), in the standing setting of a group extension `1 → A → B → C → 1`
with `A` abelian and `B` finitely generated: if `C` is polycyclic, and `B` does not have
exponential growth, then `B` must be polycyclic also. -/
theorem isPolycyclic_of_isPolycyclic_quotient_of_not_hasExponentialGrowth {B : Type*} [Group B]
    [Group.FG B] (A : Subgroup B) [A.Normal] [IsMulCommutative A]
    (hC : MilnorWolf.IsPolycyclic (B ⧸ A)) (h : ¬ Chou.HasExponentialGrowth B) :
    MilnorWolf.IsPolycyclic B := by
  sorry

end Milnor
Source
Milnor, J., Growth of finitely generated solvable groups, Journal of Differential Geometry 2 (1968) 447–449, https://doi.org/10.4310/jdg/1214428659, Lemma 3, p. 448
Read-back

What the Lean code literally says, in plain math · claude-opus-5

Read-back

The file contains one declaration, a theorem. Its proof is not part of what is being read back here; only the statement is rendered.


The statement

Let BBB be a group. (BBB ranges over all groups, in any universe; neither the way it is supplied nor the way its group structure is supplied restricts it in any manner beyond its being a group.)

Assume:

  1. BBB is finitely generated as a group. Unfolded: there is a finite subset S⊆BS \subseteq BS⊆B such that the smallest subgroup of BBB containing SSS is all of BBB. (The subgroup generated by a set is defined as the intersection of all subgroups containing it.)

  2. AAA is a subgroup of BBB. This is the one argument that is explicit; the theorem is quantified universally over it.

  3. AAA is normal in BBB. Unfolded: for every n∈An \in An∈A and every g∈Bg \in Bg∈B, one has gng−1∈Ag n g^{-1} \in Agng−1∈A.

  4. AAA is abelian. Unfolded: the multiplication of BBB, restricted to AAA (where AAA is regarded as a group in its own right, with the multiplication inherited from BBB), is commutative — that is, xy=yxxy = yxxy=yx for all x,y∈Ax, y \in Ax,y∈A. Nothing is assumed about commutativity anywhere else in BBB.

  5. The quotient group B/AB/AB/A is polycyclic, in the sense spelled out in §"Polycyclic" below. Here B/AB/AB/A is the set of left cosets of AAA in BBB, carried to a group by hypothesis 3.

  6. BBB does not have exponential growth, in the sense spelled out in §"Exponential growth" below.

Then:

BBB is polycyclic, in the same sense as in hypothesis 5.

Item 2 is a universally quantified variable; items 1, 3, 4, 5 and 6 are hypotheses — 1, 3 and 4 supplied as background structural assumptions and 5 and 6 as ordinary named ones. Logically all five hypotheses stand on equal footing, and the statement carries every one of them.


Polycyclic

A group GGG is polycyclic, in the sense used here, when:

There exist a natural number ttt and a family of subgroups

A0,  A1,  …,  At  ≤  GA_0,\; A_1,\; \dots,\; A_t \;\le\; GA0​,A1​,…,At​≤G

(that is, a function from the index set {0,1,…,t}\{0, 1, \dots, t\}{0,1,…,t}, which has t+1t+1t+1 elements, to the subgroups of GGG) such that

  • A0=GA_0 = GA0​=G (the whole group),
  • At={1}A_t = \{1\}At​={1} (the trivial subgroup),
  • and for every index iii with 0≤i≤t−10 \le i \le t-10≤i≤t−1, both of the following hold:
    • Ai+1≤AiA_{i+1} \le A_iAi+1​≤Ai​, and
    • the subgroup Ai+1∩AiA_{i+1} \cap A_iAi+1​∩Ai​, viewed as a subgroup of AiA_iAi​, is normal in AiA_iAi​, and the quotient group Ai/(Ai+1∩Ai)A_i / (A_{i+1} \cap A_i)Ai​/(Ai+1​∩Ai​) formed with respect to that normality is cyclic.

Several points of fine print:

  • The subgroup appearing in the quotient is literally the preimage of Ai+1A_{i+1}Ai+1​ under the inclusion Ai↪GA_i \hookrightarrow GAi​↪G, i.e. {x∈Ai:x∈Ai+1}=Ai+1∩Ai\{x \in A_i : x \in A_{i+1}\} = A_{i+1} \cap A_i{x∈Ai​:x∈Ai+1​}=Ai+1​∩Ai​. Because Ai+1≤AiA_{i+1} \le A_iAi+1​≤Ai​ is asserted alongside it, this is the same as Ai+1A_{i+1}Ai+1​ itself regarded inside AiA_iAi​; but the two conjuncts are asserted independently, and the intersection form is what the quotient is actually taken by.

  • The normality assertion is part of the existential claim, not a side condition: the statement asserts that such a chain exists together with proofs that each step is normal in the previous one. Since normality is a proposition (proof-irrelevant), this is equivalent to the conjunction "Ai+1∩AiA_{i+1} \cap A_iAi+1​∩Ai​ is normal in AiA_iAi​, and the resulting quotient is cyclic".

  • Only subnormality is claimed. The AiA_iAi​ are not required to be normal in GGG, only each one normal (after intersecting) in its predecessor.

  • Cyclic here means: there exists an element ggg of the quotient group such that the map Z→Ai/(Ai+1∩Ai)\mathbb{Z} \to A_i/(A_{i+1}\cap A_i)Z→Ai​/(Ai+1​∩Ai​), k↦gkk \mapsto g^kk↦gk, is surjective. This includes the trivial group (take g=1g = 1g=1), and allows either a finite cyclic group or an infinite cyclic group.

  • Nothing forces the chain to descend strictly. Repetitions Ai+1=AiA_{i+1} = A_iAi+1​=Ai​ are permitted (the quotient is then trivial, hence cyclic), and the length ttt is not required to be minimal or to bound anything.

  • Degenerate case t=0t = 0t=0. Then the family has a single member A0A_0A0​, the index set of steps is empty so no step conditions are imposed, and the two remaining conditions read A0=GA_0 = GA0​=G and A0={1}A_0 = \{1\}A0​={1}. So "polycyclic with t=0t = 0t=0" says exactly that GGG is the trivial group. This case is genuinely included, and the trivial group is polycyclic.


Word balls and exponential growth

For a group GGG, a subset S⊆GS \subseteq GS⊆G and a natural number nnn, the word ball BS(n)B_S(n)BS​(n) is

BS(n)  =  { g∈G  :  ∃ k≤n and x1,…,xk∈G with (xj∈S or xj−1∈S) for each j, and g=x1x2⋯xk }.B_S(n) \;=\; \Bigl\{\, g \in G \;:\; \exists\, k \le n \text{ and } x_1,\dots,x_k \in G \text{ with } \bigl(x_j \in S \text{ or } x_j^{-1} \in S\bigr) \text{ for each } j, \text{ and } g = x_1 x_2 \cdots x_k \,\Bigr\}.BS​(n)={g∈G:∃k≤n and x1​,…,xk​∈G with (xj​∈S or xj−1​∈S) for each j, and g=x1​x2​⋯xk​}.

Fine print on this set:

  • The word is a finite list of elements, read in order, and the product is taken in list order x1x2⋯xkx_1 x_2 \cdots x_kx1​x2​⋯xk​ (the product is formed by folding from the right against the identity, so a list [x1,x2,x3][x_1,x_2,x_3][x1​,x2​,x3​] gives x1(x2(x3⋅1))x_1(x_2(x_3 \cdot 1))x1​(x2​(x3​⋅1)) — by associativity, the product in the written order).

  • The generating set SSS is not assumed symmetric. Each letter is allowed to lie in SSS or to have its inverse in SSS, so the ball is the ball with respect to S∪S−1S \cup S^{-1}S∪S−1.

  • The length condition is k≤nk \le nk≤n, a closed ball. In particular the empty list (k=0k = 0k=0, empty product =1= 1=1) always qualifies, so 1∈BS(n)1 \in B_S(n)1∈BS​(n) for every nnn, and BS(0)={1}B_S(0) = \{1\}BS​(0)={1} exactly. The balls are nested increasing in nnn.

A group GGG has exponential growth, in the sense used here, when:

There exists a finite subset S⊆GS \subseteq GS⊆G such that

  • the subgroup generated by SSS is all of GGG, and
  • there exists a real number ccc with c>1c > 1c>1 (strictly) such that
c n  ≤  ∣BS(n)∣for every natural number n,c^{\,n} \;\le\; \bigl|B_S(n)\bigr| \qquad \text{for every natural number } n,cn≤​BS​(n)​for every natural number n,

the cardinality being taken as a natural number and then compared in R\mathbb{R}R.

Fine print:

  • The inequality is demanded for all nnn, not merely for all sufficiently large nnn, and it is non-strict (≤\le≤). The n=0n = 0n=0 instance is c0=1≤∣BS(0)∣=1c^0 = 1 \le |B_S(0)| = 1c0=1≤∣BS​(0)∣=1, so it is automatic and imposes nothing.

  • The cardinality is the natural-number cardinality, which is 000 by convention for an infinite set. Here no such junk value can arise: for a finite SSS the ball BS(n)B_S(n)BS​(n) is a finite set, so the cardinality is the honest count.

  • The quantifier over SSS is existential: exponential growth asks only that some finite generating set exhibit the exponential lower bound.

Hypothesis 6 is the negation of this. Unfolded, it says:

For every finite subset S⊆BS \subseteq BS⊆B whose generated subgroup is all of BBB, and for every real c>1c > 1c>1, there exists a natural number nnn with

∣BS(n)∣  <  c n.\bigl|B_S(n)\bigr| \;<\; c^{\,n}.​BS​(n)​<cn.

Note the strength of this by contrast with the existential in the positive form: the negation is a statement about every finite generating set of BBB, and for each it needs only a single witnessing radius nnn where the bound fails.


Satisfiability

None of the hypotheses is vacuous or impossible. They are simultaneously satisfiable — for instance by the trivial group BBB with AAA the trivial subgroup, or by B=ZB = \mathbb{Z}B=Z with A=ZA = \mathbb{Z}A=Z — so the theorem is not vacuously true for want of a model.

Nothing requires AAA to be proper or nontrivial: A={1}A = \{1\}A={1} and A=BA = BA=B are both permitted by hypotheses 2–4, and in the latter case hypothesis 5 concerns the trivial quotient and hypothesis 4 says BBB itself is abelian.

Nothing in the statement asserts a bound on the length ttt of the resulting chain for BBB, nor any relation between it and the length of the chain furnished for B/AB/AB/A by hypothesis 5.

Human review
  • Endorsed by Shuze Chen · Sep 19, 2026

  • Endorsed by dbenbenn · Sep 19, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, licensed under Apache 2.0.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTermsJoin SlackJoin Zulip© 2026 Prove2Me