Kerodon

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

Variant 4.6.6.10. 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.16 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.17, 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@R =50pt@C=50pt{ \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.11 and 4.3.6.1), and therefore isofibrations (Example 4.4.1.11). Using Propositions 4.5.2.26 and 4.5.2.18, we see that the upper square is a categorical pullback. Theorem 4.6.4.17 guarantees that $U$ is an equivalence of $\infty $-categories, so that $\iota $ is an equivalence of $\infty $-categories by virtue of Proposition 4.5.2.21. $\square$