Read-back

The file contains a single declaration. What follows is a rendering of what it literally asserts.

Ambient data and standing hypotheses

The statement is about an arbitrary type $\Gamma$, living in an arbitrary universe, carrying two pieces of instance data:

1. a group structure on $\Gamma$ (a multiplication, an identity $1$, an inverse, with the group axioms);
2. a proof that $\Gamma$ is solvable, in the following specific sense. Define a sequence of subgroups of $\Gamma$ by

$$D_0 = \Gamma, \qquad D_{n+1} = [D_n, D_n],$$

where for subgroups $H, K \le \Gamma$ the symbol $[H,K]$ denotes the subgroup of $\Gamma$ generated by the set $\{\, h k h^{-1} k^{-1} : h \in H,\ k \in K \,\}$ (that is, the smallest subgroup of $\Gamma$ containing that set, not merely the set of such products). The solvability assumption is the existence of some $n \in \mathbb{N}$ with $D_n = \{1\}$.

Both are typeclass assumptions, discharged by instance search rather than named; the type $\Gamma$ itself is an implicit argument. No further assumption is made: $\Gamma$ is not assumed finitely generated, not assumed nontrivial, not assumed finite, and no bound on its derived length is fixed.

Throughout, subgroups of $\Gamma$ are ordered by inclusion: $H \le K$ means exactly that every element of $H$ is an element of $K$, and $H < K$ means $H \le K$ together with $K \not\le H$ (i.e. $H$ is a proper subgroup of $K$). $\top$ denotes the subgroup $\Gamma$ itself (which every element belongs to) and $\bot$ denotes the trivial subgroup $\{1\}$. For subgroups $H$ and $K$, $H \vee K$ denotes their join in the lattice of subgroups, equivalently the subgroup generated by $H \cup K$ — the smallest subgroup containing both. For a subset $S \subseteq \Gamma$, $\langle S \rangle$ denotes the smallest subgroup of $\Gamma$ containing $S$.

The assertion

Under those hypotheses, the declaration asserts that the following three propositions $P_1$, $P_2$, $P_3$ are equivalent — literally: that for every proposition $x$ in the list $[P_1, P_2, P_3]$ and every proposition $y$ in that same list, $x \leftrightarrow y$. For a three-element list this is exactly the pairwise equivalence of $P_1$, $P_2$ and $P_3$ (the diagonal instances $x = y$ being trivial).

Indexing convention used in $P_1$ and $P_2$

Both $P_1$ and $P_2$ speak of a family of subgroups indexed by a finite index type of size $u+1$ (respectively $v+1$), which is to say a finite chain

$$B_0,\ B_1,\ \dots,\ B_u$$

of subgroups of $\Gamma$, with $u+1$ terms in all. The statement refers to the index $0$, to the last index $u$, and, for each $i$ in the $u$-element index set $\{0, 1, \dots, u-1\}$, to the pair of consecutive terms $B_i$ and $B_{i+1}$. There are $u$ such consecutive pairs; when $u = 0$ there are none.

$P_1$ — existence of a finitely generated abelian-factor chain

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

• $B_0 = \Gamma$,
• $B_u = \{1\}$, and
• 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}$ (this is normality of $B_{i+1}$ in $B_i$, written out as a closure condition on conjugates, with the conjugating element ranging over the larger term $B_i$);
  3. $[B_i, B_i] \le B_{i+1}$, with $[\cdot,\cdot]$ the generated commutator subgroup described above (so the commutators of pairs of elements of $B_i$, and everything they generate, all lie in $B_{i+1}$);
  4. there exists a finite subset $T$ of $\Gamma$ with

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

 i.e. $B_i$ is precisely the smallest subgroup of $\Gamma$ containing both $T$ and $B_{i+1}$.

Three points about item 4. The finite set $T$ is a finite subset of the whole group $\Gamma$; it is not required a priori to be contained in $B_i$ (though the displayed equation forces $\langle T \rangle \le B_i$, hence $T \subseteq B_i$). The set $T$ is chosen separately for each index $i$, inside the quantifier over $i$. And $T$ may be empty, in which case $\langle T\rangle$ is trivial and the condition reads $B_i = B_{i+1}$.

Degenerate case $u = 0$: the index set for the family has one element, the index $0$ is the last index, and there are no consecutive pairs, so the per-$i$ conditions are vacuous. What remains is $B_0 = \Gamma$ and $B_0 = \{1\}$, i.e. $\Gamma = \{1\}$. So the choice $u = 0$ can be made only when $\Gamma$ is the trivial group; for a nontrivial $\Gamma$ the witness $u$ must be at least $1$.

$P_2$ — every chain with abelian factors automatically has finitely generated factors

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

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

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

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

So $P_2$ takes as hypothesis exactly conditions 1–3 of $P_1$ (the first three of the four), for an arbitrary chain from $\Gamma$ down to $\{1\}$, and concludes condition 4 of $P_1$ for that same chain, at every index. The three chain hypotheses are curried: $C_0 = \Gamma$ and $C_v = \{1\}$ are separate antecedents, and the per-index conditions form a third antecedent.

$P_2$ asserts nothing about whether any such chain exists. If no family $C_0,\dots,C_v$ satisfies the hypotheses for a given $v$, the $v$-th instance is vacuously true. In particular, for $v = 0$ the hypotheses force $\Gamma = \{1\}$ and the conclusion is a claim about an empty set of indices, so the $v = 0$ instance holds for every $\Gamma$ and contributes nothing.

Note also that $P_2$ is an assertion of the form "for all chains …", not "there is a chain …": it is a universally quantified statement, and it is the finite generation of the successive factors that it concludes, not the existence of the chain.

$P_3$ — the maximal condition on subgroups

The relation "properly contains" on the set of subgroups of $\Gamma$ is well-founded. Precisely: consider the binary relation $R$ on subgroups of $\Gamma$ given by

$$R(H, K) \quad \text{iff} \quad H > K, \text{ i.e. } K < H, \text{ i.e. } K \le H \text{ and } H \not\le K.$$

$P_3$ is the assertion that $R$ is a well-founded relation — that every subgroup of $\Gamma$ is accessible for $R$, accessibility being the least predicate such that a subgroup $H$ is accessible as soon as every subgroup properly containing $H$ is accessible.

Unwinding the direction: an $R$-descending sequence is a sequence $H_0, H_1, H_2, \dots$ of subgroups with $R(H_{n+1}, H_n)$ for all $n$, i.e. with

$$H_0 < H_1 < H_2 < \cdots,$$

each properly contained in the next. So $P_3$ is well-foundedness with respect to strict inclusion upwards: it is the ascending-chain / maximal condition on the subgroup lattice of $\Gamma$, not the descending one.

$P_3$ mentions neither solvability, nor chains, nor finite generation, nor any particular subgroup: it is purely a condition on the poset of all subgroups of $\Gamma$ under inclusion. It is stated as the instance-style well-foundedness predicate for the relation $>$, applied to the type of subgroups of $\Gamma$ with its inclusion order.

Scope reminder

The three equivalences are asserted only for a $\Gamma$ that is a group and is solvable in the sense spelled out above. Nothing is claimed for a non-solvable group, and nothing is claimed about $\Gamma$ beyond the equivalence of $P_1$, $P_2$ and $P_3$ — in particular the declaration does not assert any one of $P_1$, $P_2$, $P_3$ outright.

The body of the declaration is deliberately omitted; only the statement above is being read back.