Kerodon

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

Corollary 7.4.5.15. Suppose we are given a pullback diagram of small simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [r] \ar [d]^{U} & \overline{\operatorname{\mathcal{E}}} \ar [d]^{ \overline{U} } \ar [d] \\ \operatorname{\mathcal{C}}\ar [r] & \operatorname{\mathcal{C}}^{\triangleright }, } \]

where $U$ and $\overline{U}$ are left fibrations. The following conditions are equivalent:

$(1)$

The inclusion map $\operatorname{\mathcal{E}}\hookrightarrow \overline{\operatorname{\mathcal{E}}}$ is a weak homotopy equivalence of simplicial sets.

$(2)$

The inclusion map $\operatorname{\mathcal{E}}\hookrightarrow \overline{\operatorname{\mathcal{E}}}$ is left cofinal.

$(3)$

The covariant transport representation $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleright } }: \operatorname{\mathcal{C}}^{\triangleright } \rightarrow \operatorname{\mathcal{S}}$ is a colimit diagram in the $\infty $-category $\operatorname{\mathcal{S}}$.

Proof. Let ${\bf 1}$ denote the cone point of $\operatorname{\mathcal{C}}^{\triangleright }$, and let $\overline{\operatorname{\mathcal{E}}}_{ {\bf 1} } = \{ {\bf 1} \} \times _{\operatorname{\mathcal{C}}^{\triangleright } } \overline{\operatorname{\mathcal{E}}}$ denote the corresponding fiber of $\overline{\operatorname{\mathcal{E}}}$. Since the inclusion map $\{ {\bf 1} \} \hookrightarrow \operatorname{\mathcal{C}}^{\triangleright }$ is right anodyne (Example 4.3.7.11), the inclusion $\iota : \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} } \hookrightarrow \overline{\operatorname{\mathcal{E}}}$ is also right anodyne (Corollary 7.2.3.13). In particular, $\iota $ is a weak homotopy equivalence of simplicial sets. Let $\mathrm{Rf}: \operatorname{\mathcal{E}}\rightarrow \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ be a covariant refraction diagram (Proposition 7.4.3.3), so that the inclusion map $\operatorname{\mathcal{E}}\hookrightarrow \overline{\operatorname{\mathcal{E}}}$ is homotopic to the composition $\iota \circ \mathrm{Rf}$. It follows that condition $(1)$ can be reformulated as follows:

$(1')$

The covariant refraction diagram $\mathrm{Rf}: \operatorname{\mathcal{E}}\rightarrow \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ is a weak homotopy equivalence.

The equivalence $(1') \Leftrightarrow (3)$ follows by combining Proposition 7.4.5.1, Theorem 7.4.3.6, and Proposition 6.3.1.20.

The implication $(2) \Rightarrow (1)$ follows from Proposition 7.2.1.5. We will complete the proof by showing that $(1')$ implies $(2)$. Choose an inner anodyne monomorphism $\operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{C}}'$, where $K'$ is an $\infty $-category. Then the induced map $\operatorname{\mathcal{C}}^{\triangleright } \rightarrow \operatorname{\mathcal{C}}'^{\triangleright }$ is also inner anodyne (Corollary 4.3.6.6); in particular, it is a categorical equivalence. Using Proposition 5.6.7.2 (and Remark 5.6.7.4), we can assume that $\overline{U}$ is the pullback of a left fibration $\overline{U}': \overline{\operatorname{\mathcal{E}}}' \rightarrow \operatorname{\mathcal{C}}'^{\triangleright }$. Setting $\operatorname{\mathcal{E}}' = \operatorname{\mathcal{C}}' \times _{ \operatorname{\mathcal{C}}'^{\triangleright } } \overline{\operatorname{\mathcal{E}}}'$, we have a commutative diagram of inclusion maps

\[ \xymatrix@C =50pt@R=50pt{ \operatorname{\mathcal{E}}\ar [r] \ar [d] & \overline{\operatorname{\mathcal{E}}} \ar [d] \\ \operatorname{\mathcal{E}}' \ar [r] & \overline{\operatorname{\mathcal{E}}'}, } \]

where the vertical maps are categorical equivalences (Corollary 5.6.7.6). Consequently, to prove that the inclusion map $\operatorname{\mathcal{E}}\hookrightarrow \overline{\operatorname{\mathcal{E}}}$ is left cofinal, it will suffice to show that the inclusion $\operatorname{\mathcal{E}}' \hookrightarrow \overline{\operatorname{\mathcal{E}}}'$ is left cofinal (Corollary 7.2.1.22). We may therefore replace $\overline{U}$ by the left fibration $\overline{U}': \overline{\operatorname{\mathcal{E}}}' \rightarrow \operatorname{\mathcal{C}}'^{\triangleright }$, and thereby reduce to proving the implication $(1') \Rightarrow (2)$ under the assumption that $\operatorname{\mathcal{C}}$ is an $\infty $-category.

Let $\operatorname{\mathcal{E}}\operatorname{\vec{\times }}_{ \overline{\operatorname{\mathcal{E}}} } \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ denote the oriented fiber product of Definition 4.6.4.1, and consider the projection maps

\[ \operatorname{\mathcal{E}}\xleftarrow {\pi } \operatorname{\mathcal{E}}\operatorname{\vec{\times }}_{ \overline{\operatorname{\mathcal{E}}} } \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} } \xrightarrow {\pi '} \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }. \]

The functor $\pi $ is a trivial Kan fibration, and the refraction functor $\mathrm{Rf}$ is obtained by composing $\pi '$ with a choice of section of $\pi $. Consequently, assumption $(1')$ guarantees that $\pi '$ is a weak homotopy equivalence of simplicial sets. For each vertex $X \in \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$, we have a pullback diagram of simplicial sets

7.50
\begin{equation} \begin{gathered}\label{equation:diagram-for-left-cofinality} \xymatrix@C =50pt@R=50pt{ \operatorname{\mathcal{E}}\operatorname{\vec{\times }}_{ \overline{\operatorname{\mathcal{E}}} } \{ X \} \ar [r] \ar [d] & \{ X\} \ar [d] \\ \operatorname{\mathcal{E}}\operatorname{\vec{\times }}_{ \overline{\operatorname{\mathcal{E}}} } \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} } \ar [r]^-{ \pi } & \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }. } \end{gathered} \end{equation}

Since $\pi '$ is an isofibration of $\infty $-categories (Corollary 5.3.7.3), the diagram( 7.50 ) is a categorical pullback square (Corollary 4.5.2.27). Because $\overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ is a Kan complex, the diagram ( 7.50) is also a homotopy pullback square (Variant 4.5.2.11). Our assumption that $\pi '$ is a weak homotopy equivalence guarantees that the upper horizontal map is also a weak homotopy equivalence: that is, the simplicial set $\operatorname{\mathcal{E}}\operatorname{\vec{\times }}_{ \overline{\operatorname{\mathcal{E}}} } \{ X\} $ is weakly contractible (Corollary 3.4.1.5). Condition $(2)$ now follows by allowing the object $X$ to vary and applying the criterion of of Theorem 7.2.3.1 (together with Remark 7.2.3.2). $\square$