Kerodon

Proof. The implication $(1) \Rightarrow (2)$ follows from Corollary 5.2.2.7 (and does not require the assumption that $q$ is a locally cartesian fibration), and the implication $(2) \Rightarrow (3)$ is immediate. We will complete the proof by showing that $(3) \Rightarrow (1)$. Using Remarks 5.2.1.10 and 5.2.3.6, we can reduce to the case where $\operatorname{\mathcal{D}}= \Delta ^ n$ is a simplex. By virtue of Corollary 5.2.2.4, it will suffice to show that for each object $X \in \operatorname{\mathcal{C}}$ satisfying $q(X) \leq q(Y)$, the composition map

of Notation 5.2.2.3 is an isomorphism in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$. Since $q$ is a locally cartesian fibration, we can choose a locally $q$-cartesian morphism $f: X \rightarrow Y$ satisfying $q(W) = q(X)$. Using the fact that $\operatorname{\mathcal{C}}$ is an $\infty $-category, we can choose a $2$-simplex $\sigma $ of $\operatorname{\mathcal{C}}$ satisfying $d_0(\sigma ) = g$ and $d_2(\sigma ) = f$. Set $h= d_1(\sigma )$, so that we have a commutative diagram

in the $\infty $-category $\operatorname{\mathcal{C}}$. If assumption $(3)$ is satisfied, then $h$ is also a locally $q$-cartesian morphism of $\operatorname{\mathcal{C}}$. Invoking Proposition 4.6.3.12, we conclude that the diagram

commutes (in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$). Since $f$ and $h$ are locally $q$-cartesian, the horizontal and left diagonal map in this diagram are isomorphisms (in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$), so the right diagonal map is an isomorphism as well. $\square$

Proof. The implication $(1) \Rightarrow (2)$ follows from Remark 5.2.4.5, the implication $(2) \Rightarrow (1)$ is immediate, and the equivalence $(2) \Leftrightarrow (3)$ follows from Proposition 5.2.6.9. $\square$

Proof. As in the proof of Proposition 5.2.4.14, we factor $q'$ as a composition

where $u$ is a cartesian fibration and every edge of $X_{f/}$ is $u$-cartesian (Proposition 5.2.4.12). The morphism $v$ is a pullback of $q$, and is therefore a locally cartesian fibration (Remark 5.2.6.5). Moreover, an edge of $X \times _{S} S_{/(q \circ f)}$ is locally $v$-cartesian if and only if its image in $X$ is locally $q$-cartesian (Remark 5.2.3.6). Assertions $(1)$ and $(2)$ now follow from Remark 5.2.6.7. $\square$

Proof of Proposition 5.2.6.13. Choose a vertex $z \in X$ and an edge $\overline{h}: \overline{x} \rightarrow r(z)$ of the simplicial set $Y$. We wish to prove that there exists a locally $r$-cartesian edge $h: x \rightarrow z$ satisfying $r(h) = \overline{h}$. Since $p$ is a locally cartesian fibration, we can choose a locally $p$-cartesian edge $g: y \rightarrow z$ satisfying $p(g) = q(\overline{h})$. Assumption $(2)$ guarantees that $r(g)$ is locally $q$-cartesian, so we can choose a $2$-simplex $\overline{\sigma }$ of $Y$ satisfying

as indicated in the diagram

Set $s = q( \overline{x} )$, so that $\overline{f}$ can be regarded as an edge of the simplicial set $Y_{s}$. Invoking assumption $(3)$, we conclude that there exists a locally $r_{s}$-cartesian edge $f: x \rightarrow y$ of $X_{s}$ satisfying $r(f) = \overline{f}$. Since $r$ is an inner fibration, we can choose a $2$-simplex $\sigma $ of $X$ satisfying

as depicted in the diagram

We will complete the proof by showing that $h$ is locally $r$-cartesian. To prove this, we can replace $X$ and $Y$ by their pullbacks along the edge $\Delta ^1 \xrightarrow { q(\overline{h})} S$, and thereby reduce to the case $S = \Delta ^1$. In this case, the morphisms $p$ and $q$ are cartesian fibration (Remark 5.2.6.6), so that $g$ is $p$-cartesian and $r(g)$ is $q$-cartesian (Remark 5.2.4.5). Applying Corollary 5.2.2.7, we conclude that $g$ is $r$-cartesian. It follows from Remark 5.2.3.6 that $f$ is locally $r$-cartesian, so that $h$ is locally $r$-cartesian by virtue of Proposition 5.2.3.8. $\square$

Proof. The “only if” direction follows from Proposition 4.6.2.6. 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.19). Assumption $(3)$ guarantees that the lower horizontal map is a homotopy equivalence. By virtue of Proposition 3.2.7.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 locally cartesian fibration, there exists a locally $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.2.3.11. 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.2.3.12). 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. If $F$ is an equivalence of $\infty $-categories, then Corollary 4.5.4.4 guarantees that each $F_{D}$ is an equivalence of $\infty $-categories. The converse follows by combining Proposition 5.2.6.15, Remark 4.6.2.16, and Theorem 4.6.2.17. $\square$

Proof. This is a special case of Corollary 5.2.6.16, since every cartesian fibration is a locally cartesian isofibration (Example 5.2.6.2 and Proposition 5.2.4.7). $\square$

Proof. Combine Corollary 5.2.6.17, Proposition 5.2.4.12, and Example 4.5.1.14. $\square$