Kerodon

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

Proposition 7.3.4.3. Let $\delta : \operatorname{\mathcal{K}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of $\infty $-categories and let $F: \operatorname{\mathcal{K}}\star _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ and $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ be functors. The following conditions are equivalent:

$(1)$

The functor $F$ is $U$-left Kan extended from $\operatorname{\mathcal{K}}$.

$(2)$

For every object $C \in \operatorname{\mathcal{C}}$, the functor

\[ F_{C}: \operatorname{\mathcal{K}}_{C}^{\triangleright } \simeq \operatorname{\mathcal{K}}_{C} \star _{ \{ C\} } \{ C\} \hookrightarrow \operatorname{\mathcal{K}}\star _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}\xrightarrow {F} \operatorname{\mathcal{D}} \]

is a $U$-colimit diagram.

Proof. By virtue of Proposition 7.3.3.7, it will suffice to show that for each object $C \in \operatorname{\mathcal{C}}$, the following conditions are equivalent:

$(1_ C)$

The functor $F$ is $U$-left Kan extended from $\operatorname{\mathcal{K}}$ at $C$.

$(2_ C)$

The functor $F_{C}$ is a $U$-colimit diagram.

This follows from Corollary 7.2.2.3, since the tautological map

\[ \operatorname{\mathcal{K}}_{C} \simeq \{ \operatorname{id}_ C \} \times _{ \operatorname{\mathcal{C}}_{/C} } \operatorname{\mathcal{K}}_{/C} \hookrightarrow \operatorname{\mathcal{K}}_{/C} \]

is right cofinal (as noted in the proof of Proposition 7.3.4.1). $\square$