Kerodon

Proof of Lemma 7.4.4.3. Fix an $\infty $-category $\operatorname{\mathcal{D}}$; we wish to show that precomposition with $\widetilde{F}$ induces an equivalence of $\infty $-categories $\operatorname{Fun}( \operatorname{\mathcal{E}}[ W^{-1} ], \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}_0[W_0^{-1}], \operatorname{\mathcal{D}})$ (see Notation 6.3.1.1). Corollary 5.6.7.6 guarantees that $\widetilde{F}$ is a categorical equivalence of simplicial sets, so that precomposition with $\widetilde{F}$ induces an equivalence of $\infty $-categories $\operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{D}})$. It will therefore suffice to prove the following:

$(\ast )$

Let $G: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ be a morphism of simplicial sets with the property that $G \circ \widetilde{F}$ carries every $U_0$-cocartesian edge of $\operatorname{\mathcal{E}}_0$ to an isomorphism in $\operatorname{\mathcal{D}}$. Then $G$ carries each $U$-cocartesian edge of $\operatorname{\mathcal{E}}$ to an isomorphism in $\operatorname{\mathcal{D}}$.

Let us henceforth regard the $\infty $-category $\operatorname{\mathcal{D}}$ and the functor $G: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ as fixed. For every morphism of simplicial sets $K \rightarrow \operatorname{\mathcal{C}}$, let $\operatorname{\mathcal{E}}_{K}$ denote the fiber product $K \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$, let $U_{K}: \operatorname{\mathcal{E}}_{K} \rightarrow K$ be the projection map, and let $G_{K}$ denote the restriction of $G$ to $\operatorname{\mathcal{E}}_{K}$. Let us say that a monomorphism of simplicial sets $K' \hookrightarrow K$ is good if, for every morphism $K \rightarrow \operatorname{\mathcal{C}}$ with the property that $G_{K'}$ carries $U_{K'}$-cocartesian morphisms of $\operatorname{\mathcal{E}}_{K'}$ to isomorphisms in $\operatorname{\mathcal{D}}$, the morphism $G_{K}$ carries $U_{K}$-cocartesian morphisms of $\operatorname{\mathcal{E}}_{K}$ to isomorphisms in $\operatorname{\mathcal{D}}$. To prove $(\ast )$, it will suffice to show that $F: \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{\mathcal{C}}$ is weakly saturated. It is not difficult to see that the collection of good morphisms is weakly saturated, in the sense of Definition 1.5.4.12. It will therefore suffice to show that the horn inclusion $\Lambda ^{n}_{i} \hookrightarrow \Delta ^ n$ is good for $0 < i < n$. In other words, it will suffice to prove $(\ast )$ in the special case where $\operatorname{\mathcal{C}}= \Delta ^ n$ is a standard simplex and $F: \Lambda ^{n}_{i} \hookrightarrow \Delta ^ n$ is the inclusion of an inner horn.

If $n \geq 3$, then every edge of $\operatorname{\mathcal{C}}= \Delta ^ n$ is contained in the horn $\Lambda ^{n}_{i}$; it follows that the morphism $\widetilde{F}: \operatorname{\mathcal{E}}_0 \rightarrow \operatorname{\mathcal{E}}$ induces a bijection $W_0 \xrightarrow {\sim } W$, so there is nothing to prove. We may therefore assume without loss of generality that $n=2$. Let $w: X \rightarrow Z$ be a $U$-cocartesian of $\operatorname{\mathcal{E}}$ which does not belong to the simplicial subset $\operatorname{\mathcal{E}}_0 = \Lambda ^{2}_{1} \times _{\Delta ^2} \operatorname{\mathcal{E}}$, so that $U(X) = 0$ and $U(Z) = 2$. Since $U$ is a cocartesian fibration, we can choose a $U$-cocartesian morphism $u: X \rightarrow Y$ with $U(Y) = 1$. Our assumption that $u$ is $U$-cocartesian guarantees that there exists a $2$-simplex of $\operatorname{\mathcal{E}}'$ whose boundary is indicated in the diagram

Invoking Corollary 5.1.2.4, we see that $v$ is also $U$-cocartesian, so that $u$ and $v$ can be regarded as elements of $W_0$. It now suffices to observe that if $G: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ is any functor which carries both $u$ and $v$ to isomorphisms in $\operatorname{\mathcal{D}}$, then $G$ also carries $w$ to an isomorphism in $\operatorname{\mathcal{D}}$. $\square$