Kerodon

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

Proposition 5.1.4.11. 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. & } \]

Let $q: Z \rightarrow S$ be a morphism of simplicial sets and let $\theta : \operatorname{Fun}_{/S}(Y,Z) \rightarrow \operatorname{Fun}_{/S}(X,Z)$ be the morphism given by precomposition with $f$. If $f$ is a covariant equivalence relative to $S$ and $q$ is a left fibration, then $\theta $ is homotopy equivalence. Similarly, if $f$ is a contravariant equivalence relative to $S$ and $q$ is a right fibration, then $\theta $ is a homotopy equivalence.

Proof. We will prove the first assertion; the second follows from the same argument. We will prove that $\theta $ is a homotopy equivalence by showing that, for every simplicial set $K$, the induced map $\theta _{K}: \pi _0( \operatorname{Fun}(K, \operatorname{Fun}_{/S}(Y,Z) ) \rightarrow \pi _0( \operatorname{Fun}(K, \operatorname{Fun}_{/S}(X,Z) )$ is a bijection. Form a pullback diagram of simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ Z' \ar [r] \ar [d]^{q'} & \operatorname{Fun}(K,Z) \ar [d]^{ \circ q} \\ S \ar [r] & \operatorname{Fun}(K,S). } \]

The assumption that $q$ is a left fibration guarantees that the right vertical map is also a left fibration (Corollary 4.2.3.2), so that $q': Z' \rightarrow S$ is also a left fibration. Unwinding the definitions, we see that $\theta _{K}$ can be identified with the map $\pi _0( \operatorname{Fun}_{/S}(Y, Z') ) \xrightarrow {\circ f} \pi _0( \operatorname{Fun}_{/S}(X, Z') )$, and is therefore bijective by virtue of our assumption that $f$ is a covariant equivalence relative to $S$. $\square$