Kerodon

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

7.3.3 Proof of the Diffraction Criterion

The goal of this section is to prove Theorem 7.3.1.8. Our proof will require a relative version of the construction described in Notation 7.3.1.1.

Notation 7.3.3.1 (Cocartesian Direct Images). Let $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ and $V: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ be morphisms of simplicial sets, and let $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}})$ be the simplicial set of Construction 7.3.2.1. Using Remark 7.3.2.8, we can identify vertices of the simplicial set $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}})$ with pairs $(C, F)$, where $C$ is a vertex of $\operatorname{\mathcal{C}}$ and

$F: \operatorname{\mathcal{D}}_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}\rightarrow \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}= \operatorname{\mathcal{E}}_{C}$

is a section of the map $V|_{\operatorname{\mathcal{E}}_ C}: \operatorname{\mathcal{E}}_ C \rightarrow \operatorname{\mathcal{D}}_{C}$. If $V$ is a cocartesian fibration, we let $\operatorname{Res}^{\operatorname{CCart}}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}})$ denote the full simplicial subset of $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}})$ spanned by those vertices $(C,F)$ where $F$ carries each edge of $\operatorname{\mathcal{D}}_{C}$ to $V_{C}$-cocartesian edge of $\operatorname{\mathcal{E}}_{C}$. We will refer to $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}})$ as the cocartesian direct image of $\operatorname{\mathcal{E}}$ along $U$.

Remark 7.3.3.2. Let $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be a morphism of simplicial sets and let $V: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ be a cocartesian fibration of simplicial sets. Then the projection map $\pi : \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}}$ restricts to a projection map $\pi ^{\operatorname{CCart}}: \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}}$. Moreover, for each vertex $C \in \operatorname{\mathcal{C}}$, the isomorphism $\{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}) \simeq \operatorname{Fun}_{ / \operatorname{\mathcal{D}}_ C }( \operatorname{\mathcal{D}}_ C, \operatorname{\mathcal{E}}_ C )$ of Remark 7.3.2.8 restricts to an isomorphism of full subcategories $\{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{E}}) \simeq \operatorname{Fun}^{\operatorname{CCart}}_{/\operatorname{\mathcal{D}}_ C }( \operatorname{\mathcal{D}}_ C, \operatorname{\mathcal{E}}_ C )$.

Proposition 7.3.3.3. Let $V: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ be a cocartesian fibration of simplicial sets, let $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be a cartesian fibration of simplicial sets. Then:

$(1)$

The projection map $\pi : \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}}$ is a cocartesian fibration of simplicial sets.

$(2)$

Let $e: X \rightarrow Y$ be a $\pi$-cocartesian edge of the simplicial set $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}})$. If $X$ belongs to the simplicial subset $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}})$, then $Y$ also belongs to the simplicial subset $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}})$.

$(3)$

The morphism $\pi$ restricts to a cocartesian fibration $\pi ^{\operatorname{CCart}}: \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}}$.

$(4)$

An edge of the simplicial set $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}})$ is $\pi ^{\operatorname{CCart}}$-cocartesian if and only if it is $\pi$-cocartesian.

Proof. Assertion $(1)$ follows from Proposition 7.3.2.20 (after passing to opposite simplicial sets). To prove $(2)$, we may assume without loss of generality that $\operatorname{\mathcal{C}}= \Delta ^1$ and $\pi (e)$ is the nondegenerate edge of $\operatorname{\mathcal{C}}$. In this case, the simplicial sets $\operatorname{\mathcal{D}}$ and $\operatorname{\mathcal{E}}$ are $\infty$-categories, and we can identify the edge $e$ with a morphism of simplicial sets $E: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ satisfying $V \circ E = \operatorname{id}_{\operatorname{\mathcal{D}}}$. Let $u: D \rightarrow D'$ be a morphism in the $\infty$-category $\operatorname{\mathcal{D}}_1 = \{ 1\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$; we wish to show that $E(u)$ is a $V$-cocartesian morphism of $\operatorname{\mathcal{E}}$. To prove this, let $G: \operatorname{\mathcal{D}}_{1} \rightarrow \operatorname{\mathcal{D}}_0 = \{ 0\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$ be given by contravariant transport along the nondegenerate edge of $\operatorname{\mathcal{C}}$, so that we have a commutative diagram

$\xymatrix@R =50pt@C=50pt{ G(D) \ar [d]^{ G(u) } \ar [r] & D \ar [d]^{u} \\ G(D') \ar [r] & D', }$

in the $\infty$-category where the horizontal maps are $U$-cartesian. Our assumption that $e$ is $\pi$-cocartesian guarantees that the functor $E$ carries $U$-cartesian morphisms of $\operatorname{\mathcal{D}}$ to $V$-cocartesian morphisms of $\operatorname{\mathcal{E}}$ (Proposition 7.3.2.20). We therefore obtain a commutative diagram

$\xymatrix@R =50pt@C=50pt{ (E \circ G)(D) \ar [d]^{ (E \circ G)(u) } \ar [r] & E(D) \ar [d]^{ E(u) } \\ (E \circ G)(D') \ar [r] & E(D' ), }$

where the horizontal maps are $V$-cocartesian. By virtue of Corollary 5.1.2.4, it will suffice to show that the morphism $(E \circ G)(u)$ is $V$-cocartesian, which follows from our assumption that $X$ belongs to $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}})$. This completes the proof of $(2)$; assertions $(3)$ and $(4)$ then follow by applying Proposition 5.1.4.16. $\square$

In the situation of Proposition 7.3.3.3, the cocartesian direct image $\operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}})$ can be characterized by a universal property:

