# Kerodon

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

Theorem 7.4.1.1 (Diffraction 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}}^{\triangleleft }, }$

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

$(1)$

The restriction map

$\operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} ) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$

is an equivalence of $\infty$-categories.

$(2)$

The covariant transport representation

$\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleleft } }: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{\mathcal{QC}}$

of Notation 5.6.5.14 is a limit diagram in the $\infty$-category $\operatorname{\mathcal{QC}}$.

Proof of Theorem 7.4.1.1. 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}}^{\triangleleft }, }$

where $U$ and $\overline{U}$ are cocartesian fibrations. Assume first that the restriction map

$\theta : \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} ) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$

is an equivalence of $\infty$-categories; we wish to show that the covariant transport representation $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleleft } }: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{\mathcal{QC}}$ is a limit 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}}^{\triangleleft } \hookrightarrow \operatorname{\mathcal{C}}'^{\triangleleft }$ 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}}'^{\triangleleft }$. Set $\operatorname{\mathcal{E}}' = \operatorname{\mathcal{C}}' \times _{ \operatorname{\mathcal{C}}'^{\triangleleft } } \overline{\operatorname{\mathcal{E}}}'$, so that we have a commutative diagram of restriction functors

$\xymatrix@R =50pt@C=50pt{ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}'^{\triangleleft } }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}'^{\triangleleft }, \overline{\operatorname{\mathcal{E}}}' ) \ar [r]^-{ \theta ' } \ar [d] & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}' }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}', \operatorname{\mathcal{E}}' ) \ar [d] \\ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} ) \ar [r]^-{\theta } & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}), }$

where the vertical maps are trivial Kan fibrations (Proposition 5.3.1.21). It follows that $\theta '$ is also an equivalence of $\infty$-categories.

Using Corollary 5.6.5.11, we can extend $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleleft } }$ to a functor

$\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}}' / \operatorname{\mathcal{C}}'^{\triangleleft } }: \operatorname{\mathcal{C}}'^{\triangleleft } \rightarrow \operatorname{\mathcal{QC}}$

which is a covariant transport representation for the cocartesian fibration $\overline{U}'$. Since $\operatorname{\mathcal{C}}'$ is an $\infty$-category, Proposition 7.4.2.1 guarantees that $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}}' / \operatorname{\mathcal{C}}'^{\triangleleft } }$ is a limit diagram in the $\infty$-category $\operatorname{\mathcal{QC}}$. Since the inclusion map $\operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{C}}'$ is left cofinal (Proposition 7.2.1.3), it follows that $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleleft } }$ is also a limit diagram in $\operatorname{\mathcal{QC}}$.

We now prove the converse. Assume that the covariant transport representation $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleleft } }$ is a limit diagram in the $\infty$-category $\operatorname{\mathcal{QC}}$; we wish to show that $\theta$ is an equivalence of $\infty$-categories. Using Proposition 7.4.1.6, 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}}^{\triangleleft }, }$

where $U^{+}$ is a cocartesian fibration for which the restriction map $\theta ^{+}: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}^{\triangleleft }, \operatorname{\mathcal{E}}^{+} ) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}^{+} )$ is an equivalence of $\infty$-categories. Applying Corollary 5.6.5.11, we see that $U^{+}$ admits a covariant transport representation $\operatorname{Tr}_{ \operatorname{\mathcal{E}}^{+} / \operatorname{\mathcal{C}}^{\triangleleft } }: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{\mathcal{QC}}$ satisfying $(\operatorname{Tr}_{ \operatorname{\mathcal{E}}^{+} / \operatorname{\mathcal{C}}^{\triangleleft } })|_{\operatorname{\mathcal{C}}} = (\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleleft } })|_{\operatorname{\mathcal{C}}}$. The first part of the proof shows that $\operatorname{Tr}_{ \operatorname{\mathcal{E}}^{+} / \operatorname{\mathcal{C}}^{\triangleleft } }$ is also a limit diagram in the $\infty$-category $\operatorname{\mathcal{QC}}$, and is therefore isomorphic to $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleleft } }$ as an object of the $\infty$-category $\operatorname{Fun}( \operatorname{\mathcal{C}}^{\triangleleft }, \operatorname{\mathcal{QC}})$. Applying Theorem 5.6.0.2, we deduce that there exists a morphism $F: \overline{\operatorname{\mathcal{E}}} \rightarrow \overline{\operatorname{\mathcal{E}}}^{+}$ which is an equivalence of cocartesian fibrations over $\operatorname{\mathcal{C}}^{\triangleleft }$. We have a commutative diagram of $\infty$-categories

$\xymatrix@R =50pt@C=50pt{ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}^{\triangleleft }, \operatorname{\mathcal{E}}^{+} ) \ar [r]^-{ \theta ^{+} } \ar [d] & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}' ) \ar [d] \\ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} ) \ar [r]^-{\theta } & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}), }$

where the vertical maps are given by precomposition with $F$ and are therefore equivalences of $\infty$-categories. Since $\theta ^{+}$ is an equivalence of $\infty$-categories, it follows that $\theta$ is also an equivalence of $\infty$-categories. $\square$