Kerodon

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

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

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

Proof. We will prove the first assertion; the second follows by a similar argument. Assume first that $U'$ is a right fibration of $\infty $-categories. Then $U'$ is a cartesian fibration (Proposition 5.1.4.14), so Corollary 5.1.6.2 implies that $U$ is a cartesian fibration. To prove that $U$ is a right fibration, it will suffice to show that for every object $D \in \operatorname{\mathcal{D}}$, the fiber $\operatorname{\mathcal{C}}_{D} = \{ D\} \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}}$ is a Kan complex (Proposition 5.1.4.14). This follows from Remark 4.5.1.21, since the functor $F$ induces an equivalence of $\infty $-categories $F_{D}: \operatorname{\mathcal{C}}_{D} \rightarrow \operatorname{\mathcal{C}}'_{ \overline{F}(D)}$ (Corollary 4.5.2.32).

We now prove the reverse implication. Arguing as in the proof of Corollary 5.1.6.2, we can construct a commutative diagram

where $G$ and $\overline{G}$ are homotopy inverses of the equivalences $F$ and $\overline{F}$, respectively. It then follows from the preceding argument that if $U$ is a right fibration of $\infty $-categories, then $U'$ is also a right fibration of $\infty $-categories. $\square$

Proof. By virtue of Proposition 5.1.2.1, it will suffice to show that for every object $X \in \operatorname{\mathcal{C}}$, the diagram of Kan complexes

is a homotopy pullback square. Set $X' = F(X)$, $Y' = F(Y)$, $Z' = F(Z)$, and $g' = F(g)$. Since the functors $F$ and $\overline{F}$ are fully faithful, (5.9) is homotopy equivalent to the diagram

Our assumption that $g'$ is $U'$-cartesian guarantees that (5.10) is a homotopy pullback square of Kan complexes (Proposition 5.1.2.1), so that (5.9) is also a homotopy pullback square (Corollary 3.4.1.12). $\square$

Proof. It follows from Lemma 5.1.6.5 that if $F(g)$ is $U'$-cartesian, then $g$ is $U$-cartesian. For the converse, suppose that $g$ is $U$-cartesian. Arguing as in the proof of Corollary 5.1.6.2, we can construct a commutative diagram

where $G$ and $\overline{G}$ are homotopy inverses of the equivalences $F$ and $\overline{F}$, respectively. Then $G( F(g) )$ is isomorphic to $g$ as an object of the arrow $\infty $-category $\operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}})$. Invoking Corollary 5.1.2.5, we conclude that $G( F(g) )$ is $U$-cartesian, so that $F(g)$ is $U'$-cartesian by virtue of Lemma 5.1.6.5. $\square$

Proof. The “only if” direction follows from Proposition 4.6.2.8. For the converse, assume that each of the functors $F_{D}$ is fully faithful; we will show that $F$ is fully faithful. Let $X$ and $Z$ be objects of $\operatorname{\mathcal{C}}$ having images $\overline{X}, \overline{Z} \in \operatorname{\mathcal{D}}$; we wish to show that the upper horizontal map in the diagram of Kan complexes

is a homotopy equivalence. Since $q$ and $q'$ are inner fibrations, the vertical maps are Kan fibrations (Proposition 4.6.1.21). Assumption $(3)$ guarantees that the lower horizontal map is a homotopy equivalence. By virtue of Proposition 3.2.8.1, it will suffice to show that for every morphism $\overline{e}: \overline{X} \rightarrow \overline{Z}$ in $\operatorname{\mathcal{D}}$, the induced map of fibers

is a homotopy equivalence.

Let $[\theta ]$ denote the homotopy class of $\theta $, regarded as a morphism in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$. Since $q$ is a cartesian fibration, there exists a $q$-cartesian morphism $g: Y \rightarrow Z$ of $\operatorname{\mathcal{C}}$ satisfying $q(g) = \overline{e}$. We then have a commutative diagram

