# Kerodon

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

Proposition 5.2.1.3. Let $q: X \rightarrow S$ be an inner fibration of simplicial sets and let $Y \subseteq \operatorname{Fun}( \Delta ^1, X)$ be the full simplicial subset of $\operatorname{Fun}( \Delta ^1, X)$ spanned by those edges $e: \Delta ^1 \rightarrow X$ which are $q$-cartesian (see Definition 4.1.2.17). Let $\theta : Y \rightarrow \operatorname{Fun}( \Delta ^1, S) \times _{ \operatorname{Fun}( \{ 1\} , S) } \operatorname{Fun}( \{ 1\} , X)$ denote the restriction map, and let $Z \subseteq \operatorname{Fun}( \Delta ^1, S) \times _{ \operatorname{Fun}(\{ 1\} , S) } \operatorname{Fun}(\{ 1\} , X)$ be the full simplicial subset spanned by those vertices which belong to the image of $\theta$. Then $\theta : Y \rightarrow Z$ is a trivial Kan fibration of simplicial sets.

Proof of Proposition 5.2.1.3. Let $n > 0$ be an integer; we wish to show that every lifting problem of the form

5.11
\begin{equation} \label{equation:lifting-problem-for-cartesian-lift-uniqueness} \xymatrix@R =50pt@C=50pt{ \operatorname{\partial \Delta }^ n \ar [r] \ar [d] & Y \ar [d]^-{\theta } \\ \Delta ^ n \ar [r] \ar@ {-->}[r] & \operatorname{Fun}( \Delta ^1, S) \times _{ \operatorname{Fun}( \{ 1\} , S) } \operatorname{Fun}( \{ 1\} , X) } \end{equation}

admits a solution. Unwinding the definitions, we can rephrase (5.11) as a lifting problem

$\xymatrix@R =50pt@C=75pt{ (\Delta ^1 \times \operatorname{\partial \Delta }^ n) \coprod _{ (\{ 1\} \times \operatorname{\partial \Delta }^ n)} (\{ 1\} \times \Delta ^ n) \ar [r]^-{h_0} \ar [d] & X \ar [d]^-{q} \\ \Delta ^1 \times \Delta ^ n \ar [r]^-{\overline{h}} \ar@ {-->}[ur]^{h} & S, }$

where the morphism $h_0$ has the property that $h_0|_{ \Delta ^1 \times \{ i\} }$ is a $q$-cartesian edge of $X$ for $0 \leq i \leq n$. Let

$(\Delta ^1 \times \operatorname{\partial \Delta }^ n) \cup (\{ 1\} \times \Delta ^ n) = Y(0) \subset Y(1) \subset X(2) \subset \cdots \subset Y(n+1) = \Delta ^{1} \times \Delta ^ n$

be the sequence of simplicial subsets appearing in the proof of Lemma 3.1.2.11, so that $h_0$ can be identified with a morphism of simplicial sets from $Y(0)$ to $X$. We will show that, for $0 \leq j \leq n+1$, there exists a morphism of simplicial sets $h_ j: Y(j) \rightarrow X$ satisfying $h_ j|_{Y(0)} = h_0$ and $q \circ h_ j = \overline{h}|_{ Y(j)}$ (taking $j = n+1$, this will complete the proof of Proposition 5.2.1.3). We proceed by induction on $j$, the case $j=0$ being vacuous. Assume that $j > 0$ and that we have already constructed a morphism $h_{j-1}: Y(j-1) \rightarrow X$ satisfying $h_{j-1}|_{Y(0)} = h_0$ and $q \circ h_{j-1} = \overline{h}|_{ Y(j-1)}$. By virtue of Lemma 3.1.2.11, we have a pushout diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ \Lambda ^{n+1}_{j} \ar [r]^-{\sigma _0} \ar [d] & Y(j-1) \ar [d] \\ \Delta ^{n+1} \ar [r]^-{\sigma } & Y(j). }$

Consequently, to prove the existence of $h_{i}$, it suffices to solve the lifting problem

$\xymatrix@R =50pt@C=50pt{ \Lambda ^{n+1}_{j} \ar [r]^-{ h_{j-1} \circ \sigma _0} \ar [d] & X \ar [d]^-{q} \\ \Delta ^{n+1} \ar [r]^-{ \overline{h} \circ \sigma } \ar@ {-->}[ur] & S. }$

For $0 < j < n+1$, the existence of the desired solution follows from our assumption that $q$ is an inner fibration. In the case $j = n+1$, the existence follows from the fact that the composite map

$\Delta ^1 \simeq \operatorname{N}_{\bullet }( \{ n < n+1 \} ) \hookrightarrow \Lambda ^{n+1}_{j} \xrightarrow { \sigma _0} Y(n) \xrightarrow { h_ n} X$

is the edge of $X$ given by the restriction $h_0|_{ \Delta ^1 \times \{ n\} }$, and is therefore $q$-cartesian. $\square$