Tor symmetry over a commutative ring

AC implies the DC required by [L2]: for an entire relation on a nonempty set, choose one successor at each point using AC and iterate that self-map from the prescribed start using The recursion theorem. This gives the required dependent-choice sequence. The two cyclic modules have the explicit resolutions in [L1], so no unspecified resolution-existence theorem is used.

By [L1], the first Tor group is the kernel of multiplication by $4$ on $\mathbb{Z}\mathrm{/}6$, namely $\{0,3\}$, and the reversed group is the kernel of multiplication by $6$ on $\mathbb{Z}\mathrm{/}4$, namely $\{0,2\}$. Each is cyclic of order two, in agreement with $\gcd (4,6)=2$.

Apply [L2] under step 1.1. Its termwise tensor swap and coherent comparison give an isomorphism between the two groups in step 2.1. An isomorphism between groups of order two must send the unique nonzero element to the unique nonzero element. Thus under the explicit kernel identifications it sends $[3{]}_6$ to $[2{]}_4$, so the concrete calculation agrees with the natural symmetry, not merely with equality of the two gcds.