Kerodon

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

Variant 4.6.4.23. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $f: K \rightarrow \operatorname{\mathcal{C}}$ be a diagram, which we identify with an object $F$ of the $\infty $-category $\operatorname{Fun}(K, \operatorname{\mathcal{C}})$. Then the functors

\[ \operatorname{\mathcal{C}}_{/f} \rightarrow \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{Fun}(K, \operatorname{\mathcal{C}})_{/F} \quad \quad \operatorname{\mathcal{C}}_{f/} \rightarrow \operatorname{Fun}(K, \operatorname{\mathcal{C}})_{/F} \times _{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{\mathcal{C}} \]

of Exercise 4.6.4.15 are equivalences of $\infty $-categories.

Proof. We will show that the slice diagonal $\delta _{/f}$ induces an equivalence of $\infty $-categories $\operatorname{\mathcal{C}}_{/f} \rightarrow \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{Fun}(K, \operatorname{\mathcal{C}})_{/F}$; the analogous assertion for coslice $\infty $-categories follows by a similar argument. By virtue of Theorem 4.6.4.16, it will suffice to show that the inclusion map

\[ \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{Fun}(K, \operatorname{\mathcal{C}})_{/F} \hookrightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \{ F \} \]

is an equivalence of $\infty $-categories. By construction, this map fits into a commutative diagram of $\infty $-categories

\[ \xymatrix { \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{Fun}(K, \operatorname{\mathcal{C}})_{/F} \ar [r] \ar [d]^{\iota } & \operatorname{Fun}(K, \operatorname{\mathcal{C}})_{/F} \ar [d]^{U} \\ \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \{ F \} \ar [r] \ar [d] & \operatorname{Fun}(K, \operatorname{\mathcal{C}}) \operatorname{\vec{\times }}_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \{ F \} \ar [d]^{V} \\ \operatorname{\mathcal{C}}\ar [r] & \operatorname{Fun}(K, \operatorname{\mathcal{C}}), } \]

where the upper square and lower square are both pullback diagrams. Note that the morphisms $V$ and $V \circ U$ are both right fibrations (Propositions 4.6.4.10 and 4.3.6.1), and therefore isofibrations (Example 4.4.1.10). By virtue of Corollary 4.5.4.5, it will suffice to show that the morphism $U$ is an equivalence of $\infty $-categories, which is a special case of Theorem 4.6.4.16. $\square$