# Kerodon

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

Lemma 5.2.4.12. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}'$ be an inner fibration of simplicial sets. Then the induced map

$\Delta ^1 \times \operatorname{\mathcal{E}}= \operatorname{\mathcal{E}}\star _{\operatorname{\mathcal{E}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}\star _{\operatorname{\mathcal{E}}'} \operatorname{\mathcal{E}}$

is also an inner fibration of simplicial sets.

Proof. Suppose we are given integers $0 < i < n$; we wish to show that every lifting problem

5.18
\begin{equation} \begin{gathered}\label{equation:inner-fibration-silliness} \xymatrix@R =50pt@C=50pt{ \Lambda ^{n}_{i} \ar [r]^-{ \sigma _0 } \ar [d] & \Delta ^1 \times \operatorname{\mathcal{E}}\ar [d] \\ \Delta ^ n \ar@ {-->}[ur]^{\sigma } \ar [r]^-{ \overline{\sigma } } & \operatorname{\mathcal{E}}\star _{\operatorname{\mathcal{E}}'} \operatorname{\mathcal{E}}} \end{gathered} \end{equation}

admits a solution. Let $\alpha$ denote the composite map

$\Delta ^ n \xrightarrow { \overline{\sigma } } \operatorname{\mathcal{E}}\star _{\operatorname{\mathcal{E}}'} \operatorname{\mathcal{E}}\rightarrow \Delta ^0 \star _{\Delta ^0} \Delta ^0 \simeq \Delta ^1.$

If $\alpha$ is a constant morphism, then the existence of $\sigma$ is immediate. We may therefore assume without loss of generality that $\alpha$ is not constant. Write $\sigma _0 = (\alpha _0, \tau _0)$, where $\alpha _0 = \alpha |_{ \Lambda ^{n}_{i} }$ and $\tau _0: \Lambda ^{n}_{i} \rightarrow \operatorname{\mathcal{E}}$ is a morphism of simplicial sets, and let $\overline{\tau }$ denote the composite map $\Delta ^ n \xrightarrow { \overline{\sigma } } \operatorname{\mathcal{E}}\star _{\operatorname{\mathcal{E}}'} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}'$. Since $F$ is an inner fibration, the lifting problem

$\xymatrix { \Lambda ^{n}_{i} \ar [r]^{ \tau _0 } \ar [d] & \operatorname{\mathcal{E}}\ar [d]^{U} \\ \Delta ^ n \ar [r]^{ \overline{\tau } } \ar@ {-->}[ur]^{ \tau } & \operatorname{\mathcal{E}}' }$

admits a solution. We now observe that the pair $\sigma = (\alpha , \tau )$ can be regarded as an $n$-simplex of $\Delta ^1 \times \operatorname{\mathcal{E}}$ which solves the lifting problem (5.18). $\square$