Kerodon

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

Proposition 3.4.2.16. Suppose we are given a commutative diagram of simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ X \ar [rr]^{f} \ar [dr] & & Y \ar [dl] \\ & S & } \]

with the following property: for every simplex $\sigma : \Delta ^ k \rightarrow S$, the induced map $f_{\sigma }: \Delta ^ k \times _{S} X \rightarrow \Delta ^ k \times _{S} Y$ is a weak homotopy equivalence of simplicial sets. Then $f$ is a weak homotopy equivalence of simplicial sets.

Proof. We will prove the following stronger assertion: for every morphism of simplicial sets $S' \rightarrow S$, the induced map

\[ f_{S'}: S' \times _{S} X \rightarrow S' \times _{S} Y \]

is a weak homotopy equivalence of simplicial sets. By virtue of Proposition 3.2.8.3, (and Remark 1.1.4.4), we may assume without loss of generality that $S'$ has dimension $\leq k$ for some integer $k \geq -1$. We proceed by induction on $k$. In the case $k=-1$, the simplicial set $S'$ is empty and there is nothing to prove. Assume therefore that $k \geq 0$. Let $S''$ denote the $(k-1)$-skeleton of $S'$ and let $I$ be the set of nondegenerate $k$-simplices of $S'$, so that Proposition 1.1.4.12 supplies a pushout diagram of simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ \underset { i \in I }{\coprod } \operatorname{\partial \Delta }^{k} \ar [r] \ar [d] & \underset { i \in I }{\coprod } \Delta ^{k} \ar [d] \\ S'' \ar [r] & S', } \]

where the horizontal maps are monomorphisms. It follows that the front and back faces of the diagram

\[ \xymatrix@R =50pt@C=40pt{ (\underset { i \in I }{\coprod } \operatorname{\partial \Delta }^{k}) \times _{S} X \ar [rr] \ar [dd] \ar [dr]^{u} & & \underset { i \in I }{\coprod } (\Delta ^{k} \times _{S} X) \ar [dd] \ar [dr]^{v} & \\ & \underset { i \in I }{\coprod } (\operatorname{\partial \Delta }^{k} \times _{S} Y) \ar [dd] \ar [rr] & & \underset { i \in I }{\coprod } (\Delta ^{k} \times _{S} Y) \ar [dd] \\ S'' \times _{S} X \ar [rr] \ar [dr]^{f_{S''}} & & S' \times _{S} X \ar [dr]^{ f_{S'} } & \\ & S'' \times _{S} Y \ar [rr] & & S' \times _{S} Y } \]

are homotopy pushout squares (Proposition 3.4.2.11). Consequently, to show that $f_{S'}$ is a weak homotopy equivalence, it will suffice to show that $f_{S''}$, $u$, and $v$ are weak homotopy equivalences (Proposition 3.4.2.9). In the first two cases, this follows from our inductive hypothesis. We may therefore replace $S'$ by the coproduct $\coprod _{i \in I} \Delta ^{k}$, and thereby reduce to the case of a coproduct of simplices. Using Remark 3.1.6.20, we can further reduce to the case where $S' \simeq \Delta ^{k}$ is a standard simplex, in which case the desired result follows from our hypothesis on $f$. $\square$