Kerodon

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

Proposition 8.1.2.5. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category. For every object $X \in \operatorname{\mathcal{C}}$, the coslice inclusion

\[ \iota _{X}: \operatorname{\mathcal{C}}_{X/} \hookrightarrow \{ X\} \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \]

is an equivalence of $\infty $-categories.

Proof. By construction, we have a commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}_{X/} \ar [rr]^-{ \iota _{X} } \ar [dr] & & \{ X\} \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \ar [dl]^-{ \lambda _{+} } \\ & \operatorname{\mathcal{C}}, & } \]

where the vertical maps are left fibrations of $\infty $-categories (Propositions 4.3.6.1 and 8.1.1.10). Moreover, the $\infty $-category $\operatorname{\mathcal{C}}_{X/}$ has an initial object $\widetilde{X}$, given by the identity morphism $\operatorname{id}_{X}: X \rightarrow X$ (Proposition 4.6.6.23). Proposition 8.1.2.1 guarantees that $\iota _{X}( \widetilde{X} )$ is an initial object of the $\infty $-category $\{ X\} \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}})$, so that $\iota _{X}$ is an equivalence of $\infty $-categories by virtue of Corollary 5.7.6.20. $\square$