Kerodon

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

Remark 8.6.1.14. In the situation of Proposition 8.6.1.13, suppose that $T$ exhibits $U^{\dagger }$ as a cartesian conjugate of $U$. Then we have the following stronger version condition of $(2'')$:

$(\ast )$

Let $f: X \rightarrow Y$ be an edge of $\operatorname{\mathcal{E}}^{\dagger }$. Set $\overline{X} = U^{\dagger }(X)$ and $\overline{Y} = U^{\dagger }(Y)$, so that $U^{\dagger }(f)$ can be identified with an edge $e: \overline{Y} \rightarrow \overline{X}$ of the simplicial set $\operatorname{\mathcal{C}}$. Then $f$ is $U^{\dagger }$-cartesian if and only if $T(f, e_{R} )$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{E}}_{ \overline{Y} }$.

The “only if” direction follows from Proposition 8.6.1.13. To prove the converse, choose a $2$-simplex $\sigma $ of $\operatorname{\mathcal{E}}^{\dagger }$ corresponding to a diagram

\[ \xymatrix@R =50pt@C=50pt{ & X' \ar [dr]^{f'} & \\ X \ar [rr]^{f} \ar [ur]^{u} & & Y } \]

of the simplicial set $\operatorname{\mathcal{E}}^{\dagger }$, where $U^{\dagger }(\sigma )$ is a left-degenerate $2$-simplex of $\operatorname{\mathcal{C}}^{\operatorname{op}}$ and $f'$ is $U^{\dagger }$-cartesian. We then obtain a $2$-simplex

\[ \xymatrix@R =50pt@C=50pt{ & T(X',f) \ar [dr]^{ T( f', e_ R ) } & \\ T(X,f) \ar [ur]^{ T_{\overline{Y} }(u) } \ar [rr]^{ T( f, e_{R} ) } & & T(Y, \operatorname{id}_{Y} ) } \]

in the $\infty $-category $\operatorname{\mathcal{E}}_{ \overline{Y} }$. If both $T( f, e_ R )$ and $T( f', e_ R )$ are isomorphisms, then $T_{ \overline{Y} }(u)$ is an isomorphism as well. Since the functor $T_{ \overline{Y} }: \operatorname{\mathcal{E}}^{\dagger }_{ \overline{Y} } \rightarrow \operatorname{\mathcal{E}}_{ \overline{Y} }$ is an equivalence of $\infty $-categories, we conclude that $u$ is an isomorphism in the $\infty $-category$ \operatorname{\mathcal{E}}^{\dagger }_{ \overline{Y} }$, so that $f$ is also $U^{\dagger }$-cartesian (see Remark 5.1.3.8).