Hyper-Ext spectral sequence

In the first branch write $M\to I^{\bullet }$ for the resolution and set $C^{q,p}={\mathrm{Hom}}_R(K^{-q},I^p)$. Put $h(f)=(-1{)}^{q+1}f{d}_K$ and $v(f)=d_{I}f$. They commute and square to zero. Its total differential is $h+(-1{)}^{q}v$. Multiplication by $(-1{)}^{pq}$ in bidegree $(q,p)$ changes this into $d_{I}f-(-1{)}^{p+q}f{d}_K$, the derived Hom differential. Each diagonal is finite, and F1 identifies total cohomology with ${\mathrm{Ext}}^{p+q}(K,M)$.

For fixed $p$, a horizontal cocycle is a map on $K^{-q}\mathrm{/}{B}^{-q}K$ to $I^p$. Restriction to $H^{-q}K\subset K^{-q}\mathrm{/}{B}^{-q}K$ is surjective by injectivity. Its kernel consists of maps factoring through $K^{-q}\mathrm{/}{Z}^{-q}K\cong B^{-q+1}K$; each such map extends to $K^{-q+1}$ by injectivity, and therefore is a horizontal boundary. This proves the canonical identity $H_h^q(C^{\bullet ,p})={\mathrm{Hom}}_R(H^{-q}K,I^p)$. Taking vertical cohomology gives ${\mathrm{Ext}}_R^p(H^{-q}K,M)$; the constant vertical sign $(-1{)}^q$ does not change kernels or images.

In the second branch apply F3 to the additive left-exact functor ${\mathrm{Hom}}_R(M,-)$. Left exactness follows because maps into a kernel are exactly maps annihilated by the next arrow. Its derived functors are Ext computed by an injective resolution. A Cartan–Eilenberg total $T$ of $K$ is a bounded-below injective model under the declared data convention. Additivity identifies $\mathrm{Tot}\mathrm{Hom}(M,I)$ with $\mathrm{Hom}(M,T)$, since its diagonals are finite. F1 therefore identifies the target with ${\mathrm{Ext}}^n(M,K)$.

F2 now gives the first sequence. In degree $n\ge -b$, the resolution filtration has $F^0{H}^n=H^n$ and $F^{n+b+1}{H}^n=0$, and its quotients are $E_{\mathrm{\infty }}^{p,n-p}$. Thus convergence is strong and finite. Maps of $K$ and comparison maps of $I$ induce the asserted maps on the double complex. A comparison homotopy in $I$ becomes a vertical homotopy on each horizontal-cohomology column, so gives identical $E_2$ maps; identical subsequent maps follow by taking page homology. F5 and the total Hom homotopy give independence and naturality, with precisely its choice qualification.

F3 gives the second displayed $E_2$, bidegree and naturality. Its filtration endpoints in degree $n\ge a$ are $F^0=H^n$ and $F^{n-a+1}=0$. Below the respective lower bounds both targets vanish; at the bound there is one possible graded quotient. Zero inputs with zero replacements give zero sequences. No splitting of a multi-piece filtration is asserted, and no additional choice is used in the finite-diagonal or injective-extension calculations.