Kerodon

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

Theorem 7.3.7.1. Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{B}}$ be an exponentiable inner fibration of $\infty $-categories, let $V: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ be a functor of $\infty $-categories, and let $V': \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{E}})$ denote the functor given by postcomposition with $V$. Let $f: \operatorname{\mathcal{A}}\rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}})$ be a functor of $\infty $-categories, corresponding to a morphism $\operatorname{\mathcal{A}}\rightarrow \operatorname{\mathcal{B}}$ and a functor $F: \operatorname{\mathcal{A}}\times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$. Let $\operatorname{\mathcal{A}}^{0} \subseteq \operatorname{\mathcal{A}}$ be a full subcategory. If $F$ is $V$-left Kan extended from $\operatorname{\mathcal{A}}^{0} \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}$, then $f$ is $V'$-left Kan extended from $\operatorname{\mathcal{A}}^{0}$.

Proof of Theorem 7.3.7.1. Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{B}}$ be an inner fibration of $\infty $-categories, let $V: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ be a functor of $\infty $-categories, and let $V': \operatorname{Fun}(\operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{E}})$ be the functor given by postcomposition with $V'$. Suppose we are given a functor $f: \operatorname{\mathcal{A}}\rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}})$ and a full subcategory $\operatorname{\mathcal{A}}^{0} \subseteq \operatorname{\mathcal{A}}$. Assume that the induced map $F: \operatorname{\mathcal{A}}\times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ is $V$-left Kan extended from $\operatorname{\mathcal{A}}^{0} \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}$; we ish show that $f$ is $V'$-left Kan extended from $\operatorname{\mathcal{A}}^{0}$. Fix an object $A \in \operatorname{\mathcal{A}}$ and set $\operatorname{\mathcal{A}}^{0}_{/A} = \operatorname{\mathcal{A}}^{0} \times _{\operatorname{\mathcal{A}}} \operatorname{\mathcal{A}}_{/A}$; we wish to show that the composite map

\[ (\operatorname{\mathcal{A}}^{0}_{/A})^{\triangleright } \hookrightarrow (\operatorname{\mathcal{A}}_{/A})^{\triangleright } \rightarrow \operatorname{\mathcal{A}}\xrightarrow {f} \operatorname{Fun}(\operatorname{\mathcal{C}}/\operatorname{\mathcal{B}},\operatorname{\mathcal{D}}) \]

is a $V$-colimit diagram. Let $F_{A}$ denote the composition

\[ ( \operatorname{\mathcal{A}}^{0}_{/A})^{\triangleright } \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{A}}\times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}\xrightarrow {F} \operatorname{\mathcal{D}}. \]

By virtue of Proposition 7.3.7.13, it will suffice to show that $F_{A}$ is $V$-left Kan extended from $\operatorname{\mathcal{A}}^{0}_{/A} \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}$. Let $X$ denote the cone point of $(\operatorname{\mathcal{A}}^{0}_{/A})^{\triangleright }$, let $B$ denote its image in $\operatorname{\mathcal{B}}$, and let $C \in \operatorname{\mathcal{C}}$ be an object satisfying $U(C) = B$. Unwinding the definitions, we see that $F_{A}$ is $V$-left Kan extended from $\operatorname{\mathcal{A}}^{0}_{/A} \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}$ at the object $(X,C)$ if and only if the diagram

\[ (\operatorname{\mathcal{A}}^{0}_{/A} \times _{\operatorname{\mathcal{B}}_{/B} } \operatorname{\mathcal{C}}_{/C} )^{\triangleright } \rightarrow ( \operatorname{\mathcal{A}}^{0}_{/A} )^{\triangleright } \times _{ (\operatorname{\mathcal{B}}_{/B})^{\triangleright } } (\operatorname{\mathcal{C}}_{/C})^{\triangleright } \rightarrow \operatorname{\mathcal{A}}\times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}\xrightarrow {F} \operatorname{\mathcal{D}} \]

is a $V$-colimit diagram. This follows from our assumption that $F$ is $V$-left Kan extended from the full subcategory $\operatorname{\mathcal{A}}^{0} \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}$ at the object $(A,C)$. $\square$