Kerodon

Proof. Let $W$ be the collection of all morphisms $f$ of $\operatorname{\mathcal{E}}$ which satisfy conditions $(a)$ and $(b)$. We will show that $W$ satisfies the hypotheses of Lemma 6.2.3.11:

$(0)$

Every morphism $w: X \rightarrow Y$ belonging to $W$ is an $\operatorname{\mathcal{E}}'$-local equivalence. Fix an object $Z \in \operatorname{\mathcal{E}}'$; we wish to show that precomposition with $w$ induces a homotopy equivalence $\theta : \operatorname{Hom}_{\operatorname{\mathcal{E}}}(Y,Z) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{E}}}(X,Z)$. Let us abuse notation by identifying $\theta $ with the restriction map $\{ w\} \times _{ \operatorname{Hom}_{\operatorname{\mathcal{E}}}(X,Y) } \operatorname{Hom}_{\operatorname{\mathcal{E}}}(X,Y,Z) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{E}}}(X,Z)$, so that we have a commutative diagram of Kan complexes

\[ \xymatrix@R =50pt@C=45pt{ \{ f\} \times _{ \operatorname{Hom}_{\operatorname{\mathcal{E}}}(X,Y) } \operatorname{Hom}_{\operatorname{\mathcal{E}}}(X,Y,Z) \ar [r]^-{ \theta } \ar [d] & \operatorname{Hom}_{\operatorname{\mathcal{E}}}(X,Z) \ar [d] \\ \{ U(w) \} \times _{ \operatorname{Hom}_{\operatorname{\mathcal{C}}}( U(X), U(Y) ) } \operatorname{Hom}_{\operatorname{\mathcal{C}}}( U(X), U(Y), U(Z) ) \ar [r]^-{ \overline{\theta } } & \operatorname{Hom}_{\operatorname{\mathcal{C}}}( U(X), U(Z) ). } \]

Assumption $(a)$ guarantees that this diagram is a homotopy pullback square (Proposition 5.1.2.1), and assumption $(b)$ guarantees that $\overline{\theta }$ is a homotopy equivalence of Kan complexes. Applying Corollary 3.4.1.5, we conclude that $\theta $ is also a homotopy equivalence.

$(1)$

Every isomorphism of $\operatorname{\mathcal{E}}$ belongs to $W$: this follows from Proposition 5.1.1.9 and Remark 6.2.2.4.

$(2_{-})$

If $v: Y \rightarrow Z$ belongs to $W$ and there is a commutative diagram

\[ \xymatrix@C =50pt@R=50pt{ & Y \ar [dr]^{v} & \\ X \ar [ur]^{u} \ar [rr]^{w} & & Z, } \]

then $u$ belongs to $W$ if and only if $w$ belongs to $W$. This follows from Corollary 5.1.2.4 and Remark 6.2.2.5.

$(3)$

For every object $X \in \operatorname{\mathcal{E}}$, there exists a morphism $w: X \rightarrow Y$ which belongs to $W$, where $Y$ is contained in the subcategory $\operatorname{\mathcal{E}}'$. By virtue of our assumption that $U$ is a cocartesian fibration, it will suffice to show that there exists a $\operatorname{\mathcal{C}}'$-local equivalence $\overline{w}: U(X) \rightarrow \overline{Y}$, where $\overline{Y}$ is contained in $\operatorname{\mathcal{C}}'$ (we can then take $w$ to be a $U$-cocartesian lift of $\overline{f}$). This follows from our assumption that the subcategory $\operatorname{\mathcal{C}}' \subseteq \operatorname{\mathcal{C}}$ is reflective.

Proof. Let $X$ be an object of $\operatorname{\mathcal{E}}$ having image $C = U(X)$ in $\operatorname{\mathcal{C}}$. It follows from $(a)$ that there exists a $\operatorname{\mathcal{E}}'_{C}$-local equivalence $w: X \rightarrow Y$ in the $\infty $-category $\operatorname{\mathcal{E}}_{C}$, where $Y$ belongs to $\operatorname{\mathcal{E}}'_{C}$. To complete the proof, it will suffice to show that $w$ is a $\operatorname{\mathcal{E}}'$-local equivalence (and therefore exhibits $Y$ as a $\operatorname{\mathcal{E}}'$-localization of $X$). Fix an object $Z \in \operatorname{\mathcal{E}}'$ having image $D = U(Z)$ in $\operatorname{\mathcal{C}}$; we wish to show that precomposition with $w$ induces a homotopy equivalence $\theta : \operatorname{Hom}_{\operatorname{\mathcal{E}}}( Y, Z ) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{E}}}(X,Z)$. As in the proof of Proposition 6.2.4.1, we can identify $\theta $ with the upper horizontal map of a commutative diagram

where the lower horizontal map is a homotopy equivalence and the vertical maps are Kan fibrations (see Propositions 4.6.1.21 and 4.6.9.4). To show that this map is a homotopy equivalence, it will suffice to show that it restricts to a homotopy equivalence of vertical fibers over any vertex $\sigma \in \{ \operatorname{id}_{C} \} \times _{ \operatorname{Hom}_{\operatorname{\mathcal{C}}}( C,C) } \operatorname{Hom}_{\operatorname{\mathcal{C}}}( C,C,D )$ (Proposition 3.2.8.1). Since $\overline{\theta }$ is a homotopy equivalence, we may assume without loss of generality that $\sigma $ corresponds to a left-degenerate $2$-simplex of $\operatorname{\mathcal{C}}$, given by $s^{1}_{0}(f)$ for some morphism $f: C \rightarrow D$ in the $\infty $-category $\operatorname{\mathcal{C}}$. Replacing $\operatorname{\mathcal{E}}$ by the fiber product $\Delta ^1 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$, we are reduced to proving that $\theta $ is a homotopy equivalence in the special case where $\operatorname{\mathcal{C}}= \Delta ^1$, $C = 0$, and $D = 1$.

