Kerodon

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

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.13). 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$