Tor Flatness and Global Dimension

For $r\in R$, $d((pr)\otimes q)=d_{P}pr\otimes q+(-1{)}^{p}pr\otimes d_{Q}q=d(p\otimes rq)$, since both differentials are $R$-linear; thus the formula descends from elementary tensors.

Applying $d$ again gives $d_P^{2}p\otimes q+(-1{)}^{p-1}{d}_{P}p\otimes d_{Q}q+(-1{)}^p{d}_{P}p\otimes d_{Q}q+p\otimes d_Q^{2}q$.

The first and last terms vanish and the two middle terms cancel. Linearity then proves $d^2=0$ on every finite sum in each total degree.

Write $d:P_1\to P_0$ and $ϵ:P_0\to M$. The complex is concentrated in nonnegative degrees, so its degree-zero homology is the abelian group $T=(N{\otimes }_R{P}_0)\mathrm{/}\mathrm{im}(1\otimes d)$, by Tor from a projective resolution of the left module. The balanced formula $n\otimes p\mapsto n\otimes ϵ(p)$ induces $a:T\to N{\otimes }_{R}M$ by Universal property of the tensor product for balanced maps into abelian groups, since $ϵd=0$.

For $n\in N$ and $m\in M$, define $b(n,m)=[n\otimes p]$ using any lift $ϵ(p)=m$. Any two lifts differ by $d(u)$, so their classes agree. Sums and scalar multiples of lifts show that $b$ is additive in both variables and $b(nr,m)=b(n,rm)$. Thus the tensor universal property gives $\bar{b}:N{\otimes }_{R}M\to T$. This definition uses unique classes, not a simultaneous selection of lifts.

The composites $a\bar{b}$ and $\bar{b}a$ fix respectively $n\otimes m$ and $[n\otimes p]$. These elements generate the two abelian groups, so the maps are inverse.

Write $e:Q_1\to Q_0$ and $\eta :Q_0\to N$. For the right-resolved construction in Tor from a projective resolution of the right module, use $U=(Q_0{\otimes }_{R}M)\mathrm{/}\mathrm{im}(e\otimes 1)$. The augmentation gives $U\to N{\otimes }_{R}M$; its inverse sends $n\otimes m$ to $[q\otimes m]$ for any $\eta (q)=n$. Differences of lifts belong to $\mathrm{im}e$, so the class is unique, and balancing follows from using $qr$ as a lift of $nr$. Both composites fix the generating tensors, proving the second canonical identification.

DC supplies a comparison map $f:P_{\bullet }\to P_{\bullet }^{\mathrm{\prime }}$ lifting $v$. The tensor map $u\otimes f$ gives the map on the left-resolution complexes, hence on homology. DC is used only in the countable compatible selections of comparison and homotopy components supplied by the cited theorems.

If $f-g=dh+hd$, tensoring gives $u\otimes (f-g)=d(u\otimes h)+(u\otimes h)d$. On a cycle the difference is therefore a boundary. Thus the induced homology map is independent of the comparison lift.

Identity chain maps lift identities, and a composite of lifts lifts the composite module map. Any other lift is homotopic to it, so step 2.1 gives the identity and composition laws. Tensor maps in different variables commute on pure tensors and hence on the whole tensor product. For the right-resolution construction lift $u$ to $g:Q\to Q^{\mathrm{\prime }}$ and use $g\otimes v$; its homotopies and the same computations give both functor laws.

Put $K_{-1}=M$, let $q_0:P_0\to K_{-1}$ be the augmentation, and put $K_0=\ker q_0$. For $j\ge 1$, exactness factors the differential as $d_j={\iota }_{j-1}{q}_j$, where $q_j:P_j\twoheadrightarrow K_{j-1}$ is surjective, $K_j=\ker q_j$, and ${\iota }_j:K_j\hookrightarrow P_j$ is inclusion.

If $K_{j-1}$ is projective, [F1] applied to its identity gives a section $s_j:K_{j-1}\to P_j$ of $q_j$. The map $p\mapsto p-s_j{q}_j(p)$ takes values in $K_j$; write it $r_j:P_j\to K_j$. Then $r_j{\iota }_j=1$ and ${\iota }_j{r}_j+s_j{q}_j=1$. A retract of a projective module is projective: for $f:K_j\to B$ and a surjection $E\to B$, lift $f{r}_j:P_j\to B$ and restrict the lift along ${\iota }_j$. Thus $K_j$ is projective.