Proposition 7.3.3.4. Let $V: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ be a cocartesian fibration of simplicial sets and let $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be a cartesian fibration of simplicial sets. For every cocartesian fibration of simplicial sets $W: \operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{C}}$, the isomorphism

$\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}', \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}) ) \xrightarrow {\sim } \operatorname{Fun}_{/\operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}})$

of Remark 7.3.2.3 restricts to an isomorphism of full simplicial subsets

$\operatorname{Fun}^{\operatorname{CCart}}_{/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}', \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}) ) \xrightarrow {\sim } \operatorname{Fun}^{\operatorname{CCart}}_{/\operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}}).$

Proof. Let $\pi : \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}}$ denote the projection map and let $f: \operatorname{\mathcal{C}}' \rightarrow \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}})$ be a morphism satisfying $\pi \circ f = W$, corresponding to a morphism of simplicial sets $F: \operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ for which $V \circ F$ is given by projection to the second factor. Note that we can regard $F$ as a vertex of the simplicial subset $\operatorname{Fun}^{\operatorname{CCart}}_{/\operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}})$ if and only if it satisfies the following condition:

$(a)$

For every edge $(e',e)$ of the fiber product $\operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$ for which $e'$ is a $W$-cocartesian edge of $\operatorname{\mathcal{C}}'$, the image $F(e',e)$ is a $V$-cocartesian edge of $\operatorname{\mathcal{E}}$.

We wish to show that $(a)$ is equivalent to the following pair of conditions:

$(b)$

The morphism $f$ factors through the full simplicial subset $\operatorname{Res}^{\operatorname{CCart}}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}) \subseteq \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}})$. In other words, for every edge $(e',e)$ of the fiber product $\operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$ for which $e'$ is a degenerate edge of $\operatorname{\mathcal{C}}'$, the image $F(e',e)$ is a $V$-cocartesian edge of $\operatorname{\mathcal{E}}$.

$(c)$

For every $W$-cocartesian edge $e'$ of $\operatorname{\mathcal{C}}'$, the image $f(e')$ is a $\pi |_{ \operatorname{Res}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}) }$-cocartesian edge of $\operatorname{Res}^{\operatorname{CCart}}_{\operatorname{\mathcal{D}}/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}})$. By virtue of Propositions 7.3.3.3 and 7.3.2.20, this is equivalent to the assertion that for every edge $(e',e)$ of the fiber product $\operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$ where $e'$ is $W$-cocartesian and $e$ is $U$-cartesian, the image $F(e',e)$ is a $V$-cocartesian edge of $\operatorname{\mathcal{E}}$.

The implications $(a) \Rightarrow (b)$ and $(a) \Rightarrow (c)$ are clear. For the converse, suppose that $(b)$ and $(c)$ are satisfied; we wish to prove $(a)$. Let $(e',e): (X',X) \rightarrow (Z',Z)$ be an edge of the fiber product $\operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$, where $e': X' \rightarrow Z'$ is $W$-cocartesian. Let $\overline{e} = U(e) = W(e')$ denote the corresponding edge of $\operatorname{\mathcal{C}}$. Since $U$ is a cartesian fibration, there exists a $U$-cartesian morphism $f: Y \rightarrow Z$ satisfying $U(f) = \overline{e}$. Let $\overline{\sigma }$ denote the left-degenerate $2$-simplex $s_0(\overline{e})$. Since $f$ is $U$-cartesian, we can lift $\overline{\sigma }$ to a $2$-simplex of $\operatorname{\mathcal{D}}$ as indicated in the diagram

$\xymatrix@R =50pt@C=50pt{ & Y \ar [dr]^{f} & \\ X \ar [ur] \ar [rr]^{e} & & Z. }$

Writing $\sigma '$ for the left-degenerate $2$-simplex $s_0(e')$ of $\operatorname{\mathcal{C}}'$, we obtain a $2$-simplex $\tau = F( \sigma ', \sigma )$ of $\operatorname{\mathcal{E}}$. It follows from assumption $(b)$ that the restriction $\tau |_{ \operatorname{N}_{\bullet }( \{ 0 < 1\} ) }$ is a $V$-cocartesian edge of $\operatorname{\mathcal{E}}$, and from assumption $(c)$ that the restriction $\tau |_{ \operatorname{N}_{\bullet }( \{ 1 < 2 \} ) }$ is a $V$-cocartesian edge of $\operatorname{\mathcal{E}}$. Applying Proposition 5.1.4.12, we conclude that $F(e',e) = \tau |_{ \operatorname{N}_{\bullet }( \{ 0 < 2 \} ) }$ is also a $V$-cocartesian edge of $\operatorname{\mathcal{E}}$. $\square$

We are now ready to prove a special case of Theorem 7.3.1.8 (which is sufficient for most of our applications).

Proposition 7.3.3.5. 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.6.4.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\}$ (see Exercise 5.2.4.20). 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}}= \operatorname{Res}^{\operatorname{CCart}}_{ \operatorname{\partial \Delta }^{n} \star \operatorname{\mathcal{C}}/ \operatorname{\partial \Delta }^{n} \star \{ c\} }( \overline{\operatorname{\mathcal{E}}}^{+} )$, so that the projection map $\pi : \operatorname{\mathcal{D}}\rightarrow \operatorname{\partial \Delta }^{n} \star \{ c\}$ is a cocartesian fibration of simplicial sets (Proposition 7.3.3.3).

Applying Corollary 5.6.2.10, 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 7.3.3.4, 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 7.3.2.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.4.1. Applying Lemma 5.2.4.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.6.2.9, 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.3.1.8. 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.4.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 (Corollary 7.3.1.11). It follows that $\theta '$ is also an equivalence of $\infty$-categories.

Using Corollary 5.6.2.9, 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.3.3.5 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.3.1.16, 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.2.9, 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$