Lemma 45.10.9. Assume given (D0), (D1), (D2), and (D3) satisfying (A), (B), and (C). Let $k''/k'/k$ be finite separable algebras and let $X$ be a smooth projective scheme over $k'$. Then

$H^*(X) \otimes _{H^0(\mathop{\mathrm{Spec}}(k'))} H^0(\mathop{\mathrm{Spec}}(k'')) = H^*(X \times _{\mathop{\mathrm{Spec}}(k')} \mathop{\mathrm{Spec}}(k''))$

Proof. We will use the results of Lemma 45.10.2 without further mention. Write

$k' \otimes _ k k'' = k'' \times l$

for some finite separable $k'$-algebra $l$. Write $F' = H^0(\mathop{\mathrm{Spec}}(k'))$, $F'' = H^0(\mathop{\mathrm{Spec}}(k''))$, and $G = H^0(\mathop{\mathrm{Spec}}(l))$. Since $\mathop{\mathrm{Spec}}(k') \times \mathop{\mathrm{Spec}}(k'') = \mathop{\mathrm{Spec}}(k'') \amalg \mathop{\mathrm{Spec}}(l)$ we deduce from axiom (B)(a) and Lemma 45.9.9 that we have

$F' \otimes _ F F'' = F'' \times G$

The map from left to right identifies $F''$ with $F' \otimes _{F'} F''$. By the same token we have

$H^*(X) \otimes _ F F'' = H^*(X \times _{\mathop{\mathrm{Spec}}(k')} \mathop{\mathrm{Spec}}(k'')) \times H^*(X \times _{\mathop{\mathrm{Spec}}(k')} \mathop{\mathrm{Spec}}(l))$

as modules over $F' \otimes _ F F'' = F'' \times G$. This proves the lemma. $\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).