Starting with the projective $K_{-1}=M$, repeat step 2.1 through $j=i+1$. This is a finite succession of existential choices for the fixed integer $i$, not a simultaneous choice of splittings in all degrees. It needs neither AC nor dependent choice.

Write $T(f)=1_N\otimes f$. If $z\in N{\otimes }_R{P}_i$ is a cycle, then $T({\iota }_{i-1})T(q_i)z=0$. Since $T(r_{i-1})T({\iota }_{i-1})=1$, it follows that $T(q_i)z=0$. The identity from step 2.1 therefore gives $z=T({\iota }_i)T(r_i)z$.

Set $w=T(s_{i+1})T(r_i)z\in N{\otimes }_R{P}_{i+1}$. Then $T(d_{i+1})w=T({\iota }_i)T(q_{i+1})T(s_{i+1})T(r_i)z=T({\iota }_i)T(r_i)z=z$. Every cycle is a boundary, so $H_i(N{\otimes }_R{P}_{\bullet })=0$.

For a projective right module $N$ and any supplied right projective resolution $Q_{\bullet }\to N$, perform the same construction with right-linear maps and apply $T(f)=f\otimes 1_M$. The identities in steps 4.1 and 5.1 are unchanged and give $H_i(Q_{\bullet }{\otimes }_{R}M)=0$. Since $i>0$ was arbitrary, [F2] gives both claimed vanishings for every supplied resolution, without selecting a family of splittings over all $i$.

The choice-free implication in Equivalent characterizations of projective modules supplies a split free cover $F=R^{(I)}\cong P\oplus P^{\mathrm{\prime }}$: lift the identity of $P$ through its canonical free cover. Fix the resulting inclusion $i:P\to F$ and retraction $p:F\to P$.

For any right module $N$, the balanced pairing $(n,(r_j))\mapsto (n{r}_j{)}_j$ induces $N{\otimes }_{R}F\to N^{(I)}$ by Universal property of the tensor product for balanced maps into abelian groups. Its inverse sends a finite-support tuple $(n_j)$ to ${\sum }_j{n}_j\otimes e_j$. The two composites fix elementary tensors and coordinate generators, since $n\otimes {\sum }_j{r}_j{e}_j={\sum }_{j}n{r}_j\otimes e_j$. These identifications commute with homomorphisms in $N$.

Direct sums of exact sequences are exact: kernels are computed coordinatewise, and an element of the kernel has finite support, so finitely many preimages suffice to lift it from the preceding term. Finite choices require no AC. Thus step 2.1 shows that $-{\otimes }_{R}F$ is exact.

Tensoring $i$ and $p$ gives natural maps with composite the identity. If $z$ is a cycle in a sequence tensored with $P$, include it into the sequence tensored with $F$, lift it there by step 3.1, and retract that lift using $p$. This proves exactness after tensoring with $P$, including the endpoint conditions. Hence $P$ is flat by Left and right flat modules over an arbitrary ring.

For a projective right module, use its split right free cover and the balanced isomorphism $R^{(I)}{\otimes }_{R}N\to N^{(I)}$, $(r_j)\otimes n\mapsto (r_{j}n{)}_j$, whose inverse is $(n_j)\mapsto {\sum }_j{e}_j\otimes n_j$. The same coordinatewise and retract arguments prove right flatness, without invoking tensor symmetry or choice.

The module $Q_p$ is flat as a right module, so $Q_p{\otimes }_R-$ preserves the exact augmented complex $P_{\bullet }\to M$.

Its degree-$q$ terms are exactly $Q_p{\otimes }_R{P}_q$, and its augmentation is $Q_p{\otimes }_R{P}_0\to Q_p{\otimes }_{R}M$.

Thus the row indexed by $p$ is exact, including the augmentation; this is the claimed augmented-row condition.

The module $P_q$ is flat as a left module, so $-{\otimes }_R{P}_q$ preserves exactness of $Q_{\bullet }\to N$.

The resulting degree-$p$ terms are $Q_p{\otimes }_R{P}_q$, with augmentation $Q_0{\otimes }_R{P}_q\to N{\otimes }_R{P}_q$.

