Rf_* \circ Rg_* = R(g o f)_* on topological spaces

cohomology.tex

@@ -6042,6 +6042,24 @@ \section{Derived pullback}
 indeed computed in the way described above.
 \end{proof}
 
+\begin{lemma}
+\label{lemma-derived-pullback-composition}
+Let $f : X \to Y$ and $g : Y \to Z$ be morphisms of ringed spaces.
+Then $Lf^* \circ Lg^* = L(g \circ f)^*$ as functors
+$D(\mathcal{O}_Z) \to D(\mathcal{O}_X)$.
+\end{lemma}
+
+\begin{proof}
+Let $E$ be an object of $D(\mathcal{O}_Z)$.
+By construction $Lg^*E$ is computed by choosing a K-flat complex
+$\mathcal{K}^\bullet$ representing $E$ on $Z$ and
+setting $Lg^*E = g^*\mathcal{K}^\bullet$.
+By Lemma \ref{lemma-pullback-K-flat} we see that $g^*\mathcal{K}^\bullet$
+is K-flat on $Y$. Then $Lf^*Lg^*E$ is given by
+$f^*g^*\mathcal{K}^\bullet = (g \circ f)^*\mathcal{K}^\bullet$
+which also represents $L(g \circ f)^*E$.
+\end{proof}
+
 \begin{lemma}
 \label{lemma-pullback-tensor-product}
 Let $f : (X, \mathcal{O}_X) \to (Y, \mathcal{O}_Y)$
@@ -6165,6 +6183,22 @@ \section{Cohomology of unbounded complexes}
 Derived Categories, Lemma \ref{derived-lemma-derived-adjoint-functors}.
 \end{proof}
 
+\begin{lemma}
+\label{lemma-derived-pushforward-composition}
+Let $f : X \to Y$ and $g : Y \to Z$ be morphisms of ringed spaces.
+Then $Rg_* \circ Rf_* = R(g \circ f)_*$ as functors
+$D(\mathcal{O}_X) \to D(\mathcal{O}_Z)$.
+\end{lemma}
+
+\begin{proof}
+By Lemma \ref{lemma-adjoint} we see that $Rg_* \circ Rf_*$
+is adjoint to $Lf^* \circ Lg^*$. We have
+$Lf^* \circ Lg^* = L(g \circ f)^*$ by
+Lemma \ref{lemma-derived-pullback-composition}
+and hence by
+uniqueness of adjoint functors we have $Rg_* \circ Rf_* = R(g \circ f)_*$.
+\end{proof}
+
 \begin{remark}
 \label{remark-base-change}
 The construction of unbounded derived functor $Lf^*$ and $Rf_*$