Kerodon

Proof. For every morphism of simplicial sets $S \rightarrow \operatorname{\mathcal{C}}$, we can apply Construction 7.4.1.13 to the left fibration $S \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow S$ to obtain a comparison map

Let us say that $S$ is good if the morphism $T_{S}$ is a homotopy equivalence. We now proceed in several steps.

$(a)$

Let $S = \{ C\} $ be a vertex of the simplicial set $\operatorname{\mathcal{C}}$. In this case, $T_{S}$ agrees with the comparison map $\alpha _{C}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}( \Delta ^0, \mathscr {F}(C) )$ appearing in Definition 7.4.1.8, which is a homotopy equivalence by virtue of our assumption on $\alpha $.

$(b)$

The construction of $T_{S}$ depends functorially on $S$: that is, if we are given a morphism $f: S' \rightarrow S$ in $(\operatorname{Set_{\Delta }})_{ / \operatorname{\mathcal{C}}}$, then the diagram of Kan complexes

7.47

\begin{equation} \begin{gathered}\label{equation:witness-vs-sections0} \xymatrix { \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}(S, \operatorname{\mathcal{E}}) \ar [r] \ar [d]^{T_ S} & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}(S', \operatorname{\mathcal{E}}) \ar [d]^{ T_{S'} } \\ \operatorname{Hom}_{ \operatorname{Fun}(S,\operatorname{\mathcal{C}}) }( \underline{\Delta ^{0}}_{S}, \mathscr {F}|_{S} ) \ar [r] & \operatorname{Hom}_{ \operatorname{Fun}(S',\operatorname{\mathcal{C}}) }( \underline{\Delta ^{0}}_{S'}, \mathscr {F}|_{S'} ) } \end{gathered} \end{equation}

is commutative. For the upper horizontal map, this follows from Corollaries 4.2.5.2 and Corollary 4.4.3.8.

$(c)$

Let $S = \Delta ^ n$ be a standard simplex and let $S' = \{ 0\} $ be its initial vertex, so that the inclusion $S' \hookrightarrow S$ is left anodyne (Corollary 4.2.4.11). Then horizontal maps appearing in (7.47) are homotopy equivalences. For the upper horizontal map this follows from Proposition 4.2.5.4, and for the lower horizontal map it follows from Proposition 7.3.6.7. Combining this observation with $(a)$, we conclude that $S$ is good.

$(d)$

The construction $S \mapsto T_{S}$ carries coproducts in the category $(\operatorname{Set_{\Delta }})_{ / \operatorname{\mathcal{C}}}$ to products in the category $\operatorname{Fun}( [1], \operatorname{Kan})$. Consequently, the collection of good simplicial sets is closed under coproducts.

$(e)$

Suppose we are given a pushout square

7.48

\begin{equation} \begin{gathered}\label{equation:witness-vs-section} \xymatrix { S \ar [r] \ar [d] & S_0 \ar [d] \\ S_1 \ar [r] & S_{01} } \end{gathered} \end{equation}

in the category $(\operatorname{Set_{\Delta }})_{ / \operatorname{\mathcal{C}}}$. Then the induced diagram

7.49

\begin{equation} \begin{gathered}\label{equation:witness-vs-section2} \xymatrix { T_{S} & T_{ S_0 } \ar [l] \\ T_{ S_1 } \ar [u] & T_{S_{01}} \ar [l] \ar [u] } \end{gathered} \end{equation}

is a pullback square in the category $\operatorname{Fun}( [1], \operatorname{Kan})$. Moreover, if the horizontal maps in the diagram (7.48) are monomorphisms, then (7.49) is a (levelwise) homotopy pullback square: this follows from $(b)$ and Example 3.4.1.3. Consequently, if $S$, $S_{0}$, and $S_{1}$ are good, then $S$ is also good (see Corollary 3.4.1.12).

$(f)$

Let $S$ be a simplicial set of dimension $\leq k$, for some integer $k \geq -1$. To prove this, we proceed by induction on $k$. If $k = -1$, then $S = \emptyset $ and the statement is clear. To handle the general case, let $S' = \operatorname{sk}_{n-1}(S)$ denote the $(n-1)$-skeleton of $S$, so that Proposition 1.1.4.12 supplies a pushout square

\[ \xymatrix { \coprod \operatorname{\partial \Delta }^{k} \ar [r] \ar [d] & \coprod \Delta ^{k} \\ S' \ar [r] & S, } \]

where the horizontal maps are monomorphisms. It follows from our inductive hypothesis that $S'$ and $\coprod \operatorname{\partial \Delta }^{k}$ are good. By virtue of $(e)$, we are reduced to showing that the coproduct $\coprod \Delta ^ k$ is good, which follows from $(c)$ and $(d)$.

We now complete the proof by showing that every object $S \in (\operatorname{Set_{\Delta }})_{/\operatorname{\mathcal{C}}}$ is good. Note that $T_{S}$ can be realized as the limit of a tower

where the horizontal maps are Kan fibrations. Consequently, to show that $T_{S}$ is a homotopy equivalence, it will suffice to show that $T_{ \operatorname{sk}_{k}(S) }$ is a homotopy equivalence for every integer $k \geq 0$ (see Example 4.5.6.18), which follows from $(f)$. $\square$