Kerodon

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

Theorem 3.3.8.1. Let $f: X \rightarrow S$ be a Kan fibration between simplicial sets, and let $g: S \hookrightarrow S'$ be an anodyne map. Then there exists a pullback diagram of simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ X \ar [d]^{f} \ar [r] & X' \ar [d]^{f'} \\ S \ar [r]^-{g} & S', } \]

where $f'$ is a Kan fibration.

Proof of Theorem 3.3.8.1. Let $f: X \rightarrow S$ be a Kan fibration of simplicial sets. Let us abuse notation by identifying $X$ and $S$ with simplicial subsets of $Y = \operatorname{Ex}^{\infty }(X)$ and $T = \operatorname{Ex}^{\infty }(S)$, respectively (via the monomorphisms $\rho _{X}^{\infty }: X \hookrightarrow \operatorname{Ex}^{\infty }(X)$ and $\rho _{S}^{\infty }: S \hookrightarrow \operatorname{Ex}^{\infty }(S)$), and let $Y' \subseteq \operatorname{Ex}^{\infty }(X)$ be the simplicial subset defined in the statement of Lemma 3.3.8.4. Let $g: S \hookrightarrow S'$ be an anodyne morphism of simplicial sets. Since $\operatorname{Ex}^{\infty }(S)$ is a Kan complex (Proposition 3.3.6.9), the morphism $\rho ^{\infty }_{S}: S \rightarrow \operatorname{Ex}^{\infty }(S)$ extends to a map of simplicial sets $u: S' \rightarrow \operatorname{Ex}^{\infty }(S)$. Set $X' = S' \times _{ \operatorname{Ex}^{\infty }(S)} Y'$, so that we have a commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ X \ar [d]^{f} \ar [r] & X' \ar [d]^{f'} \ar [r] & Y' \ar [d] \\ S \ar [r]^-{g} & S' \ar [r]^-{u} & \operatorname{Ex}^{\infty }(S) } \]

where the right square and outer rectangle are pullback diagrams, so the left square is a pullback diagram as well. Since the projection map $Y' \rightarrow \operatorname{Ex}^{\infty }(S)$ is a Kan fibration (Lemma 3.3.8.4), it follows that $f'$ is also a Kan fibration. $\square$