Pointwise evaluation of the Beck-Chevalley map in $\infty$-categories

Question

In Higher Algebra Lemma 6.1.6.3, most of the proof is pretty straightforward, but after thinking I understood it all correctly, I realized I had a gap in my understanding.

Suppose we have a homotopy cartesian square of $\infty$-categories (the Lemma has these as Kan complexes, but I think this is irrelevant to my question here) $$\begin{matrix}X'&\xrightarrow{f'}&Y'\\ \downarrow^{g_X}&&\downarrow^{g_Y}\\X&\xrightarrow{f}&Y \end{matrix}$$

and for simplicity, $C$ is an $\infty$-category with enough limits for $f^*$ and $f'^*$ to admit right adjoints.

In the proposition (which has more conditions, though they are irrelevant to this question), we want to see if the Beck-Chevalley transformation $$g^*_Yf_* \to f'_*f'^*g_Y^*f_* \simeq f'_*g_X^*f^*f_*\to f'_*g_X^*$$ is an is an equivalence.

Lurie suggests we prove this by pointwise evaluation on a functor $F:X\to C$ and an object $y$ of $Y'$ of the Beck-Chevalley transformation as the induced map $$\operatorname{lim}(F|X\times_Y Y_{g_Y(y)/}) \to \operatorname{lim}(F|X'\times_Y' Y'_{y/}).$$

The trouble is, it's not clear to me why this map, induced by the diagram

$$\begin{matrix} X' & \to & Y'& \leftarrow & Y'_{y/}\\ \downarrow &&\downarrow&&\downarrow\\ X&\to&Y&\leftarrow&Y_{g_Y(y)/} \end{matrix}$$

is homotopic to the component of the Beck-Chevalley map at $F$ and $y$.

I tried evaluating the intermediate terms, but they are huge and messy, and I can't find a reference showing that they are indeed homotopic.

Is the proof easy? Does anybody have a reference?

Edit: I think this is related to the proof of 4.3.3 in Ambidexterity paper of Lurie and Hopkins. It looks like he uses cartesianness of the square there to identify (the adjuncts of) these maps (in the dual case of left Kan extensions), so I have added a cartesianness condition.

Answer 1

The Beck-Chevalley transformation $g^*_Y f_* \rightarrow f'_* g^*_X$ from a square of $\infty$-groupoids as above is an equivalence iff it's an equivalence when evaluated at every point of $Y'$, i.e. iff the transformation $p^*g^*_Y f_* \rightarrow p^*f'_* g^*_X$ is an equivalence for all maps $p : * \rightarrow Y'$. Consider the homotopy pullback square $$\begin{matrix} F & \xrightarrow{r} & *\\ \downarrow^{q} & &\downarrow^{p}\\ X' & \xrightarrow{f'} & Y'. \end{matrix}$$ The corresponding Beck-Chevalley transformation $p^*f'_* \rightarrow r_{*}q^*$ is clearly an equivalence - this just says that $f'_*$ evaluated at $p$ is the limit over the homotopy fibre $F$. Indeed, the Beck-Chevalley transformation for a square of this form (with $*$ in the upper right corner) is an equivalence (for all targets) iff the square is Cartesian. By the naturality of Beck-Chevalley transformations, the composite $(g_Y p)^* f_* \simeq p^*g^*_Y f_* \rightarrow p^*f'_* g^*_X \rightarrow r_{*}q^*g^*_X \simeq r_*(g_X q)^*$ is equivalent to the Beck-Chevalley transformation for the composite square $$\begin{matrix} F & \xrightarrow{r} & *\\ \downarrow^{g_X q} & &\downarrow^{g_Y p}\\ X & \xrightarrow{f} & Y \end{matrix}$$ (this follows from the adjunction identities). This transformation is again an equivalence if this square is Cartesian. So by 2-of-3 the original transformation is an equivalence at every $p$ if the square $$\begin{matrix} X' & \xrightarrow{f'} & Y'\\ \downarrow^{g_X} & &\downarrow^{g_Y}\\ X & \xrightarrow{f} & Y \end{matrix}$$ is Cartesian. (And conversely, this square is Cartesian if the Beck-Chevalley transformation is always invertible (or if it is invertible for functors to spaces).)

For $\infty$-categories you have to replace the homotopy fibre square with the lax pullback square $$\begin{matrix} X'_{p/} & \to & *\\ \downarrow & \Rightarrow &\downarrow\\ X' & \xrightarrow{f'} & Y' \end{matrix}$$ (which commutes up to a natural transformation in a direction I'm too lazy to work out) - the Beck-Chevalley transformation for this gives the limit formula for a right Kan extension. I'm not aware of a nice criterion for a square of ($\infty$-)categories to have an invertible Beck-Chevalley transformation, but the same argument shows that it can be checked pointwise.