# Kerodon

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

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$