Kerodon

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

Lemma 5.3.7.1. Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be an inner fibration of simplicial sets, let $e$ be an edge of $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}})$, and let

\[ V: \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) = \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}} \]

denote the morphism induced by $U$. Let $\operatorname{ev}_0, \operatorname{ev}_1: \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}$ be the evaluation maps. If $\operatorname{ev}_0(e)$ is $U$-cocartesian, then $e$ is $V$-cocartesian. If $\operatorname{ev}_1(e)$ is $U$-cartesian, then $e$ is $V$-cartesian.

Proof. Assume that $\operatorname{ev}_0(e)$ is $U$-cocartesian; we will show that $e$ is $V$-cocartesian (the second assertion follows by a similar argument). Let $n \geq 2$; we wish to show that every lifting problem

5.34
\begin{equation} \begin{gathered}\label{equation:cocartesian-in-oriented-fiber-product-ultimate} \xymatrix@R =50pt@C=50pt{ \Lambda ^{n}_{0} \ar [r]^-{ \sigma _0 } \ar [r] \ar [d] & \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) \ar [d]^-{ V } \\ \Delta ^{n} \ar [r]^-{ \overline{\sigma } } \ar@ {-->}[ur]^{\sigma } & \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}}} \end{gathered} \end{equation}

admits a solution, provided that the composite map

\[ \Delta ^1 \simeq \operatorname{N}_{\bullet }( \{ 0 < 1 \} ) \hookrightarrow \Lambda ^{n}_0 \xrightarrow { \tau _0 } \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) \]

coincides with $e$. Let $X(0)$ denote the simplicial subset of $\Delta ^1 \times \Delta ^ n$ given by the union of $\operatorname{\partial \Delta }^1 \times \Delta ^ n$ with $\Delta ^1 \times \Lambda ^{n}_0$. Unwinding the definitions, we can rewrite (5.34) as a lifting problem

\[ \xymatrix@R =50pt@C=50pt{ X(0) \ar [r]^-{ \tau _0 } \ar [r] \ar [d] & \operatorname{\mathcal{C}}\ar [d]^-{ U } \\ \Delta ^1 \times \Delta ^{n} \ar [r]^-{ \overline{\tau } } \ar@ {-->}[ur]^{\tau } & \operatorname{\mathcal{D}}. } \]

Choose a filtration

\[ X(0) \subset X(1) \subset X(2) \subset \cdots \subset X(t) = \Delta ^{1} \times \Delta ^{n} \]

satisfying the requirements of Lemma 4.4.4.7. We will complete the proof by showing that, for each $s \leq t$, the morphism $\tau _0$ admits an extension $\tau _ s: X(s) \rightarrow \operatorname{\mathcal{C}}$ satisfying $U \circ \tau _{s} = \overline{\tau }|_{ X(s) }$. The proof proceeds by induction on $s$, the case $s = 0$ being vacuous. Let us therefore assume that $0 < s \leq t$ and that $\tau _0$ has already been extended to a morphism of simplicial sets $\tau _{s-1}: X(s-1) \rightarrow \operatorname{\mathcal{C}}$. By construction, we have a pushout diagram of simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ \Lambda ^{q}_{p} \ar [r]^-{\varphi _0} \ar [d] & X(s-1) \ar [d] \\ \Delta ^{q} \ar [r]^{\varphi } & X(s) } \]

for some $q \geq 2$ and $0 \leq p < q$. Consequently, to prove the existence of $\tau _ s$, it will suffice to show that $\tau _{s-1} \circ \varphi _0$ can be extended to a $q$-simplex of $\operatorname{\mathcal{C}}$ lying over the simplex $\overline{\tau } \circ \varphi : \Delta ^ q \rightarrow \operatorname{\mathcal{D}}$. For $p \neq 0$, the existence of this extension follows from our assumption that $U$ is an inner fibration. To handle the case $p= 0$, we observe that the morphism $\varphi $ carries the initial edge of $\Delta ^{q}$ to the edge $(0,0) \rightarrow (0,1)$ of $\Delta ^{1} \times \Delta ^ n$, so that $\tau _{s-1} \circ \varphi _0$ carries the initial edge of $\Delta ^ q$ to the edge $\operatorname{ev}_0(e)$ of $\operatorname{\mathcal{C}}$, which is $U$-cocartesian by assumption. $\square$