The long exact Tor sequence in the right-module variable

Each $P_j$ is flat by Projective left and right modules are flat over an arbitrary ring, whose projective-to-flat implication is choice-free and valid over arbitrary rings. Therefore $0\to N^{\mathrm{\prime }}{\otimes }_R{P}_{\bullet }\to N{\otimes }_R{P}_{\bullet }\to N^{\mathrm{\prime }\mathrm{\prime }}{\otimes }_R{P}_{\bullet }\to 0$ is a degreewise short exact sequence of complexes. No horseshoe resolution or commutative-ring tensor theorem is needed.

Apply The long exact sequence in homology to step 1.1. Its homology groups are the left-resolution Tor groups in The balanced Tor bifunctor. The degree-zero identifications of Degree-zero Tor is the tensor product in either construction give the displayed tensor tail; negative homology is zero because the complexes are nonnegative.

A morphism of right-module short exact sequences gives a morphism of the complexes in step 1.1. Under DC, a map between left modules lifts to a comparison of their supplied resolutions as in Each resolution-defined Tor construction is covariant in both variables. Tensoring this comparison also gives a morphism of the three complexes. In both cases Naturality of the homology connecting morphism proves the connecting squares commute. The covariance proposition makes the edge homology maps independent of comparison lifts, so replacing $P$ identifies the whole exact sequence canonically.

The identifications in The Tor balance isomorphism is natural and coherent under a change of resolutions transport these connecting maps to any supplied right-resolution presentations of the same Tor groups. Thus the sequence defines the stated balanced natural sequence, with the boundary defined by step 2.1 and transported coherently.