diff --git a/dualizing.tex b/dualizing.tex
index 73a436f4c..f4b651972 100644
--- a/dualizing.tex
+++ b/dualizing.tex
@@ -2058,20 +2058,17 @@ \section{Trivial duality for a ring map}
 M \longmapsto \Hom_A(B, M)
 $$
 This functor is left exact and has a derived extension
-$R\Hom(B, -) : D(A) \to D(B)$. If $f_* : D(B) \to D(A)$ is the restriction
-functor, then $f_*R\Hom(B, K) = R\Hom_A(B, K)$ for every $K \in D(A)$.
-Since $R\Hom_A(A, K) = K$, the map $A \to B$ induces a canonical map
-$f_*R\Hom(B, K) \to K$ in $D(A)$ functorial in $K$.
+$R\Hom(B, -) : D(A) \to D(B)$.
 
 \begin{lemma}
 \label{lemma-right-adjoint}
 Let $A \to B$ be a ring homomorphism. The functor $R\Hom(B, -)$
-constructed above is the right adjoint to the restriction functor
-$f_* : D(B) \to D(A)$.
+constructed above is right adjoint to the restriction functor
+$D(B) \to D(A)$.
 \end{lemma}
 
 \begin{proof}
-This is a consequence of the fact that $f_*$ and $\Hom_A(B, -)$ are
+This is a consequence of the fact that restriction and $\Hom_A(B, -)$ are
 adjoint functors by Algebra, Lemma \ref{algebra-lemma-adjoint-tensor-restrict}.
 See Derived Categories, Lemma \ref{derived-lemma-derived-adjoint-functors}.
 \end{proof}
@@ -2089,13 +2086,19 @@ \section{Trivial duality for a ring map}
 
 \begin{lemma}
 \label{lemma-RHom-ext}
-Let $A \to B$ be a ring homomorphism. For $K$ in $D(A)$ we have
-$f_*R\Hom(B, K) = R\Hom_A(B, K)$ where $f_* : D(B) \to D(A)$ is
-restriction. In particular $R^q\Hom(B, K) = \Ext_A^q(B, K)$.
+Let $\varphi : A \to B$ be a ring homomorphism. For $K$ in $D(A)$ we have
+$$
+\varphi_*R\Hom(B, K) = R\Hom_A(B, K)
+$$
+where $\varphi_* : D(B) \to D(A)$ is restriction. In particular
+$R^q\Hom(B, K) = \Ext_A^q(B, K)$.
 \end{lemma}
 
 \begin{proof}
-Omitted, but see above.
+Choose a K-injective complex $I^\bullet$ representing $K$.
+Then $R\Hom(B, K)$ is represented by the complex $\Hom_A(B, I^\bullet)$
+of $B$-modules. Since this complex, as a complex of $A$-modules,
+represents $R\Hom_A(B, K)$ we see that the lemma is true.
 \end{proof}
 
 \noindent
@@ -2285,6 +2288,118 @@ \section{Trivial duality for a ring map}
 
 
 
