Kerodon

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

Remark 7.3.3.3. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $\operatorname{\mathcal{C}}^{0} \subseteq \operatorname{\mathcal{C}}$ be a full subcategory, and let $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ be a functor of $\infty $-categories. Consider the evaluation functor

\[ \operatorname{ev}: \operatorname{\mathcal{C}}\times \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{\mathcal{D}}\quad \quad (C,F) \mapsto F(C). \]

For every object $C \in \operatorname{\mathcal{C}}$ and every functor $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$, the following conditions are equivalent:

$(a)$

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

$(b)$

The evaluation functor $\operatorname{ev}$ is $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0} \times \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ at $(C,F)$.

To prove this, it will suffice to show that the inclusion map

\[ \operatorname{\mathcal{C}}^{0}_{/C} \times \{ \operatorname{id}_{F} \} \hookrightarrow \operatorname{\mathcal{C}}^{0}_{/C} \times \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})_{/F} \]

is right cofinal (Corollary 7.2.2.2). This follows from Corollary 7.2.1.19, since the inclusion map $\{ \operatorname{id}_{F} \} \hookrightarrow \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})_{/F}$ is right cofinal (the identity morphism $\operatorname{id}_{F}$ is an isomorphism in $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$, and therefore final when regarded as an object of the $\infty $-category $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})_{/F}$ by virtue of Proposition 4.6.7.22).