Is the derived category of inverse systems the inverse systems of the derived category?

Let $\omega$ be the first infinite ordinal, viewed as a category (it is a poset). That is, $\omega$ is the category where $\operatorname{ob}\omega=\mathbb{N}$ and where for $n,m\in\omega$ there is one morphism from $n$ to $m$ if $n\leq m$ and none otherwise. Write $\overline{\omega}=\omega^\mathrm{op}$. The category of inverse systems over a category $\mathcal{C}$ is the functor category $\mathcal{C}^{\overline{\omega}}$. Let $\mathcal{A}$ be an abelian category. There is a natural isomorphism $\operatorname{Ch}(\mathcal{A}^{\overline{\omega}})\cong\operatorname{Ch}(\mathcal{A})^{\overline{\omega}}$, which identifies the quasi-isomorphisms in $\operatorname{Ch}(\mathcal{A}^{\overline{\omega}})$ with the natural transformations $\alpha:F\Rightarrow G$ between functors $F,G:{\overline{\omega}}\rightrightarrows\operatorname{Ch}(\mathcal{A})$ whose components are qis, i.e., $\alpha_n$ is a qis for every $n\in\omega$ [1, Lemma 3]. Thus, by the universal property of the category localization (for $D(\mathcal{A})=\operatorname{Ch}(\mathcal{A})[\mathrm{qis}^{-1}]$), we have a unique functor $D(\mathcal{A}^{\overline{\omega}})\to D(\mathcal{A})^{\overline{\omega}}$ fitting into a commutative square $$ \require{AMScd} \begin{CD} \operatorname{Ch}(\mathcal{A}^\overline{\omega})@>\cong>>\operatorname{Ch}(\mathcal{A})^\overline{\omega}\\ @VVV@VVV\\ D(\mathcal{A}^\overline{\omega})@>>>D(\mathcal{A})^\overline{\omega} \end{CD} $$

I think I came up with a proof that $D(\mathcal{A}^{\overline{\omega}})\to D(\mathcal{A})^{\overline{\omega}}$ is a category equivalence. However, I am dubious about this result, since the functor $K(\mathcal{A}^{\overline{\omega}})\to K(\mathcal{A})^{\overline{\omega}}$ is not an equivalence (it is does need be faithful nor full, see [2]). I wanted to know if there is some error in my argument for the derived category or if it is sound. The obstruction in [2] does not seem to apply in the derived category case (as long as one works with the presentation $\operatorname{Ch}(\mathcal{A})[\mathrm{qis}^{-1}]$ of $D(\mathcal{A})$ instead of $K(\mathcal{A})[\mathrm{qis}^{-1}]$).

Here is the proof:

On the one hand, $D(\mathcal{A}^{\overline{\omega}})\to D(\mathcal{A})^{\overline{\omega}}$ is essentially surjective [3, 0CQ9].

This functor is full: Let $(K_n^\bullet),(L_n^\bullet)$ be objects of $D(\mathcal{A}^{\overline{\omega}})$ (i.e., of $\operatorname{Ch}(\mathcal{A}^{\overline{\omega}})$) and let $a=(a_n):(K_n^\bullet)\to(L_n^\bullet)$ be a morphism in $D(\mathcal{A})^{\overline{\omega}}$. Using [3, 05Q3] applied to the commutative square $$ \require{AMScd} \begin{CD} K_{n+1}^\bullet@>{a_{n+1}}>>L_{n+1}^\bullet\\ @VVV@VVV\\ K_n^\bullet@>{\smash a_n}>>L_n^\bullet \end{CD} $$ and induction (actually dependent choice), we may construct an object $(U_n^\bullet)$ of $\operatorname{Ch}(\mathcal{A}^{\overline{\omega}})$, morphisms $f_n:K_n^\bullet\to U_n^\bullet$ and quasi-isomorphisms $s_n:U_n^\bullet\to L_n^\bullet$ ($f_n$ and $s_n$ are morphisms in $\operatorname{Ch}(\mathcal{A})$) with $a_n=s_n^{-1}f_n$ and such that $(f_n):(K_n^\bullet)\to (U_n^\bullet)$ and $(s_n):(U_n^\bullet)\to (L_n^\bullet)$ are morphisms in $\operatorname{Ch}(\mathcal{A}^{\overline{\omega}})$. Note that $(s_n)$ is a quasi-isomorphism in $\operatorname{Ch}(\mathcal{A}^{\overline{\omega}})$. Thus $(s_n)^{-1}(f_n):(K_n^\bullet)\to(L_n^\bullet)$ is a morphism in $D(\mathcal{A}^\omega)$ which is a lift for $a$.

