Lemma 47.24.4. Let $R \to R'$ be a flat homomorphism of Noetherian rings. Let $\varphi : R \to A$ be a finite type ring map. 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)$.

Proof. 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 15.60.5 it suffices to construct maps

$R\mathop{\mathrm{Hom}}\nolimits (A, K \otimes _ R^\mathbf {L} P[n]) \otimes _ A^\mathbf {L} A' \longrightarrow R\mathop{\mathrm{Hom}}\nolimits (A', (K \otimes _ R^\mathbf {L} P[n]) \otimes _ P^\mathbf {L} P')$

functorial in $K$. For this we use the map (47.14.0.1) constructed in Section 47.14 for $P, A, P', A'$. The map is an isomorphism for $K \in D^+(R)$ by Lemma 47.14.2. $\square$

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).