# Kerodon

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

Lemma 5.4.6.8. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be an equivalence of $\infty$-categories. If $\operatorname{\mathcal{C}}$ is minimal, then $F$ is a monomorphism of simplicial sets.

Proof. Let $\sigma , \sigma ': \Delta ^ n \rightarrow \operatorname{\mathcal{C}}$ be $n$-simplices of $\operatorname{\mathcal{C}}$ satisfying $F(\sigma ) = F(\sigma ')$; we wish to show that $\sigma = \sigma '$. Our proof proceeds by induction on $n$. Set $\tau = F(\sigma ) = F(\sigma ')$ and $\sigma _0 = \sigma |_{ \operatorname{\partial \Delta }^ n }$, so that our inductive hypothesis guarantees that $\sigma _0 = \sigma '|_{ \operatorname{\partial \Delta }^ n}$.

Fix a functor $G: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ which is homotopy inverse to $F$, so that there exists a $2$-simplex

$\xymatrix@R =50pt@C=50pt{ \operatorname{id}_{ \operatorname{\mathcal{C}}} \ar [rr]^-{ \operatorname{id}} \ar [dr]_{\alpha } & & \operatorname{id}_{ \operatorname{\mathcal{C}}} \\ & G \circ F \ar [ur]_{\beta } & }$

in the $\infty$-category $\operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{C}})$, where $\alpha$ and $\beta$ are (mutually inverse) isomorphisms. Precomposing with the morphism $\sigma _0: \operatorname{\partial \Delta }^ n \rightarrow \operatorname{\mathcal{C}}$, we obtain a $2$-simplex

5.35
$$\begin{gathered}\label{equation:minimal-is-mono} \xymatrix@R =50pt@C=50pt{ \sigma _0 \ar [rr]^-{ \operatorname{id}} \ar [dr]_{\alpha (\sigma _0)} & & \sigma _0 \\ & (G \circ F)(\sigma _0) \ar [ur]_{\beta (\sigma _0)} & } \end{gathered}$$

in the $\infty$-category $\operatorname{Fun}( \operatorname{\partial \Delta }^ n, \operatorname{\mathcal{C}})$. Since $\operatorname{\mathcal{C}}$ is an $\infty$-category, Theorem 1.4.6.1 guarantees that we can lift (5.35) to a $2$-simplex

$\xymatrix@R =50pt@C=50pt{ \sigma \ar [rr]^-{ \gamma } \ar [dr]_{\alpha (\sigma )} & & \sigma ' \\ & G(\tau ). \ar [ur]_{\beta (\sigma ')} & }$

in the $\infty$-category $\operatorname{Fun}( \Delta ^ n, \operatorname{\mathcal{C}})$. By construction, $\gamma$ is an isomorphism whose image in $\operatorname{Fun}( \operatorname{\partial \Delta }^ n, \operatorname{\mathcal{C}})$ is an identity morphism. Invoking our assumption that $\operatorname{\mathcal{C}}$ is minimal, we deduce that $\sigma = \sigma '$. $\square$