Kerodon

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

Proposition 3.2.1.5. Let $(X,x)$ and $(Y,y)$ be pointed simplicial sets, and suppose we are given a pair of pointed morphisms $f,g: X_{} \rightarrow Y_{}$. Then:

  • The morphisms $f$ and $g$ are pointed homotopic if and only if there exists a sequence of pointed morphisms $f = f_0, f_1, \ldots , f_ n = g$ from $X_{}$ to $Y_{}$ having the property that, for each $1 \leq i \leq n$, either there exists a pointed homotopy from $f_{i-1}$ to $f_{i}$ or a pointed homotopy from $f_{i}$ to $f_{i-1}$.

  • Suppose that $Y_{}$ is a Kan complex. Then $f$ and $g$ are pointed homotopic if and only if there exists a pointed homotopy from $f$ to $g$.

Proof. The first assertion follows by applying Remark 1.1.6.23 to the simplicial set

\[ \operatorname{Fun}( X, Y ) \times _{ \operatorname{Fun}( \{ x\} , Y) } \{ y\} . \]

If $Y_{}$ is a Kan complex, then the evaluation map $\operatorname{Fun}(X,Y) \rightarrow \operatorname{Fun}( \{ x\} , Y)$ is a Kan fibration (Corollary 3.1.3.3), so the fiber $\operatorname{Fun}(X,Y) \times _{ \operatorname{Fun}( \{ x\} , Y) } \{ y\} $ is a Kan complex (Remark 3.1.1.7). The second assertion now follows from Proposition 1.1.9.10. $\square$