Kerodon

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

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

\[ \xymatrix { X_0 \ar [r]^{F_0} \ar [dr]_{U_0} & X \ar [d]^{U} & X_1 \ar [dl]^{ U_1 } \ar [l]_{F_1} \\ & S & } \]

satisfying the following conditions:

  • The morphisms $U_0$ and $U_1$ are cartesian fibrations.

  • The morphism $F_0$ carries $U_0$-cartesian edges of $X_0$ to $U$-cartesian edges of $X$.

  • The morphism $F_1$ carries $U_1$-cartesian edges of $X_1$ to $U$-cartesian edges of $X$.

  • The morphism $F_1$ is an isofibration.

Then the induced map $U_{01}: X_0 \times _{X} X_1 \rightarrow S$ is also a cartesian fibration. Moreover, an edge $e = (e_0, e_1)$ of $X_0 \times _{X} X_1$ is $U_{01}$-cartesian if and only if $e_0$ is $U_0$-cartesian and $e_1$ is $U_1$-cartesian.

Proof. Let $\pi : X_0 \times _{X} X_1 \rightarrow X_0$ and $\pi ': X_0 \times _{X} X_1 \rightarrow X_1$ be the projection maps. Since $F_1$ is an isofibration, $\pi $ is also an isofibration. In particular, $\pi $ is an inner fibration, so the composition $U_{01} = U_0 \circ \pi $ is also an inner fibration. Let us say that an edge $e = (e_0, e_1)$ of $X_0 \times _{X} X_1$ is special if $e_0$ is $U_0$-cartesian and $e_1$ is $U_1$-cartesian. The second assumption guarantees that $e$ is $\pi $-cartesian (Remark 5.1.1.11) and the first guarantees that $\pi (e)$ is $U_0$-cartesian. Applying Corollary 5.1.2.4, we deduce that every special edge of $X_0 \times _{X} X_1$ is $U_{01}$-cartesian.

To prove that $U_{01}$ is a cartesian fibration, it will suffice to show that for every vertex $x = (x_0, x_1)$ of $X_{0} \times _{X} X_1$ and every edge $\overline{e}: s \rightarrow U_{01}(x)$ in $S$, there exists a special edge $e: y \rightarrow x$ of $X_{0} \times _{X} X_1$ satisfying $U_{01}(e) = \overline{e}$. Since $U_0$ is a cartesian fibration, we can choose a $U_0$-cartesian edge $e_0: y_0 \rightarrow x_0$ of $X_0$ satisfying $U_0(e_0) = \overline{e}$. Similarly, we can choose a $U_1$-cartesian edge $e_1: y_1 \rightarrow x_1$ of $X_1$ satisfying $U_1(e_1) = \overline{e}$. We now observe that $F_0(e_0)$ and $F_1(e_1)$ are $U$-cartesian edges of $X$ having the same target and the same image in the simplicial set $S$. Applying Remark 5.1.3.8, we can choose a $2$-simplex $\sigma $ of $X$ as indicated in the diagram

\[ \xymatrix { & F_1(y_1) \ar [dr]^{ F_1(e_1) } & \\ F_0(y_0) \ar [ur]^{v} \ar [rr]^{ F_0( e_0) } & & F_1(x_1), } \]

where $v$ is an isomorphism in the $\infty $-category $X_{s} = \{ s\} \times _{S} X$. Our assumption that $F_1$ is an isofibration guarantees that we can lift $v$ to an isomorphism $\widetilde{v}: y'_1 \rightarrow y_1$ in the $\infty $-category $\{ s\} \times _{S} X_1$. Since $F_1$ is an inner fibration, we can lift $\sigma $ to a $2$-simplex $\widetilde{\sigma }$ of $X_1$ with boundary indicated in the diagram

\[ \xymatrix { & y_1 \ar [dr]^{ e_1 } & \\ y'_1 \ar [ur]^{ \widetilde{v} } \ar [rr]^{ e'_1 } & & x_1. } \]

It follows from Propositions 5.1.4.11 and 5.1.4.12 that $e'_1$ is a $U_1$-cartesian edge of $X_1$, so that $e = (e_0, e'_1)$ is a special edge of $X_0 \times _{X} X_1$ with target $x = (x_0, x_1)$ which satisfies $U_{01}(e) = \overline{e}$.

To complete the proof of Proposition 5.1.4.20, it will suffice to show that if $f: z \rightarrow x$ is a $U_{01}$-cartesian edge of the fiber product $X_{0} \times _{X} X_{1}$, then $f$ is special. Set $s = U_{01}(z)$. Applying the above argument, we can choose a special edge $e: y \rightarrow x$ satisfying $U_{01}(e) = U_{01}(f)$. Using Remark 5.1.3.8, we can choose a $2$-simplex $\tau $ of $X_0 \times _{X} X_1$ with boundary indicated in the diagram

\[ \xymatrix { & y \ar [dr]^{ e} & \\ z \ar [ur]^{v} \ar [rr]^{ f} & & x, } \]

where $v$ is an isomorphism in the $\infty $-category $\{ s\} \times _{S} (X_0 \times _{X} X_1)$. Applying Propositions 5.1.4.11 and 5.1.4.12 to the $2$-simplices $\pi (\tau )$ and $\pi '(\tau )$, we conclude that the edges $\pi (f)$ and $\pi '(f)$ are $U_0$-cartesian and $U_1$-cartesian, as desired. $\square$