# Kerodon

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

Corollary 5.1.6.2. Suppose we are given a commutative diagram of $\infty$-categories

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}\ar [r]^-{F} \ar [d]^-{U} & \operatorname{\mathcal{C}}' \ar [d]^-{U'} \\ \operatorname{\mathcal{D}}\ar [r]^-{ \overline{F} } & \operatorname{\mathcal{D}}'. }$

Assume that $U$ and $U'$ are isofibrations of $\infty$-categories and that $F$ and $\overline{F}$ are equivalences of $\infty$-categories. Then:

• The functor $U$ is a cartesian fibration if and only if $U'$ is a cartesian fibration.

• The functor $U$ is a cocartesian fibration if and only if $U'$ is a cocartesian fibration.

Proof. We will prove the first assertion; the second follows by a similar argument. It follows from Theorem 5.1.6.1 that if $U$ is a cartesian fibration, then $U'$ is also a cartesian fibration. To prove the converse, choose functors $G': \operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{C}}$ and $\overline{G}: \operatorname{\mathcal{D}}' \rightarrow \operatorname{\mathcal{D}}$ which are homotopy inverse to the equivalences $F$ and $\overline{F}$, respectively. We then have isomorphisms

$U \circ G' \circ F \simeq U \simeq \overline{G} \circ \overline{F} \circ U = \overline{G} \circ U' \circ F$

in the functor $\infty$-category $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$. Since $F$ is an equivalence of $\infty$-categories, it follows that there exists an isomorphism $\overline{\alpha }: U \circ G' \rightarrow \overline{G} \circ U'$ in the functor $\infty$-category $\operatorname{Fun}(\operatorname{\mathcal{C}}', \operatorname{\mathcal{D}})$. Using our assumption that $U$ is an isofibration, we can lift $\overline{\alpha }$ to an isomorphism of functors $\alpha : G' \rightarrow G$ (Proposition 4.4.5.8). Applying Theorem 5.1.6.1 to the commutative diagram

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}' \ar [r]^-{G} \ar [d]^-{U'} & \operatorname{\mathcal{C}}\ar [d]^-{U} \\ \operatorname{\mathcal{D}}' \ar [r]^-{\overline{G}} & \operatorname{\mathcal{D}}, }$

we conclude that if $U'$ is a cartesian fibration, then $U$ is also a cartesian fibration. $\square$