Kerodon

Proof. Note that we have a commutative diagram

where the vertical maps are left fibrations (Propositions 4.3.6.1 and 8.1.1.11). For every object $C \in \operatorname{\mathcal{C}}$, set $X(K) = \operatorname{\mathcal{C}}_{f/} \times _{ \operatorname{\mathcal{C}}} \{ C\} $ and $Y(K) = \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\operatorname{op}} }( K^{\operatorname{op}}, \operatorname{Tw}(\operatorname{\mathcal{C}}) ) \times _{ \operatorname{Fun}(K^{\operatorname{op}}, \operatorname{\mathcal{C}}) } \{ C\} $, so that $\iota $ restricts to a map of Kan complexes $\theta _{K}: X(K) \rightarrow Y(K)$. By virtue of Corollary 5.1.6.4, it will suffice to show that $\theta _{K}$ is a homotopy equivalence (for each $C \in \operatorname{\mathcal{C}}$). In what follows, we regard the object $C \in \operatorname{\mathcal{C}}$ as fixed. We now proceed in several steps.

$(a)$

The morphism $\theta _{K}$ is contravariantly functorial in $K$ (as an object of the category $(\operatorname{Set_{\Delta }})_{/\operatorname{\mathcal{C}}}$). That is, every morphism of simplicial sets $u: K_0 \rightarrow K$ determines a commutative diagram of Kan complexes

8.5

\begin{equation} \begin{gathered}\label{equation:coslice-inclusion-equivalence} \xymatrix@R =50pt@C=50pt{ X(K) \ar [r]^-{\theta _ K} & Y(K) \ar [d] \\ X(K_0) \ar [r]^-{ \theta _{K_0} } & Y(K_0 ), } \end{gathered} \end{equation}

where the vertical maps are given by restriction along $u$. Moreover, if $u$ is a monomorphism of simplicial sets, then the vertical maps are left fibrations between Kan complexes (Propositions 4.3.6.8 and 4.2.5.1), and are therefore Kan fibrations (Corollary 4.4.3.8).

$(b)$

The constructions $K \mapsto X(K)$ and $K \mapsto Y(K)$ carry colimits (in the category $( \operatorname{Set_{\Delta }})_{ /\operatorname{\mathcal{C}}}$) to limits (in the category of simplicial sets). In particular, the collection of objects $K \in (\operatorname{Set_{\Delta }})_{/\operatorname{\mathcal{C}}}$ for which $\theta _{K}$ is a homotopy equivalence is closed under coproducts (Remark 3.1.7.8).

$(c)$

If $K = \Delta ^0$, then $\theta _{K}$ is a homotopy equivalence. This is a restatement of Corollary 8.1.2.11.

$(d)$

If $K_0 \hookrightarrow K$ is a right anodyne morphism of simplicial sets, then the vertical maps appearing in the diagram (8.5) are trivial Kan fibrations (see Propositions 4.3.6.13 and 4.2.5.4). In particular, $\theta _{K}$ is a homotopy equivalence if and only if $\theta _{K_0}$ is a homotopy equivalence.

$(e)$

If $K = \Delta ^ n$ is a standard simplex, then $\theta _{K}$ is a homotopy equivalence. This follows from $(c)$ and $(d)$, since the inclusion map $\Delta ^0 \simeq \{ n\} \hookrightarrow \Delta ^ n$ is right anodyne.

$(f)$

Suppose we are given a pushout diagram

\[ \xymatrix@R =50pt@C=50pt{ K_0 \ar [r] \ar [d] & K \ar [d] \\ L_0 \ar [r] & L } \]

in the category $(\operatorname{Set_{\Delta }})_{/\operatorname{\mathcal{C}}}$, where the horizontal maps are monomorphisms. Then the diagrams of Kan complexes

\[ \xymatrix@R =50pt@C=50pt{ X(K_0) & X(K) \ar [l] & Y(K_0) & Y(K) \ar [l] \\ X(L_0) \ar [u] & X(L) \ar [l] \ar [u] & Y(L_0) \ar [u] & Y(L) \ar [u] \ar [l] } \]

are pullback square (by virtue of $(b)$) where the horizontal maps are Kan fibrations (by virtue of $(a)$), and are therefore homotopy pullback squares (Example 3.4.1.3). Consequently, if $\theta _{K_0}$, $\theta _{K}$, and $\theta _{L_0}$ are homotopy equivalences, then $\theta _{L}$ is also a homotopy equivalence (Corollary 3.4.1.13).

$(g)$

Suppose that the simplicial set $K$ has dimension $\leq d$, for some integer $d$. Then $\theta _{K}$ is a homotopy equivalence. The proof proceeds by induction on $d$. If $d < 0$, then $K$ is empty and $\theta _{K}$ is an isomorphism. For $d \geq 0$, we can use $(f)$ and Proposition 1.1.4.12 to reduce to the case where $K$ is a coproduct of standard $d$-simplices, which follows from $(b)$ and $(e)$.

$(h)$

We now show that $\theta _{K}$ is a homotopy equivalence for every diagram $f: K \rightarrow \operatorname{\mathcal{C}}$. Using $(b)$, we can realize $\theta _{K}$ as the limit of a tower

\[ \xymatrix@R =50pt@C=50pt{ X( \operatorname{sk}_0(K) ) \ar [d]^{ \theta _{ \operatorname{sk}_{0}(K) } } & X( \operatorname{sk}_{1}(K) ) \ar [l] \ar [d]^{ \theta _{ \operatorname{sk}_1(K) } } & X( \operatorname{sk}_2(K) ) \ar [l] \ar [d]^{ \theta _{ \operatorname{sk}_2(K) }} & \cdots \ar [l] \\ Y( \operatorname{sk}_0(K) ) & Y( \operatorname{sk}_1(K) ) \ar [l] & Y( \operatorname{sk}_2(K) ) \ar [l] & \cdots \ar [l] } \]

where the horizontal maps are Kan fibrations (by virtue of $(a)$) and the vertical maps are homotopy equivalences (by virtue of $(g)$). The desired result now follows from Example 4.5.7.18.