From 87c901d61bea8ef639c96d81c2965238e85b2423 Mon Sep 17 00:00:00 2001
From: Aise Johan de Jong <aise.johan.de.jong@gmail.com>
Date: Wed, 17 Apr 2024 15:45:13 -0400
Subject: [PATCH] Fix another proof in derived
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Thanks to  Elías Guisado
https://stacks.math.columbia.edu/tag/05TD#comment-8400
---
 derived.tex | 40 ++++++++++++++++++++++++++--------------
 1 file changed, 26 insertions(+), 14 deletions(-)

diff --git a/derived.tex b/derived.tex
index 5b1410a8..9d0e0d67 100644
--- a/derived.tex
+++ b/derived.tex
@@ -5547,20 +5547,8 @@ \section{Higher derived functors}
 \end{lemma}
 
 \begin{proof}
-Let $A$ be an object of $\mathcal{A}$. Let $A[0] \to K^\bullet$
-be any quasi-isomorphism. Then it is also true that
-$A[0] \to \tau_{\geq 0}K^\bullet$ is a quasi-isomorphism.
-Hence in the category $A[0]/\text{Qis}^{+}(\mathcal{A})$ the
-quasi-isomorphisms $s : A[0] \to K^\bullet$ with $K^n = 0$ for $n < 0$
-are cofinal. Thus it is clear that $H^i(RF(A[0])) = 0$ for $i < 0$.
-Moreover, for such an $s$ the sequence
-$$
-0 \to A \to K^0 \to K^1
-$$
-is exact. Hence if $F$ is left exact, then $0 \to F(A) \to F(K^0) \to F(K^1)$
-is exact as well, and we see that $F(A) \to H^0(F(K^\bullet))$ is an
-isomorphism for every $s : A[0] \to K^\bullet$ as above which implies
-that $H^0(RF(A[0])) = F(A)$.
+Let $A$ be an object of $\mathcal{A}$. By Lemma \ref{lemma-negative-vanishing}
+we have $H^i(RF(A[0]) = 0$ for $i < 0$. This proves (1).
 
 \medskip\noindent
 Let $0 \to A \to B \to C \to 0$ be a short exact sequence of $\mathcal{A}$.
@@ -5572,6 +5560,30 @@ \section{Higher derived functors}
 proved above) we deduce that $0 \to R^0F(A) \to R^0F(B) \to R^0F(C)$
 is exact. Hence $R^0F$ is left exact. Of course this also proves that if
 $F \to R^0F$ is an isomorphism, then $F$ is left exact.
+
+\medskip\noindent
+Assume $F$ is left exact. Recall that $RF(A[0])$ is the value of the
+essentially constant system $F(K^\bullet)$ for $s : A[0] \to K^\bullet$
+quasi-isomorphisms. It follows that $R^0F(A)$ is the value of the essentially
+constant system $H^0(F(K^\bullet))$ for $s : A[0] \to K^\bullet$
+quasi-isomorphisms, see Categories, Lemma
+\ref{categories-lemma-image-essentially-constant}.
+But if $s : A[0] \to K^\bullet$ is a quasi-isomorphism, then
+$A[0] \to \tau_{\geq 0}K^\bullet$ is a quasi-isomorphism.
+Hence in the category $A[0]/\text{Qis}^{+}(\mathcal{A})$ the
+quasi-isomorphisms $s : A[0] \to K^\bullet$ with $K^n = 0$ for $n < 0$
+are cofinal. It follows from
+Categories, Lemma \ref{categories-lemma-cofinal-essentially-constant}
+that we may restrict to such $s$.
+Moreover, for such an $s$ the sequence
+$$
+0 \to A \to K^0 \to K^1
+$$
+is exact. Since $F$ is left exact we see that
+$0 \to F(A) \to F(K^0) \to F(K^1)$ is exact as well.
+It follows that $F(A) \to H^0(F(K^\bullet))$ is an isomorphism
+and the system is actually constant with value $F(A)$.
+We conclude $R^0F = F$ as desired.
 \end{proof}
 
 \begin{lemma}