Kerodon

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

Corollary 7.3.5.7. Let $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be a cartesian fibration of $\infty $-categories. Suppose that, for every object $C \in \operatorname{\mathcal{C}}$, the fiber $\operatorname{\mathcal{D}}_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$ has an initial object. Then the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ has an initial object. Moreover, an object $F \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ is initial if and only if it satisfies the following condition:

$(\ast )$

For each object $C \in \operatorname{\mathcal{C}}$, the image $F(C)$ is an initial object of $\operatorname{\mathcal{D}}_{C}$.

Proof. Since $U$ is a cartesian fibration, an object $D \in \operatorname{\mathcal{D}}$ is $U$-initial if and only if it is initial when viewed as an object of the $\infty $-category $\operatorname{\mathcal{D}}_{C}$ for $C = U(D)$ (Corollary 7.1.5.21). It follows from Example 7.3.5.6 that there exists a functor $F \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ which satisfies condition $(\ast )$. Proposition 7.1.7.12 then guarantees that $F$ is an initial object of $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$. Any other initial object of $\operatorname{Fun}_{ /\operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ is isomorphic to $F$, and therefore also satisfies condition $(\ast )$. $\square$