Supplied inverse bimodule complexes give derived tensor equivalences

Apply [L5, L6] separately to $F$ and $G$. This defines the two tensor functors on the bounded homotopy categories of finite graded projectives and on ordinary and graded bounded derived categories; in each setting their values are represented by signed ordinary totalization.

For a bounded left $B$-complex $X$, define ${\eta }_X:F{\otimes }_A(G{\otimes }_{B}X)\to X$ by the inverse associator to $(F{\otimes }_{A}G){\otimes }_{B}X$, followed by $u{\otimes }_B{1}_X$ and the unit $B{\otimes }_{B}X\to X$. Define ${ϵ}_X:X\to F{\otimes }_A(G{\otimes }_{B}X)$ in reverse order using the inverse unit, $v{\otimes }_B{1}_X$, and the associator. By [L1, L2, L3] these are chain maps on the balanced total complexes.

For a bounded left $A$-complex $Y$, use the inverse associator to write $G{\otimes }_B(F{\otimes }_{A}Y)$ as $(G{\otimes }_{B}F){\otimes }_{A}Y$, then apply $u^{\mathrm{\prime }}{\otimes }_A{1}_Y$ and the unit $A{\otimes }_{A}Y\to Y$. The reverse natural map uses the inverse unit, $v^{\mathrm{\prime }}{\otimes }_A{1}_Y$, and the associator. These are chain maps by [L1, L2, L3].

If $h$ is a supplied homotopy between $vu$ and $1_H$, [L4] gives the homotopy $K_X(z\otimes x)=h(z)\otimes x$ after tensoring with $X$; the homotopy between $uv$ and $1_B$ transfers in the same way. Conjugating these homotopies by the associator and unit maps shows that ${ϵ}_X{\eta }_X$ and ${\eta }_X{ϵ}_X$ are homotopic to the respective identity maps. Thus the two maps are inverse in the homotopy category.

For a chain map $g:X\to X^{\mathrm{\prime }}$, the naturality square for $u\otimes 1$ commutes on each elementary tensor, since both routes send $z\otimes x$ to $u(z)\otimes g(x)$; the same holds for $v\otimes 1$. The associator and units are natural by [L1, L2], and the transferred homotopies are natural because $h(z)\otimes g(x)$ is independent of the order of applying $g$ and the homotopy. Hence $\eta$ and $ϵ$ are inverse natural isomorphisms on the bounded homotopy category of left $B$-complexes.

Transfer the supplied homotopies between $v^{\mathrm{\prime }}{u}^{\mathrm{\prime }}$ and $1_J$, and between $u^{\mathrm{\prime }}{v}^{\mathrm{\prime }}$ and $1_A$, by [L4]. They show that the maps of Step 1.3 are mutually inverse in the homotopy category. Naturality follows on elementary tensors exactly as in Step 3.1, so the two maps give inverse natural isomorphisms for the $G{\otimes }_B-$ and $F{\otimes }_A-$ composite on bounded left $A$-complexes.

By [L5], $F{\otimes }_A-$ and $G{\otimes }_B-$ restrict to the indicated bounded homotopy categories of finite graded projectives. Steps 2.1–4.1 give inverse natural isomorphisms there. Each functor is exact by [L5], so these are exact equivalences. The adjacent proposition [L7] assumes two-sided projectivity for both complexes being compared; that has not been included for $H$ or $J$, so it is not applied to them. No projectivity of $H$ or $J$ is needed because [L4] transfers the supplied homotopies directly in the first variable.

By [L6], each tensor functor preserves quasi-isomorphisms and its derived functor is represented by ordinary signed totalization. The natural transformations from Steps 3.1 and 4.1 commute with every quasi-isomorphism. After localization, the vertical maps in each such naturality square are invertible; the same square therefore commutes for the inverse of a quasi-isomorphism and hence for every morphism generated in the localization. The transformations descend, and their inverse identities from Steps 2.1 and 4.1 remain identities there. The two derived tensor functors are thus quasi-inverse exact equivalences in both ordinary and graded settings.

Empty or zero complexes give zero totalizations, where the maps and homotopies still satisfy the identity equations. One-term complexes and zero-differential complexes use the same formulas; bounded endpoints add only zero summands. All inverse maps and homotopies are supplied in the hypotheses, and the derived models use the supplied $F$ and $G$, so no family of choices or Axiom of Choice is used. The theorem is an implication and proves no biconditional. It gives inverse functors for the specified pair but proves no coherence for comparison isomorphisms indexed by a group. [step 1.2, step 2.1, step 1.3, step 4.1, step 5.1, step 5.2, given, algebra] $\mathrm{\square }$