# Kerodon

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

Proposition 8.6.1.10. Let $\operatorname{\mathcal{C}}$ be a category and let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \mathbf{Cat}$ be a functor. Then, after passing to nerves, the functor

$T: ( \int ^{\operatorname{\mathcal{C}}^{\operatorname{op}} } \mathscr {F} ) \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \int _{\operatorname{\mathcal{C}}} \mathscr {F}$

of Construction 8.6.1.9 exhibits the forgetful functor $U^{\dagger }: \int ^{\operatorname{\mathcal{C}}^{\operatorname{op}}} \mathscr {F} \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ as a cartesian conjugate of the forgetful functor $U: \int _{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \operatorname{\mathcal{C}}$.

Proof. Condition $(0)$ of Definition 8.6.1.1 follows immediately from the construction. To verify condition $(1)$, we observe that for each object $C \in \operatorname{\mathcal{C}}$, the functor

$T_{C}: ( \int ^{\operatorname{\mathcal{C}}^{\operatorname{op}} } \mathscr {F} ) \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \{ C\} \rightarrow \{ C \} \times _{ \operatorname{\mathcal{C}}} ( \int _{\operatorname{\mathcal{C}}} \mathscr {F} )$

can be identified with the functor $\mathscr {F}( \operatorname{id}_{C} ): \mathscr {F}(C) \rightarrow \mathscr {F}(C)$. The identity constraint of $\mathscr {F}$ supplies an isomorphism of functors $\operatorname{id}_{ \mathscr {F}(C) } \xrightarrow {\sim } T_{C}$, so that $T_{C}$ is an equivalence of categories. To verify condition $(2)$, suppose we are given a morphism $e$ in the category $( \int ^{\operatorname{\mathcal{C}}^{\operatorname{op}} } \mathscr {F} ) \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}})$. We wish to show that, if the image of $e$ in the category $\int ^{\operatorname{\mathcal{C}}^{\operatorname{op}} } \mathscr {F}$ is $U^{\dagger }$-cartesian, then $T(e)$ is a $U$-cocartesian morphism in the category $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$. Writing $e = (f,f',u)$ and $T(e) = (f,v)$ as in Construction 8.6.1.9, we are reduced to showing that if $u$ is an isomorphism, then $v$ is also an isomorphism (Proposition 5.6.1.15), which is immediate from the construction. $\square$