# Kerodon

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

Variant 4.6.4.24. 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.10). Using Propositions 4.5.2.20 and 4.5.2.16, 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.19. $\square$