Kerodon

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

Proposition 7.3.3.18 (Change of Source). Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ and $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ be functors of $\infty $-categories and let $\operatorname{\mathcal{C}}^{0} \subseteq \operatorname{\mathcal{C}}$ be a replete full subcategory. Let $G: \operatorname{\mathcal{B}}\rightarrow \operatorname{\mathcal{C}}$ be an equivalence of $\infty $-categories, and set $\operatorname{\mathcal{B}}^{0} = \operatorname{\mathcal{C}}^{0} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{B}}$. Then $F$ is $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0}$ if and only if $F \circ G$ is $U$-left Kan extended from $\operatorname{\mathcal{B}}^{0}$.

Proof. Assume first that $F$ is $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0}$; we will show that $F \circ G$ is $U$-left Kan extended from $\operatorname{\mathcal{B}}^{0}$. Fix an object $B \in \operatorname{\mathcal{B}}$ and set $\operatorname{\mathcal{B}}^{0}_{/B} = \operatorname{\mathcal{B}}^{0} \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{B}}_{/B}$; we wish to show that the composite map

\[ \theta : ( \operatorname{\mathcal{B}}^{0}_{/B} )^{\triangleright } \hookrightarrow \operatorname{\mathcal{B}}_{/B}^{\triangleright } \rightarrow \operatorname{\mathcal{B}}\xrightarrow { F \circ G} \operatorname{\mathcal{D}} \]

is a $U$-colimit diagram. Set $C = G(B)$ and $\operatorname{\mathcal{C}}^0_{/C} = \operatorname{\mathcal{C}}^{0} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}^{0}$. Since $G$ is an equivalence of $\infty $-categories, the induced map $G_{/B}: \operatorname{\mathcal{B}}_{/B} \rightarrow \operatorname{\mathcal{C}}_{/C}$ is also an equivalence of $\infty $-categories (Corollary 4.6.4.19). Our assumption that $\operatorname{\mathcal{C}}^{0}$ is a replete subcategory of $\operatorname{\mathcal{C}}$ guarantees that $\operatorname{\mathcal{C}}_{/C}^{0}$ is a replete subcategory of $\operatorname{\mathcal{C}}_{/C}$. In particular, the inclusion map $\operatorname{\mathcal{C}}_{/C}^{0} \hookrightarrow \operatorname{\mathcal{C}}_{/C}$ is an isofibration, so that $G_{/B}$ restricts to an equivalence of $\infty $-categories $G_{/B}^{0}: \operatorname{\mathcal{B}}_{/B}^{0} \rightarrow \operatorname{\mathcal{C}}_{/C}^{0}$. By construction, the morphism $\theta $ is the composition of $(G_{/B}^{0})^{\triangleright }$ with the map

\[ \theta ': ( \operatorname{\mathcal{C}}^{0}_{/C} )^{\triangleright } \hookrightarrow \operatorname{\mathcal{C}}_{/C}^{\triangleright } \rightarrow \operatorname{\mathcal{C}}\xrightarrow {F} \operatorname{\mathcal{D}}, \]

which is a $U$-colimit diagram by virtue of our assumption that $F$ is $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0}$. Applying Corollary 7.2.2.2, we deduce that $\theta $ is also a $U$-colimit diagram.

We now prove the converse. Assume that $F \circ G$ is $U$-left Kan extended from $\operatorname{\mathcal{B}}^{0}$; we wish to show that $F$ is $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0}$. Let $H: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{B}}$ be a homotopy inverse to $G$, so that $(G \circ H): \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}$ is isomorphic to the identity functor $\operatorname{id}_{\operatorname{\mathcal{C}}}$. Since $\operatorname{\mathcal{C}}^{0} \subseteq \operatorname{\mathcal{C}}$ is replete, it coincides with the inverse image $(G \circ H)^{-1} \operatorname{\mathcal{C}}^{0} = H^{-1} \operatorname{\mathcal{B}}^{0}$. Applying the first part of the proof, we deduce that the functor $(F \circ G \circ H): \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ is $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0}$. The functor $F$ is isomorphic to $F \circ G \circ H$, and is therefore also $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0}$ (Remark 7.3.3.17). $\square$