Let $\mathscr{C}$, $\mathscr{D}$, and $\mathscr{E}$ be (infinity) categories, and assume we're given a Cartesian diagram: $\require{AMScd}$
\begin{CD}
\mathscr{C} \times\_{\mathscr{E}} \mathscr{D} @>\operatorname{pr}\_1>> \mathscr{D}\\
@V \operatorname{pr}\_2 V V @VV \varphi V\\
\mathscr{C} @>>\psi> \mathscr{E}
\end{CD}
Now let $\mathbf{C}$ be some other cocomplete infinity category and let $F: \mathscr{D} \to \mathbf{C}$ be a functor.


Since $\mathbf{C}$ is cocomplete, we can consider the left Kan extension $\varphi\_!(F)$ of $F$ along $\varphi$. By definition, $\varphi\_!$ is the left adjoint of the restriction functor $$\varphi^\*: \operatorname{Fun}(\mathscr{E},\mathbf{C}) \longrightarrow \operatorname{Fun}(\mathscr{D},\mathbf{C}),$$ where $\operatorname{Fun}(-,-)$ denotes the category of functors between two categories. Similarly, we can consider the left Kan extension $(\operatorname{pr}\_2)\_!(\operatorname{pr}\_1)^\*(F)$ of the pullback of $F$ to the fiber product along $\operatorname{pr}\_2$.


By the universal property of left Kan extensions, there is a natural transformation $$\beta\_F:(\operatorname{pr}\_2)\_!(\operatorname{pr}\_1)^\*(F) \longrightarrow \psi^\* \varphi\_!(F)$$
and I would like to know if there are reasonable conditions we can put on the categories and functors involved so that $\beta\_F$ is an isomorphism. Probably this doesn't always hold, but my hope is that there are some nice situations in which it does.



Base change isomorphism for left Kan extensions
I believe one set of conditions is for either $\varphi$ to be proper or $\psi$ to be smooth. The dual of this (using right Kan extensions rather than left Kan extensions) is proven by Cisinski in "Higher Categories and Homotopical Algebra", Theorem 6.4.13.


For completeness, a map between simplicial sets $p : X \to Y$ is said to be proper when pullback along any pullback of $p$ preserves final maps (right cofinal in Lurie's terminology). More precisely, $p$ is proper if for any pair of cartesian squares in the following form, if $f$ is final then $g$ is final:
$\require{AMScd}$
\begin{CD}
X'' @>g>> X' @>>> X\\
@V V V @V V V @V V p V \\
Y'' @>>f> Y' @>>> Y
\end{CD}


A map is smooth just when its opposite is proper.


