# Kerodon

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

Corollary 3.4.5.8. Let $X$ and $Y$ be simplicial sets and let $f: X \rightarrow Y$ be a morphism of semisimplicial sets. Then $f$ is a weak homotopy equivalence of semisimplicial sets if and only if the induced map $\operatorname{Ex}(f): \operatorname{Ex}(X) \rightarrow \operatorname{Ex}(Y)$ is a weak homotopy equivalence of semisimplicial sets.

Proof. By definition, $f: X \rightarrow Y$ is a weak homotopy equivalence of semisimplicial sets if and only if the induced map $f^{+}: X^{+} \rightarrow Y^{+}$ is a weak homotopy equivalence of simplicial sets. By virtue of Corollary 3.3.5.2, this is equivalent to the assertion that $\operatorname{Ex}(f^{+}): \operatorname{Ex}(X^{+} ) \rightarrow \operatorname{Ex}(Y^{+} )$ is a weak homotopy equivalence when viewed as a morphism of simplicial sets, or equivalently when viewed as a morphism of semisimplicial sets (Corollary 3.4.5.5). The desired result now follows by inspecting the commutative diagram of semisimplicial sets

$\xymatrix@R =50pt@C=50pt{ \operatorname{Ex}(X) \ar [r]^-{ \operatorname{Ex}(f) } \ar [d] & \operatorname{Ex}(Y) \ar [d] \\ \operatorname{Ex}(X^{+} ) \ar [r]^-{ \operatorname{Ex}(f^{+} )} & \operatorname{Ex}(Y^{+} ), }$

since the vertical maps are weak homotopy equivalences by virtue of Variant 3.4.5.7. $\square$