Theorem 7.4.3.6 (Refraction Criterion). Suppose we are given a pullback diagram of small simplicial sets
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [d]^{U} \ar [r] & \overline{\operatorname{\mathcal{E}}} \ar [d]^{ \overline{U} } \\ \operatorname{\mathcal{C}}\ar [r] & \operatorname{\mathcal{C}}^{\triangleright }, } \]
where $U$ and $\overline{U}$ are cocartesian fibrations. Let ${\bf 1}$ denote the cone point of $\operatorname{\mathcal{C}}^{\triangleright }$ and let $W$ be the collection of all $U$-cocartesian edges of $\operatorname{\mathcal{E}}$. The following conditions are equivalent:
- $(1)$
The covariant refraction diagram $\mathrm{Rf}: \operatorname{\mathcal{E}}\rightarrow \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ of Proposition 7.4.3.3 exhibits $\overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ as a localization of $\operatorname{\mathcal{E}}$ with respect $W$.
- $(2)$
The covariant transport representation $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleright } }: \operatorname{\mathcal{C}}^{\triangleright } \rightarrow \operatorname{\mathcal{QC}}$ of Notation 5.6.5.14 is a colimit diagram in the $\infty $-category $\operatorname{\mathcal{QC}}$.
Proof of Theorem 7.4.3.6.
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} } \\ \operatorname{\mathcal{C}}\ar [r] & \operatorname{\mathcal{C}}^{\triangleright }, } \]
where $U$ and $\overline{U}$ are cocartesian fibrations. Let $W$ denote the collection of all $U$-cocartesian edges of $\operatorname{\mathcal{E}}$, let ${\bf 1}$ denote the cone point of $\operatorname{\mathcal{C}}^{\triangleright }$, let $\mathrm{Rf}: \operatorname{\mathcal{E}}\rightarrow \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ be a covariant refraction diagram (Definition 7.4.3.1). Assume first that $\mathrm{Rf}$ exhibits the $\infty $-category $\overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ as a localization of $\operatorname{\mathcal{E}}$ with respect to $W$. We wish to show that the covariant transport representation $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleright } }: \operatorname{\mathcal{C}}^{\triangleright } \rightarrow \operatorname{\mathcal{QC}}$ is a colimit diagram in the $\infty $-category $\operatorname{\mathcal{QC}}$.
Using Corollary 4.1.3.3, we can choose an inner anodyne morphism $\operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{C}}'$, where $\operatorname{\mathcal{C}}'$ is an $\infty $-category. Note that the induced map $\operatorname{\mathcal{C}}^{\triangleright } \hookrightarrow \operatorname{\mathcal{C}}'^{\triangleright }$ is also inner anodyne (Proposition 4.3.6.4). Applying Corollary 5.6.7.3, we can realize $\overline{U}$ as the pullback of a cocartesian fibration of $\infty $-categories $\overline{U}': \overline{\operatorname{\mathcal{E}}}' \rightarrow \operatorname{\mathcal{C}}'^{\triangleright }$. Form a pullback diagram
7.49
\begin{equation} \begin{gathered}\label{equation:hard-half-of-detection} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}' \ar [d]^{U'} \ar [r] \ar [d] & \overline{\operatorname{\mathcal{E}}}' \ar [d]^{ \overline{U}' } \\ \operatorname{\mathcal{C}}' \ar [r] & \operatorname{\mathcal{C}}'^{\triangleright }, } \end{gathered} \end{equation}
and let $W'$ denote the collection of all $U'$-cocartesian morphisms of $\operatorname{\mathcal{E}}'$. Using Proposition 7.4.3.3, we can choose a covariant refraction diagram $\mathrm{Rf}': \operatorname{\mathcal{E}}' \rightarrow \overline{\operatorname{\mathcal{E}}}'_{{\bf 1}} = \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ for the cocartesian fibration $\overline{U}'$. Note that the restriction $\mathrm{Rf}|_{\operatorname{\mathcal{E}}}$ is a covariant refraction collapse diagram for the cocartesian fibration $\overline{U}$, and is therefore isomorphic to $\mathrm{Rf}$ as an object of the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{E}}, \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$. It follows that $\mathrm{Rf}'|_{\operatorname{\mathcal{E}}}$ also exhibits the $\infty $-category $\overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ as a localization of $\operatorname{\mathcal{E}}$ with respect to $W$ (Exercise 6.3.1.11). Applying Lemma 7.4.4.3, we see that $\mathrm{Rf}$ exhibits $\overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ as a localization of $\operatorname{\mathcal{E}}'$ with respect to $W$.
Using Corollary 5.6.5.11, we can extend $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleright } }$ to a functor
\[ \operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}}' / \operatorname{\mathcal{C}}'^{\triangleright } }: \operatorname{\mathcal{C}}'^{\triangleright } \rightarrow \operatorname{\mathcal{QC}} \]
which is a covariant transport representation for $\overline{U}'$. Applying Proposition 7.4.4.2 to the diagram of $\infty $-categories (7.49), we deduce that $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}}' / \operatorname{\mathcal{C}}'^{\triangleright } }$ is a colimit diagram in the $\infty $-category $\operatorname{\mathcal{QC}}$. Since the inclusion map $\operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{C}}'$ is right cofinal (Proposition 7.2.1.3), it follows that $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleright } }$ is also a colimit diagram in $\operatorname{\mathcal{QC}}$, as desired.
We now prove the converse. Assume that the covariant transport representation $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleright } }$ is a colimit diagram in the $\infty $-category $\operatorname{\mathcal{QC}}$; we wish to show that the covariant refraction diagram $\mathrm{Rf}$ exhibits $\overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ as a localization of $\operatorname{\mathcal{E}}$ with respect to $W$. By virtue of Proposition 7.4.3.9 (and Remark 7.4.3.10), we can choose another pullback diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [d]^{U} \ar [r] & \operatorname{\mathcal{E}}^{+} \ar [d]^{ U^{+} } \\ \operatorname{\mathcal{C}}\ar [r] & \operatorname{\mathcal{C}}^{\triangleright }, } \]
where $U^{+}$ is a cocartesian fibration for which the covariant refraction diagram $\mathrm{Rf}^{+}: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}^{+}_{ {\bf 1} }$ exhibits $\operatorname{\mathcal{E}}^{+}_{ {\bf 1} }$ as a localization of $\operatorname{\mathcal{E}}$ with respect to $W$. Applying Corollary 5.6.5.11, we see that $U^{+}$ admits a covariant transport representation $\operatorname{Tr}_{ \operatorname{\mathcal{E}}^{+} / \operatorname{\mathcal{C}}^{\triangleright } }: \operatorname{\mathcal{C}}^{\triangleright } \rightarrow \operatorname{\mathcal{QC}}$ satisfying $(\operatorname{Tr}_{ \operatorname{\mathcal{E}}^{+} / \operatorname{\mathcal{C}}^{\triangleright } })|_{\operatorname{\mathcal{C}}} = (\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleright } })|_{\operatorname{\mathcal{C}}}$. The first part of the proof shows that $\operatorname{Tr}_{ \operatorname{\mathcal{E}}^{+} / \operatorname{\mathcal{C}}^{\triangleright } }$ is also a colimit diagram in the $\infty $-category $\operatorname{\mathcal{QC}}$, and is therefore isomorphic to $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleright } }$ as an object of the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}^{\triangleright }, \operatorname{\mathcal{QC}})$. Applying Theorem 5.6.0.2, we see $\overline{U}: \overline{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{C}}^{\triangleright }$ and $U^{+}: \operatorname{\mathcal{E}}^{+} \rightarrow \operatorname{\mathcal{C}}^{\triangleright }$ are equivalent as cocartesian fibrations over $\operatorname{\mathcal{C}}^{\triangleright }$. Applying Exercise 7.4.3.8, we conclude that $\mathrm{Rf}$ also exhibits $\overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ as a localization of $\operatorname{\mathcal{E}}$ with respect to $W$, as desired.
$\square$