Read-back: exists_independent_commutator_generating_sets_lowerCentralSeries

There is exactly one declaration in the artifact. What follows is a complete rendering of what it asserts.

The objects it is built from

Throughout, $\Gamma$ is a type (living in an arbitrary universe) carrying a group structure. Both the type and the group structure are arguments of the statement: the type is implicit, the group structure is a typeclass assumption, and there are no other assumptions on $\Gamma$ — it is not assumed finitely generated, finite, abelian, nilpotent or nontrivial as a hypothesis.

The descending chain. For each $k \in \mathbb{N}$ the statement uses a subgroup $\gamma_k \le \Gamma$, defined by iterating the commutator with the whole group, starting from the whole group:

$$\gamma_0 = \Gamma, \qquad \gamma_{k+1} = [\gamma_k, \Gamma].$$

Here $[H_1,H_2]$ denotes the subgroup of $\Gamma$ generated by the set of commutators $\{\,h_1h_2h_1^{-1}h_2^{-1} : h_1 \in H_1,\ h_2 \in H_2\,\}$ (the generated subgroup, not the set of commutators itself), and the commutator of two elements is taken in the order $[a,b] = a\,b\,a^{-1}\,b^{-1}$. So $\gamma_0$ is $\Gamma$ itself, $\gamma_1 = [\Gamma,\Gamma]$ is the derived subgroup, and each subsequent term is $\gamma_{k+1} = [\gamma_k,\Gamma]$. Every $\gamma_k$ is a subgroup of the ambient group $\Gamma$, and the chain is decreasing, $\gamma_{k+1} \le \gamma_k$ (this is a fact about the definition, not an extra hypothesis).

Strictly speaking, $\gamma_0$ is not the type $\Gamma$ but the subgroup "everything", so the elements of $\gamma_k$ are pairs consisting of an element of $\Gamma$ together with a proof of membership; whenever such an element is multiplied or compared inside $\Gamma$ below, it is its underlying element of $\Gamma$ that is meant.

The successive quotients. For each $k \in \mathbb{N}$ put

$$Q_k \;=\; \gamma_k \,\big/\, \{\,x \in \gamma_k : x \in \gamma_{k+1}\,\},$$

the quotient of the group $\gamma_k$ by the subgroup of $\gamma_k$ consisting of those of its elements that also lie in $\gamma_{k+1}$. (Because the chain is decreasing, that subgroup is just $\gamma_{k+1}$, regarded as a subgroup of $\gamma_k$; the statement writes it as the intersection seen from inside $\gamma_k$.) This subgroup is normal in $\gamma_k$ for every $k$ — no hypothesis is needed for that, and none is assumed — so $Q_k$ is a group, and there is a canonical surjective homomorphism $\pi_k : \gamma_k \to Q_k$ sending an element to its coset.

The hypotheses

1. A natural number $s$ (an explicit argument: the assertion is made for every $s$).

2. $\gamma_{s+1} = \{1\}$, i.e. the $(s+1)$-st term of the chain is the trivial subgroup.

   This is the only place $s$ occurs. It says that $\Gamma$ is nilpotent, of class at most $s+1$. Since $s+1 \ge 1$, the weakest instance is $s = 0$, which says $[\Gamma,\Gamma] = \{1\}$, i.e. $\Gamma$ abelian. Note that this hypothesis is unsatisfiable for any group that is not nilpotent: for such $\Gamma$ the statement is vacuously true, and the statement therefore makes no assertion about non-nilpotent groups. Nothing requires $s$ to be least, so $s$ is only an upper bound for the class.

3. $Q_0$ is finitely generated as a group: there is a finite set of elements of $Q_0 = \Gamma/[\Gamma,\Gamma]$ whose generated subgroup is all of $Q_0$.

   This is an assumption about the abelianisation only. It is not an assumption that $\Gamma$ itself is finitely generated, and no such assumption is made anywhere in the hypotheses.

What is asserted

Under those hypotheses, there exist

• a function $r : \mathbb{N} \to \mathbb{N}$, and
• a family $\tau$ which, for every $k \in \mathbb{N}$, assigns to each index $i \in \{0,1,\dots,r_k-1\}$ an element $\tau_k(i)$ of the subgroup $\gamma_k$

(the index set for level $k$ is the set of naturals strictly below $r_k$, which is empty when $r_k = 0$), such that the following three groups of conditions all hold.

(A) For every $k \in \mathbb{N}$, four conditions on the quotient $Q_k$

1. $Q_k$ is finitely generated: some finite subset of $Q_k$ generates it.

2. $Q_k$ is commutative: $xy = yx$ for all $x,y \in Q_k$. (This is stated as an equation for all pairs of elements, not as a structural assumption.)

3. The family of cyclic subgroups

