A cyclically reduced sequence has no pinch in an HNN extension either internally or across its cyclic junction. If its stable-letter length is positive, every positive power remains reduced, so Britton's lemma gives infinite order. Repeated cyclic conjugation and pinch removal shows that any finite-order element of an HNN extension is conjugate into its base group.
We exhibit a nonidentity element killed by every finite quotient.
In any finite image, let be the order of the image of . The relation conjugating to gives
Thus . Since is invertible modulo , the relation implies that the image of is a power of the image of . Therefore every finite image kills the group commutator
using .
View as an HNN extension of , with associated subgroups and . A pinch in an HNN extension would be or . The word has none: its intervening exponents are , incompatible with the required divisibilities . By Britton's lemma, . Hence finite quotients fail to separate this nonidentity element, proving the conclusion.
The HNN extension in the convention used here is
The new generator is its stable letter, and are its associated subgroups of an HNN extension. We prove the normal form theorem for an HNN extension, which also proves that the natural map is injective.
Set , , , and . For each sign , choose a right coset transversal for , containing as the representative of . Thus every has a unique decomposition , with and . A normal form is
where is unrestricted and the case is just .
Here is a constructive proof. Let be the set of these formal sequences. Left multiplication by changes only to . To prepend , uniquely decompose using and use
If the old first stable letter is and , cancel this pair and multiply into the now-leading coefficient . Otherwise retain the new first stable letter. Both cases give a sequence in ; after a cancellation the leading coefficient is unrestricted, so no further normalization is needed at that end. Prepending the letters of a word from right to left proves existence.
These operations define permutations of . The base-group operations satisfy . The operations and are inverse: if prepending did not cancel, the reverse operation decomposes the new leading coefficient with representative and cancels the newly inserted letter; if it did cancel, the reverse operation decomposes with representative , restoring the original prefix. The normal-form restriction rules out an unwanted second cancellation in the latter case.
For , decomposing uses the same representative as decomposing , and changes its subgroup coefficient from to . Both the cancelling and noncancelling cases therefore give
Thus all defining relations act identically on , and we obtain a group action of the presented HNN extension. Each written normal form sends the empty form, whose leading coefficient is , to that normal form itself. Equal group elements must have the same image of the empty form, proving uniqueness and the embedding of .
A reduced sequence in an HNN extension is a word containing no pinch in an HNN extension: no with and no with . Equivalently, whenever , one requires .
Britton's lemma states that
More strongly it cannot represent an element of . To prove this from the normal form theorem for an HNN extension, normalize the coefficients from right to left. Splitting moves to the coefficient immediately on its left. If the preceding stable letter has the opposite sign, this transported factor belongs to the subgroup relevant to that inverse pair; multiplying by it cannot turn a coefficient outside that subgroup into one inside it. If the signs agree, cancellation is impossible anyway. Hence no stable letter disappears during normalization of a reduced sequence. Its unique normal form has , whereas every element of has stable-letter length zero. This proves Britton's lemma. The same proof works with finitely many stable letters, with pinches requiring the same letter and its inverse.
A reduced sequence is a word with no pinch in an HNN extension. If , Britton's lemma makes it nontrivial and prevents it from representing a base-group element. Reduced sequences need not be unique; uniqueness requires the fixed coset representatives in the normal form theorem for an HNN extension.