# Kerodon

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

Proposition 5.3.7.2. Suppose we are given a commutative diagram of simplicial sets

$\xymatrix { \operatorname{\mathcal{C}}_0 \ar [d]^{U_0} \ar [r]^{F_0} & \operatorname{\mathcal{C}}\ar [d]^{U} & \operatorname{\mathcal{C}}_1 \ar [l]_{F_1} \ar [d]_{U_1} \\ \operatorname{\mathcal{D}}_0 \ar [r]^{G_0} & \operatorname{\mathcal{D}}& \operatorname{\mathcal{D}}_1 \ar [l]_{G_1} }$

where $U_0$, $U_1$, and $U$ are cocartesian fibrations, and $F_0$ carries $U_0$-cocartesian edges of $\operatorname{\mathcal{C}}_0$ to $U$-cocartesian edges of $\operatorname{\mathcal{C}}$. Then the induced map

$V: \operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1 \rightarrow \operatorname{\mathcal{D}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}_1$

is a cocartesian fibration of simplicial sets. Moreover, an edge $e$ of $\operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1$ is $V$-cocartesian if and only if it satisfies the following condition:

$(\ast )$

Let $e_0$ and $e_1$ denote the images of $e$ in $\operatorname{\mathcal{C}}_0$ and $\operatorname{\mathcal{C}}_1$, respectively. Then $e_0$ is $U_0$-cocartesian and $e_1$ is $U_1$-cocartesian.

Proof. Let us say that an edge $e$ of $\operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1$ is special if it satisfies condition $(\ast )$. We first show that if $e$ is a special edge of $\operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1$, then $e$ is $V$-cocartesian. Let $e_0$ and $e_1$ denote the images of $e$ in $\operatorname{\mathcal{C}}_0$ and $\operatorname{\mathcal{C}}_1$, respectively. Note that $V$ factors as a composition

$\operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1 \xrightarrow {V'} \operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}}_1 \xrightarrow {V''} \operatorname{\mathcal{D}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}_1.$

Here $V'$ is a pullback of the projection map $\overline{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}}$. Since $F( e_0 )$ is $U$-cocartesian, Lemma 5.3.7.1 implies that $e$ is $V'$-cocartesian. Moreover, $V''$ is a pullback of the product map $(U_0 \times U_1): \operatorname{\mathcal{C}}_0 \times \operatorname{\mathcal{C}}_1 \rightarrow \operatorname{\mathcal{D}}_0 \times \operatorname{\mathcal{D}}_1$. By assumption, $e_0$ is $U_0$-cocartesian and $e_1$ is $U_1$-cocartesian. It follows that $V'(e)$ is $V''$-cocartesian, so that $e$ is $V$-cocartesian by virtue of Remark 5.1.1.6.

Since $U_0$, $U_1$, and $U$ are inner fibrations, the morphisms $\overline{V}'$ and $(U_0 \times U_1)$ are also inner fibrations (see Proposition 4.1.4.1). It follows that $V'$ and $V''$ are inner fibrations (Remark 4.1.1.5), so that $V$ is an inner fibration (Remark 4.1.1.8). To show that $V$ is a cocartesian fibration, it will suffice to show that if $C$ is an object of $\operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1$ and $\overline{e}: V(C) \rightarrow \overline{C}'$ is an edge of $\operatorname{\mathcal{D}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}_1$, then there exists a special edge $e: C \rightarrow C'$ satisfying $V(e) = \overline{e}$. Let us identify $C$ with a triple $(C_0, C_1, u)$ where $C_0$ is a vertex of $\operatorname{\mathcal{C}}_0$, $C_1$ is a vertex of $\operatorname{\mathcal{C}}_1$, and $u: F_0(C_0) \rightarrow F_1(C_1)$ is an edge of $\operatorname{\mathcal{C}}$. Similarly, we can identify $\overline{C}'$ with a triple $(\overline{C}'_0, \overline{C}'_1, \overline{u}' )$ where $\overline{C}_0$ is a vertex of $\operatorname{\mathcal{D}}_0$, $\overline{C}'_1$ is a vertex of $\operatorname{\mathcal{D}}_1$, and $\overline{u}': G_0( \overline{C}'_0 ) \rightarrow G_1( \overline{C}'_1 )$ is an edge of $\operatorname{\mathcal{D}}$. The edge $\overline{e}$ has images $\overline{e}_{0}: U_0(C_0) \rightarrow \overline{C}'_0$ an $\overline{e}_{1}: U_1(C_1) \rightarrow \overline{C}'_{1}$ in $\operatorname{\mathcal{D}}_0$ and $\operatorname{\mathcal{D}}_1$-respectively. Since $U_0$ is a cocartesian fibration, we can lift $\overline{e}_0$ to a $U_0$-cocartesian edge $e_0: C_0 \rightarrow C'_0$ of $\operatorname{\mathcal{C}}_0$. Similarly, we can lift $\overline{e}_1$ to a $U_1$-cocartesian edge $e_1: C_1 \rightarrow C'_1$ of $\operatorname{\mathcal{C}}_1$. The edge $\overline{e}$ also determines a map $\Delta ^1 \times \Delta ^1 \rightarrow \operatorname{\mathcal{D}}$, which we depict informally in the diagram

