# Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$

Corollary 7.3.2.13. 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.10 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.17. $\square$