Corollary 7.2.3.15 (Fiberwise Cofinality Criterion). Suppose we are given a commutative diagram of simplicial sets
\[ \xymatrix@C =50pt@R=50pt{ \operatorname{\mathcal{E}}' \ar [dr]_{U'} \ar [rr]^{ F } & & \operatorname{\mathcal{E}}\ar [dl]^{U} \\ & \operatorname{\mathcal{C}}& } \]
where $U$ and $U'$ are cartesian fibrations, and the morphism $F$ carries $U'$-cartesian edges of $\operatorname{\mathcal{E}}'$ to $U$-cartesian edges of $\operatorname{\mathcal{E}}$. The following conditions are equivalent:
- $(1)$
The morphism $F$ is right cofinal.
- $(2)$
For every vertex $C \in \operatorname{\mathcal{C}}$, the induced map of fibers $F_{C}: \operatorname{\mathcal{E}}'_{C} \rightarrow \operatorname{\mathcal{E}}_{C}$ is right cofinal.
Proof.
We first reduce to the case where $\operatorname{\mathcal{C}}$ is an $\infty $-category. Using Corollary 4.1.3.3, we can choose an inner anodyne morphism $\iota : \operatorname{\mathcal{C}}\hookrightarrow \overline{\operatorname{\mathcal{C}}}$, where $\overline{\operatorname{\mathcal{C}}}$ is an $\infty $-category. Using Proposition 5.6.7.2, we can extend $U$ and $U'$ to cocartesian fibrations of $\infty $-categories $\overline{U}: \overline{\operatorname{\mathcal{E}}} \rightarrow \overline{\operatorname{\mathcal{C}}}$ and $\overline{U}': \overline{\operatorname{\mathcal{E}}}' \rightarrow \overline{\operatorname{\mathcal{C}}}$. Then the inclusion maps $\operatorname{\mathcal{E}}\hookrightarrow \overline{\operatorname{\mathcal{E}}}$ and $\operatorname{\mathcal{E}}' \hookrightarrow \overline{\operatorname{\mathcal{E}}}'$ are categorical equivalences (Lemma 5.3.6.5). Since $\overline{U}$ is an isofibration (Proposition 5.1.4.9), we can extend $F$ to a functor $\overline{F}: \overline{\operatorname{\mathcal{E}}}' \rightarrow \overline{\operatorname{\mathcal{E}}}$ satisfying $\overline{U} \circ \overline{F} = \overline{U}'$ (Proposition 4.5.5.1). It follows from Remark 5.3.1.12 that the functor $\overline{F}$ carries $\overline{U}'$-cartesian morphisms of $\overline{\operatorname{\mathcal{E}}}'$ to $\overline{U}$-cartesian morphisms of $\overline{\operatorname{\mathcal{E}}}$. Moreover, the morphism $F$ is right cofinal if and only if $\overline{F}$ is right cofinal (Corollary 7.2.1.22). Consequently, we can replace $\operatorname{\mathcal{C}}$ by $\overline{\operatorname{\mathcal{C}}}$ and thereby reduce to proving Corollary 7.2.3.15 in the case where $\operatorname{\mathcal{C}}$ is an $\infty $-category.
Fix an object $X \in \operatorname{\mathcal{E}}$, let $C = U(X)$ denote its image in $\operatorname{\mathcal{C}}$, and wlet $\operatorname{\mathcal{E}}_{C}$ and $\operatorname{\mathcal{E}}'_{C}$ denote the fibers $\{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ and $\{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}'$, respectively. We will prove that the following conditions are equivalent:
- $(1_ X)$
The $\infty $-category $\operatorname{\mathcal{E}}' \times _{ \operatorname{\mathcal{E}}} \operatorname{\mathcal{E}}_{ X/ }$ is weakly contractible.
- $(2_ X)$
The $\infty $-category $\operatorname{\mathcal{E}}'_{C} \times _{ \operatorname{\mathcal{E}}_{C} } (\operatorname{\mathcal{E}}_{C})_{X/}$ is weakly contractible.
Corollary 7.2.3.15 will then follow by allowing the object $X$ to vary and applying the criterion of Theorem 7.2.3.1.
To complete the proof, it will suffice to show that the inclusion map
\[ \operatorname{\mathcal{E}}'_{C} \times _{ \operatorname{\mathcal{E}}_{C} } (\operatorname{\mathcal{E}}_{C})_{X/} \hookrightarrow \operatorname{\mathcal{E}}' \times _{ \operatorname{\mathcal{E}}} \operatorname{\mathcal{E}}_{ X/ } \]
is a weak homotopy equivalence. In fact, we will show that it is left anodyne. Unwinding the definitions, we have a pullback diagram
\[ \xymatrix@C =50pt@R=50pt{ \operatorname{\mathcal{E}}'_{C} \times _{ \operatorname{\mathcal{E}}_{C} } (\operatorname{\mathcal{E}}_{C})_{X/} \ar [r] \ar [d] & \operatorname{\mathcal{E}}' \times _{ \operatorname{\mathcal{E}}} \operatorname{\mathcal{E}}_{ X/ } \ar [d] \\ \{ \operatorname{id}_{C} \} \ar [r] & \operatorname{\mathcal{C}}_{C/}, } \]
where the right vertical map is a cartesian fibration (Corollary 5.1.4.22). By virtue of Proposition 7.2.3.12, we are reduced to showing that the inclusion map $\{ \operatorname{id}_{C} \} \hookrightarrow \operatorname{\mathcal{C}}_{C/}$ is left anodyne, or equivalently that $\{ \operatorname{id}_{C} \} $ is an initial object of the $\infty $-category $\operatorname{\mathcal{C}}_{C/}$ (Corollary 4.6.7.23). This is a special case of Proposition 4.6.7.22.
$\square$