The Stacks project

An alternative reference for this result is Kashiwara, Schapira, Categories and Sheaves, Corollary 14.1.8.

This is a minor point that would not confuse anyone who knows what is going on, but I am not certain what it would mean for a sequence of sets to be exact, considering that the category of sets does not have a zero object.

It seems to me that if you want your definition to make sense for sheaves of sets (in addition to abelian groups, etc.) it might be clearer to speak of the fragment of the diagram starting with $F(U)$ and ending with $\prod_{i,j}F(U_i\times_U U_j)$ being limiting or an equaliser diagram.

Small typo in the statement of the lemma: the derived tensor product on the right side should be over $f^{-1}\mathcal{O}'$, not $f^{-1}\mathcal{O}_Y$.

Sorry, the first formula in the previous comment is $\mathbb{\m z}$, and the second one is $k=\mathbb{\m q}$

I understand what you want to illustrate here, but your rings $R_n$ are not essentially of finite type over $\m z$ (unless maybe $k=\mathfrak{\m q}$)?

If you want, you can add in condition (3) that actually $S_{\lambda}$ is essentially of finite presentation over $R_{\lambda}$

Are you sure that assumption of $f$ being local is not needed?

I think it should be made clear that $f$ is required to be non-zero.

Minor correction: in the last sentence of the proof, $y$ should be replaced with $D(a)^{i+1}y$.

It should be $\varphi(I_n)\subseteq\varphi(I)^{2^{n-1}}R'$, but who cares...

There is a typo in the first displayed short exact sequence in the proof: the last term should be $H^0\otimes_B C$ instead of $N^0 \otimes_B C$.

typo: $J^\bullet$ and $I^\bullet$ are used for the same complex

A silly question: how can we deduce that the pro-objects $( H^ p(E_ n) )$ and $( H^ p(D_ n) )$ are isomorphic?

Typo: in the fourth line "to an object $M$ of $D(\textit{Ab}(\mathbf{N}))$".

Is $S_q$ intended in the statement of part (3) (in which case we indeed have it immediately from part (1)), instead of $S$?

I don't think it is necessarily the case that commutativity of the diagram $(FGA\to FGB\to FX\to (FGA)[1])\to(A\to B\to C\to A[1])$ implies commutativity of the diagram $(GA\to GB\to X\to (GA)[1])\to(GA\to GB\to GC\to (GA)[1])$. My worry is that when $G$ is regarded as a triangulated functor with the isomorphism $G\circ [1]\cong [1]\circ G$ as built in the proof it may happen that the unit $\eta:1\Rightarrow GF$ and counit $\varepsilon: FG\Rightarrow 1$ won't be trinatural (in the sense of #9797). Only if $\eta,\varepsilon$ are trinatural we will have an adjunction in the $2$-category of categories with translation (that contains (pre-)triangulated categories as a subcategory), which will induce an adjunction between categories of triangles via the $2$-functor $\mathrm{t}(-)$ (explained in #9797). From inspection of the current proof, the isomorphism $\xi':G\circ [1]\cong [1]\circ G$ can be seen to equal $$\xi'=T[GT^{-1}(\varepsilon_{T}\circ \xi_{T^{-1}GT}^{-1})\circ\eta_{T^{-1}GT}]$$ (where $\xi$ is the isomorphism $F\circ[1]\cong [1]\circ F$). However, it is not clear that $\eta,\varepsilon$ will be trinatural (i.e., compatible with $\xi,\xi'$). In [M, Proposition 47], Murfet chooses a different $\xi'$, namely (after dualizing his proof by assuming $F\dashv G$), $$(\xi')^{-1}=GT\varepsilon\cdot G\xi_G\cdot\eta_G.$$ With this definition for $\xi'$, Murfet shows that $\eta$ and $\varepsilon$ turn out to be trinatural.

References

[M] D. Murfet, Triangulated Categories Part I, http://therisingsea.org/notes/TriangulatedCategories.pdf

There is a typo at the last statement of the lemma: it should be "any $c$ elements of $I_{q'}$ which generate $(I/I^2)_q$..."

Definition 005A (3) The notion of retrocompact set is not intrinsic to the set, it's relative to the enclosing space $X$. So to emphasize that, we can write "We say a subset $Z\subset X$ is retrocompact in $X$ if ...".

There seems to be a typo: a family of morphisms $\{f_i\colon X_i\to Y\}_{i\in I}$ is completely decomposed if $\coprod f_i\colon\coprod X_i \to Y$ is completely decomposed?

I think it is interesting to give reasons to care for the definition of a $2$-morphism in the category of triangulated categories (given before Definition 13.3.4), instead of just staying with plain natural transformations. I will call a $2$-morphism as the one before Definition 13.3.4 a trinatural transformation (as other authors already do). Given a pre-triangulated category $\mathcal{D}$, I will denote $\operatorname{t}(\mathcal{D})$ to the category of triangles of $\mathcal{D}$, and $\operatorname{dt}(\mathcal{D})\subset\operatorname{t}(\mathcal{D})$ to the full subcategory of distinguished triangles. A triangulated functor $F:\mathcal{D}\to\mathcal{D}'$ of pre-triangulated categories induces functors $\operatorname{t}(F):\operatorname{t}(\mathcal{D})\to\operatorname{t}(\mathcal{D}')$ and $\operatorname{dt}(F):\operatorname{dt}(\mathcal{D})\to\operatorname{dt}(\mathcal{D}')$. If $G:\mathcal{D}\to\mathcal{D}'$ is another triangulated functor, then a trinatural transformation $\eta:F\Rightarrow G$ induces natural transformations $\operatorname{t}(\eta):\operatorname{t}(F)\Rightarrow\operatorname{t}(G)$ and $\operatorname{dt}(\eta):\operatorname{dt}(F)\Rightarrow\operatorname{dt}(G)$. That is, if $A\to B\to C\to A[1]$ is a (distinguished) triangle in $\mathcal{D}$ then we have a morphism $$\require{AMScd} \begin{CD} F(A)@>>> F(B) @>>> F(C)@>>> F(A)[1]\\ @VVV@VVV@VVV@VVV\\ G(A)@>>> G(B) @>>> G(C)@>>> G(A)[1] \end{CD}$$ of (distinguished) triangles in $\mathcal{D}'$. We remark this is possible only if $\eta$ is trinatural, just naturality is not enough. (Note the assignments $\operatorname{t}(-)$ and $\operatorname{dt}(-)$ become $2$-functors from pre-triangulated categories to categories.) In particular, if $\eta$ is a trinatural isomorphism, then the triangle on top of the last diagram is distinguished if and only if the bottom one is.