Kerodon

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

Corollary 4.5.3.13. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, and let $\operatorname{Isom}(\operatorname{\mathcal{C}})$ denote the full subcategory of $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}})$ spanned by the isomorphisms of $\operatorname{\mathcal{C}}$ (Example 4.4.1.14). Then the diagonal embedding

\[ \delta : \operatorname{\mathcal{C}}\hookrightarrow \operatorname{Isom}(\operatorname{\mathcal{C}}) \quad \quad C \mapsto \operatorname{id}_{C} \]

is an equivalence of $\infty $-categories.

Proof. Let $\operatorname{ev}_{0}: \operatorname{Isom}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}$ denote the evaluation map

\[ \operatorname{Isom}(\operatorname{\mathcal{C}}) \hookrightarrow \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}( \{ 0\} , \operatorname{\mathcal{C}}) \simeq \operatorname{\mathcal{C}}. \]

Then $\operatorname{ev}_0 \circ \delta $ is the identity functor $\operatorname{id}_{\operatorname{\mathcal{C}}}$. Corollary 4.4.5.10 guarantees that $\operatorname{ev}_0$ is a trivial Kan fibration, and therefore an equivalence of $\infty $-categories (Corollary 4.5.3.12). Applying the two-out-of-three property (Remark 4.5.1.18), we conclude that $\delta $ is also an equivalence of $\infty $-categories. $\square$