The Stacks project

Proof. Suppose that $H^ i(K_1) = 0$ for $i > b$. Then we can find a complex of free $A/I$-modules $P_1^\bullet $ representing $K_1$ with $P_1^ i = 0$ for $i > b$. By Lemma 15.74.3 we can, by induction on $n > 1$, find complexes $P_ n^\bullet $ of free $A/I^ n$-modules representing $K_ n$ and maps $P_ n^\bullet \to P_{n - 1}^\bullet $ representing the maps $K_ n \to K_{n - 1}$ inducing isomorphisms (!) of complexes $P_ n^\bullet /I^{n - 1}P_ n^\bullet \to P_{n - 1}^\bullet $.

Thus we have arrived at the situation where $R\mathop{\mathrm{lim}}\nolimits K_ n$ is represented by $P^\bullet = \mathop{\mathrm{lim}}\nolimits P_ n^\bullet $, see Lemma 15.86.1 and Remark 15.86.6. The complexes $P_ n^\bullet $ are uniformly bounded above complexes of flat $A/I^ n$-modules and the transition maps are termwise surjective. Then $P^\bullet $ is a bounded above complex of flat $A$-modules by Lemma 15.27.4. It follows that $K \otimes _ A^\mathbf {L} A/I^ t$ is represented by $P^\bullet \otimes _ A A/I^ t$. We have $P^\bullet \otimes _ A A/I^ t = \mathop{\mathrm{lim}}\nolimits P_ n^\bullet \otimes _ A A/I^ t$ termwise by Lemma 15.27.4. The transition maps $P_{n + 1}^\bullet \otimes _ A A/I^ t \to P_ n^\bullet \otimes _ A A/I^ t$ are isomorphisms for $n \geq t$. Hence we have $\mathop{\mathrm{lim}}\nolimits P_ n^\bullet \otimes _ A A/I^ t = R\mathop{\mathrm{lim}}\nolimits P_ n^\bullet \otimes _ A A/I^ t$. By assumption and our choice of $P_ n^\bullet $ the complex $P_ n^\bullet \otimes _ A A/I^ t = P_ n^\bullet \otimes _{A/I^ n} A/I^ t$ represents $K_ n \otimes _{A/I^ n}^\mathbf {L} A/I^ t = K_ t$ for all $n \geq t$. We conclude

In other words, we have $K \otimes _ A^\mathbf {L} A/I^ t = K_ t$. This proves the lemma as it follows that $K$ is derived complete by Proposition 15.92.2. $\square$