Kerodon

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

Proposition 7.3.1.15 (Change of Diagram). Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty $-categories, let $\delta : K \rightarrow \operatorname{\mathcal{C}}$ and $F_0: K \rightarrow \operatorname{\mathcal{D}}$ be diagrams, and let $\epsilon : K' \rightarrow K$ be a categorical equivalence of simplicial sets. Then:

$(1)$

A natural transformation $\alpha : F \circ \delta \rightarrow F_0$ exhibits $F$ as a right Kan extension of $F_0$ along $\delta $ if and only if the induced transformation $\alpha ': F \circ (\delta \circ \epsilon ) \rightarrow F_0 \circ \epsilon $ exhibits $F$ as a right Kan extension of $F_0 \circ \epsilon $ along $\delta \circ \epsilon $.

$(2)$

A natural transformation $\beta : F_0 \rightarrow F \circ \delta $ exhibits $F$ as a left Kan extension of $F_0$ along $\delta $ if and only if the induced transformation $\beta ': F_0 \circ \epsilon \rightarrow F \circ (\delta \circ \epsilon )$ exhibits $F$ as a left Kan extension of $F_0 \circ \epsilon $ along $\delta \circ \epsilon $.

Proof. We will prove $(1)$; the proof of $(2)$ is similar. Fix an object $C \in \operatorname{\mathcal{C}}$. Since $\epsilon $ is a categorical equivalence and the projection map $\operatorname{\mathcal{C}}_{C/} \rightarrow \operatorname{\mathcal{C}}$ is a left fibration (Proposition 4.3.6.1), it follows that the induced map $\epsilon _{C/}: K' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{C/} \rightarrow K \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{C/}$ is also a categorical equivalence of simplicial sets (Corollary 5.6.7.6). In particular, $\epsilon _{C/}$ is left cofinal (Corollary 7.2.1.13). Applying Corollary 7.2.2.3, we see that the natural transformation $\alpha $ satisfies condition $(\ast _ C)$ of Definition 7.3.1.2 if and only if $\alpha '$ satisfies condition $(\ast _ C)$. The desired result now follows by allowing the object $C \in \operatorname{\mathcal{C}}$ to vary. $\square$