Corollary 7.3.2.14. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty $-categories, and let $U: \operatorname{\mathcal{C}}\rightarrow \Delta ^1$ be a cocartesian fibration having fibers $\operatorname{\mathcal{C}}_{0} = \{ 0\} \times _{ \Delta ^1} \operatorname{\mathcal{C}}$ and $\operatorname{\mathcal{C}}_{1} = \{ 1\} \times _{\Delta ^1} \operatorname{\mathcal{C}}$. Choose a functor $G: \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{\mathcal{C}}_1$ and a natural transformation $\beta : \operatorname{id}_{\operatorname{\mathcal{C}}_0} \rightarrow G$ which exhibits $G$ as given by covariant transport along the nondegenerate edge of $\Delta ^1$ (see Definition 5.2.2.4). The following conditions are equivalent:
- $(1)$
The functor $F$ is left Kan extended from $\operatorname{\mathcal{C}}_0$.
- $(2)$
The natural transformation $F(\beta ): F|_{ \operatorname{\mathcal{C}}_0} \rightarrow F|_{ \operatorname{\mathcal{C}}_1 } \circ G$ exhibits $F|_{ \operatorname{\mathcal{C}}_1 }$ as a left Kan extension of $F|_{ \operatorname{\mathcal{C}}_0 }$ along $G$.
Proof.
Let us regard the functor $G$ as fixed. Let $M = (\Delta ^1 \times \operatorname{\mathcal{C}}_0) {\coprod }_{ ( \{ 1\} \times \operatorname{\mathcal{C}}_0 )} \operatorname{\mathcal{C}}_{1}$ be the mapping cylinder of $G$, and let us abuse notation by identifying $\operatorname{\mathcal{C}}_0 \simeq \{ 0\} \times \operatorname{\mathcal{C}}_0$ and $\operatorname{\mathcal{C}}_1$ with (disjoint) simplicial subsets of $M$. We can then identify $\alpha $ with a morphism of simplicial sets $\mu : M \rightarrow \operatorname{\mathcal{C}}$ which is the identity when restricted to $\operatorname{\mathcal{C}}_0$ and $\operatorname{\mathcal{C}}_1$.
Note that the tautological map
\[ \Delta ^1 \times \operatorname{\mathcal{C}}_0 \simeq \operatorname{\mathcal{C}}_{0} \star _{ \operatorname{\mathcal{C}}_0} \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{\mathcal{C}}_{0} \star _{ \operatorname{\mathcal{C}}_1 } \operatorname{\mathcal{C}}_1 \]
extends to a morphism of simplicial sets $\lambda : M \rightarrow \operatorname{\mathcal{C}}_0 \star _{ \operatorname{\mathcal{C}}_1} \operatorname{\mathcal{C}}_1$ which is the identity on $\operatorname{\mathcal{C}}_1$; moreover, $\lambda $ is a categorical equivalence (Proposition 5.2.4.5). It follows that precomposition with $\lambda $ induces an equivalence of $\infty $-categories
\[ \operatorname{Fun}_{ \operatorname{\mathcal{C}}_0 \coprod \operatorname{\mathcal{C}}_1 / }( \operatorname{\mathcal{C}}_0 \star _{ \operatorname{\mathcal{C}}_1 } \operatorname{\mathcal{C}}_1, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}_{ \operatorname{\mathcal{C}}_0 \coprod \operatorname{\mathcal{C}}_1 / }( M, \operatorname{\mathcal{C}}). \]
We can therefore choose a functor $G: \operatorname{\mathcal{C}}_0 \star _{\operatorname{\mathcal{C}}_1} \operatorname{\mathcal{C}}_1 \rightarrow \operatorname{\mathcal{C}}$ satisfying $G|_{ \operatorname{\mathcal{C}}_0 } = \operatorname{id}_{\operatorname{\mathcal{C}}_0}$ and $G|_{ \operatorname{\mathcal{C}}_1} = \operatorname{id}_{ \operatorname{\mathcal{C}}_1 }$, where $G \circ \lambda $ is isomorphic to $\mu $ as an object of the $\infty $-category $\operatorname{Fun}_{ \operatorname{\mathcal{C}}_0 \coprod \operatorname{\mathcal{C}}_1 / }( M, \operatorname{\mathcal{C}})$ Since condition $(2)$ depends only on the homotopy class of the natural transformation $\beta $ (Remark 7.3.1.9), we are free to modify $\beta $ and may therefore assume that $G \circ \lambda = \mu $. In this case, Proposition 7.3.2.11 allows us to reformulate condition $(2)$ as follows:
- $(2')$
The functor $(F \circ G): \operatorname{\mathcal{C}}_0 \star _{ \operatorname{\mathcal{C}}_1} \operatorname{\mathcal{C}}_1 \rightarrow \operatorname{\mathcal{D}}$ is left Kan extended from $\operatorname{\mathcal{C}}_0$.
Since $\lambda $ and $\mu $ are categorical equivalences of simplicial sets (Proposition 5.2.4.5), the functor $G$ is an equivalence of $\infty $-categories (Remark 4.5.3.5). The equivalence of $(1)$ and $(2')$ is now a special case of Proposition 7.3.3.18.
$\square$