Kerodon

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

Corollary 7.3.8.9. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ and $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ be functors of $\infty $-categories, let $\operatorname{\mathcal{C}}^{0} \subseteq \operatorname{\mathcal{C}}$ be a full subcategory, and let $C,C' \in \operatorname{\mathcal{C}}$ be objects which are isomorphic. If $F$ is $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0}$ at $C$, then it is $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0}$ at $C'$.

Proof. Let $\operatorname{\mathcal{C}}^{1} \subseteq \operatorname{\mathcal{C}}$ be the full subcategory spanned by the objects of $\operatorname{\mathcal{C}}^{0}$ together with the object $C$, and let $\operatorname{\mathcal{C}}^{2} \subseteq \operatorname{\mathcal{C}}$ be the full subcategory spanned by the objects of $\operatorname{\mathcal{C}}$ together with the objects $C$ and $C'$. If $F$ is $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0}$ at $C$, then the functor $F|_{ \operatorname{\mathcal{C}}^{1}}$ is $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0}$. Since every object of $\operatorname{\mathcal{C}}^{2}$ is isomorphic to an object of $\operatorname{\mathcal{C}}^{1}$. the functor $F|_{ \operatorname{\mathcal{C}}^{2} }$ is automatically $U$-left Kan extended from $\operatorname{\mathcal{C}}^{1}$ (Proposition 7.3.3.7). Applying Proposition 7.3.8.6, we see that $F|_{ \operatorname{\mathcal{C}}^{2} }$ is also $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0}$. In particular, $F$ is $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0}$ at the object $C' \in \operatorname{\mathcal{C}}^{2}$. $\square$