Read-back

The single declaration in the artifact

Setting and hypotheses

The statement is about one arbitrary object, introduced implicitly (the reader never has to supply it explicitly; it is inferred):

• a type $\Gamma$, living in an arbitrary universe;
• a group structure on $\Gamma$ — multiplication, an identity element $1$, and inversion, satisfying the group axioms, so $\Gamma$ is a group with no commutativity, no finiteness and no topology assumed;
• a proof that $\Gamma$ is solvable. This hypothesis is spelled out as: there exists an $n \in \mathbb{N}$ with $\Gamma^{(n)} = \{1\}$, where the derived series of $\Gamma$ is the sequence of subgroups defined by recursion on $\mathbb{N}$,

$$\Gamma^{(0)} = \Gamma, \qquad \Gamma^{(k+1)} = [\Gamma^{(k)},\Gamma^{(k)}].$$

Throughout, "subgroup of $\Gamma$" means a subset containing $1$ and closed under multiplication and inversion; the subgroups of $\Gamma$ are partially ordered by inclusion, the largest one is $\Gamma$ itself and the smallest one is the trivial subgroup $\{1\}$.

Two pieces of notation recur below and are fixed here.

The commutator of two subgroups. For subgroups $H, K \le \Gamma$, the symbol $[H,K]$ denotes the subgroup of $\Gamma$ generated by the set of commutators $\{\,h k h^{-1} k^{-1} : h \in H,\ k \in K\,\}$ — that is, the smallest subgroup of $\Gamma$ containing all of them. It is not the bare set of commutators.

The subgroup generated by a set, and joins. For a subset $S \subseteq \Gamma$, $\langle S\rangle$ denotes the intersection of all subgroups of $\Gamma$ containing $S$, i.e. the smallest such subgroup. For subgroups $H,K$, the expression $H \vee K$ denotes their join in the lattice of subgroups: the smallest subgroup containing both, equivalently $\langle H \cup K\rangle$. So an equation of the form $H = \langle T\rangle \vee K$ says that $H$ is exactly the subgroup generated by the finite set $T$ together with $K$. (The finite set $T$ is drawn from the ambient group $\Gamma$, not from $H$; but the asserted equality itself forces $T \subseteq H$.)

What is asserted

The assertion is that the following seven properties of $\Gamma$ are pairwise equivalent. Precisely, the claim is: for every pair of statements $P, Q$ drawn from the list below (including the case $P = Q$), $P \iff Q$. This is a conjunction of all $21$ distinct pairwise biconditionals — no single "hard" implication is singled out, and no ordering of the list is asserted to matter.

---

(1) $\Gamma$ is polycyclic, in the following spelled-out sense.

There exist a natural number $t$ and a family of subgroups $A_0, A_1, \dots, A_t$ of $\Gamma$ (indexed by the $t+1$ integers $0,\dots,t$) such that

$$A_0 = \Gamma, \qquad A_t = \{1\},$$

and for every index $i$ with $0 \le i \le t-1$, all of the following hold:

• $A_{i+1} \le A_i$;
• the subgroup $\{x \in A_i : x \in A_{i+1}\}$ of the group $A_i$ — i.e. $A_{i+1}$ regarded as a subgroup of $A_i$, which is what the preimage of $A_{i+1}$ under the inclusion $A_i \hookrightarrow \Gamma$ amounts to — is a normal subgroup of $A_i$; and
• with respect to the group structure that this normality provides on the set of left cosets, the quotient group $A_i / A_{i+1}$ is cyclic, which is spelled out as: there is an element $g$ of that quotient such that the map $\mathbb{Z} \to A_i/A_{i+1}$, $n \mapsto g^n$, is surjective.

The normality and the cyclicity are packaged together as a single existential statement ("there is a proof of normality such that the quotient is cyclic"); since normality is a proposition, this is the same as asserting normality and cyclicity of the resulting quotient.

Degenerate case: $t = 0$ is permitted. Then the index set is the single index $0$, the per-$i$ conditions are vacuous (there is no $i$ with $0 \le i \le -1$), and the two displayed equations read $A_0 = \Gamma$ and $A_0 = \{1\}$ simultaneously — so $t = 0$ can be used exactly when $\Gamma$ is the trivial group. Note also that the family $A$ is an arbitrary function of the index; the only descent required is the consecutive containment $A_{i+1} \le A_i$.

---

(2) There is a finite subnormal series with abelian, finitely generated steps.

There exist a natural number $u$ and subgroups $B_0, \dots, B_u$ of $\Gamma$ with

$$B_0 = \Gamma, \qquad B_u = \{1\},$$

such that for every index $i$ with $0 \le i \le u-1$ all four of the following hold:

1. $B_{i+1} \le B_i$;
2. for every $g \in B_i$ and every $x \in B_{i+1}$, one has $g x g^{-1} \in B_{i+1}$ (i.e. $B_{i+1}$ is normal in $B_i$, stated as closure under conjugation by elements of $B_i$);
3. $[B_i, B_i] \le B_{i+1}$ (i.e. the quotient $B_i/B_{i+1}$ is abelian);
4. there exists a finite subset $T$ of $\Gamma$ with

$$B_i = \langle T \rangle \vee B_{i+1}.$$

Here $T$ is allowed to depend on $i$, and is allowed to be empty. As in (1), $u = 0$ is permitted and then forces $\Gamma = \{1\}$ via $B_0 = \Gamma$ and $B_0 = \{1\}$.

---

(3) Every finite subnormal series with abelian steps automatically has finitely generated steps.

