Base change isomorphism for left Kan extensions

Question

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.

Answer 1

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.