Hence every augmented fixed-$q$ row is exact, on the correct right-module/left-module tensor convention.

The augmentations give degreewise surjective chain maps $a:\mathrm{Tot}K\to N{\otimes }_R{P}_{\bullet }$ and $b:\mathrm{Tot}K\to Q_{\bullet }{\otimes }_{R}M$, supported respectively on $p=0$ and $q=0$. Their surjectivity and exact augmented fixed-$q$ and fixed-$p$ complexes follow from The augmented fixed-q rows of the tensor double complex are exact and The augmented rows of the tensor double complex are exact, respectively. The differential is $d_h+d_v$, with $d_v=(-1{)}^p(1\otimes d_P)$ as in The first-quadrant tensor double complex of two projective resolutions.

The kernel of $a$ is the total of the double complex obtained by replacing $K_{0,q}$ by $\ker (Q_0\otimes P_q\to N\otimes P_q)$. Every fixed-$q$ horizontal complex is exact. For a total cycle $z$ of degree $n\ge 0$, take its largest nonzero $q$ component $z_{p,q}$. The cycle equation at that $q$ says $d_h{z}_{p,q}=0$, because the next higher $q$ component is zero. Horizontal exactness gives $y_{p+1,q}$ with $d_{h}y=z_{p,q}$. Subtracting $dy$ removes that component and introduces only a component at $q-1$. Repeating terminates at $q=0$ and expresses $z$ as a boundary. Thus $\ker a$ is acyclic, including degree zero; negative degrees are zero. This is the filtration by $q$, not by $p$.

The kernel of $b$ is obtained by replacing $K_{p,0}$ by $\ker (Q_p\otimes P_0\to Q_p\otimes M)$. Its fixed-$p$ vertical complexes are exact, with multiplication of their differentials by $(-1{)}^p$ harmless. Now eliminate a cycle's largest $p$ component by solving $d_{v}y=z_{p,q}$ in bidegree $(p,q+1)$. Subtracting $dy$ leaves only lower $p$ components; finitely many repetitions show that $\ker b$ is acyclic. This uses the filtration by $p$, not by $q$.

The short exact sequences of each kernel, total complex and edge, together with The long exact sequence in homology, make both $a$ and $b$ quasi-isomorphisms. Hence $H_i(N{\otimes }_R{P}_{\bullet })\stackrel{H_i(a)}{\leftarrow }{H}_i(\mathrm{Tot}K)\stackrel{H_i(b)}{\to }{H}_i(Q_{\bullet }{\otimes }_{R}M)$ gives the asserted isomorphism $H_i(b)H_i(a{)}^{-1}$.

Under DC, maps of modules lift to maps of their supplied resolutions by Projective comparison maps exist. The resulting tensor double-complex maps commute with $a,b$, proving naturality of the ratio in step 3.1. Two lifts are chain-homotopic by Projective comparison maps are unique up to chain homotopy. Tensor homotopies in the first factor are $h_Q\otimes 1$ and in the second factor $(-1{)}^{p}1\otimes h_P$; direct substitution gives the total homotopy equation. Thus induced homology maps are independent of lifts. Taking module identities also gives independence and coherence under change of the supplied resolutions.

Form $K_{p,q}=Q_p{\otimes }_R{P}_q$ as in The first-quadrant tensor double complex of two projective resolutions. The augmentations define degreewise surjective chain maps $a:\mathrm{Tot}K\to N{\otimes }_{R}P$ and $b:\mathrm{Tot}K\to Q{\otimes }_{R}M$.

Choose comparison maps $g:Q\to Q^{\mathrm{\prime }}$ and $f:P\to P^{\mathrm{\prime }}$ lifting $u,v$ by Projective comparison maps exist. The map $T=\mathrm{Tot}(g\otimes f)$ commutes with both augmented edge maps: $a^{\mathrm{\prime }}T=(u\otimes f)a$ and $b^{\mathrm{\prime }}T=(g\otimes v)b$. These identities hold on pure tensors because comparison maps preserve augmentations.

