Kerodon

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

Lemma 6.2.3.5. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets and let $g: Y \rightarrow Z$ be an edge of $\operatorname{\mathcal{E}}$. Then $g$ is $U$-cartesian if and only if it is locally $U$-cartesian.

Proof. By virtue of Remark 5.1.1.13, we may assume without loss of generality that $\operatorname{\mathcal{C}}= \Delta ^ n$ is a standard simplex. For $0 \leq i \leq n$, let $\operatorname{\mathcal{E}}_{i}$ denote the fiber $\{ i\} \times _{\Delta ^ n} \operatorname{\mathcal{E}}$, which we regard as a full subcategory of $\operatorname{\mathcal{E}}$. Set $j = U(Y)$ and $k = U(Z)$. We wish to show that, for every integer $0 \leq i \leq j$ and every object $X \in \operatorname{\mathcal{E}}_{i}$, composition with the homotopy class $[g]$ induces an isomorphism $\operatorname{Hom}_{\operatorname{\mathcal{E}}}( X, Y) \xrightarrow { [g] \circ } \operatorname{Hom}_{\operatorname{\mathcal{E}}}(X,Z)$ in the homotopy category of Kan complexes $\mathrm{h} \mathit{\operatorname{Kan}}$ (see Corollary 5.1.2.3). Since $U$ is a cocartesian fibration, we can choose a $U$-cocartesian morphism $f: X \rightarrow X'$, where $X'$ belongs to $\operatorname{\mathcal{E}}_{j}$. We conclude by observing that there is a commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Hom}_{\operatorname{\mathcal{E}}}(X', Y) \ar [r]^-{[g] \circ }_{\sim } \ar [d]^{ \circ [f]}_{\sim }& \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X', Z) \ar [d]^{\circ [f]}_{\sim } \\ \operatorname{Hom}_{\operatorname{\mathcal{E}}}( X, Y) \ar [r]^-{ [g] \circ } & \operatorname{Hom}_{\operatorname{\mathcal{E}}}(X, Z) } \]

in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$, where the upper horizontal map is an isomorphism by virtue of our assumption that $g$ is locally $U$-cartesian, and the vertical maps are isomorphisms by virtue of our assumption that $f$ is $U$-cocartesian (Corollary 5.1.2.3). $\square$