The free-presentation Lyndon bar bicomplex

Normality of R makes left F-translation on R-orbits factor through G. A nondegenerate F-tuple has a unique form $f_0(1,a_1,\dots ,a_q)$; hence its R-orbit is specified by $\pi (f_0)$ and the relative tuple $(1,a_1,\dots ,a_q)$. Thus $C_q$ is canonically free over $\mathbb{Z}G$ on these relative tuples. Both differentials are well-defined, square to zero, and anticommute because the vertical sign changes when p decreases.

To identify $H_q(C)$ without choosing a transversal of R in F, note that the permutation module on any free R-set is tensor-exact. Each element of a tensor product has finite support in the orbit set. On the union of those finitely many orbits choose one representative per orbit; there it is a finite sum of regular free modules. Coordinate lifting proves exactness on that summand, and projection onto it shows injectivity is tested there too. Thus tensoring with the restriction of each ${\bar{B}}_q(F)$ preserves exactness even without selecting representatives of all orbits at once. The augmented complex $\bar{B}(F)\to \mathbb{Z}$ is exact also after restriction to R. Form ${\bar{B}}^{\mathrm{r}\mathrm{i}\mathrm{g}\mathrm{h}\mathrm{t}}(R){\otimes }_{\mathbb{Z}R}\bar{B}(F)$. Its exact augmented rows and columns give, by the finite elimination in F1, $H_{\ast }(C)\cong H_{\ast }(R;\mathbb{Z})$. Applying the same comparison to $\bar{B}(R)\to \bar{B}(F)$ shows that the isomorphism is induced by the literal inclusion of R-tuples.

For f in F, the maps on R-vertices $r\mapsto fr$ and $r\mapsto fr{f}^{-1}$ into F are equivariant for the same conjugated R-action. The alternating prism between them, ${\sum }_i(-1{)}^i(f{r}_0,\dots ,f{r}_i,f{r}_i{f}^{-1},\dots ,f{r}_n{f}^{-1})$, has boundary equal to their difference: off-switch faces cancel in pairs and the two surviving switch endpoints are the two maps. It preserves normalized degeneracies and descends to R-coinvariants. Hence the action on $H_q(C)$ induced by left f is conjugation by f on $H_q(R;\mathbb{Z})$. Elements of R already act trivially on C, so this is the stated G-action.

For fixed q, the horizontal complex ${\bar{B}}^{\mathrm{r}\mathrm{i}\mathrm{g}\mathrm{h}\mathrm{t}}(G)\otimes C_q$ has zero positive homology since C_q is free; its zero homology is $(C_q{)}_G=({\bar{B}}_q(F){)}_F$. The augmentation to this column induces a total homology isomorphism by the finite row elimination of F1. For fixed p, the first factor is free, so vertical homology is ${\bar{B}}_p^{\mathrm{r}\mathrm{i}\mathrm{g}\mathrm{h}\mathrm{t}}(G)\otimes H_q(C)$ (the sign does not change kernels or images). Taking horizontal homology and using step 3.1 gives exactly the asserted E2 terms. Thus the total computes $H_{\ast }(F;\mathbb{Z})$, and F3 applies.

The map from $E_{01}^2$ to total H1 sends the bar cycle $(1,r)$, r in R, to $y=(1)\otimes [(1,r){]}_R\in D_{01}$. The horizontal augmentation sends this to $[(1,r){]}_F$, which represents r in $F_{\mathrm{a}\mathrm{b}}$. F2 identifies its domain with R/[F,R], so this edge is the homomorphism induced by the subgroup inclusion $R\hookrightarrow F$; it is not asserted to be injective.

For arbitrary f in F put $g=\pi (f)$ and $y=(1)\otimes [(1,f){]}_R\in D_{01}$, $x=(1,g^{-1})\otimes [(1){]}_R\in D_{10}$. Balancing uses $(g^{-1})=(1)\cdot g$, so $hx=(1)\otimes ([f{]}_R-[1{]}_R)=vy$. Thus y-x is a total cycle whose horizontal augmentation represents [f]. The vertical augmentation sends it to $-[(1,g^{-1})]$, representing $-[g^{-1}]=[g]$ in $G_{\mathrm{a}\mathrm{b}}$. Since the [f] generate H1, the other edge is exactly the quotient map. If g=1 then x is degenerate and zero, consistent with step 5.1.

Group maps of presentations act vertexwise on bars and on R-orbits, commuting with all augmentations and component maps. The constructed homology and E2 identifications, including the edge maps, are therefore natural. Empty X, trivial R, and trivial G cause no failure in the formulas; when G=1 all horizontal positive bars vanish.