Read-back

The declaration

There is a single declaration in the artifact. Rendered in full:

Claim. Let $B$ be a group (of arbitrary universe level), and suppose:

1. $B$ is finitely generated;
2. $A$ is a subgroup of $B$;
3. $A$ is normal in $B$;
4. $A$ is abelian;
5. the quotient group $B/A$ is finitely presented.

Then there exists a finite subset $T \subseteq B$ such that

$$T \subseteq A \qquad\text{and}\qquad \langle\langle T \rangle\rangle_B \;=\; A,$$

where $\langle\langle T \rangle\rangle_B$ denotes the normal closure of $T$ in $B$.

Everything in that sentence is spelled out below, including what each of the five hypotheses unfolds to and what the conclusion's two conjuncts each assert.

The binders, one by one

The statement quantifies over the following, in this order.

• $B$ — a type, implicitly quantified, at an arbitrary universe level. Nothing constrains it beyond the structure imposed next.
• A group structure on $B$ — supplied as a typeclass assumption, so the statement is: for every group $B$.
• Finite generation of $B$ — a typeclass assumption asserting that the improper subgroup $B \le B$ is finitely generated, which in turn means: there exists a finite subset $S \subseteq B$ whose generated subgroup (the smallest subgroup of $B$ containing $S$) is all of $B$. Note this is generation as a subgroup, so $S$ generates using products and inverses, not merely products.
• $A$ — an explicitly quantified subgroup of $B$. A subgroup here is a subset of $B$ containing $1$ and closed under multiplication and inversion, packaged as an object whose underlying set is recovered by an implicit coercion; $x \in A$ means membership in that underlying set.
• Normality of $A$ — a typeclass assumption. It unfolds to: for every $n$, if $n \in A$, then for every $g \in B$ one has $g n g^{-1} \in A$. (Only this one-sided containment $g A g^{-1} \subseteq A$ for all $g$ is asserted; equality follows but is not what is written.)
• Commutativity of $A$ — a typeclass assumption on the type of elements of $A$, that is, on the subtype $\{x \in B : x \in A\}$ equipped with the multiplication it inherits from $B$. It unfolds to: multiplication on that subtype is commutative, i.e.

$$\forall\, a, b \in A,\quad ab = ba .$$

So: $A$ is an abelian group. (This is a hypothesis about $A$ alone; it says nothing about $B$, which need not be abelian.)

• Finite presentation of $B/A$ — a typeclass assumption about the quotient group $B/A$. The quotient is the usual one: the set of left cosets of $A$ in $B$, with the group structure induced by the congruence generated by $A$ — this group structure is available precisely because $A$ was assumed normal. The finite-presentation hypothesis unfolds to:

$$\exists\, n \in \mathbb{N},\ \exists\, \varphi : F_n \to B/A \text{ a group homomorphism},$$

where $F_n$ is the free group on $n$ generators (indexed by $\{0, 1, \dots, n-1\}$), such that

1. $\varphi$ is surjective, and
2. $\ker \varphi$ is the normal closure of a finite set: there exists a set $R \subseteq F_n$ with $R$ finite and $\langle\langle R \rangle\rangle_{F_n} = \ker\varphi$, where $\ker\varphi = \{w \in F_n : \varphi(w) = 1\}$.

Two points of precision here. First, $n$ is existentially quantified inside the hypothesis; the statement does not name or fix a presentation. Second, the relation set $R$ is required only to be finite as a set, and the equality demanded is an equality of subgroups of $F_n$, not merely an inclusion.

The conclusion

The conclusion asserts the existence of a finite subset of $B$, presented as a finite set $T$ of elements of $B$ (a list of elements of $B$ without repetitions, considered up to reordering; in particular $T$ may be empty), satisfying both of the following.

1. $T \subseteq A$. Literally: the underlying set of $T$ is contained in the underlying set of $A$, as subsets of $B$. Equivalently, every element of $T$ lies in $A$.

2. $\langle\langle T \rangle\rangle_B = A$. This is an equality of subgroups of $B$, not an inclusion in either direction. The normal closure on the left unfolds as follows:

   • For $a \in B$, the conjugates of $a$ are the elements $b \in B$ for which there is a $c \in B$ with $cac^{-1} = b$. (Formally the conjugating element ranges over the units of the monoid $B$, which, $B$ being a group, are exactly the elements of $B$.)
   • The set of conjugates of the elements of $T$ is the union, over $a \in T$, of the set of conjugates of $a$.
   • $\langle\langle T \rangle\rangle_B$ is the subgroup of $B$ generated by that set of conjugates, i.e. the intersection of all subgroups of $B$ containing every conjugate of every element of $T$.

   So the second conjunct says: the smallest normal subgroup of $B$ containing $T$ is exactly $A$, i.e. $A$ is generated, as a normal subgroup, by the finitely many elements of $T$.

Scope, edge cases and what is quantified how

• Existence only. The conclusion is an ordinary existential, not a unique existential: no uniqueness, minimality, or bound on the size of $T$ is asserted, and no cardinality of $T$ is related to any data in the hypotheses (not to the generating set of $B$, nor to the $n$ or the relation set of the presentation of $B/A$).
• Normal generation, not generation. The second conjunct does not say that $T$ generates $A$ as a subgroup; conjugates of elements of $T$ by arbitrary elements of $B$ are allowed when forming the closure.
• The empty case. $T$ is permitted to be empty, in which case the set of conjugates is empty and its normal closure is the trivial subgroup. So the statement is satisfiable in the degenerate case $A = \{1\}$ by taking $T = \varnothing$.
• Hypotheses are satisfiable. The five hypotheses are not vacuous: taking $B$ to be any finite group and $A$ the trivial subgroup satisfies all of them (a finite group is finitely generated, the trivial subgroup is normal and abelian, and a finite group is finitely presented). The statement therefore has content and is not quantifying over an empty situation. No hypothesis is impossible to satisfy.
• No finiteness or decidability assumption on $B$ beyond finite generation: $B$ may be infinite, and no decidable-equality assumption is imposed on $B$ in order to speak of a finite subset of it.
• $A$ is explicit, the rest implicit. $B$ is implicitly quantified, $A$ is an explicit argument, and all five numbered hypotheses are typeclass assumptions; logically all of them are universally quantified hypotheses of the claim, in the order listed above.