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 85.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 85.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 85.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 85.14.7 we obtain $E$. Uniqueness up to unique isomorphism follows from Lemmas 85.14.5 and 85.14.6. $\square$