Let $f_{!}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ be a covariant transport functor for the cocartesian fibration $U$. Then we have a commutative diagram

where the horizontal maps are $U$-cocartesian. We therefore obtain a homotopy commutative diagram of morphism spaces

where the horizontal maps are homotopy equivalences (Corollary 5.1.2.3). Consequently, to show that $\theta $ is a homotopy equivalence, it will suffice to show that $f_{!}(w)$ is a $\operatorname{\mathcal{E}}'_{D}$-local equivalence in the $\infty $-category $\operatorname{\mathcal{E}}_{D}$, which follows from assumption $(b)$. $\square$

Proof of Proposition 6.2.4.4. Let $X$ be an object of $\operatorname{\mathcal{E}}$ having image $C = U(X)$ in $\operatorname{\mathcal{C}}$. It follows from $(a)$ that there exists a $\operatorname{\mathcal{E}}'_{C}$-local equivalence $w: X \rightarrow Y$ in the $\infty $-category $\operatorname{\mathcal{E}}_{C}$, where $Y$ belongs to $\operatorname{\mathcal{E}}'_{C}$. We will complete the proof by showing that $w$ is a $\operatorname{\mathcal{E}}'$-local equivalence (and therefore exhibits $Y$ as a $\operatorname{\mathcal{E}}'$-localization of $X$). Fix an object $Z \in \operatorname{\mathcal{E}}'$ having image $D = U(Z)$ in $\operatorname{\mathcal{C}}$; we wish to show that precomposition with $w$ induces a homotopy equivalence $\theta : \operatorname{Hom}_{\operatorname{\mathcal{E}}}( Y, Z ) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{E}}}(X,Z)$. As in the proof of Proposition 6.2.4.2, it suffices to prove this in the special case where $\operatorname{\mathcal{C}}= \Delta ^1$, with $C = 0$ and $D = 1$.

Invoking assumption $(b)$, we can choose a $U$-cartesian morphism $s: Z' \rightarrow Z$, where $Z' \in \operatorname{\mathcal{E}}'_{C}$. We then have a homotopy commutative diagram of Kan complexes

Since $s$ is $U$-cartesian, the horizontal maps are homotopy equivalences (Corollary 5.1.2.3). Consequently, to show that $\theta $ is a homotopy equivalence, it will suffice to show that the left vertical map is a homotopy equivalence. This follows immediately from our assumption that $w$ is a $\operatorname{\mathcal{E}}'_{C}$-local equivalence in the $\infty $-category $\operatorname{\mathcal{E}}_{C}$. $\square$

Proof. It follows from Corollary 5.3.7.3 that projection onto the second factor determines a cocartesian fibration $V: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}_{1}$. For each object $C \in \operatorname{\mathcal{C}}_1$, let $\operatorname{\mathcal{E}}_{C}$ denote the fiber $V^{-1} \{ C\} $, and define $\operatorname{\mathcal{E}}'_{C}$ similarly. We then have a pullback diagram of simplicial sets

Recall that the $\infty $-category $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ C\} $ has a final object, and the full subcategory spanned by the final objects is the homotopy fiber product $\operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{C}}}^{\mathrm{h}} \{ C\} $ (Proposition 4.6.7.22). It follows that $\operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{C}}}^{\mathrm{h}} \{ C\} $ is a reflective subcategory of $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ C\} $ (Example 6.2.2.10). Moreover, $\operatorname{\mathcal{E}}'_{C}$ is the inverse image of this reflective subcategory under the functor $U_{C}$. Our assumption that $F_0$ is a cocartesian fibration guarantees that $U_ C$ is also a cocartesian fibration. Applying Proposition 6.2.4.1, we deduce that $\operatorname{\mathcal{E}}'_{C}$ is a reflective subcategory of $\operatorname{\mathcal{E}}_{C}$. Moreover, a morphism $w$ of $\operatorname{\mathcal{E}}_{C}$ is a $\operatorname{\mathcal{E}}'_{C}$-local equivalence if and only if it is $U_{C}$-cocartesian: that is, if and only if $Q_{C}(w)$ is an $F_0$-cocartesian morphism in $\operatorname{\mathcal{C}}_0$.

Let $f: C \rightarrow D$ be a morphism in the $\infty $-category $\operatorname{\mathcal{C}}_{1}$, and let $f_{!}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ be given by covariant transport along $f$ (for the cocartesian fibration $V$). Since the projection map $\operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}_0$ carries $V$-cocartesian morphisms to isomorphisms (Corollary 5.3.7.3), the composition $Q_{D} \circ f_{!}$ is isomorphic to $Q_{C}$ in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{C}}_0 )$. It follows that the functor $f_{!}$ carries $\operatorname{\mathcal{E}}'_{C}$-local equivalences in $\operatorname{\mathcal{E}}_{C}$ to $\operatorname{\mathcal{E}}'_{D}$-local equivalences in $\operatorname{\mathcal{E}}_{D}$. Assertion $(1)$ now follows from Proposition 6.2.4.2, and assertion $(2)$ from Remark 6.2.4.3. $\square$

Proof. Combine Corollary 6.2.4.7, Example 5.1.1.3, and Corollary 5.3.7.3. $\square$