Kerodon

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

Remark 7.4.3.5. Suppose we are given a pullback diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [d]^{U} \ar [r] & \overline{\operatorname{\mathcal{E}}} \ar [d]^{ \overline{U} } \\ \operatorname{\mathcal{C}}\ar [r] & \operatorname{\mathcal{C}}^{\triangleright }, }$

where $U$ and $\overline{U}$ are cocartesian fibrations. Let ${\bf 1}$ denote the cone point of $\operatorname{\mathcal{C}}^{\triangleright }$ and let $\mathrm{Rf}: \operatorname{\mathcal{E}}\rightarrow \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ be a covariant refraction diagram. For every $U$-cocartesian edge $e: X \rightarrow Y$ of $\operatorname{\mathcal{E}}$, the image $U(e)$ is an isomorphism in the $\infty$-category $\overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$. To prove this, we observe that there is a morphism $\Delta ^1 \times \Delta ^1 \rightarrow \overline{\operatorname{\mathcal{E}}}$ as indicated in the diagram

$\xymatrix@R =50pt@C=50pt{ X \ar [r] \ar [d]^{e} & \mathrm{Rf}(X) \ar [d]^{\mathrm{Rf}(e) } \\ Y \ar [r] & \mathrm{Rf}(Y), }$

where the horizontal maps are $\overline{U}$-cocartesian. Applying Proposition 5.1.4.12, we deduce that $\mathrm{Rf}(e)$ is an $\overline{U}$-cocartesian edge of $\overline{\operatorname{\mathcal{E}}}$, and therefore an isomorphism in the $\infty$-category $\overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ (Proposition 5.1.4.11).