Kerodon

Proof. Let $X$ and $Y$ be objects of the $\infty $-category $\operatorname{\mathcal{C}}_{D}$. We then have a cubical diagram of Kan complexes

The front and back faces of this diagram are homotopy pullback squares (Remark 4.6.1.22), the comparison maps

are homotopy equivalences by virtue of our assumptions that $F$ and $\overline{F}$ are fully faithful, and the map of singletons $\{ \operatorname{id}_{D} \} \rightarrow \{ \operatorname{id}_{ \overline{F}(D) } \} $ is an isomorphism. Applying Corollary 3.4.1.12, we conclude that the comparison map $ \operatorname{Hom}_{\operatorname{\mathcal{C}}_ D}(X,Y) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}'_{\overline{F}(D)} }( F(X), F(Y) )$ is also a homotopy equivalence. $\square$

Proof. Let $\overline{v}: F(Y) \rightarrow F(X)$ be a homotopy inverse to $F(u)$. Since $F$ is fully faithful, the natural map $\operatorname{Hom}_{\operatorname{\mathcal{C}}}(Y, X) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{D}}}( F(Y), F(X))$ is a homotopy equivalence. We may therefore assume without loss of generality that $\overline{v} = F(v)$, for some morphism $v: Y \rightarrow X$ in the $\infty $-category $\operatorname{\mathcal{C}}$. Let $v \circ u$ be a composition of $u$ and $v$ in the $\infty $-category $\operatorname{\mathcal{C}}$. Since $F(u)$ is homotopy inverse to $F(v)$, the morphism $F( v \circ u)$ is homotopic to $\operatorname{id}_{ F(C) } = F( \operatorname{id}_{C} )$. Since the map $\operatorname{Hom}_{\operatorname{\mathcal{C}}}(X, X) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{D}}}( F(X), F(X))$ is a homotopy equivalence, it follows that $v \circ u$ is homotopic to $\operatorname{id}_{C}$: that is, $v$ is a left homotopy inverse to $u$. A similar argument (with the roles of $u$ and $v$ reversed) shows that $v$ is also a right homotopy inverse to $u$. It follows that $u$ is an isomorphism. $\square$

Proof. Fix objects $X,Y \in \operatorname{\mathcal{C}}^{\simeq }$. Our assumption that $F$ is fully faithful guarantees that the induced map $\theta : \operatorname{Hom}_{\operatorname{\mathcal{C}}}( X, Y) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{D}}}( F(X), F(Y) )$ is a homotopy equivalence of Kan complexes. By virtue of Proposition 4.6.2.9, $\theta $ restricts to a homotopy equivalence from the summand of $\operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y)$ spanned by the isomorphisms from $X$ to $Y$ to the summand of $\operatorname{Hom}_{\operatorname{\mathcal{D}}}( F(X), F(Y) )$ spanned by the isomorphisms from $F(X)$ to $F(Y)$. Unwinding the definitions, we conclude that $F^{\simeq }$ induces a homotopy equivalence $\operatorname{Hom}_{\operatorname{\mathcal{C}}^{\simeq }}( X, Y) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{D}}^{\simeq }}( F(X), F(Y) )$. $\square$

Proof. Since $f$ is essentially surjective, the underlying map of connected components $\pi _0(f): \pi _0(X) \rightarrow \pi _0(Y)$ is surjective. We claim that it is also injective. To prove this, suppose that $x$ and $x'$ are vertices of $X$ such that $f(x)$ and $f(x')$ belong to the same connected component of $Y$. Then the morphism space $\operatorname{Hom}_{Y}( f(x), f(x') )$ is nonempty. Since $f$ is fully faithful, it induces a homotopy equivalence $\operatorname{Hom}_{X}(x,x') \rightarrow \operatorname{Hom}_{Y}(f(x), f(x') )$. It follows that $\operatorname{Hom}_{X}(x,x')$ is nonempty, so that $x$ and $x'$ belong to the same connected component of $X$. This completes the proof that $\pi _0(f)$ is a bijection.

By virtue of Whitehead's theorem (Theorem 3.2.7.1), it will suffice to show that for every vertex $x \in X$ having image $y =f(x) \in Y$ and every integer $n \geq 0$, the induced map $\theta : \pi _{n+1}( X, x) \rightarrow \pi _{n+1}( Y, y)$ is an isomorphism. Using Example 4.6.1.13, we can identify $\theta $ with the natural map $\pi _{n}( \operatorname{Hom}_{X}(x,x), \operatorname{id}_{x} ) \rightarrow \pi _{n}( \operatorname{Hom}_{Y}(y,y), \operatorname{id}_{y} )$, which is bijective by virtue of our assumption that $f$ induces a homotopy equivalence $\operatorname{Hom}_{X}(x,x) \rightarrow \operatorname{Hom}_{Y}(y,y)$. $\square$

Proof of Theorem 4.6.2.20. Assume first that $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ is an equivalence of $\infty $-categories. Then $F$ induces a homotopy equivalence of Kan complexes $F^{\simeq }: \operatorname{\mathcal{C}}^{\simeq } \rightarrow \operatorname{\mathcal{D}}^{\simeq }$ (Remark 4.5.1.19). Passing to connected components, we conclude that the induced map $\pi _0( \operatorname{\mathcal{C}}^{\simeq } ) \rightarrow \pi _0( \operatorname{\mathcal{D}}^{\simeq } )$ is bijective. In particular, $F$ is essentially surjective. We have a commutative diagram of Kan complexes

where the horizontal maps are homotopy equivalences (Theorem 4.5.7.1) and the vertical maps are Kan fibrations (Corollary 4.4.5.4). Applying Proposition 3.2.8.1, we conclude that for every vertex $(X,Y) \in \operatorname{Fun}( \operatorname{\partial \Delta }^1, \operatorname{\mathcal{C}})^{\simeq }$, the induced map of fibers

is a homotopy equivalence. It follows that $F$ is fully faithful.

Now suppose that $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ is a functor of $\infty $-categories which is fully faithful and essentially surjective. Using Corollary 4.6.2.10 and Remark 4.6.2.14, we see that the induced map $F^{\simeq }: \operatorname{\mathcal{C}}^{\simeq } \rightarrow \operatorname{\mathcal{D}}^{\simeq }$ is also fully faithful and essentially surjective, and is therefore a homotopy equivalence of Kan complexes (Lemma 4.6.2.21). It follows that the morphism $\theta _0$ in (4.55) is a homotopy equivalence of Kan complexes. Combining our assumption that $F$ is fully faithful with Proposition 3.2.8.1, we conclude that $\theta $ is also a homotopy equivalence. Applying Theorem 4.5.7.1, we conclude that $F$ is an equivalence of $\infty $-categories. $\square$

Proof. Using Corollary 4.6.2.22, we can replace $\operatorname{\mathcal{C}}$ by its essential image and thereby reduce to the case where $F: \operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{D}}$ is the inclusion of a full subcategory. In this case, the induced map $\operatorname{Fun}(K, \operatorname{\mathcal{C}}) \xrightarrow {F \circ } \operatorname{Fun}(K,\operatorname{\mathcal{D}})$ is also the inclusion of a full subcategory, and therefore automatically fully faithful (Example 4.6.2.2). $\square$

Proof. Combine Corollary 4.6.2.22 with Exercise 4.4.1.13. $\square$