$$C_{k,i} \;=\; \langle \pi_k(\tau_k(i))\rangle \;=\; \{\,\pi_k(\tau_k(i))^{\,m} : m \in \mathbb{Z}\,\} \le Q_k, \qquad i = 0,\dots,r_k-1,$$

is independent in the lattice of subgroups of $Q_k$: for each index $i$,

$$C_{k,i} \;\cap\; \Big\langle \bigcup_{j \ne i} C_{k,j} \Big\rangle \;=\; \{1\},$$

where the second factor is the subgroup of $Q_k$ generated by all the $C_{k,j}$ with $j \ne i$, and "$\cap$" is the trivial-intersection condition (disjointness in the subgroup lattice).

4. Those same cyclic subgroups generate everything:

$$\Big\langle \bigcup_{i=0}^{r_k-1} C_{k,i} \Big\rangle \;=\; Q_k .$$

Conditions 2–4 together say that $Q_k$ is the internal direct sum of the $r_k$ cyclic subgroups generated by the images of the chosen elements $\tau_k(0),\dots,\tau_k(r_k-1)$.

Note what is not said here: the cyclic subgroups $C_{k,i}$ are the groups of all integer powers of the given elements, and nothing asserts they are infinite cyclic, nontrivial, or pairwise distinct. An element $\tau_k(i)$ whose image in $Q_k$ is the identity gives $C_{k,i} = \{1\}$, which satisfies the independence condition automatically; so $r_k$ need not be a minimal number of generators or a rank.

(B) For every $k \in \mathbb{N}$, the level-$(k+1)$ elements are commutators

For every $k \in \mathbb{N}$ and every index $l \in \{0,\dots,r_{k+1}-1\}$ there exist indices $i \in \{0,\dots,r_0-1\}$ and $j \in \{0,\dots,r_k-1\}$ such that, as an equation between elements of $\Gamma$,

$$\tau_{k+1}(l) \;=\; \tau_0(i)\;\tau_k(j)\;\tau_0(i)^{-1}\;\tau_k(j)^{-1}.$$

The order of the four factors is exactly as written: the level-$0$ element first, then the level-$k$ element, then their inverses in the same order. So each chosen element at level $k+1$ is the commutator of some chosen level-$0$ element with some chosen level-$k$ element.

This is an existence statement for each $l$, in that direction only: it requires every chosen element at level $k+1$ to be such a commutator, and does not require that every such commutator occur among the chosen elements at level $k+1$. In particular, if $r_{k+1} = 0$ the condition is empty for that $k$; and if $r_{k+1} > 0$ while $r_k = 0$, no admissible $j$ exists and the condition cannot be met for that $k$.

(C) The level-$0$ elements generate $\Gamma$

$$\big\langle\; \{\,\tau_0(i) : i = 0,\dots,r_0-1\,\} \;\big\rangle \;=\; \Gamma,$$

the subgroup of $\Gamma$ generated by the (underlying elements of the) chosen level-$0$ elements — generated as a subgroup, so closed under inverses and products — is the whole of $\Gamma$. Thus, although $\Gamma$ was not assumed finitely generated, the conclusion supplies a generating set of at most $r_0$ elements.

Degenerate and edge cases the quantifiers include

• Conditions (A) and (B) are asserted for all $k \in \mathbb{N}$, without bound — not only for $k \le s$. For $k \ge s+1$ the hypothesis $\gamma_{s+1} = \{1\}$ together with the chain being decreasing makes $\gamma_k$ trivial, hence $Q_k$ trivial; in a trivial group the trivial subgroup is the whole group, so conditions (A)1–4 hold for any value of $r_k$ whatsoever, and each $\tau_k(i)$ is forced to be the identity. Correspondingly $r_k$ is unconstrained for large $k$, and nothing asserts that $r_k$ is eventually $0$, nor that $r$ is decreasing, bounded, or related in any way to $s$.

• $r_k = 0$ is permitted. Then the index set at level $k$ is empty, the generated subgroup in (A)4 is the trivial subgroup, and (A)4 becomes the assertion that $Q_k$ is trivial; (A)3 holds vacuously.

• $r_0 = 0$ is permitted by the syntax, but then (C) asserts that the subgroup generated by the empty set is $\Gamma$, i.e. that $\Gamma$ is the trivial group.

• The number $s$ does not appear anywhere in the conclusion.

• The assertion is plain existence ($\exists$), not unique existence: nothing says the functions $r$ and $\tau$ are unique, canonical, or in any way determined by $\Gamma$.

• $\tau$ is a single family defined at every level $k \in \mathbb{N}$ simultaneously, so the same choice must satisfy (A) at every level and be compatible with (B) at every level, with the level-$0$ part additionally satisfying (C).