By The augmented fixed-q rows of the tensor double complex are exact, each fixed-$q$ augmented horizontal complex is exact. If $z\in \ker a$ is a total cycle, choose its largest nonzero $q$-component. The cycle equation there is a horizontal cycle equation, so horizontal exactness gives a preimage one horizontal degree higher. Subtracting its total boundary removes that component and introduces terms only at lower $q$. Finite diagonal support makes the iteration terminate, so $\ker a$ is acyclic. The long exact homology sequence The long exact sequence in homology therefore makes $H(a)$ an isomorphism.

By The augmented rows of the tensor double complex are exact, the same elimination with the largest nonzero $p$-component proves that $\ker b$ is acyclic; the sign $(-1{)}^p$ on the vertical differential does not affect exactness. Hence $H(b)$ is also an isomorphism. Thus the balance map is the specified ratio $H(b)H(a{)}^{-1}$, agreeing with the natural isomorphism asserted in The left and right projective constructions of Tor are naturally isomorphic.

Taking homology in step 1.2 and using steps 2.1--2.2 gives $H(g\otimes v)H(b)H(a{)}^{-1}=H(b^{\mathrm{\prime }})H(a^{\mathrm{\prime }}{)}^{-1}H(u\otimes f)$. This is the naturality square.

Under DC, Projective comparison maps are unique up to chain homotopy makes any two lifts homotopic, and Each resolution-defined Tor construction is covariant in both variables makes their edge homology maps equal. Apply step 3.1 to identity module maps for replacement resolutions. Opposite comparison maps compose to a lift of the identity, so they induce inverse identifications; a direct and a composite comparison among three resolutions lift the same identity and therefore induce the same map. Identity comparisons induce identities. This proves independence and the cocycle laws.

By the DC-qualified The horseshoe lemma for projective resolutions, choose a projective horseshoe resolution of the middle module that fits with resolutions of the outer modules into a degreewise split short exact sequence. DC supplies the compatible choices through its successive degrees. Tensoring with $N$ preserves each splitting: tensor the inclusion, projection and their two section/retraction maps, whose splitting identities persist by additivity and composition. Hence the tensored sequence of complexes is short exact over an arbitrary ring.

Apply The long exact sequence in homology to the complexes in step 1.1. Their homology groups give the Tor presentations of The balanced Tor bifunctor. The canonical degree-zero identifications of Degree-zero Tor is the tensor product in either construction give the stated tensor tail.

For a morphism of short exact sequences, choose comparison maps on the end resolutions under DC as in Each resolution-defined Tor construction is covariant in both variables. The compatible-middle-map clause of The left derived connecting map is independent of the horseshoe resolution and lifts extends them to a commuting horseshoe ladder; that clause uses projectivity and DC, not a property of a particular derived functor. Tensor the ladder with $N$ and apply Naturality of the homology connecting morphism. Applying the same argument to identity module maps compares different horseshoes. The covariance proposition makes homology maps independent of comparison lifts, so the resulting Tor connecting maps are independent and natural. A map of right modules induces a tensor ladder directly and the same homology naturality applies. This proves the asserted natural exact sequence without assuming left exactness of tensoring.

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.

Under DC, The long exact Tor sequence in the left-module variable gives the segment ${\mathrm{Tor}}_{i+1}(N,P)\to {\mathrm{Tor}}_{i+1}(N,M)\stackrel{\mathrm{\partial }}{\to }{\mathrm{Tor}}_i(N,K)\to {\mathrm{Tor}}_i(N,P)$.

Compute the projective variable using its length-zero resolution. The positive homology groups are zero by Positive Tor vanishes when the resolved variable is projective. Under DC, The Tor balance isomorphism is natural and coherent under a change of resolutions transports that computation to the resolutions in step 1.1. Both outside terms therefore vanish since $i\ge 1$.

Exactness makes $\mathrm{\partial }$ injective and surjective. Naturality follows from the connecting-map naturality of the cited long exact sequence. For $0\to L\to Q\to N\to 0$, use The long exact Tor sequence in the right-module variable and the length-zero resolution of the projective right module $Q$; its two outside positive Tor groups vanish by the same argument, proving the second formula and its naturality.

If $M$ is flat, tensor a full projective resolution $Q_{\bullet }\to N$ with $M$. Exactness of $-{\otimes }_{R}M$ preserves its augmented exactness, so $H_i(Q_{\bullet }{\otimes }_{R}M)=0$ for every $i>0$. The right-resolution definition and The balanced Tor bifunctor give ${\mathrm{Tor}}_1^R(N,M)=0$.

