The Stacks project

Proof. To prove the existence of the derived functor $- \otimes _ R^\mathbf {L} N^\bullet $ we use the general theory developed in Derived Categories, Section 13.14. Set $\mathcal{D} = K(R)$ and $\mathcal{D}' = D(A)$. Let us write $F : \mathcal{D} \to \mathcal{D}'$ the exact functor of triangulated categories defined by the rule $F(M^\bullet ) = \text{Tot}(M^\bullet \otimes _ R N^\bullet )$. To prove the stated properties of $F$ use Lemmas 15.58.2 and 15.58.4. We let $S$ be the set of quasi-isomorphisms in $\mathcal{D} = K(R)$. This gives a situation as in Derived Categories, Situation 13.14.1 so that Derived Categories, Definition 13.14.2 applies. We claim that $LF$ is everywhere defined. This follows from Derived Categories, Lemma 13.14.15 with $\mathcal{P} \subset \mathop{\mathrm{Ob}}\nolimits (\mathcal{D})$ the collection of K-flat complexes: (1) follows from Lemma 15.59.10 and (2) follows from Lemma 15.59.12. Thus we obtain a derived functor

see Derived Categories, Equation (13.14.9.1). Finally, Derived Categories, Lemma 13.14.15 guarantees that $LF(K^\bullet ) = F(K^\bullet ) = \text{Tot}(K^\bullet \otimes _ R N^\bullet )$ when $K^\bullet $ is K-flat, i.e., $LF$ is indeed computed in the way described above. Moreover, by Lemma 15.59.3 the complex $K^\bullet \otimes _ R A$ is a K-flat complex of $A$-modules. Hence

which proves the final statement of the lemma. $\square$