Proposition 7.3.7.13 (0488)

Proposition 7.3.7.13. 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 $\operatorname{\mathcal{K}}$ be an $\infty $-category and let $f: \operatorname{\mathcal{K}}^{\triangleright } \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}})$ be a functor, corresponding to a morphism $\operatorname{\mathcal{K}}^{\triangleright } \rightarrow \operatorname{\mathcal{B}}$ and a functor $F: \operatorname{\mathcal{K}}^{\triangleleft } \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$. If $F$ is $V$-left Kan extended from $\operatorname{\mathcal{K}}\times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}$, then $f$ is a $V'$-colimit diagram.

Proof. Without loss of generality, we may assume that $V$ is an isofibration, so that $V'$ is also an isofibration (Proposition 4.5.9.17). Fix a morphism $\overline{f}: \operatorname{\mathcal{K}}^{\triangleright } \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{E}})$, and let

\[ \operatorname{Fun}'_{ / \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{E}}) }( \operatorname{\mathcal{K}}^{\triangleright }, \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}}) ) \subseteq \operatorname{Fun}_{ / \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{E}}) }( \operatorname{\mathcal{K}}^{\triangleright }, \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}}) ) \]

denote the full subcategory spanned by those morphisms $\operatorname{\mathcal{K}}^{\triangleright } \rightarrow \operatorname{Fun}(\operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}})$ which correspond to functors $\operatorname{\mathcal{K}}^{\triangleleft } \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ which are $V$-left Kan extended from $\operatorname{\mathcal{K}}$, and let $\operatorname{Fun}'_{ / \operatorname{Fun}(\operatorname{\mathcal{C}}/\operatorname{\mathcal{B}},\operatorname{\mathcal{E}}) }( \operatorname{\mathcal{K}}, \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}}) )$ denote its essential image under the restriction map

\[ \operatorname{Fun}_{ / \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{E}}) }( \operatorname{\mathcal{K}}^{\triangleright }, \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}}) ) \rightarrow \operatorname{Fun}_{ / \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{E}}) }( \operatorname{\mathcal{K}}, \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}}) ). \]

We will complete the proof by showing that every object of $\operatorname{Fun}'_{ / \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{E}}) }( \operatorname{\mathcal{K}}^{\triangleright }, \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}}) )$ is a $V'$-colimit diagram in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}})$. By virtue of Remark 7.3.7.12, it will suffice to verify condition $(\ast _{\operatorname{\mathcal{A}}})$ of Lemma 7.3.7.10 for every $\infty $-category $\operatorname{\mathcal{A}}$.

Fix a morphism $\operatorname{\mathcal{K}}^{\triangleright } \star \operatorname{\mathcal{A}}\rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{E}})$ extending $\overline{f}$, which we identify with a diagram $\operatorname{\mathcal{K}}^{\triangleright } \star \operatorname{\mathcal{A}}\rightarrow \operatorname{\mathcal{B}}$ and a functor

\[ \overline{G}: (\operatorname{\mathcal{K}}^{\triangleright } \star \operatorname{\mathcal{A}}) \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{E}}. \]

Let $\operatorname{Fun}'_{ / \operatorname{\mathcal{E}}}( ( \operatorname{\mathcal{K}}^{\triangleright } \star \operatorname{\mathcal{A}}) \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ denote denote the full subcategory of $\operatorname{Fun}_{ / \operatorname{\mathcal{E}}}( (\operatorname{\mathcal{K}}^{\triangleright } \star \operatorname{\mathcal{A}}) \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ given by the inverse image of $\operatorname{Fun}'_{ / \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{E}}) }( \operatorname{\mathcal{K}}^{\triangleright }, \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}}) )$, and define $\operatorname{Fun}'_{ / \operatorname{\mathcal{E}}}( (\operatorname{\mathcal{K}}\star \operatorname{\mathcal{A}}) \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ similarly. We wish to show that the restriction map

\[ \theta : \operatorname{Fun}'_{ / \operatorname{\mathcal{E}}}( ( \operatorname{\mathcal{K}}^{\triangleright } \star \operatorname{\mathcal{A}}) \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}'_{ / \operatorname{\mathcal{E}}}( ( \operatorname{\mathcal{K}}\star \operatorname{\mathcal{A}}) \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \]

is an equivalence of $\infty $-categories. Unwinding the definitions (and using the existence criterion of Proposition 7.3.5.5), we see that a functor $G \in \operatorname{Fun}_{ / \operatorname{\mathcal{E}}}( (\operatorname{\mathcal{K}}^{\triangleright } \star \operatorname{\mathcal{A}}) \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ belongs to the subcategory $\operatorname{Fun}'_{ / \operatorname{\mathcal{E}}}( ( \operatorname{\mathcal{K}}^{\triangleright } \star \operatorname{\mathcal{A}}) \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ if and only if it is $V$-left Kan extended from $( \operatorname{\mathcal{K}}\star \operatorname{\mathcal{A}}) \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}$, and that a functor $G_0 \in \operatorname{Fun}_{ / \operatorname{\mathcal{E}}}( (\operatorname{\mathcal{K}}^{\triangleright } \star \operatorname{\mathcal{A}}) \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ belongs to $\operatorname{Fun}'_{ / \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{E}}) }( \operatorname{\mathcal{K}}^{\triangleright }, \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}}) )$ if and only if admits a left Kan extension $G: (\operatorname{\mathcal{K}}^{\triangleright } \star \operatorname{\mathcal{A}}) \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ satisfying $V \circ G = \overline{G}$. Applying Theorem 7.3.6.14, we conclude that $\theta $ is a trivial Kan fibration. $\square$