For right modules $A\to B\to C\to 0$, the universal property Universal property of the tensor product for balanced maps into abelian groups gives $C{\otimes }_{R}M\cong (B{\otimes }_{R}M)\mathrm{/}\mathrm{im}(A{\otimes }_{R}M)$: a balanced map on $B\times M$ kills that image exactly when it factors through $C\times M$. Thus tensoring is right exact over the arbitrary ring $R$. In particular $H_0(Q_{\bullet }{\otimes }_{R}M)\cong N{\otimes }_{R}M$, naturally under augmentation-preserving maps.

Conversely, let $K\hookrightarrow P$ be an inclusion of right modules. Apply the projective horseshoe construction to $0\to K\to P\to P\mathrm{/}K\to 0$, tensor its degreewise split resolution sequence with $M$, and take the long exact homology sequence. Its degree-zero boundary identifies the kernel of $K\otimes M\to P\otimes M$ with the image of ${\mathrm{Tor}}_1(P\mathrm{/}K,M)$.

The assumed vanishing makes every such tensor map injective; together with right exactness this gives exactness on all short exact sequences, hence flatness.

If $N$ is flat, tensor a full projective resolution of $M$ with $N$. Exactness of $N{\otimes }_R-$ preserves the augmented resolution, so its positive homology, and in particular ${\mathrm{Tor}}_1(N,M)$ by The balanced Tor bifunctor, vanishes.

If $A\to B\to C\to 0$ is exact in left modules, Universal property of the tensor product for balanced maps into abelian groups identifies $N{\otimes }_{R}C$ with $(N{\otimes }_{R}B)\mathrm{/}\mathrm{im}(N{\otimes }_{R}A)$: balanced maps annihilating the image are precisely those that descend to $N\times C$. Thus $N{\otimes }_R-$ is right exact over the arbitrary ring $R$. Applied to a resolution $P_1\to P_0\to X\to 0$, this gives $H_0(N{\otimes }_R{P}_{\bullet })\cong N{\otimes }_{R}X$. This is natural under comparison maps because augmentations commute with them. By The balanced Tor bifunctor, it is the natural identification ${\mathrm{Tor}}_0^R(N,X)\cong N{\otimes }_{R}X$.

Conversely, for an inclusion $K\hookrightarrow P$ of left modules, apply The long exact Tor sequence in the left-module variable to $0\to K\to P\to P\mathrm{/}K\to 0$. Exactness identifies the kernel of $N\otimes K\to N\otimes P$ with the image of ${\mathrm{Tor}}_1(N,P\mathrm{/}K)$.

Universal vanishing gives injectivity for every such inclusion, and right exactness supplies the rest; thus $N{\otimes }_R-$ is exact.

Apply the DC-qualified The long exact Tor sequence in the left-module variable. Its exact degree-zero tail is ${\mathrm{Tor}}_1^R(N,C)\stackrel{\mathrm{\partial }}{\to }N{\otimes }_{R}A\to N{\otimes }_{R}B\to N{\otimes }_{R}C\to 0$.

By exactness of that tail, exactness already holds at $N{\otimes }_{R}B$ and $N{\otimes }_{R}C$, including surjectivity of the final tensor map. The kernel of $N{\otimes }_{R}A\to N{\otimes }_{R}B$ equals $\mathrm{im}\mathrm{\partial }$. This uses the stated Tor LES tail, not an undeclared tensor theorem for a commutative ring.

Thus injectivity of $N\otimes A\to N\otimes B$, and hence exactness of the whole tensor sequence, is equivalent to $\mathrm{\partial }=0$.

Let $Q_1=Q_0=\mathbb{Z}$, with $d_1(k)=nk$, zero terms above degree one, and augmentation the quotient map to $\mathbb{Z}\mathrm{/}n$. Multiplication by $n$ is injective and its image is the augmentation kernel. The module $\mathbb{Z}$ is projective without choice: to lift a map $\mathbb{Z}\to B$ through $E\twoheadrightarrow B$, choose one preimage of the image of $1$ and extend by integer multiplication. The zero module is projective by its unique map. Thus $Q$ is a projective resolution, also when $n=1$.

