The Stacks project

Regarding the last sentence of the proof: I think there are currently no “remarks following Definition 13.23.2.” One could instead substitute this last sentence by “This is true by the commutative square in proof of Lemma 13.23.3. In this square, if $\alpha$ is a quasi-isomorphism, then $i_{L^\bullet}\circ\alpha=j(\alpha)\circ i_{K^\bullet}$ is a quasi-isomorphism too, hence so is $j(\alpha)$; by Proposition 13.23.1, $j(\alpha)$ is an iso in $K^+(\mathcal{I})$.”

In the statement, one could sharpen:

1. “then $j=j'\circ Q$ for a unique exact functor...,” since this is what we actually get from the proof (say, from Lemma 13.5.7).

2. “which is quasi-inverse in the $2$-category of triangulated categories to the canonical functor...” (I wrote the proof below).

Finally, at the end of the proof, shouldn't we say something like “we leave to the reader to check that $j'$ is quasi-inverse to $K^+(\mathcal{I})\to K^+(\mathcal{A})$” at least? Here's the proof anyway:

First we note that the components $i_{K^\bullet}$ assemble into a natural transformation $i:\operatorname{id}_{K^+(\mathcal{A})}\to\iota\circ j$, where $\iota:K^+(\mathcal{I})\to K^+(\mathcal{A})$ is the inclusion. This is witnessed by the commutative square in the proof of Lemma 13.23.3. Now, on the one hand, $\operatorname{id}_{K^+(\mathcal{I})}$ is isomorphic to the composite $K^+(\mathcal{I})\to D^+(\mathcal{A})\xrightarrow{j'} K^+(\mathcal{I})$ since $i$ becomes a natural isomorphism when restricted to $K^+(\mathcal{I})$, i.e., $i_{I^\bullet}$ is an isomorphism if $I^\bullet\in K^+(\mathcal{I})$ (use Proposition 13.23.1). By Comment #9471, this natural isomorphism is in the $2$-category of triangulated categories. On the other hand, leveraging again naturality of $i$ it is not difficult to see that $\operatorname{id}_{D^+(\mathcal{A})}$ is isomorphic to the composite $D^+(\mathcal{A})\xrightarrow{j'}K^+(\mathcal{I})\to D^+(\mathcal{A})$. Again, Comment #9471 implies this natural isomorphism lives in the $2$-category of triangulated categories. $\square$