$\xymatrix { (G_0 \circ U_0)( C_0 ) \ar [r]^-{U(u)} \ar [d]^{ G_0(\overline{e}_0) } & (G_1 \circ U_1)(C_1) \ar [d]^{ G_1(\overline{e}_1) } \\ G_0(\overline{C}'_0) \ar [r]^{\overline{u}'} & G_1( \overline{C}'_{1} ). }$

Using our assumption that $U$ is an inner fibration, we can lift the upper right triangle to a $2$-simplex $\sigma$:

$\xymatrix { F_0(C_0) \ar [r]^{u} \ar@ {-->}[dr]^{v} & F_1(C_1) \ar [d]^{ F_1( e_1 ) } \\ & F_1( C'_1 ) }$

of the simplicial set $\operatorname{\mathcal{C}}$. Using the fact that $F_0( e_0 )$ is $U$-cocartesian, we can lift the lower triangle to a $2$-simplex $\tau$

$\xymatrix { F_0(C_0) \ar [d]^{ F_0(e_0 ) } \ar [dr]^{v} & \\ F_0( C'_0 ) \ar@ {-->}[r]^{w} & F_1( C'_1 ) }$

of $\operatorname{\mathcal{C}}$. Setting $C' = (C'_0, C'_1, w) \in \operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1$, we observe that the tuple $( e_0, e_1, \sigma , \tau )$ determines a special edge $e: C \rightarrow C'$ satisfying $V(e) = \overline{e}$.

We now complete the proof by showing that every $V$-cocartesian edge $f: C \rightarrow C''$ in $\operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1$ is special. Using the preceding argument, we can choose a special edge $e: C \rightarrow C'$ satisfying $V(e) = V(f)$. Set $\overline{C}' = V( C' ) = V(C'' )$. Applying Remark 5.1.3.8, we deduce that there is a $2$-simplex $\rho :$

$\xymatrix { & C' \ar [dr]^{s} & \\ C \ar [ur]^{ e } \ar [rr]^{f} & & C'' }$

of the simplicial set $\operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1$, where $s$ is an isomorphism in the $\infty$-category $V^{-1}( \{ \overline{C}' \} )$. Applying Example 5.1.3.6, we deduce that the images of $s$ in $\operatorname{\mathcal{C}}_0$ is $U_0$-cocartesian, and the image of $s$ in $\operatorname{\mathcal{C}}_1$ is $U_1$-cocartesian. Since the collections of $U_0$-cocartesian and $U_1$-cocartesian edges are closed under composition (Corollary 5.1.2.4), we conclude that $f$ is also special. $\square$