AC supplies DC as follows. For any nonempty set $X$ with an entire relation and specified start $a$, apply AC to the family of its nonempty successor sets to obtain a successor function $s:X\to X$. Iterate $s$ from $a$ using [L3]. The resulting sequence is precisely the chain required by The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain. This is the use of AC; it is not an appeal to a later choice theorem.

The maps $\mathbb{Z}{\otimes }_{\mathbb{Z}}M\to M$, $k\otimes m\mapsto km$, and $M\to \mathbb{Z}{\otimes }_{\mathbb{Z}}M$, $m\mapsto 1\otimes m$, are inverse: the first descends by balance and the composites are identities because $k\otimes m=1\otimes km$. Under these maps $d_1\otimes 1$ is multiplication by $n$. Hence $Q\otimes M$ is $0\to M\stackrel{n}{\to }M\to 0$ in degrees one and zero.

There are no degree-two boundaries, so $H_1(Q\otimes M)=\ker (n:M\to M)=\{m:nm=0\}$. For a homomorphism $v:M\to M^{\mathrm{\prime }}$, the map $1_Q\otimes v$ is $v$ in both degrees and induces its restriction on these kernels. This proves the calculation and its naturality without choice; for $n=1$ the kernel is zero.

Apply [L2] using the DC supplied in step 1.2. The right-resolution calculation in step 3.1 agrees canonically with that from any other supplied right resolution and, when a left resolution of $M$ is supplied, with the left-resolution calculation. Naturality and coherence of these identifications transport the explicit natural kernel map. Thus the displayed balanced-Tor formula holds under the stated conventions without assuming any unprovided resolution-existence theorem.

By [L1] with $M=\mathbb{Z}\mathrm{/}n$, the balanced Tor group is canonically the kernel of multiplication by $m$ on $\mathbb{Z}\mathrm{/}n$. Both cyclic modules have the explicit two-term projective resolutions supplied by [L1], so its supplied-resolution hypotheses are met. AC is used here through its comparison clause, not in the following arithmetic.

Put $g=\gcd (m,n)$, $m=ga$, $n=gb$, with $g,b>0$. By [L2], $\gcd (a,b)=1$ and $mx\equiv 0(\mathrm{m}\mathrm{o}\mathrm{d}n)$ is equivalent to $b\mid ax$. By [L3] choose integers $u,v$ with $ua+vb=1$. If $b\mid ax$, then $x=uax+vbx$ is divisible by $b$; the converse is immediate. Hence the kernel in step 1.1 consists precisely of the multiples of $b$ modulo $n=gb$.

The map $\mathbb{Z}\mathrm{/}g\to \mathbb{Z}\mathrm{/}n$, $[t{]}_g\mapsto [bt{]}_n$, is well defined and additive since $bg=n$. Its image is the kernel from step 2.1. It is injective because $gb\mid bt$ holds exactly when $g\mid t$, by cancellation of the nonzero integer $b$. Thus it is an isomorphism onto that kernel, including $g=1$ when both groups in this identification are trivial. Composing with step 1.1 proves the claim.

The canonical free cover $\epsilon :{\mathbb{Z}}^{(A)}\twoheadrightarrow A$ exists by Every module is a quotient of a free module. The integers are a PID: a nonzero ideal has a least positive integer $d$ by The well-ordering principle, and division with remainder by $d$ from Division with remainder in $\mathbb{Z}$: for $a\in \mathbb{Z}$ and $b>0$ there are unique $q,r\in \mathbb{Z}$ with $a=qb+r$ and $0\le r<b$ shows that every element is a multiple of $d$; the zero ideal is principal as well.

For any supplied length-one projective resolution $P_{\bullet }\to A$, the tensor complex $P_{\bullet }\otimes B$ has zero terms in every degree $i\ge 2$. Its homology in those degrees is therefore zero. This proves the conditional choice-free clause and the corresponding right-resolution construction of Tor from a projective resolution of the right module.

