# Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$

Proposition 3.2.6.8. Let $f: X \rightarrow S$ be a Kan fibration of simplicial sets. The following conditions are equivalent:

$(1)$

The morphism $f$ is a trivial Kan fibration.

$(2)$

For each vertex $s \in S$, the fiber $X_{s} = \{ s\} \times _{S} X$ is a contractible Kan complex.

$(3)$

For each vertex $s \in S$, the fiber $X_{s} = \{ s\} \times _{S} X$ is connected. Moreover, for each vertex $x \in X_{s}$, the homotopy groups $\pi _{n}(X_ s, x)$ vanish for $n > 0$.

Proof. The implication $(1) \Rightarrow (2)$ and the equivalence $(2) \Leftrightarrow (3)$ follow by applying Proposition 3.2.6.7 to the fibers of $f$. We will complete the proof by showing that $(2)$ implies $(1)$. Assume that $(2)$ is satisfied; we wish to show that every lifting problem

$\xymatrix@R =50pt@C=50pt{ \operatorname{\partial \Delta }^ n \ar [r]^-{\sigma _0} \ar [d] & X \ar [d]^{f} \\ \Delta ^ n \ar@ {-->}[ur]^{\sigma } \ar [r]^-{ \overline{\sigma } } & S }$

admits a solution. Let $q: \Delta ^1 \times \Delta ^ n \rightarrow \Delta ^ n$ be the map given on vertices by the formula $q(i,j) = \begin{cases} j & \text{ if } i = 0 \\ n & \text{ if } i = 1. \end{cases}$ Then we can regard $\overline{\sigma } \circ q$ as a homotopy from $\overline{\sigma }: \Delta ^ n \rightarrow S$ to the constant map $\Delta ^ n \rightarrow \{ s\} \subseteq S$, where $s$ denotes the vertex $\overline{\sigma }(n) \in S$. Since $f$ is a Kan fibration, the restriction $(\overline{\sigma } \circ q)|_{ \Delta ^1 \times \operatorname{\partial \Delta }^ n}$ can be lifted to a homotopy $h: \Delta ^1 \times \operatorname{\partial \Delta }^ n \rightarrow X$ from $\sigma _0$ to some map $\sigma '_0: \operatorname{\partial \Delta }^ n \rightarrow X_{s}$ (Remark 3.1.4.3). It follows from assumption $(2)$ that we can extend $\sigma '_0$ to an $n$-simplex $\sigma ': \Delta ^{n} \rightarrow X_{s}$. Invoking our assumption that $f$ is a Kan fibration again, we see that $h$ can be extended to a homotopy $\widetilde{h}: \Delta ^1 \times \Delta ^ n \rightarrow X$ from $\sigma$ to $\sigma '$, where $\sigma : \Delta ^ n \rightarrow X$ is an extension of $\sigma _0$ satisfying $f( \sigma ) = \overline{\sigma }$. $\square$