The Stacks project

Proof. Recall that $\mathop{\mathit{Sh}}\nolimits (\mathcal{C}/K_ n) = \prod _{i \in I_ n} \mathop{\mathit{Sh}}\nolimits (\mathcal{C}/u(U_{n, i}))$ and similarly for the categories of modules. This product decomposition is also inherited by the derived categories of sheaves of modules. Moreover, this product decomposition is compatible with the morphisms in the simplicial semi-representable object $K$. See Section 84.15. Hence we can set $E_ n = \prod _{i \in I_ n} E_{U_{n, i}}$ (“formal” product) in $D(\mathcal{O}_ n)$. Taking (formal) products of the maps $\rho _ a$ of Situation 84.24.1 we obtain isomorphisms $E_\varphi : f_\varphi ^*E_ n \to E_ m$. The assumption about compostions of the maps $\rho _ a$ immediately implies that $(E_ n, E_\varphi )$ defines a simplicial system of the derived category of modules as in Definition 84.14.1. The vanishing of negative exts assumed in the lemma implies that $\mathop{\mathrm{Hom}}\nolimits (E_ n[t], E_ n) = 0$ for $n \geq 0$ and $t > 0$. Thus by Lemma 84.14.7 we obtain $E$. Uniqueness up to unique isomorphism follows from Lemmas 84.14.5 and 84.14.6. $\square$