Kerodon

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

Corollary 7.3.2.8. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $\operatorname{\mathcal{C}}^{0} \subseteq \operatorname{\mathcal{C}}$ be a full subcategory, and let $F_0: \operatorname{\mathcal{C}}^{0} \rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty $-categories. The following conditions are equivalent:

$(1)$

There exists a functor $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ and a natural transformation $\beta : F_0 \rightarrow F|_{ \operatorname{\mathcal{C}}^{0} }$ which exhibits $F$ as a left Kan extension of $F_0$ along the inclusion functor $\operatorname{\mathcal{C}}^{0} \hookrightarrow \operatorname{\mathcal{C}}$.

$(2)$

There exists a functor $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ which is left Kan extended from $\operatorname{\mathcal{C}}^{0}$ and satisfies $F_0 = F|_{ \operatorname{\mathcal{C}}^{0} }$.

Proof. We will show that $(1)$ implies $(2)$; the converse is an immediate consequence of Proposition 7.3.2.6. Let $\beta : F_0 \rightarrow F'|_{ \operatorname{\mathcal{C}}^{0} }$ exhibit $F'$ as a left Kan extension of $F_0$ along the inclusion functor $\operatorname{\mathcal{C}}^{0} \hookrightarrow \operatorname{\mathcal{C}}$. Then $\beta $ is an isomorphism in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}^{0}, \operatorname{\mathcal{D}})$ (Corollary 7.3.1.16). Using Corollary 4.4.5.9, we can lift $\beta $ to an isomorphism $\widetilde{\beta }: F \rightarrow F'$ in the $\infty $-category $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$, where $F$ satisfies $F|_{ \operatorname{\mathcal{C}}^{0} } = F_0$. Applying Remark 7.3.1.12, we deduce that the identity transformation $\operatorname{id}_{F_0}$ exhibits $F$ as a left Kan extension of $F_0$ along the inclusion map $\operatorname{\mathcal{C}}^{0} \hookrightarrow \operatorname{\mathcal{C}}$. Invoking Proposition 7.3.2.6, we conclude that $F$ is left Kan extended from $\operatorname{\mathcal{C}}^{0}$. $\square$