I am trying to understand the proof of Lemma 05T0 of the Stacks Project. Before explaining the lemma, I will give the context that explains the title of this post.
Let $F:\mathcal{D}\to\mathcal{D}'$ be a triangulated functor between triangulated categories and let $S$ be a saturated multiplicative system compatible with the triangulated structure on $\mathcal{D}$ (Situation 05S8). To define the derived functors, we are using Definition 05S9 for the action on objects and Lemma 05SA for the action on morphisms (I think this is Deligne's definition of the derived functors in exposé XVII of SGA4, although I haven't read the exposé). By definition, one says that an object $X$ of $\mathcal{D}$ computes $RF$ if $RF$ is defined at $X$ and the canonical morphism $F(X)\to RF(X)$ is an isomorphism (Definition 05SX).
The full subcategory of $\mathcal{D}$ of objects computing $RF$ is strictly full. By Lemmas 05SZ and 05QX, it is a strictly full triangulated subcategory of $\mathcal{D}$. Lemma 05T0 asserts that, in addition, it is saturated.
To understand the proof, the first problem I have is with “hence $F(X') = F(X) \oplus E$ for some object $E$ of $\mathcal{D}'$ such that $E \to F(X' \oplus Y) \to RF(X'\oplus Y) = RF(X \oplus Y)$ is zero (Lemma 05QU).” I do understand why $F(X)\to F(X')$ having a retraction implies that it must be isomorphic to an inclusion $F(X)\to F(X)\oplus E$ (this is a property of monomorphisms in pre-triangulated categories), but where does the latter condition on the vanishment of $E$ comes from? On the other hand, taking for granted this vanishment condition, I think I understand everything what comes after until “$F(t')\to E$ annihilates $E$” (this last thing I understand too). But why is it that after “it follows that $F$ is essentially constant on $X/S$ with value $F(X)$”?
I found an straightforward proof of the result if we assume the additional hypothesis that $RF$ is defined at $X$ or at $Y$ (by the distinguished triangle $X\to X\oplus Y\to Y\xrightarrow{0}X[1]$ and Lemma 05SC, this is if and only if $RF$ is defined at both $X$ and $Y$. This condition is obtained for free is $\mathcal{D}'$ is Karoubian, 05SD).
Fully spelled out, the following is a proof of “if $X\oplus Y$ computes $RF$ and $RF$ is defined at $X$ and $Y$, then $X$ and $Y$ compute $RF$ too.”
For the proof, one must use the following
Exercise. Suppose $\mathcal{A}$ is a preadditive category and let $\begin{pmatrix}a&0\\0&b\end{pmatrix}:A_1\oplus B_1\to A_2\oplus B_2$ be a morphism in $\mathcal{A}$. If this morphism is an isomorphism, then so are $a:A_1\to A_2$ and $b:B_1\to B_2$.
Suppose then that $RF$ is defined at $X\oplus Y$, $X$ and $Y$ and that $F(X)\oplus F(Y)=F(X\oplus Y)\to RF(X\oplus Y)=RF(X)\oplus RF(Y)$ is an isomorphism (where we have used that $F$ and $RF$ are additive, the latter being shown at the beginning of 05SD). We claim that the morphism $F(X\oplus Y)\to RF(X\oplus Y)$ is of the form $\begin{pmatrix}a&0\\0&b\end{pmatrix}$, where $a:F(X)\to RF(X)$ and $b:F(Y)\to RF(Y)$ are the canonical maps. By the exercise, we will be done after seeing this.
By Lemma 05SA, we have a commutative diagram:
$$ \require{AMScd} \begin{CD} F(X)@>>> RF(X)\\ @VVV@VVV\\ F(X\oplus Y)@>>> RF(X\oplus Y)\\ @VVV@VVV\\ F(Y)@>>> RF(Y) \end{CD} $$
where the left (resp., right) vertical maps are the image of $F$ (resp., of $RF$) of the inclusion of $X$ and projection of $Y$ with respect to $X\oplus Y$. By additivity of $F$ (resp., of $RF$), these maps are inclusion and projection with respect to $F(X\oplus Y)$ (resp., w.r.t. $RF(X\oplus Y)$). By commutativity of the upper square, we deduce that the composite $F(X)\to F(X)\oplus F(Y)\to RF(X)\oplus RF(Y)\to RF(X)$ equals the canonical map $F(X)\to RF(X)$. By commutativity of the outer rectangle, we deduce that the composite $F(X)\to F(X)\oplus F(Y)\to RF(X)\oplus RF(Y)\to RF(Y)$ is zero. Changing $X\leftrightarrow Y$, the analogous properties follows for $Y$.
If only there was an alternative way of proving that $RF$ is defined at $X$ provided that $RF$ computed $X\oplus Y$, this proof idea would work. However, I am not sure if there is an easier way of seeing this than what the proof of 05T0 does (and which I don't understand).