Kerodon

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

Lemma 8.3.7.4. The morphism $U_{-}: \operatorname{\mathcal{E}}_{-} \rightarrow \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times ( \operatorname{\mathcal{C}}_{-} \vec{\times }_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}})$ is a left fibration, with covariant transport representation given by the composition

\[ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times ( \operatorname{\mathcal{C}}_{-} \vec{\times }_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{C}}_{-} \xrightarrow { \operatorname{Hom}_{ \operatorname{\mathcal{C}}_{-} }( \bullet , \bullet ) } \operatorname{\mathcal{S}}. \]

Similarly, $U_{+}$ is a left fibration with covariant transport representation given by the composition

\[ ( \operatorname{\mathcal{C}}_{+}^{\operatorname{op}} \vec{\times }_{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{\mathcal{C}}^{\operatorname{op}} ) \times \operatorname{\mathcal{C}}_{+} \rightarrow \operatorname{\mathcal{C}}_{+}^{\operatorname{op}} \times \operatorname{\mathcal{C}}_{+} \xrightarrow { \operatorname{Hom}_{\operatorname{\mathcal{C}}_{+}}( \bullet , \bullet )} \operatorname{\mathcal{S}}. \]

Proof. Projection onto the first factor determines morphism $\operatorname{\mathcal{E}}_{-} \subseteq \operatorname{Tw}(\operatorname{\mathcal{C}}_{-}) \vec{\times }_{ \operatorname{Tw}(\operatorname{\mathcal{C}}) } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{Tw}(\operatorname{\mathcal{C}}_{-})$ which fits into a commutative diagram

8.59
\begin{equation} \begin{gathered}\label{equation:E-plusminus-covariant-transport} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}_{-} \ar [d]^{ U_{-} } \ar [r] & \operatorname{Tw}(\operatorname{\mathcal{C}}_{-} ) \ar [d] \\ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times ( \operatorname{\mathcal{C}}_{-} \vec{\times }_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}) \ar [r] & \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{C}}_{-}. } \end{gathered} \end{equation}

To prove the first assertion, it will suffice to show that the diagram (8.59) induces a trivial Kan fibration

\[ \theta _{-}: \operatorname{\mathcal{E}}_{-} \rightarrow ( \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} \times ( \operatorname{\mathcal{C}}_{-} \vec{\times }_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}) ) \times _{ ( \operatorname{\mathcal{C}}^{\operatorname{op}}_{-} \times \operatorname{\mathcal{C}}_{-} )} \operatorname{Tw}(\operatorname{\mathcal{C}}_{-} ). \]

Unwinding the definitions, we see that $\theta _{-}$ is a pullback of the map

\[ \overline{\theta }_{-}: \operatorname{Fun}( \Delta ^1, \operatorname{Tw}(\operatorname{\mathcal{C}}) ) \rightarrow \operatorname{Fun}( \{ 0\} , \operatorname{Tw}(\operatorname{\mathcal{C}}) ) \times _{ \operatorname{Fun}( \{ 0\} , \operatorname{\mathcal{C}}^{\operatorname{op}} \times \operatorname{\mathcal{C}}) } \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}^{\operatorname{op}} \times \operatorname{\mathcal{C}}) \]

induced by the projection map $\lambda : \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}} \times \operatorname{\mathcal{C}}$. Since $\lambda $ is a left fibration (Proposition 8.1.1.11), the morphism $\overline{\theta }_{-}$ is a trivial Kan fibration (Proposition 4.2.6.1), so that $\theta _{-}$ is also a trivial Kan fibration. The proof of the second assertion is similar. $\square$