Proposition 11.10.7.16 (01B5)

Proposition 11.10.7.16. Suppose we given a commutative diagram of simplicial sets

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

where $S$ is a Kan complex. The following conditions are equivalent:

$(1)$: The morphism $f$ is a covariant equivalence relative to $S$.
$(2)$: The morphism $f$ is a contravariant equivalence relative to $S$.
$(3)$: The morphism $f$ is a weak homotopy equivalence.

Proof. The implications $(1) \Rightarrow (3)$ and $(2) \Rightarrow (3)$ follow from Remark 11.10.7.8 (and do not require the assumption that $S$ is a Kan complex). We will complete the proof by establishing the implication $(3) \Rightarrow (1)$ (the proof of the implication $(3) \Rightarrow (2)$ is similar). Assume that $f$ is a weak homotopy equivalence and let $q: Z \rightarrow S$ be a left fibration; we wish to show that the induced map $\theta : \operatorname{Fun}_{/S}(Y,Z) \rightarrow \operatorname{Fun}_{/S}(X,Z)$ is bijective on connected components. Our assumption that $S$ is a Kan complex guarantees that $q$ is a Kan fibration (Corollary 4.4.3.8), so that $Z$ is also a Kan complex. Consider the diagram of simplicial sets

11.22

\begin{equation} \begin{gathered}\label{equation:covariant-equivalence-over-Kan} \xymatrix@C =50pt@R=50pt{ \operatorname{Fun}(Y,Z) \ar [r]^-{\circ f} \ar [d]^{q \circ } & \operatorname{Fun}(X,Z) \ar [d]^{q \circ } \\ \operatorname{Fun}(Y,S) \ar [r]^-{\circ f} & \operatorname{Fun}(X,S). } \end{gathered} \end{equation}

Our assumption that $f$ is a weak homotopy equivalence guarantees that the horizontal maps in this diagram are homotopy equivalences (Corollary 11.6.0.66), so that diagram (11.22) is a homotopy Cartesian (Corollary 3.4.1.5). Corollary 3.1.3.2 guarantees that the vertical maps in the diagram (11.22) are Kan fibrations. Invoking Example 3.4.1.4, we conclude that the induced map

\[ \theta : \operatorname{Fun}_{/S}(Y,Z) = \{ q_ Y \} \times _{ \operatorname{Fun}(Y,S)} \operatorname{Fun}(Y,Z) \rightarrow \{ q_ X \} \times _{ \operatorname{Fun}(X,S) } \operatorname{Fun}(X,Z) = \operatorname{Fun}_{/S}(X,Z) \]

is also a homotopy equivalence, and is therefore bijective on connected components. $\square$