Integral Stallings theorem for finite lower-central quotients

Supply the resolution convention for [F2] by taking, for every module over each relevant group ring, the free module on its underlying set, augmented $[m]\mapsto m$, and repeating this construction on successive kernels. These surjections give an exact free resolution. By [A1] and [L1], DC also holds. The case $n=1$ is the map between two trivial quotients. For $n=2$, the bar degree-one calculation in [F2] identifies $A\mathrm{/}{\mathrm{\Gamma }}_{2}A\to B\mathrm{/}{\mathrm{\Gamma }}_{2}B$ with the assumed isomorphism on $H_1$. These are the base cases.

Fix $n\ge 2$ and assume $A\mathrm{/}{\mathrm{\Gamma }}_{n}A\to B\mathrm{/}{\mathrm{\Gamma }}_{n}B$ is an isomorphism. Apply [F1] to the extensions $1\to {\mathrm{\Gamma }}_{n}A\to A\to A\mathrm{/}{\mathrm{\Gamma }}_{n}A\to 1$ and $1\to {\mathrm{\Gamma }}_{n}B\to B\to B\mathrm{/}{\mathrm{\Gamma }}_{n}B\to 1$. Since ${\mathrm{\Gamma }}_{n}X\subseteq [X,X]$ for $n\ge 2$, the maps $H_1(X)\to H_1(X\mathrm{/}{\mathrm{\Gamma }}_{n}X)$ are isomorphisms. Exactness therefore makes the transgression $H_2(X\mathrm{/}{\mathrm{\Gamma }}_{n}X)\to {\mathrm{\Gamma }}_{n}X\mathrm{/}[X,{\mathrm{\Gamma }}_{n}X]$ onto, with kernel the image of $H_2(X)$. By definition $[X,{\mathrm{\Gamma }}_{n}X]={\mathrm{\Gamma }}_{n+1}X$.

Naturality of [F1] makes the map $H_2(A\mathrm{/}{\mathrm{\Gamma }}_{n}A)\to H_2(B\mathrm{/}{\mathrm{\Gamma }}_{n}B)$ compatible with the two transgressions. It is an isomorphism because the quotient-group map is an isomorphism by the induction hypothesis. The epimorphism $H_2(A)\to H_2(B)$ makes the image of $H_2(A)$ in $H_2(A\mathrm{/}{\mathrm{\Gamma }}_{n}A)$ map onto the image of $H_2(B)$ in $H_2(B\mathrm{/}{\mathrm{\Gamma }}_{n}B)$. The induced map on the two cokernels is consequently an isomorphism. By step 1.2 and exactness, those cokernels are ${\mathrm{\Gamma }}_{n}A\mathrm{/}{\mathrm{\Gamma }}_{n+1}A$ and ${\mathrm{\Gamma }}_{n}B\mathrm{/}{\mathrm{\Gamma }}_{n+1}B$.

The inclusions and quotient maps give exact central extensions $1\to {\mathrm{\Gamma }}_{n}X\mathrm{/}{\mathrm{\Gamma }}_{n+1}X\to X\mathrm{/}{\mathrm{\Gamma }}_{n+1}X\to X\mathrm{/}{\mathrm{\Gamma }}_{n}X\to 1,X=A,B,$ because $[X,{\mathrm{\Gamma }}_{n}X]={\mathrm{\Gamma }}_{n+1}X$. The maps on the kernel and quotient terms are isomorphisms by step 2.1 and the induction hypothesis. The middle map is injective: an element in its kernel projects to the identity in the quotient, hence lies in the kernel term, where injectivity holds. It is surjective: for a target element, lift its quotient class through the quotient isomorphism and then correct the chosen middle lift by a kernel element using the kernel isomorphism. Thus $A\mathrm{/}{\mathrm{\Gamma }}_{n+1}A\to B\mathrm{/}{\mathrm{\Gamma }}_{n+1}B$ is an isomorphism.

Steps 1.1 and 3.1 prove by induction the isomorphism for every finite $n$. Apart from the inherited AC used to obtain the homology sequence [F1], the induction uses only exactness and a single element lift at a time; no additional choice principle is used.