For every natural number $v$ and every family of subgroups $C_0, \dots, C_v$ of $\Gamma$: if

• $C_0 = \Gamma$, and
• $C_v = \{1\}$, and
• for every $i$ with $0 \le i \le v-1$: $C_{i+1} \le C_i$, and $g x g^{-1} \in C_{i+1}$ for all $g \in C_i$ and all $x \in C_{i+1}$, and $[C_i,C_i] \le C_{i+1}$,

then for every $i$ with $0 \le i \le v-1$ there exists a finite subset $T \subseteq \Gamma$ with

$$C_i = \langle T \rangle \vee C_{i+1}.$$

So (3) is the universally quantified counterpart of (2): the hypotheses of (3) are conditions 1–3 of (2), and the conclusion of (3) is condition 4 of (2). No normality of $C_i$ in $\Gamma$ is required — only in the preceding term of the chain. The three displayed hypotheses are separate implications in the Lean text (chained arrows), which is the same as one implication from their conjunction.

Degenerate cases: for $v = 0$ the hypotheses require $C_0 = \Gamma$ and $C_0 = \{1\}$ at once, so unless $\Gamma$ is trivial there is no such family and that case of the universal statement is vacuously satisfied; the conclusion for $v = 0$ is in any case an empty conjunction. More generally, for any $v$ for which no chain meets the hypotheses, that instance is vacuous.

---

(4) Each derived subgroup is finitely generated over the next.

For every $k \in \mathbb{N}$, both:

• $[\Gamma^{(k)}, \Gamma^{(k)}] \le \Gamma^{(k+1)}$; and
• there exists a finite subset $T \subseteq \Gamma$ with

$$\Gamma^{(k)} = \langle T \rangle \vee \Gamma^{(k+1)}.$$

The first of these two conjuncts carries no information: by the definition of the derived series recalled above, $\Gamma^{(k+1)}$ is $[\Gamma^{(k)},\Gamma^{(k)}]$, so the displayed inequality is an instance of $X \le X$ and holds for every group whatsoever. The substance of (4) is the second conjunct. For $k = 0$ it reads: $\Gamma$ is generated by some finite set together with its commutator subgroup.

---

(5) Every term of the derived series is a finitely generated group.

For every $k \in \mathbb{N}$, the group $\Gamma^{(k)}$ — taken as a group in its own right, on the underlying set of that subgroup — is finitely generated. "Finitely generated" is spelled out as: there is a finite subset of $\Gamma^{(k)}$ whose generated subgroup, formed inside the group $\Gamma^{(k)}$, is all of $\Gamma^{(k)}$.

The case $k = 0$ is included, and there $\Gamma^{(0)} = \Gamma$, so (5) in particular asserts that $\Gamma$ itself is finitely generated.

---

(6) Every subgroup of $\Gamma$ is a finitely generated group.

For every subgroup $H$ of $\Gamma$ — with no restriction whatsoever on $H$: not normality, not being a term of any series, not being proper or nontrivial — the group $H$, taken as a group in its own right, is finitely generated in the sense just described: some finite subset of $H$ generates $H$ inside $H$. The extreme cases $H = \Gamma$ and $H = \{1\}$ are included.

---

(7) The lattice of subgroups of $\Gamma$ satisfies a well-foundedness condition.

The strict relation $\supsetneq$ on the set of subgroups of $\Gamma$ (i.e. the relation "$H$ strictly contains $K$", read as the greater-than relation for the inclusion ordering) is a well-founded relation.

Unwinding the definition of well-foundedness for this relation: every subgroup of $\Gamma$ is accessible for $\supsetneq$; equivalently, every nonempty collection of subgroups of $\Gamma$ has an element that is maximal in it with respect to inclusion; equivalently, there is no infinite strictly increasing chain $H_0 \subsetneq H_1 \subsetneq H_2 \subsetneq \cdots$ of subgroups of $\Gamma$. This is the ascending chain condition on subgroups (note the direction: it is increasing chains that are forbidden, not decreasing ones).

This last item is, in the Lean text, a typeclass-shaped proposition; it is nonetheless an ordinary proposition about $\Gamma$, and it appears in the list on the same footing as the other six.

---

Points the quantifiers silently include

• Nothing rules out $\Gamma$ trivial or finite. If $\Gamma$ is the trivial group all seven items are about a one-element group; the hypothesis of solvability is satisfied by $n = 0$.
• The finite generating sets are allowed to be empty, and in (2), (3) and (4) they may depend on the index.
• In (2), (3) and (4) the finite sets are drawn from the ambient group $\Gamma$, not from the subgroup being generated; the asserted equalities nevertheless force them to lie inside that subgroup.
• The families of subgroups in (1), (2) and (3) are arbitrary functions of the index. Only consecutive containment is imposed; nothing asserts injectivity, strictness, or that the chain is a chain of distinct subgroups. Repetitions (a step with $B_i = B_{i+1}$) are permitted, and such a step satisfies conditions 2–4 of (2) automatically.
• The conjugation condition in (2) and (3) is stated one-sidedly — $g x g^{-1} \in B_{i+1}$ for $g$ ranging over $B_i$ — which, because $g$ ranges over a subgroup and so over inverses too, is the usual notion of $B_{i+1}$ being a normal subgroup of $B_i$.
• Item (4)'s first conjunct is satisfied by every group, as noted above.
• The list has seven entries and the assertion is all $21$ pairwise equivalences, stated as a universally quantified biconditional over membership in the list rather than as a cycle of implications.