# Kerodon

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

### 7.4.2 Proof of the Diffraction Criterion

The goal of this section is to prove Theorem 7.4.1.1. We begin by treating a special case (which is already sufficient for most applications).

Proposition 7.4.2.1. Suppose we are given a pullback diagram of small $\infty$-categories

$\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 and 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. Then 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}}$.

Proof. Suppose we are given an integer $n \geq 1$ and a diagram $\mathscr {F}_0: \operatorname{\partial \Delta }^{n} \star \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$ with the property that $\mathscr {F}_0|_{ \{ n\} \star \operatorname{\mathcal{C}}}: \{ n\} \star \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$ is a covariant transport representation for the cocartesian fibration $\overline{U}$; here we abuse notation by identifying $\{ n\} \star \operatorname{\mathcal{C}}$ with the cone $\operatorname{\mathcal{C}}^{\triangleleft }$. We wish to show that $\mathscr {F}_0$ can be extended to a diagram $\mathscr {F}: \Delta ^ n \star \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$. Using Lemma 5.7.7.1, we can choose a pullback diagram

$\xymatrix@R =50pt@C=50pt{ \overline{\operatorname{\mathcal{E}}} \ar [d]^{ \overline{U} } \ar [r] \ar [d] & \overline{\operatorname{\mathcal{E}}}^{+} \ar [d]^{ \overline{U}^{+} } \\ \{ n\} \star \operatorname{\mathcal{C}}\ar [r] & \operatorname{\partial \Delta }^{n} \star \operatorname{\mathcal{C}}, }$

where $\overline{U}^{+}$ is a cocartesian fibration having covariant transport representation $\mathscr {F}_0$. Fix an auxiliary symbol $c$, so that the projection map $\operatorname{\mathcal{C}}\rightarrow \{ c\}$ induces a cartesian fibration of $\infty$-categories $T: \Delta ^ n \star \operatorname{\mathcal{C}}\rightarrow \Delta ^ n \star \{ c\}$ (this follows by repeated application of Lemma 5.2.3.17). Note that $T$ restricts to a to a morphism of simplicial sets $T_0: \operatorname{\partial \Delta }^ n \star \operatorname{\mathcal{C}}\rightarrow \operatorname{\partial \Delta }^ n \star \{ c\}$ which is a pullback of $T$, and is therefore also a cartesian fibration. Let $\operatorname{\mathcal{D}}$ be the cocartesian direct image $\operatorname{Res}^{\operatorname{CCart}}_{ \operatorname{\partial \Delta }^{n} \star \operatorname{\mathcal{C}}/ \operatorname{\partial \Delta }^{n} \star \{ c\} }( \overline{\operatorname{\mathcal{E}}}^{+} )$ introduced in Notation 5.3.7.8, so that the projection map $\pi : \operatorname{\mathcal{D}}\rightarrow \operatorname{\partial \Delta }^{n} \star \{ c\}$ is a cocartesian fibration of simplicial sets (Proposition 5.3.7.10).

Applying Corollary 5.7.5.12, we can choose a covariant transport representation $\mathscr {G}_0: \operatorname{\partial \Delta }^{n} \star \{ c\} \rightarrow \operatorname{\mathcal{QC}}$ for the cocartesian fibration $\pi$. Note that the value of $\mathscr {G}_0$ on the edge $e = \{ n\} \star \{ c\} \subseteq \operatorname{\partial \Delta }^{n} \star \{ c\}$ can be identified with the composition

\begin{eqnarray*} \mathscr {G}_0( \{ n\} ) & \simeq & \pi ^{-1} \{ n\} \\ & \xrightarrow {s} & \operatorname{Fun}_{ / e }^{\operatorname{CCart}}( e, e \times _{ \operatorname{\partial \Delta }^{n} \star \{ c\} } \operatorname{\mathcal{D}}) \\ & \xrightarrow {u} & \pi ^{-1} \{ c\} , \end{eqnarray*}

