Kerodon

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

Lemma 5.1.5.5. Suppose we are given a commutative diagram of $\infty $-categories

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

where the functors $U$ and $U'$ are inner fibrations and the functors $F$ and $\overline{F}$ are fully faithful. Let $g: Y \rightarrow Z$ be a morphism in $\operatorname{\mathcal{C}}$. If $F(g)$ is a $U'$-cartesian morphism of $\operatorname{\mathcal{C}}'$, then $g$ is a $U$-cartesian morphism of $\operatorname{\mathcal{C}}$.

Proof. By virtue of Proposition 5.1.2.1, it will suffice to show that for every object $X \in \operatorname{\mathcal{C}}$, the diagram of Kan complexes

5.9
\begin{equation} \begin{gathered}\label{equation:fully-faithful-check-cartesian} \xymatrix@R =50pt@C=50pt{ \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y,Z) \times _{ \operatorname{Hom}_{\operatorname{\mathcal{C}}}(Y,Z) } \{ g\} \ar [r] \ar [d] & \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Z) \ar [d] \\ \operatorname{Hom}_{\operatorname{\mathcal{D}}}( U(X), U(Y), U(Z) ) \times _{ \operatorname{Hom}_{\operatorname{\mathcal{D}}}( U(Y), U(Z)) } \{ U(g) \} \ar [r] & \operatorname{Hom}_{\operatorname{\mathcal{D}}}( U(X), U(Z) ) } \end{gathered} \end{equation}

is a homotopy pullback square. Set $X' = F(X)$, $Y' = F(Y)$, $Z' = F(Z)$, and $g' = F(g)$. Since the functors $F$ and $\overline{F}$ are fully faithful, (5.9) is homotopy equivalent to the diagram

5.10
\begin{equation} \begin{gathered}\label{equation:fully-faithful-check-cartesian2} \xymatrix@R =50pt@C=25pt{ \operatorname{Hom}_{\operatorname{\mathcal{C}}'}(X',Y',Z') \times _{ \operatorname{Hom}_{\operatorname{\mathcal{C}}}(Y',Z') } \{ g'\} \ar [r] \ar [d] & \operatorname{Hom}_{\operatorname{\mathcal{C}}'}(X',Z') \ar [d] \\ \operatorname{Hom}_{\operatorname{\mathcal{D}}'}( U'(X'), U'(Y'), U'(Z') ) \times _{ \operatorname{Hom}_{\operatorname{\mathcal{D}}'}( U'(Y), U'(Z)) } \{ U'(g') \} \ar [r] & \operatorname{Hom}_{\operatorname{\mathcal{D}}'}( U'(X'), U'(Z') ). } \end{gathered} \end{equation}

Our assumption that $g'$ is $U'$-cartesian guarantees that (5.10) is a homotopy pullback square of Kan complexes (Proposition 5.1.2.1), so that (5.9) is also a homotopy pullback square (Corollary 3.4.1.10). $\square$