in $\mathrm{h} \mathit{\operatorname{Kan}}$, where the vertical maps are given by the composition law of Notation 5.1.3.10. Assumption $(2)$ guarantees that $F(g)$ is locally $q'$-cartesian, so that the vertical maps in this diagram are isomorphisms in $\mathrm{h} \mathit{\operatorname{Kan}}$ (Proposition 5.1.3.11). It will therefore suffice to show that the functor $F_{\overline{X}}$ induces a homotopy equivalence of mapping spaces $\operatorname{Hom}_{ \operatorname{\mathcal{C}}_{ \overline{X} }}(X,Y) \rightarrow \operatorname{Hom}_{ \operatorname{\mathcal{C}}'_{ \overline{F}(\overline{X})} }( F(X), F(Y) )$, which follows from our assumption that $F_{ \overline{X} }$ is fully faithful. $\square$

Proof of Theorem 5.1.6.1. Suppose we are given a commutative diagram of $\infty $-categories

where $U$ is a cartesian fibration of $\infty $-categories, $U'$ is an isofibration of $\infty $-categories, and $\overline{F}$ is an equivalence of $\infty $-categories. If $F$ satisfies conditions $(1)$ and $(2)$ of Theorem 5.1.6.1, then it is fully faithful (Proposition 5.1.6.7) and essentially surjective (Remark 4.6.2.19), hence an equivalence of $\infty $-categories by virtue of Theorem 4.6.2.20. Conversely, if $F$ is an equivalence of $\infty $-categories, then it satisfies conditions $(1)$ and $(2)$ by virtue of Corollary 4.5.2.32 and Proposition 5.1.6.7, respectively. To complete the proof, we must show that if these conditions are satisfied, then $U'$ is also a cartesian fibration of $\infty $-categories.

Let $Z'$ be an object of $\operatorname{\mathcal{C}}'$ and let $\overline{g}': \overline{Y}' \rightarrow U'(Z')$ be a morphism in $\operatorname{\mathcal{D}}'$; we wish to show that $\overline{g}'$ can be lifted to a $U'$-cartesian morphism $Y' \rightarrow Z'$ in $\operatorname{\mathcal{C}}'$. Since $F$ is essentially surjective, we can choose an object $Z \in \operatorname{\mathcal{C}}$ and an isomorphism $v: F(Z) \rightarrow Z'$ in the $\infty $-category $\operatorname{\mathcal{C}}'$. Since $\overline{F}$ is essentially surjective, we can choose an object $\overline{Y} \in \operatorname{\mathcal{D}}$ and an isomorphism $\overline{u}: \overline{F}(\overline{Y}) \rightarrow \overline{Y}'$ in the $\infty $-category $\operatorname{\mathcal{D}}'$. Since $\overline{F}$ is fully faithful at the level of homotopy categories, we can choose a morphism $\overline{g}: \overline{Y} \rightarrow U(Z)$ in $\operatorname{\mathcal{D}}$ for which the diagram

commutes in the homotopy category $\mathrm{h} \mathit{\operatorname{\mathcal{D}}'}$, and can therefore be lifted to a commutative diagram $\overline{\sigma }$ in $\infty $-category $\operatorname{\mathcal{D}}'$ (see Exercise 1.5.2.10). Using our assumption that $U$ is a cartesian fibration, we can lift $\overline{g}$ to a $U$-cartesian morphism $g: Y \rightarrow Z$ of $\operatorname{\mathcal{C}}$. Since $U'$ is an isofibration, Corollary 4.4.5.9 guarantees that we can lift $\overline{\sigma }$ to a commutative diagram $\sigma :$

in the $\infty $-category $\operatorname{\mathcal{C}}'$, where the vertical maps are isomorphisms. To complete the proof, it will suffice to show that the morphism $g'$ is $U'$-cartesian. This follows from Corollary 5.1.2.5, since the morphism $F(g)$ is $U'$-cartesian (Proposition 5.1.6.6). $\square$