Hyper-Tor spectral sequence

Form the double complex $M{\otimes }_R{P}_{q,p}$ and filter by resolution degree $p$. For every $p$, the horizontal complex $P_{\ast ,p}$ is split into its homology and contractible identity disks. Tensoring preserves those split identities, so its horizontal homology is canonically $M{\otimes }_R{H}_q(P_{\ast ,p})$. This identification comes from tensors of cycles and is independent of the splittings used to verify it.

The vertical complex $H_q(P_{\ast ,p})$, augmented to $H_{q}K$, is a projective resolution. The differential on the first page is its induced signed resolution differential. Taking its degree-$p$ homology gives ${\mathrm{Tor}}_p^R(M,H_{q}K)$ by F2. To verify the target model directly, filter the augmented total $\mathrm{Tot}P\to K$ by original complex degree. Its first page is $K$ in resolution degree zero and zero in higher resolution degrees because the augmented term columns in F1 are exact. Finite diagonals therefore make the augmentation a quasi-isomorphism. Each total term is a finite biproduct of projectives and hence projective, so this bounded-below total is the displayed supplied projective model for $M{\otimes }_R^{\mathbf{L}}K$.

F3 supplies strong convergence and the image filtration, with $F_{-1}=0$ and $F_{n-b}=H_n$ in total degree $n\ge b$. If $n<b$ the target is zero; for $n=b$ there is one possible quotient. Under DC or the corresponding supplied projective comparisons and homotopies, F1's naturality and resolution-independence assertion applies to this one-factor specialization; tensoring a comparison or homotopy with $M$ preserves its equations and the resolution-degree filtration. Hence the sequence is independent from $E^2$ onward and on the target under exactly the stated qualification. For a stalk $K$ this reduces to the ordinary Tor construction in F2, and zero $M$ gives zero throughout.