# Kerodon

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

Theorem 4.6.5.14. Let $\operatorname{\mathcal{C}}$ be an $\infty$-category and let $X$ be an object of $\operatorname{\mathcal{C}}$. Then the pinch inclusion maps

$\iota ^{\mathrm{L}}_{X}: \operatorname{\mathcal{C}}_{X/} \hookrightarrow (X \downarrow \operatorname{\mathcal{C}}) \quad \quad \iota ^{\mathrm{R}}_{X}: \operatorname{\mathcal{C}}_{/X} \hookrightarrow (\operatorname{\mathcal{C}}\downarrow X)$

are equivalences of $\infty$-categories.

Proof of Theorem 4.6.5.14. Let $\operatorname{\mathcal{C}}$ be an $\infty$-category containing an object $X$. We will show that the left-pinch inclusion morphism $\iota ^{\mathrm{L}}_{X}: \operatorname{\mathcal{C}}_{X/} \hookrightarrow (X \downarrow \operatorname{\mathcal{C}})$ is an equivalence of $\infty$-categories; the analogous statement for $\iota ^{\mathrm{R}}_{X}$ follows by a similar argument. Let $K$ be a simplicial set and

$\rho : \pi _0( \operatorname{Fun}(K, \operatorname{\mathcal{C}}_{X/})^{\simeq } ) \rightarrow \pi _0( \operatorname{Fun}(K, X \downarrow \operatorname{\mathcal{C}})^{\simeq } )$

be the map induced by composition with $\iota ^{\mathrm{L}}_{X}$; we wish to show that $\rho$ is a bijection. Using Lemma 4.6.5.15 and Remark 4.6.5.8, we can identify $\rho$ with the map

$\pi _0( \operatorname{Fun}_{\{ x\} / }( \{ x\} \star K, \operatorname{\mathcal{C}})^{\simeq } ) \rightarrow \pi _0( \operatorname{Fun}_{ \{ x\} }( \{ x\} \diamond K, \operatorname{\mathcal{C}})^{\simeq } )$

given by composition with the comparison map $c: \{ x\} \diamond K \rightarrow \{ x\} \star K$. We will complete the proof by showing that composition with $c$ induces an equivalence of $\infty$-categories $\operatorname{Fun}_{ \{ x\} / }( \{ x\} \star K, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}_{ \{ x\} }( \{ x\} \diamond K, \operatorname{\mathcal{C}})$. This follows by applying Corollary 4.5.4.4 to the commutative diagram

$\xymatrix@R =50pt@C=50pt{ \operatorname{Fun}( \{ x\} \star K, \operatorname{\mathcal{C}}) \ar [r]^-{\circ c} \ar [d] & \operatorname{Fun}( \{ x\} \diamond K, \operatorname{\mathcal{C}}) \ar [d] \\ \operatorname{Fun}( \{ x\} , \operatorname{\mathcal{C}}) \ar@ {=}[r] & \operatorname{Fun}( \{ x\} , \operatorname{\mathcal{C}}); }$

here the vertical maps are isofibrations (Corollary 4.4.5.3) and the upper horizontal map is an equivalence of $\infty$-categories by Proposition 4.5.2.8 (and the fact that $c$ is a categorical equivalence, by Theorem 4.5.5.7). $\square$