Bimodule homotopy equivalences induce natural tensor-functor isomorphisms

For every bounded graded left $A$-complex $X$, define ${\eta }_X=u{\otimes }_A{1}_X:F{\otimes }_{A}X\to F^{\mathrm{\prime }}{\otimes }_{A}X$ and ${ϵ}_X=v{\otimes }_A{1}_X:F^{\mathrm{\prime }}{\otimes }_{A}X\to F{\otimes }_{A}X$. Since $u$ and $v$ are degree-zero bimodule chain maps, [L1] makes these balanced, internal-degree-zero $B$-linear chain maps.

Transfer $h$ to $H_X(f\otimes x)=h(f)\otimes x$. By [L2], $d{H}_X+H_{X}d=(d_{F}h+h{d}_F)\otimes 1_X=((vu-{\mathrm{id}}_F)\otimes 1_X)$, which is ${ϵ}_X{\eta }_X-\mathrm{id}$. Transferring $h^{\mathrm{\prime }}$ gives ${\eta }_X{ϵ}_X-\mathrm{id}=d{H}_X^{\mathrm{\prime }}+H_X^{\mathrm{\prime }}d$. These homotopies are natural in $X$, since for every $g:X\to Y$ both orders send $f\otimes x$ to $h(f)\otimes g(x)$, and likewise for $h^{\mathrm{\prime }}$. Thus $[\eta ]$ and $[ϵ]$ are mutually inverse natural isomorphisms in the homotopy categories.

For every degree-zero chain map $g:X\to Y$, the composites in the naturality square for $\eta$ both send $f\otimes x$ to $u(f)\otimes g(x)$; the same check with $v$ proves naturality of $ϵ$. The maps are well defined on homotopy classes by [L2], so these are natural transformations on the bounded homotopy categories.

If $X$ has finite graded projective terms, [L3] places both totalizations and both tensor maps in the stated bounded projective homotopy categories. Step 1.2 proves that their composites are the identity morphisms there, so $[\eta ]$ and $[ϵ]$ give inverse natural isomorphisms on $K^b({\mathrm{proj}}^{gr}A)$.

For bounded ordinary or graded module complexes, [L4] makes both totalization functors preserve quasi-isomorphisms and [L5] identifies their localizations with the derived tensor functors. The natural transformations of Step 2.1 therefore descend through the localizations, and the homotopies of Step 1.2 still make their composites identities. They are mutually inverse natural isomorphisms on both ordinary and graded bounded derived categories.

Empty diagonals and a zero input give zero total complexes, so the formulas remain valid there. For a one-term input, the same first-variable map and homotopy formulas apply; if either supplied homotopy is zero, its equation reduces to a strict inverse equation. Bounded endpoints add only zero components, and the homotopy formulas have no terms outside the given bounded supports. No map or representative is selected: all maps and homotopies are supplied in the hypotheses. The proposition is an implication, not an iff claim. [step 1.1, step 1.2, given, algebra] $\mathrm{\square }$