Kerodon

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

Proposition 4.6.2.9. Suppose we are given a commutative diagram of $\infty $-categories

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}\ar [r]^-{F} \ar [d]^{q} & \operatorname{\mathcal{C}}' \ar [d]^{q'} \\ \operatorname{\mathcal{D}}\ar [r]^-{\overline{F}} & \operatorname{\mathcal{D}}'. } \]

Assume that the functors $q$ and $q'$ are inner fibrations and that the functors $F$ and $\overline{F}$ are fully faithful. Then, for every object $D \in \operatorname{\mathcal{D}}$, the induced functor $F_{D}: \operatorname{\mathcal{C}}_{D} \rightarrow \operatorname{\mathcal{C}}'_{ \overline{F}(D) }$ is fully faithful.

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

\[ \xymatrix@R =50pt@C=10pt{ \operatorname{Hom}_{\operatorname{\mathcal{C}}_ D}(X,Y) \ar [rr] \ar [dd] \ar [dr] & & \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y) \ar [dr] \ar [dd] & \\ & \operatorname{Hom}_{\operatorname{\mathcal{C}}'_{\overline{F}}(D)}( F(X), F(Y) ) \ar [rr] \ar [dd] & & \operatorname{Hom}_{ \operatorname{\mathcal{C}}' }( F(X), F(Y) ) \ar [dd] \\ \{ \operatorname{id}_{D} \} \ar [rr] \ar [dr] & & \operatorname{Hom}_{\operatorname{\mathcal{D}}}(D,D) \ar [dr] & \\ & \{ \operatorname{id}_{ \overline{F}(D) } \} \ar [rr] & & \operatorname{Hom}_{\operatorname{\mathcal{D}}'}( \overline{F}(D), \overline{F}(D) ). } \]

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

\[ \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{D}}}(F(X), F(Y) ) \quad \quad \operatorname{Hom}_{\operatorname{\mathcal{D}}}(D,D) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{D}}}( \overline{F}(D), \overline{F}(D) ) \]

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$