Lastly, the functor $D(\mathcal{A}^{\overline{\omega}})\to D(\mathcal{A})^{\overline{\omega}}$ is faithful: suppose $(f_n):(K_n^\bullet)\to(L_n^\bullet)$ is a morphism in $D(\mathcal{A}^{\overline{\omega}})$ that becomes zero after being mapped to $D(\mathcal{A})^{\overline{\omega}}$. Then $f_n=0$ in $D(\mathcal{A})$. Since $f_{1}=0$ in $D(\mathcal{A})$, there is a quasi-isomorphism $s_{1}:L_{1}^\bullet\to U^\bullet_{1}$ such that $f_{1}s_{1}=0$ in $\operatorname{Ch}(\mathcal{A})$. Given $n$, suppose we have a quasi-isomorphism $s_i:U_i^\bullet\to K_i^\bullet$ for each $i=1,\dots,n$ with $f_is_i=0$ in $\operatorname{Ch}(\mathcal{A})$ and maps $\varphi_i:U_i^\bullet\to U_{i-1}^\bullet$ for each $1{s_i}>>K_{i}^\bullet\\ @V{\varphi_i}VV@VVV\\ U_{i-1}^\bullet@>{\smash s_{i-1}}>>K_{i-1}^\bullet \end{CD} $$ commutes. Since $f_{n+1}=0$ in $D(\mathcal{A})$, there is a quasi-isomorphism $\tilde{s}_{n+1}:\tilde{U}_{n+1}^\bullet\to K^\bullet_{n+1}$ such that $f_{n+1}\tilde{s}_{n+1}=0$ in $\operatorname{Ch}(\mathcal{A})$. Define $U_{n+1}^\bullet=\tilde{U}_{n+1}^\bullet\times^h_{K_n^\bullet}V_{n+1}^\bullet$, the homotopy pullback (see [2] for the definition). Define $\varphi_{n+1}:U_{n+1}^\bullet\to U_n^\bullet$ to be the canonical projection. Since $s_n:U_n^\bullet\to K_n^\bullet$ is a quasi-isomorphism, so is $U_{n+1}^\bullet\to \tilde{U}_{n+1}^\bullet$ (proven in [2]). Thus define the quasi-isomorphism $s_{n+1}=U_{n+1}^\bullet\to\tilde{U}_{n+1}^\bullet\xrightarrow{\tilde{s}_{n+1}}K_n^\bullet$. Thus the square \eqref{sqr} with $i=n+1$ commutes in $K(\mathcal{A}^{\overline{\omega}})$, whence also in $D(\mathcal{A}^{\overline{\omega}})$. By induction, we can construct a quasi-isomorphism $(s_n):(U_n^\bullet)\to (K_n^\bullet)$ in $\operatorname{Ch}(\mathcal{A}^{\overline{\omega}})$ with $(f_n)\circ(s_n)=0$ in $\operatorname{Ch}(\mathcal{A}^{\overline{\omega}})$; therefore $(f_n)=0$ in $D(\mathcal{A}^{\overline{\omega}})$.

―, Mathematics Stack Exchange, A characterization of AB5 and AB4 categories. Does this result show up in the literature? https://math.stackexchange.com/a/4486908/394668

―, Mathematics Stack Exchange, Quasi-isomorphisms are stable under homotopy base change in $\operatorname{Ch}(\mathcal{A})$ https://math.stackexchange.com/q/4467269/394668

The Stacks Project Authors, The Stacks Project

Mathoverflow, Derivators - diagrams in homotopy category of chain complexes, Derivators - diagrams in homotopy category of chain complexes

The forgetful functor is not faithful. Since you're not considering pro-categories, just diagram categories, it suffices to show it for arrow categories, with commutative squares as morphisms, since you can then extend by zero. This is the ordinal $\mathbf{1}$: $1\rightarrow 0$.

Let $X$ be a complex with non-trivial cohomology. Consider the following objects in $\operatorname{Ch}(\mathcal{A})^{\mathbf{1}}$: $$X\rightarrow 0,\qquad 0\rightarrow X[1].$$ There's obviously no non-trivial map from left to right in $D(\mathcal{A})^{\mathbf{1}}$. However in $D(\mathcal{A}^{\mathbf{1}})$, there's one, represented by the following commutative square: $$\begin{array}{ccc} X&\rightarrow & CX\\ \downarrow&&\downarrow\\ CX&\rightarrow&X[1] \end{array}$$ Here, $CX$ is the cone of $X$ and the maps are those appearing in the following obvious "exact triangle" in $\operatorname{Ch}(\mathcal{A})$: $$X\stackrel{1}\longrightarrow X\longrightarrow CX\longrightarrow X[1].$$ In order to check that the previous commutative square is a non-trivial morphism in $D(\mathcal{A}^{\mathbf{1}})$ it suffices to notice that the mapping cone construction defines an additive functor $$D(\mathcal{A}^{\mathbf{1}})\longrightarrow D(\mathcal{A}).$$ This functor takes the previous commutative square to the identity in $X[1]$, which is non-trivial because $X$, and hence $X[1]$, has non-trivial cohomology.

I think that the gap in your argument is assuming that if a morphism is trivial in $D(\mathcal{A})$ you can represent it by a trivial morphism in $\operatorname{Ch}(A)$ upon replacing the source (or target) with a quasi-isomorphic complex.