where $u$ is given by evaluation on the final vertex $\{ c\} \subseteq e$, and $s$ is a section of the trivial Kan fibration $\operatorname{Fun}_{ / e }^{\operatorname{CCart}}( e, e \times _{ \operatorname{\partial \Delta }^{n} \star \{ c\} }, \operatorname{\mathcal{D}}) \rightarrow \pi ^{-1} \{ n\}$ given by evaluation at the initial vertex $\{ n\} \subseteq e$. Using Proposition 5.3.7.11, we can identify $u$ with the restriction map $\operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }( \operatorname{\mathcal{C}}^{\triangleleft }, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$, which is an equivalence of $\infty$-categories (by assumption). It follows that the diagram $\mathscr {G}_0$ carries the edge $e$ to an isomorphism in the $\infty$-category $\operatorname{\mathcal{QC}}$. Identifying $\operatorname{\partial \Delta }^{n} \star \{ c\}$ with the outer horn $\Lambda ^{n+1}_{n+1}$ and applying Theorem 4.4.2.6, we deduce that $\mathscr {G}_0$ can be extended to a diagram $\mathscr {G}: \Delta ^{n} \star \{ c\} \rightarrow \operatorname{\mathcal{QC}}$.

Note that we have a commutative diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ ( \operatorname{\partial \Delta }^ n \star \operatorname{\mathcal{C}}) \times _{ (\operatorname{\partial \Delta }^{n} \star \{ c\} )} \operatorname{\mathcal{D}}\ar [rr]^{\operatorname{ev}} \ar [dr]^{\pi '} & & \overline{\operatorname{\mathcal{E}}}^{+} \ar [dl]^{ \overline{U}^{+} } \\ & \operatorname{\partial \Delta }^{n} \star \operatorname{\mathcal{C}}, & }$

where $\pi '$ is given given by projection onto the first factor and $\operatorname{ev}$ is the restriction of the evaluation map described in Construction 4.5.9.1. Note that $\operatorname{ev}$ carries $\pi '$-cocartesian edges of $( \operatorname{\partial \Delta }^ n \star \operatorname{\mathcal{C}}) \times _{ (\operatorname{\partial \Delta }^{n} \star \{ c\} )} \operatorname{\mathcal{D}}$ to $\overline{U}^{+}$-cocartesian edges of $\overline{\operatorname{\mathcal{E}}}^{+}$. Let $\overline{\operatorname{\mathcal{E}}}^{++}$ denote the relative join

$(\operatorname{\partial \Delta }^ n \star \operatorname{\mathcal{C}}) \times _{ (\operatorname{\partial \Delta }^{n} \star \{ c\} )} \operatorname{\mathcal{D}}) \star _{ \overline{\operatorname{\mathcal{E}}}^{+} } \overline{\operatorname{\mathcal{E}}}^{+}$

of Construction 5.2.3.1. Applying Lemma 5.2.3.17, we see that $\pi '$ and $\overline{U}^{+}$ induce a cocartesian fibration

$\overline{U}^{++}: \overline{\operatorname{\mathcal{E}}}^{++} \rightarrow (\operatorname{\partial \Delta }^{n} \star \operatorname{\mathcal{C}}) \star _{( \operatorname{\partial \Delta }^{n} \star \operatorname{\mathcal{C}})} (\operatorname{\partial \Delta }^{n} \star \operatorname{\mathcal{C}}) \simeq \Delta ^1 \times ( \operatorname{\partial \Delta }^{n} \star \operatorname{\mathcal{C}}).$

Applying Corollary 5.7.5.11, we deduce that $\overline{U}^{++}$ admits a covariant transport representation $\mathscr {H}_0: \Delta ^1 \times (\operatorname{\partial \Delta }^ n \star \operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{QC}}$ having the property that $\mathscr {H}_{0}|_{ \{ 0\} \times (\operatorname{\partial \Delta }^ n \star \operatorname{\mathcal{C}}) } = \mathscr {G}_0 \circ T_0$ and $\mathscr {H}_{0}|_{ \{ 1\} \times ( \operatorname{\partial \Delta }^ n \star \operatorname{\mathcal{C}})} = \mathscr {F}_0$. Note that, for $0 \leq i \leq n$, the evaluation map $\operatorname{ev}$ restricts to an isomorphism of $\infty$-categories $\{ i\} \times _{ (\operatorname{\partial \Delta }^ n \star \{ c\} ) } \operatorname{\mathcal{D}}\rightarrow \{ i\} \times _{ ( \operatorname{\partial \Delta }^ n \star \operatorname{\mathcal{C}})} \overline{\operatorname{\mathcal{E}}}^{+}$, so that the diagram $\mathscr {H}_{0}$ carries the edge $\Delta ^1 \times \{ i\}$ to an isomorphism in the $\infty$-category $\operatorname{\mathcal{QC}}$. Moreover, if $\sigma : \Delta ^{m} \rightarrow \Delta ^{n} \star \operatorname{\mathcal{C}}$ is any simplex which does not factor through $\operatorname{\partial \Delta }^{n} \star \operatorname{\mathcal{C}}$, then the vertex $\sigma (0)$ must belong to $\operatorname{\partial \Delta }^{n}$. Applying Proposition 4.4.5.8, we can extend $\mathscr {H}_0$ to a diagram $\mathscr {H}: \Delta ^1 \times ( \Delta ^ n \star \operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{QC}}$ satisfying $\mathscr {H}|_{ \{ 0\} \times ( \Delta ^ n \star \operatorname{\mathcal{C}})} = \mathscr {G} \circ T$. We complete the proof by observing that the restriction $\mathscr {F} = \mathscr {H}|_{ \{ 1\} \times ( \Delta ^ n \star \operatorname{\mathcal{C}}) }$ provides the desired extension of the diagram $\mathscr {F}_0$. $\square$

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.7.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.7.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.7.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.7.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$