Write $F={\mathbb{Z}}^{(A)}$ and $K=\ker \epsilon$. Under The Axiom of Choice, well-order its standard basis index set $A$ by The well-ordering theorem. For an index $a$ write $F_{\le a}$ and $F_{<a}$ for the spans of the indicated initial segments. Let $I_a\le \mathbb{Z}$ be the image of $K\cap F_{\le a}$ under the $a$-coordinate map. The integer calculation of step 1.1 gives $I_a=d_a\mathbb{Z}$ with $d_a>0$ if it is nonzero.

For every $a$ with $I_a\mathrm{\ne }0$, the set of vectors $x\in K\cap F_{\le a}$ having $a$-coordinate $d_a$ is nonempty. AC chooses one such $x_a$ for every such index at once. Each vector has finite support by The free module on a set and its standard basis. These simultaneous lifts and the preceding well-order are the two uses of AC in kernel freeness.

Use Transfinite induction on the basis order to prove that $K\cap F_{\le a}$ is spanned by the $x_b$ with $b\le a$. For $y$ in that subgroup, if $I_a=0$ its $a$-coordinate is zero; otherwise write that coordinate as $c{d}_a$ and subtract $c{x}_a$. The resulting vector lies in $K\cap F_{<a}$. If it is nonzero, its finite support has a greatest index $b<a$, and the induction hypothesis at $b$ applies. A zero remainder needs no terms. This proves the assertion at least, successor, and limit positions alike. Every nonzero member of $K$ has a greatest support index, so the chosen family spans $K$.

In a nonzero finite integer relation among the $x_a$, take the greatest index $a$ with nonzero coefficient $c_a$. Its $a$-coordinate is $c_a{d}_a\mathrm{\ne }0$, since every lower-index vector has zero coordinate there. This contradicts the relation. Thus the family is independent and is a basis of $K$; the empty family correctly handles $K=0$.

By Free modules are projective, with the exact choice boundary, AC makes both $K$ and $F$ projective. Hence $0\to K\to F\to A\to 0$ is a projective resolution of length at most one. This last use of AC selects preimages of arbitrary basis families in the free-projectivity theorem; the canonical free cover itself used no choice.

To obtain DC locally, given an entire relation $E$ on a nonempty set $X$ and $x_0\in X$, AC chooses $s(x)\in \{y:xEy\}$ for every $x\in X$; The recursion theorem then gives $x_{n+1}=s(x_n)$ from the prescribed $x_0$. This proves the exact DC hypothesis of The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain. The short resolutions from step 6.1 (also applied to $B$) and that DC hypothesis permit The balanced Tor bifunctor to identify the specified-resolution homology with the balanced groups ${\mathrm{Tor}}_i^{\mathbb{Z}}(A,B)$. Step 1.2 gives their vanishing for all $i\ge 2$. This accounts separately for the choice needed by the change-of-resolution interface.

First every subgroup $K\le {\mathbb{Z}}^r$ is finite free, by induction on the finite integer $r$. The case $r=0$ is immediate. Project $K$ to the last coordinate. If its image is zero, apply induction in ${\mathbb{Z}}^{r-1}$. Otherwise let $d$ be the least positive integer in the image, using The well-ordering principle. Division with remainder by $d$, from Division with remainder in $\mathbb{Z}$: for $a\in \mathbb{Z}$ and $b>0$ there are unique $q,r\in \mathbb{Z}$ with $a=qb+r$ and $0\le r<b$, shows that every image element is a multiple of $d$: its remainder also lies in the image and cannot be positive and smaller than $d$. Choose one $u\in K$ with last coordinate $d$. Subtracting integer multiples of $u$ gives $K=\mathbb{Z}u\oplus \ker (\pi {\mathrm{\mid }}_K)$, and the kernel is a subgroup of ${\mathbb{Z}}^{r-1}$, so induction completes the proof. These are finitely many existential choices, not a choice function on an infinite family.

Let $f:A\to B$ be injective and $z={\sum }_{i=1}^t{a}_i\otimes m_i\in A\otimes M$ have zero image in $B\otimes M$. By The tensor product $M{\otimes }_{R}N$ from the additive group underlying the free $\mathbb{Z}$-module on $M\times N$, elementary tensors, and finite tensor sums, this equality to zero has a finite witness: the formal sum ${\sum }_i{e}_{(f(a_i),m_i)}$ is a finite integer linear combination of defining additivity and balancing relations in the free abelian group on $B\times M$.