Kerodon

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

Corollary 5.7.6.20. Suppose we are given a commutative diagram of $\infty $-categories

\[ \xymatrix { \operatorname{\mathcal{D}}\ar [rr]^{F} \ar [dr]^{U} & & \operatorname{\mathcal{E}}\ar [dl]_{V} \\ & \operatorname{\mathcal{C}}& } \]

where $U$ and $V$ are left fibrations. Let $\widetilde{X} \in \operatorname{\mathcal{D}}$ be an initial object. Then $F$ is an equivalence of $\infty $-categories if and only if $F(\widetilde{X})$ is an initial object of $\operatorname{\mathcal{E}}$.

Proof. If $F$ is an equivalence of $\infty $-categories, then it carries initial objects to initial objects by virtue of Corollary 4.6.6.21. Conversely, suppose that $F( \widetilde{X} )$ is an initial object of $\operatorname{\mathcal{E}}$; we wish to show that $F$ is an equivalence of $\infty $-categories. Set $X = U( \widetilde{X} )$. Applying Proposition 5.7.6.19, we deduce that there is a functor $G \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}, \operatorname{\mathcal{D}})$ such that $(G \circ F)( \widetilde{X} )$ is isomorphic to $\widetilde{X}$ as an object of the $\infty $-category $\operatorname{\mathcal{D}}_{X} = \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}$. Applying Proposition 5.7.6.19 again, we deduce that $G \circ F$ is isomorphic to $\operatorname{id}_{\operatorname{\mathcal{D}}}$ as an object of the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{D}}, \operatorname{\mathcal{D}})$; in particular, $F$ is a right homotopy inverse to $G$. Since $G$ carries $F( \widetilde{X} )$ to an initial object of $\operatorname{\mathcal{D}}$, we can apply the same argument (with the roles of $\operatorname{\mathcal{D}}$ and $\operatorname{\mathcal{E}}$ reversed) to show that $G$ has a left homotopy inverse. It follows that $G$ is an equivalence of $\infty $-categories, so that $F$ is also an equivalence of $\infty $-categories. $\square$