+\section{Base change for trivial duality}
+\label{section-base-change-trivial-duality}
+
+\noindent
+In this section we consider a cocartesian square of rings
+$$
+\xymatrix{
+A \ar[r]_\alpha & A' \\
+R \ar[u]^\varphi \ar[r]^\rho & R' \ar[u]_{\varphi'}
+}
+$$
+In other words, we have $A' = A \otimes_R R'$. If $A$ and $R'$
+are {\bf tor independent over} $R$ then there is a canonical base change map
+\begin{equation}
+\label{equation-base-change}
+R\Hom(A, K) \otimes_A^\mathbf{L} A'
+\longrightarrow
+R\Hom(A', K \otimes_R^\mathbf{L} R')
+\end{equation}
+in $D(A')$ functorial for $K$ in $D(R)$. Namely, by the adjointness
+of Lemma \ref{lemma-right-adjoint} such an arrow is the same thing as a map
+$$
+\varphi'_*\left(R\Hom(A, K) \otimes_A^\mathbf{L} A'\right)
+\longrightarrow
+K \otimes_R^\mathbf{L} R'
+$$
+in $D(R')$ where $\varphi'_* : D(A') \to D(R')$ is the restriction functor.
+We may apply
+More on Algebra, Lemma \ref{more-algebra-lemma-base-change-comparison}
+to the left hand side to get that this is the same thing as a map
+$$
+\varphi_*(R\Hom(A, K)) \otimes_R^\mathbf{L} R'
+\longrightarrow
+K \otimes_R^\mathbf{L} R'
+$$
+in $D(R')$ where $\varphi_* : D(A) \to D(R)$ is the restriction functor.
+For this we can choose $can \otimes^\mathbf{L} \text{id}_{R'}$
+where $can : \varphi_*(R\Hom_R(A, K)) \to K$ is the
+counit of the adjunction between $R\Hom(A, -)$ and $\varphi_*$.
+
+\begin{lemma}
+\label{lemma-check-base-change-is-iso}
+In the situation above, the map (\ref{equation-base-change})
+is an isomorphism if and only if the map
+$$
+R\Hom_R(A, K) \otimes_R^\mathbf{L} R'
+\longrightarrow
+R\Hom_R(A, K \otimes_R^\mathbf{L} R')
+$$
+of More on Algebra, Lemma
+\ref{more-algebra-lemma-internal-hom-diagonal-better} is an isomorphism.
+\end{lemma}
+
+\begin{proof}
+To see that the map is an isomorphism, it suffices to prove it
+is an isomorphism after applying $\varphi'_*$.
+Applying the functor $\varphi'_*$ to (\ref{equation-base-change})
+and using that $A' = A \otimes_R^\mathbf{L} R'$
+we obtain the base change map
+$R\Hom_R(A, K) \otimes_R^\mathbf{L} R' \to
+R\Hom_{R'}(A \otimes_R^\mathbf{L} R', K \otimes_R^\mathbf{L} R')$
+for derived hom of
+More on Algebra, Equation (\ref{more-algebra-equation-base-change-RHom}).
+Unwinding the left and right hand side exactly as in the proof of
+More on Algebra, Lemma \ref{more-algebra-lemma-base-change-RHom}
+and in particular using
+More on Algebra, Lemma \ref{more-algebra-lemma-upgrade-adjoint-tensor-RHom}
+gives the desired result.
+\end{proof}
+
+\begin{lemma}
+\label{lemma-flat-bc-surjection}
+Let $R \to A$ and $R \to R'$ be ring maps and $A' = A \otimes_R R'$.
+Assume
+\begin{enumerate}
+\item $A$ is pseudo-coherent as an $R$-module,
+\item $R'$ has finite tor dimension as an $R$-module (for example
+$R \to R'$ is flat),
+\item $A$ and $R'$ are tor independent over $R$.
+\end{enumerate}
+Then (\ref{equation-base-change}) is an isomorphism for $K \in D^+(R)$.
+\end{lemma}
+
+\begin{proof}
+Follows from Lemma \ref{lemma-check-base-change-is-iso} and
+More on Algebra, Lemma
+\ref{more-algebra-lemma-internal-hom-evaluate-tensor-isomorphism} part (4).
+\end{proof}
+
+\begin{lemma}
+\label{lemma-bc-surjection}
+Let $R \to A$ and $R \to R'$ be ring maps and $A' = A \otimes_R R'$.
+Assume
+\begin{enumerate}
+\item $A$ is perfect as an $R$-module,
+\item $A$ and $R'$ are tor independent over $R$.
+\end{enumerate}
+Then (\ref{equation-base-change}) is an isomorphism for all $K \in D(R)$.
+\end{lemma}
+
+\begin{proof}
+Follows from Lemma \ref{lemma-check-base-change-is-iso} and
+More on Algebra, Lemma
+\ref{more-algebra-lemma-internal-hom-evaluate-tensor-isomorphism} part (1).
+\end{proof}
+
+
+
+
+
+
+
 \section{Dualizing complexes}
 \label{section-dualizing}
 
@@ -4103,58 +4218,6 @@ \section{Upper shriek algebraically}
 \ref{lemma-dualizing-quotient},
 \end{proof}
 
-\begin{lemma}
-\label{lemma-flat-bc-surjection}
-Let $\varphi : R \to A$ be a surjective homomorphism of Noetherian rings.
-Let $R \to R'$ be a flat homomorphism of Noetherian rings.
-Let $\varphi' : R' \to A' = A \otimes_R R'$ be the map induced by $\varphi$.
-Then we have a functorial maps
-$$
-\varphi^!(K) \otimes_A^\mathbf{L} A'
-\longrightarrow
-(\varphi')^!(K \otimes_R^\mathbf{L} R')
-$$
-for $K$ in $D(R)$ which are isomorphisms for $K \in D^+(R)$.
-\end{lemma}
-
-\begin{proof}
-Let $K \in D(R)$. Choose a K-injective complex $I^\bullet$ representing
-$K$. Then $I^\bullet \otimes_R R'$ represents $K \otimes_R^\mathbf{L} R'$.
-Choose a quasi-isomorphism $I^\bullet \otimes_R R' \to J^\bullet$
-where $J^\bullet$ is a K-injective complex of $R'$-modules.
-Then there is a canonical map
-$$
-\Hom_R(A, I^\bullet) \otimes_R R' \to
-\Hom_{R'}(A \otimes_R R', I^\bullet \otimes_R R') \to
-\Hom_{R'}(A', J^\bullet)
-$$
-Since $R \to R'$ is flat, the map $A \to A'$ is flat and
-$D(A) \to D(A')$ is given by $L^\bullet \mapsto L^\bullet \otimes_R R'$
-on the level of complexes. Hence the source of the arrow,
-viewed as a complex of $A'$-modules represents
-$\varphi^!(K) \otimes_A^\mathbf{L} A'$.
-Similarly, the target viewed as a complex of $A'$-modules
-represents $(\varphi')^!(K \otimes_R^\mathbf{L} R')$.
-This defines the natural transformation of the lemma.
-
-\medskip\noindent
-To see that the map is an isomorphism for some $K$ we may do so after
-applying the restriction functor $D(A') \to D(R)$.
-Since $J^\bullet$ is K-injective as a complex of $R$-modules
-(More on Algebra, Lemma \ref{more-algebra-lemma-K-injective-flat})
-and since $\Hom_{R'}(A', -) = \Hom_R(A, -)$ we see that
-$\Hom_{R'}(A', J^\bullet)$ represents
-$R\Hom_R(A, K \otimes_R^\mathbf{L} R')$ in $D(R)$.
-The right hand side represents $R\Hom(A, K) \otimes_R^\mathbf{L} R'$
-in $D(R)$. Checking the definitions we see our map is the map
-$$
-R\Hom(A, K) \otimes_R^\mathbf{L} R' \to R\Hom(A, K \otimes_R^\mathbf{L} R')
-$$
-of More on Algebra, Lemma
-\ref{more-algebra-lemma-internal-hom-evaluate-tensor-isomorphism}.
-In this way we conclude the final assertion of the lemma is true.
-\end{proof}
-
 \begin{lemma}
 \label{lemma-flat-bc}
 Let $R \to R'$ be a flat homomorphism of Noetherian rings.
@@ -4169,133 +4232,22 @@ \section{Upper shriek algebraically}
 \end{lemma}
 
 \begin{proof}
-We can choose a factorization $R \to P \to A$ where $P$ is a polynomial
-ring over $R$. This gives a corresponding factorization
-$R' \to P' \to A'$ by base change. Since we have
-$(K \otimes_R^\mathbf{L} P) \otimes_P^\mathbf{L} P' =
+Choose a factorization $R \to P \to A$ where $P$ is a polynomial ring over $R$.
+This gives a corresponding factorization $R' \to P' \to A'$ by base change.
+Since we have $(K \otimes_R^\mathbf{L} P) \otimes_P^\mathbf{L} P' =
 (K \otimes_R^\mathbf{L} R') \otimes_{R'}^\mathbf{L} P'$
 by More on Algebra, Lemma \ref{more-algebra-lemma-double-base-change}
-it suffices to prove the statement for
-$P \to A$ and $P \to P'$. This case is proved in
-Lemma \ref{lemma-flat-bc-surjection}.
-\end{proof}
-
-\begin{lemma}
-\label{lemma-bc-surjection}
-Let $\varphi : R \to A$ be a surjective homomorphism of Noetherian rings.
-Let $R \to R'$ be a homomorphism of Noetherian rings. Assume
-\begin{enumerate}
-\item $A$ is a perfect $R$-module,
-\item $R'$ and $A$ are Tor independent over $R$.
-\end{enumerate}
-Let $\varphi' : R' \to A' = A \otimes_R R'$ be the map induced by $\varphi$.
-Then we have a functorial isomorphism
+it suffices to construct maps
 $$
-\varphi^!(K) \otimes_A^\mathbf{L} A' =
-(\varphi')^!(K \otimes_R^\mathbf{L} R')
-$$
-for $K$ in $D(R)$.
-\end{lemma}
-
-\begin{proof}
-Because $A$ is a perfect $R$-module, we see that
-$A \otimes_R^\mathbf{L} R'$ is a perfect object of $D(R')$, see
-More on Algebra, Lemma \ref{more-algebra-lemma-pull-perfect}.
-By assumption (2) we have $A' = A \otimes_R^\mathbf{L} R'$
-is a perfect $R'$-module. Thus it follows from
-Lemma \ref{lemma-RHom-is-tensor-special}
-that $\varphi^!$ and $(\varphi')^!$ are given by
-derived tensor product with $N = R\Hom(A, R)$ and
-$N' = R\Hom(A', R')$. Hence it suffices to show that
-$$
-(K \otimes_R^\mathbf{L} N) \otimes_A^\mathbf{L} A' =
-(K \otimes_R^\mathbf{L} R') \otimes_{R'}^\mathbf{L} N'
-$$
-functorially for $K \in D(R)$. By transitivity of tensor
-functors (More on Algebra, Lemma \ref{more-algebra-lemma-double-base-change})
-we conclude that it suffices to construct
-an isomorphism $N \otimes_A^\mathbf{L} A' \to N'$
-in $D(A')$.
-
-\medskip\noindent
-Choose a Tate resolution $R \to (E, \text{d}) \to A$ with $E^0 = R$ as in
-Divided Power Algebra, Lemma \ref{dpa-lemma-tate-resolution}.
-Then $E^n = 0$ for $n > 0$ and $E^n$ is a finite free $R$-module
-for all $n$. Write $E' = E \otimes_R R'$ with induced differential $\text{d}$.
-Since $E^\bullet \to A$ is a flat resolution of $A$ as an $R$-module,
-we see that the map $E' \to A'$ is a quasi-isomorphism by assumption (2).
-The diagram
-$$
-\xymatrix{
-D(A) \ar[r]_{- \otimes_A^\mathbf{L} A'} & D(A') \\
-D(E, \text{d})
-\ar[u]^{- \otimes_E^\mathbf{L} A} \ar[r]^{- \otimes_E^\mathbf{L} E'} &
-D(E', \text{d}) \ar[u]_{- \otimes_{E'}^\mathbf{L} A'}
-}
-$$
-is commutative (each of the functors as well as the compositions
-are adjoints to restriction the restriction functors satisfy
-the corresponding commutativity). The vertical arrows
-are equivalences because $E \to A$ and $E' \to A'$
-are quasi-isomorphisms
-(Differential Graded Algebra, Lemma \ref{dga-lemma-qis-equivalence}).
-
-\medskip\noindent
-Putting this together with Lemma \ref{lemma-RHom-dga} we find that it suffices
-to construct an isomorphism
-\begin{equation}
-\label{equation-bc-map-algebraic}
-R\Hom(E, R) \otimes_E^\mathbf{L} E'
+R\Hom(A, K \otimes_R^\mathbf{L} P[n]) \otimes_A^\mathbf{L} A'
 \longrightarrow
-R\Hom(E', R')
-\end{equation}
-in $D(E')$.
-
-\medskip\noindent
-By Differential Graded Algebra, Lemma
-\ref{dga-lemma-compute-derived-restriction}
-the differential graded $E$-module
-$$
-H = \Hom_{\text{Mod}^{dg}_R}(E, R)
-$$
-represents $R\Hom(E, R)$ in $D(E, \text{d})$.
-The underlying complex of $R$-modules is
-$H^\bullet = \Hom^\bullet_R(E^\bullet, K^\bullet)$. This is a
-K-flat complex of $R$-modules by
-More on Algebra, Lemma \ref{more-algebra-lemma-hom-complex-K-flat}
-and our assumption that $E^\bullet$ is perfect.
-By Differential Graded Algebra, Lemma \ref{dga-lemma-base-change-K-flat}
-we see that the LHS of (\ref{equation-bc-map-algebraic})
-is represented by $H \otimes_R R'$ whose
-underlying complex of $R'$-modules is $H^\bullet \otimes_R R'$.
-
-\medskip\noindent
-Arguing as above we find that
-$$
-H' = \Hom_{\text{Mod}^{dg}_R}(E', R')
+R\Hom(A', (K \otimes_R^\mathbf{L} P[n]) \otimes_P^\mathbf{L} P')
 $$
-represents the RHS of (\ref{equation-bc-map-algebraic})
-and that as a complex of $R'$-modules we have
-$$
-(H')^\bullet =
-\Hom^\bullet_{R'}((E')^\bullet, R') =
-\Hom^\bullet_{R'}(E^\bullet \otimes_R R', R') =
-\Hom^\bullet_R(E^\bullet, R')
-$$
-The last equality is proved by applying
-Algebra, Lemma \ref{algebra-lemma-adjoint-tensor-restrict}
-to the terms making up the Hom complex.
-
-\medskip\noindent
-We define our map (\ref{equation-bc-map-algebraic}) to be the map
-$$
-H \otimes_R R' \longrightarrow H'
-$$
-defined by the following rule. An element $f$ of $H^n$ is an $R$-linear
-map from $E^{-n}$ to $R$. Thus we send $f \otimes \lambda$ to
-$\lambda f'$ where $f' : E^{-n} \to R'$ is the composition of
-$f$ with $R \to R'$. It is immediately clear that this is
-an isomorphism of $E'$-modules which finishes the proof.
+functorial in $K$. For this we use the map (\ref{equation-base-change})
+constructed in Section \ref{section-base-change-trivial-duality}
+for $P, A, P', A'$.
+The map is an isomorphism for $K \in D^+(R)$ by
+Lemma \ref{lemma-flat-bc-surjection}.
 \end{proof}
 
 \begin{lemma}
@@ -4315,28 +4267,33 @@ \section{Upper shriek algebraically}
 \end{lemma}
 
 \begin{proof}
-We can choose a factorization $R \to P \to A$ where $P$ is a polynomial
-ring over $R$ and then $A$ is a perfect $P$-module, see
+We may choose a factorization $R \to P \to A$ where $P$
+is a polynomial ring over $R$ such that $A$ is a perfect $P$-module, see
 More on Algebra, Lemma \ref{more-algebra-lemma-perfect-ring-map}.
-This gives a corresponding factorization
-$R' \to P' \to A'$ by base change. Since we have
-$(K \otimes_R^\mathbf{L} P) \otimes_P^\mathbf{L} P' =
+This gives a corresponding factorization $R' \to P' \to A'$ by base change.
+Since we have $(K \otimes_R^\mathbf{L} P) \otimes_P^\mathbf{L} P' =
 (K \otimes_R^\mathbf{L} R') \otimes_{R'}^\mathbf{L} P'$
 by More on Algebra, Lemma \ref{more-algebra-lemma-double-base-change}
-it suffices to prove the statement for
-$P \to A$ and $P \to P'$.
-By Lemma \ref{lemma-bc-surjection}
-it suffices to prove that $A$ is a perfect $P$-module
-and that $A$ and $P'$ are tor independent over $P$.
-The $P$-module $A$ is a perfect as seen above.
-For tor independence
+it suffices to construct maps
+$$
+R\Hom(A, K \otimes_R^\mathbf{L} P[n]) \otimes_A^\mathbf{L} A'
+\longrightarrow
+R\Hom(A', (K \otimes_R^\mathbf{L} P[n]) \otimes_P^\mathbf{L} P')
+$$
+functorial in $K$. We have
 $$
 A \otimes_P^\mathbf{L} P' = A \otimes_R^\mathbf{L} R' = A'
 $$
 The first equality by
 More on Algebra, Lemma \ref{more-algebra-lemma-base-change-comparison}
 applied to $R, R', P, P'$. The second equality because
-$A$ and $R'$ are tor independent over $R$.
+$A$ and $R'$ are tor independent over $R$. Hence $A$ and $P'$ are
+tor independent over $P$ and we can use the map (\ref{equation-base-change})
+constructed in Section \ref{section-base-change-trivial-duality} for
+$P, A, P', A'$
+get the desired arrow. By Lemma \ref{lemma-bc-surjection}
+to finish the proof it suffices to prove that $A$ is a perfect $P$-module
+which we saw above.
 \end{proof}
 
 \begin{lemma}