Read-back

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

Preliminary: what "finitely presented" unfolds to

The statement is built from one non-elementary notion, applied twice. For a group $H$, the assertion "$H$ is finitely presented" unfolds, with nothing left abbreviated, to:

There exist a natural number $n$ and a group homomorphism

$$\varphi : F_n \longrightarrow H$$

from the free group $F_n$ on the $n$-element index set $\{0, 1, \dots, n-1\}$ into $H$, such that

1. $\varphi$ is surjective, and
2. there exists a subset $S \subseteq F_n$ such that $S$ is finite and

$$\langle\langle S \rangle\rangle \;=\; \ker \varphi ,$$

an equality of subgroups of $F_n$ (each contains the other).

Here two further items are themselves unfolded as follows.

• $\ker\varphi$ is the subgroup $\{w \in F_n : \varphi(w) = 1\}$ of $F_n$.

• $\langle\langle S \rangle\rangle$, the normal closure of $S$, is the subgroup of $F_n$ generated by the set of all conjugates of all elements of $S$; that is, the subgroup generated by

$$\bigcup_{a \in S} \{\, b \in F_n : b = c\,a\,c^{-1} \text{ for some } c \in F_n \,\} .$$

It is the smallest subgroup of $F_n$ that contains $S$ and is closed under conjugation. Note that it is the normal closure that must equal $\ker\varphi$ on the nose, not merely the ordinary subgroup generated by $S$, and not merely a subgroup contained in or containing $\ker\varphi$.

So "finitely presented" means: $H$ admits a presentation with finitely many generators and finitely many relations — the generators being $n$ in number and indexed by $\{0,\dots,n-1\}$, and the relators being the finitely many elements of $S$, whose normal closure is required to be exactly the set of words that die in $H$.

Two degenerate readings are included by the quantifiers. The case $n = 0$ is permitted: $F_0$ is the trivial group, and surjectivity of $\varphi$ then forces $H$ to be trivial. The case $S = \emptyset$ is permitted: the normal closure of the empty set is the trivial subgroup, so this case says $\varphi$ is an isomorphism and $H$ is free of rank $n$. Neither $n$ nor $S$ is claimed to be unique or minimal, and no bound on either is asserted.

The declaration

Fix

• a type $G$, living in an arbitrary universe (the universe is a free parameter of the statement, not fixed to any particular one);
• a group structure on $G$;
• a subgroup $N$ of $G$.

Assume:

(H1) $N$ is normal in $G$, i.e. for every $x \in N$ and every $g \in G$ one has $g\,x\,g^{-1} \in N$.

(H2) $N$, regarded as a group in its own right, is finitely presented. The group in question is the one carried by the set $\{x \in G : x \in N\}$, with the multiplication, identity and inverse inherited from $G$. "Finitely presented" means precisely what is unfolded above, with $H$ taken to be this group: there are $n \in \mathbb{N}$ and a surjective homomorphism $F_n \twoheadrightarrow N$ whose kernel is the normal closure — taken inside $F_n$ — of some finite subset of $F_n$.

(H3) The quotient $G/N$ is a finite type. The object $G/N$ is the set of equivalence classes of the relation on $G$ given by

$$x \sim y \iff x^{-1}y \in N,$$

i.e. the set of left cosets $gN$. (Under (H1) left and right cosets coincide, but the relation as written is the left-coset relation.) Finiteness of this type means: there is a natural number $m$ and a bijection between $G/N$ and $\{0,1,\dots,m-1\}$. Equivalently, $N$ has finite index in $G$. No bound on that index is fixed, and $m = 0$ is formally allowed by the definition of finiteness but cannot occur, since $G/N$ always contains the class of the identity.

Conclusion. $G$ is finitely presented — again in exactly the unfolded sense above, with $H$ taken to be $G$: there exist $n' \in \mathbb{N}$, a surjective homomorphism $\psi : F_{n'} \twoheadrightarrow G$, and a finite subset $S' \subseteq F_{n'}$ whose normal closure inside $F_{n'}$ equals $\ker\psi$ exactly.

Remarks on scope and edge cases

The number of generators $n'$ and the relator set $S'$ asserted for $G$ are bare existential claims. Nothing relates them to the corresponding data for $N$: no formula, no bound in terms of the index of $N$ or of the presentation of $N$, and no statement that a presentation of $G$ can be computed from one of $N$.

The subgroup $N$ is an explicit parameter of the statement; the type $G$, its group structure, and the three hypotheses (H1)–(H3) are all supplied implicitly, (H1)–(H3) by instance resolution. This affects only how the statement is invoked, not what it asserts.

The hypotheses are jointly satisfiable, so the statement is not vacuous. For instance, $G$ any finite group with $N$ trivial satisfies all three; or $N = G$ with $G$ any finitely presented group, in which case $G/N$ is a one-element set. The extreme cases are all inside the statement's scope:

• $N$ the trivial subgroup: (H2) holds automatically, and (H3) says $G$ itself is finite.
• $N = G$: (H3) holds automatically, and the statement degenerates to an implication from $G$ finitely presented to $G$ finitely presented.
• $G$ trivial: everything holds.

The statement is a one-directional implication. It does not assert the converse (that a finitely presented group has finitely presented finite-index normal subgroups), nor any equivalence.