Kerodon

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

Proposition 8.6.1.12. Let $\operatorname{\mathcal{C}}$ be a category equipped with a functor $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{QCat}$, let $U: \operatorname{N}_{\bullet }^{\mathscr {F}}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ denote the cocartesian fibration of Corollary 5.3.3.16, and define $U^{\dagger }: {\operatorname{N}_{\bullet }^{\mathscr {F}^{\operatorname{op}} }(\operatorname{\mathcal{C}})}^{\operatorname{op}} \rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})^{\operatorname{op}}$ similarly. Then the functor

\[ T: {\operatorname{N}_{\bullet }^{\mathscr {F}^{\operatorname{op}} }(\operatorname{\mathcal{C}})}^{\operatorname{op}} \times _{ \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}})^{\operatorname{op}} } \operatorname{Tw}( \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) ) \rightarrow \operatorname{N}_{\bullet }^{\mathscr {F}}(\operatorname{\mathcal{C}}) \]

of Construction 8.6.1.11 exhibits $U^{\dagger }$ as a cartesian conjugate of $U$.

Proof. Condition $(0)$ of Definition 8.6.1.1 follows immediately from the construction. Condition $(1)$ follows from the observation that, for each object $C \in \operatorname{\mathcal{C}}$, the induced map

\[ T_{C}: {\operatorname{N}_{\bullet }^{\mathscr {F}^{\operatorname{op}} }(\operatorname{\mathcal{C}})}^{\operatorname{op}} \times _{ \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}})^{\operatorname{op}} } \{ C\} \rightarrow \{ C\} \times _{ \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}) } \operatorname{N}_{\bullet }^{\mathscr {F}}(\operatorname{\mathcal{C}}) \]

is an isomorphism of simplicial sets (under the identifications supplied by Example 5.3.3.8, it corresponds to the identity functor from the $\infty $-category $\mathscr {F}(C)$ to itself). Condition $(2)$ follows from the characterization of $U$-cocartesian and $U^{\dagger ,\operatorname{op}}$-cocartesian morphisms given in Corollary 5.3.3.16. $\square$