Does one have a base change theorem in crystalline cohomology like in étale cohomology?


Suppose one has the following cartesian diagram


$$
\newcommand{\ra}[1]{\!\!\!\!\!\!\!\xrightarrow{\quad#1\quad}\!\!\!\!\!\!\!\!}
\newcommand{\da}[1]{\left\downarrow{\scriptstyle#1}\vphantom{\displaystyle\int\_0^1}\right.}
%
\begin{array}{lll}
U & \to & V \\
\da{f} & & \da{g} \\
X & \ra{h} & Y \\
\end{array}
$$


Where $U,V, X, Y$ are all smooth proper scheme over $\mathbb{Z}\_p$ and $h$ is embedding. Assume $g$ is a good enough map (smooth, proper, etc..).
Consier the map 
$$
h^\* R^1(g\_\*)\_{cry}(\mathcal{O}\_{V})\to R^1 (f\_{\*})\_{cry}(\mathcal{O}\_U)
$$
Is the above map an isomorphism (but not in the sense of derived categories)?



Base change in crystalline cohomology?
You finish your question by insisting that the isomorphism be such but "not in the sense of derived categories", which I do not understand completely, since both objects you have at hands naturally live in a derived category. If you are happy with that, Corollary 7.12 of Berthelot&Ogus' *"Notes on Crystalline Cohomology"* says that if you assume that


* $g$ is quasi-separated and smooth;
* $Y$ is quasi-compact; and, *most important*
* $U=X\times\_Y V$,


then indeed
$$
\mathbb{L}h\_\mathrm{cris}^\*\mathbb{R}g\_{\mathrm{cris}\*}\mathcal{O}\_V\to \mathbb{R}f\_{\mathrm{cris}\*}\mathcal{O}\_U
$$
is an isomorphism in the derived category of crystals on $X$ (a priori both terms live in the derived category of $\mathcal{O}\_{X/\mathbb{Z}\_p}$-modules, but Corollary 7.11 tells you that they are actually in the derived category of crystals under the above assumptions).


