Read-back

The declaration

There is one declaration in the artifact. It is a theorem with three hypotheses and one conclusion, all of them carried by unnamed (typeclass) assumptions on a single implicit variable.

What it asserts

Let $G$ be a set carrying a group structure. Assume that $G$ is finitely generated and that $G$ is nilpotent. Then $G$ is finitely presented.

The variable $G$ is implicit and universally quantified: the statement is about every type $G$, in every universe, together with every group structure on it. No further assumption is made on $G$ — it is not assumed finite, countable, abelian, torsion-free, or nontrivial.

Below, each of the four conditions is expanded to what it literally unfolds to.

---

The group structure

$G$ is equipped with a group structure: an associative multiplication with a two-sided identity $1$ and two-sided inverses (together with the derived division and integer-power operations, which play no role in the statement). Throughout, "subgroup" means a subset of $G$ containing $1$ and closed under multiplication and inversion, and for a subset $X \subseteq G$ the subgroup generated by $X$ means the intersection of all subgroups of $G$ that contain $X$ — the smallest such subgroup.

---

Hypothesis 1: $G$ is finitely generated

This unfolds to:

$$\exists\, S \subseteq G \text{ finite},\qquad \langle S \rangle = G .$$

More precisely, $S$ is given as a finite list of elements of $G$ without repetitions (so it is finite by construction, not merely asserted to be finite), and the assertion is that the subgroup generated by the underlying set of $S$ is the whole subgroup $G$ — equality of subgroups, not merely containment in one direction.

Degenerate cases included: $S$ may be empty, in which case the condition says $G$ is the trivial group. So the trivial group satisfies this hypothesis.

---

Hypothesis 2: $G$ is nilpotent

Define a sequence $Z_0, Z_1, Z_2, \dots$ of subgroups of $G$ by

$$Z_0 = \{1\},\qquad Z_{n+1} \;=\; \bigl\{\, x \in G \;:\; \forall\, y \in G,\ x y x^{-1} y^{-1} \in Z_n \,\bigr\}.$$

(The commutator convention in force is $[x,y] = x y x^{-1} y^{-1}$; the bracket in the definition of $Z_{n+1}$ is that one, with $x$ the element being tested and $y$ the quantified element.) Each $Z_{n+1}$ is exactly the preimage in $G$ of the centre of $G/Z_n$ under the quotient map; in particular $Z_1$ is the centre of $G$. This is the upper central series, indexed by the natural numbers starting at $0$.

The hypothesis is:

$$\exists\, n \in \mathbb{N},\qquad Z_n = G .$$

Note the quantifier: some $n$ works, with no bound supplied and no claim about which $n$. The index $n = 0$ is permitted, and $Z_0 = \{1\}$, so for $n = 0$ the condition says $G$ is trivial. The statement is the existence of a finite index at which the upper central series reaches all of $G$ — equality with $G$, not merely a containment or a limit/union condition.

---

Conclusion: $G$ is finitely presented

For $n \in \mathbb{N}$, write $F_n$ for the free group on the $n$-element index set $\{0, 1, \dots, n-1\}$ — concretely, words in $n$ letters and their formal inverses modulo free reduction, which has the usual universal property (every function from the $n$ letters into a group extends uniquely to a group homomorphism out of $F_n$). For $n = 0$ this is the trivial group.

For a subset $R$ of a group $H$, the normal closure of $R$ means the subgroup of $H$ generated by the set of all conjugates of elements of $R$, namely by

$$\{\, c\, r\, c^{-1} \;:\; r \in R,\ c \in H \,\}.$$

The conclusion is:

$$\exists\, n \in \mathbb{N},\ \exists\, \varphi : F_n \to G \text{ a group homomorphism, such that}$$

1. $\varphi$ is surjective (every element of $G$ is $\varphi(w)$ for some $w \in F_n$), and
2. the kernel $\ker \varphi = \{\, w \in F_n : \varphi(w) = 1 \,\}$ is the normal closure, in $F_n$, of some finite subset $R \subseteq F_n$; that is,

$$\exists\, R \subseteq F_n \text{ with } R \text{ finite},\qquad \langle\!\langle R \rangle\!\rangle_{F_n} = \ker\varphi ,$$

where $\langle\!\langle R \rangle\!\rangle_{F_n}$ is the normal closure just described.

Several points of precision:

• Both quantifiers are existential, not unique-existential: no $n$, no $\varphi$ and no $R$ is singled out, and nothing is asserted about how small $n$ or $R$ can be taken, nor any relationship between them and the generating set from Hypothesis 1 or the nilpotency index from Hypothesis 2.
• The relation set $R$ is a subset of $F_n$ and is not separately required to lie inside $\ker\varphi$; the asserted equality of the normal closure with $\ker\varphi$ forces $R \subseteq \ker\varphi$ anyway.
• "Finite" for $R$ means the set is finite in the ordinary sense (it is in bijection with $\{0,\dots,k-1\}$ for some $k \in \mathbb{N}$). The empty set is allowed: then the normal closure is the trivial subgroup and the condition says $\varphi$ is an isomorphism onto $G$, i.e. $G$ is free of finite rank.
• $n = 0$ is allowed: then $F_0$ is trivial and surjectivity forces $G$ to be trivial.
• The conclusion is stated as the existence of such a presentation. It does not say that every surjection from a finitely generated free group onto $G$ has finitely normally generated kernel, and it does not produce a presentation from any given generating set.
• The number of generators is $n$, a natural number, so the generating set of the presentation is finite; the relators are finite in number. These are two separate finiteness conditions, both asserted.

---

Overall shape, and satisfiability

The whole declaration is an implication with $G$, its group structure, and both hypotheses universally quantified:

$$\forall\, G \text{ a group},\quad \bigl(G \text{ finitely generated}\bigr) \wedge \bigl(G \text{ nilpotent}\bigr) \;\Longrightarrow\; \bigl(G \text{ finitely presented}\bigr).$$

It is an implication, not a biconditional: nothing is asserted in the converse direction.

The two hypotheses are not vacuous and are jointly satisfiable — for instance any finite group, or the trivial group, satisfies both — so the statement is not an assertion about an empty class of groups. The trivial group is included in the scope of the statement, as are all finite groups and all finitely generated abelian groups.