Question about the proof of Kerodon tag 030V (Proposition 7.3.7.1)

Question

$\require{AMScd}$

Related to this, I have a question about the proof given in Kerodon of the following result:

Proposition 7.3.7.1: Let $C$ be an $\infty$-category, let $\bar{F} : C^\rhd \to D$ be a functor of $\infty$-categories, and let $U : D \to E$ be another functor of $\infty$-categories. Assume that $F = \bar{F}_{\vert C}$ is U-left Kan extended from a full subcategory $C_0 \subseteq C$. Then $\bar{F}$ is a U-colimit diagram if and only if the composite map $C_0^\rhd \to C^\rhd \to D$ is a $U$-colimit diagram.

The proof proceeds by observing that $\bar{F}$ is a $U$-colimit diagram iff for each $Y : D$, the following commutative diagram is a homotopy pullback square (regarding $D$ as a constant functor):

$$ \begin{CD} \hom(\bar{F},D) @>{}>> \hom(F,D)\\ @VVV @VVV \\ \hom(U \circ \bar{F},U(D)) @>>> \hom(U \circ F,U(D)) \end{CD} $$

Likewise, the composite is a $U$-colimit diagram if and only if for each $Y : D$ the following is a homotopy pullback square:

$$ \begin{CD} \hom(\bar{F}_{\vert C_0^\rhd},D) @>{}>> \hom(F_{\vert C_0},D)\\ @VVV @VVV \\ \hom(U \circ \bar{F}_{\vert C_0^\rhd},U(D)) @>>> \hom(U \circ F_{\vert C_0},U(D)) \end{CD} $$

Accordingly, it suffices to show that the first diagram is a pullback square if and only if the second is. Restriction maps assemble these two squares into a cube, with the first as the back face and the second as the front face. Therefore, it suffices to argue that each restriction map is a homotopy equivalence. To this end, Kerodon uses another lemma to observe that the assumption that $\bar{F}$ is $U$-Kan extended from $F$ yields two pullback squares (the left and right faces of the cube):

$$ \begin{CD} \hom(\bar{F},D) @>{}>> \hom(\bar{F}_{\vert C_0^\rhd},D)\\ @VVV @VVV \\ \hom(U \circ \bar{F},U(D)) @>>> \hom(U \circ \bar{F}_{\vert C_0^\rhd},U(D)) \end{CD} $$

$$ \begin{CD} \hom(F,D) @>{}>> \hom(F_{\vert C_0},D)\\ @VVV @VVV \\ \hom(U \circ F,U(D)) @>>> \hom(U \circ F_{\vert C_0},U(D)) \end{CD} $$

Question I fail to see how the existence of pullback squares shows that the four restriction maps are homotopy equivalences, as Kerodon indicates. It would now suffice to argue that only $\hom(U \circ F,U(D)) \to \hom(U \circ F_{\vert C_0},U(D))$ and $\hom(U \circ \bar{F},U(D)) \to \hom(U \circ \bar{F}_{\vert C_0^\rhd},U(D))$, but I cannot show this. As is, using 2-for-3 with pullbacks we can conclude that the front face being a pullback square implies that the back face is a pullback square, so the "if" is already easily shown. Is an alternative approach needed for "only if"?

Answer 1

I think you are right that the cube is not a levelwise equivalence - I saw you already put a comment on the Kerodon page so you should get an answer soon.

Here's how I would fix the proof: call your first square $S$ and your second square $S_0$ (for "restriction to $C^0$). Restriction is a map $S\to S^0$. Draw this as a cube where arrows are facing a- towards the screen, b- down and c- towards the right. I strongly recommend actually drawing the cube to follow what I say below.

Then the left face has equivalences as screen-facing arrows. This left face is the following square: $$\require{AMScd}\begin{CD}\hom(\overline F,D) @>>> \hom(\overline F_{\mid (C^0)^\triangleright},D) \\ @VVV @VVV \\ \hom(U\circ \overline F,U(D)) @>>> \hom(U\circ \overline F_{\mid (C^0)^\triangleright},U(D))\end{CD}$$

Here the horizontal maps (which are facing the screen in my cube) are equivalences : indeed writing $\star$ for the point of a cone, in $\text{Fun}(X^\triangleright, Y)$, $\hom(G,y) \simeq \hom(G(\star), y)$, and here $\star$ is preserved by $(C^0)^\triangleright \to C^\triangleright$.

The right face of the cube does not have equivalences as screen-facing arrows, it is the following: $$\begin{CD}\hom( F,D) @>>> \hom( F_{\mid C^0},D) \\ @VVV @VVV \\ \hom(U\circ F,U(D)) @>>> \hom(U\circ F_{\mid C^0},U(D))\end{CD}$$

It is, however, a pullback square by definition of $U$-left Kan extension (or by some previous lemma).

In any case, the left face having equivalences as mentioned above means that the big cube can be seen as an equivalence between two squares: the rectangle that covers the back face and the right face on the one hand, and the front face on the other hand.

In more detail, the left face having equivalences as mentioned above implies that the outer square in the following: $$\begin{CD}\hom(\overline F, D) @>>>\hom(F,D) @>>> \hom( F_{\mid C^0},D) \\ @VVV @VVV @VVV \\ \hom(U\circ \overline F,U(D)) @>>> \hom(U\circ F, U(D)) @>>> \hom(U\circ F_{\mid C^0},U(D))\end{CD}$$

is equivalent to the front face, namely:

$$\begin{CD}\hom(\overline F_{\mid C^0}, D) @>>>\hom(F_{\mid C^0},D)\\ @VVV @VVV \\ \hom(U\circ \overline F_{\mid C^0},U(D)) @>>> \hom(U\circ F_{\mid C^0}, U(D))\end{CD}$$

Now in the first rectangle, the rightmost square is a pullback, so by the pullback lemma, the outer rectangle is a pullback if and only if the leftmost square is.

The outer rectangle is a pullback if and only if the equivalent one is.

So the leftmost square is a pullback if and only if the last square I drew is one. I think this is what you wanted.