Kerodon

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

Proposition 3.1.6.23. Let $f: X \rightarrow Y$ and $f': X' \rightarrow Y'$ be weak homotopy equivalences of simplicial sets. Then the induced map $(f \times f'): X \times X' \rightarrow Y \times Y'$ is also a weak homotopy equivalence.

Proof. By virtue of Remark 3.1.6.16, it will suffice to show that the morphisms $f \times \operatorname{id}_{X'}$ and $\operatorname{id}_{Y} \times f'$ are weak homotopy equivalences. We will give the proof for $f \times \operatorname{id}_{X'}$; the analogous statement for $\operatorname{id}_{Y} \times f'$ follows by a similar argument. Let $Z$ be a Kan complex; we wish to show that precomposition with $f$ induces a bijection

\begin{eqnarray*} \pi _0( \operatorname{Fun}(X \times X', Z) ) & \simeq & \pi _0( \operatorname{Fun}(X, \operatorname{Fun}(X',Z) ) ) \\ & \rightarrow & \pi _0( \operatorname{Fun}(Y, \operatorname{Fun}(X',Z) ) ) \\ & \simeq & \pi _0( \operatorname{Fun}(Y \times X', Z ) ). \end{eqnarray*}

This follows from our assumption that $f$ is a weak homotopy equivalence, since the simplicial set $\operatorname{Fun}(X',Z)$ is a Kan complex (Corollary 3.1.3.4). $\square$