Kerodon

Proof. Assume that $(2)$ is satisfied; we will prove $(1)$ (the reverse implication is immediate from the definitions). Let $X$ be a small Kan complex; we wish to show composition with $\beta $ induces a homotopy equivalence $\theta _{X}: \operatorname{Hom}_{\operatorname{\mathcal{S}}}( X, Y ) \rightarrow \operatorname{Hom}_{ \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}) }( \underline{X}_{\operatorname{\mathcal{C}}}, \mathscr {F} )$. Choose a simplicial set $K$ equipped with a weak homotopy equivalence $u: K \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{S}}}( \Delta ^0, X )$ (for example, we can take $K = X$ and $u$ to be the homotopy equivalence of Remark 5.5.1.5). It follows from Example 7.1.2.10 that $u$ exhibits $X$ as a copower of $\Delta ^0$ by $K$ in the $\infty $-category $\operatorname{\mathcal{S}}$, so that the composite map

determines a homotopy equivalence $T: \operatorname{Hom}_{\operatorname{\mathcal{S}}}(X,Y) \rightarrow \operatorname{Fun}(K, \operatorname{Hom}_{\operatorname{\mathcal{S}}}( \Delta ^0, Y) )$. Similarly, the composite map

exhibits $\underline{X}_{\operatorname{\mathcal{C}}}$ as a copower of $\underline{ \Delta ^0 }_{\operatorname{\mathcal{C}}}$ by $K$ in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}})$ (see Proposition 7.1.7.3), so that $u$ also determines a homotopy equivalence $T': \operatorname{Hom}_{\operatorname{Fun}(\operatorname{\mathcal{C}},\operatorname{\mathcal{S}})}( \underline{X}_{\operatorname{\mathcal{C}}}, \mathscr {F} ) \rightarrow \operatorname{Fun}(K, \operatorname{Hom}_{ \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}) }( \underline{ \Delta ^0 }_{\operatorname{\mathcal{C}}}, \mathscr {F} )$. Note that we have a homotopy commutative diagram of Kan complexes

where the bottom horizontal map is obtained by applying the functor $\operatorname{Fun}(K, \bullet )$ to $\theta $ and is therefore a homotopy equivalence by virtue of assumption $(2)$. It follows that $\theta _{X}$ is also a homotopy equivalence. $\square$

Proof. Let $Y$ be a Kan complex and let $u: Y \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{S}}}( \Delta ^0, Y)$ be the homotopy equivalence of Remark 5.5.1.5. As in the proof of Proposition 7.4.1.1, we observe that $u$ exhibits the constant functor $\underline{Y}_{\operatorname{\mathcal{C}}}$ as a copower of $\underline{ \Delta ^0 }_{\operatorname{\mathcal{C}}}$ by $Y$, and therefore induces a homotopy equivalence

Setting $Y = M$, it follows that there exists a natural transformation $\beta : \underline{M}_{\operatorname{\mathcal{C}}} \rightarrow \mathscr {F}$ such that $T( \beta )$ is homotopic to the identity morphism $\operatorname{id}_{M}$. In particular, $T( \beta )$ is a homotopy equivalence, so that $\beta $ exhibits $M$ as a limit of $\mathscr {F}$ (Proposition 7.4.1.1). $\square$

Proof. Apply Proposition 7.4.1.6 to the left fibration $U: \int _{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \operatorname{\mathcal{C}}$ of Example 5.6.2.9. $\square$

Proof. Unwinding the definitions, we see that commutative diagrams

can be identified with morphisms $\alpha : \underline{ \Delta ^{0} }_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {F}|_{\operatorname{\mathcal{E}}}$ in the $\infty $-category $\operatorname{Fun}(\operatorname{\mathcal{E}}, \operatorname{\mathcal{S}})$. Under this identification, $T$ is an equivalence of left fibrations over $\operatorname{\mathcal{C}}$ if and only if $\alpha $ exhibits $\mathscr {F}$ as a covariant transport representation for $U$ (Corollary 5.1.7.16). This proves the equivalence $(2) \Leftrightarrow (3)$. The equivalence $(1) \Leftrightarrow (3)$ follows from the observation that the coslice diagonal

is an equivalence of left fibrations over $\operatorname{\mathcal{S}}$ (Corollary 4.6.4.18). $\square$

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$

Proof of Proposition 7.4.1.6. Let $\operatorname{\mathcal{C}}$ be a small simplicial set and let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$ be the covariant transport representation of a left fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$. Combining Propositions 7.4.1.9 and Proposition 7.4.1.14, we deduce that the Kan complex $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ is homotopy equivalent to the morphism space $\operatorname{Hom}_{ \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{S}}) }( \underline{ \Delta ^{0} }_{\operatorname{\mathcal{C}}}, \mathscr {F} )$ and is therefore a limit of $\mathscr {F}$ in the $\infty $-category $\operatorname{\mathcal{S}}$ (Corollary 7.4.1.2). $\square$

Proof of Proposition 7.4.1.16. Using Proposition 7.4.1.9, we can choose a natural transformation $\overline{\alpha }: \underline{ \Delta ^0 }_{\overline{\operatorname{\mathcal{E}}}} \rightarrow \overline{\mathscr {F}}|_{ \overline{\operatorname{\mathcal{E}}} }$ which exhibits $\overline{\mathscr {F}}$ as a covariant transport representation for $\overline{U}$. Set $\mathscr {F} = \overline{\mathscr {F}}|_{\operatorname{\mathcal{C}}}$, so that we have a commutative diagram of Kan complexes

where the vertical maps are given by Construction 7.4.1.13, and are therefore homotopy equivalences (Proposition 7.4.1.14). It follows that $(2)$ is equivalent the following:

$(2')$

The restriction map $Q': \operatorname{Hom}_{\operatorname{Fun}( \operatorname{\mathcal{C}}^{\triangleleft }, \operatorname{\mathcal{S}})}( \underline{\Delta ^0}_{ \operatorname{\mathcal{C}}^{\triangleleft } }, \overline{\mathscr {F}} ) \rightarrow \operatorname{Hom}_{ \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}})}( \underline{ \Delta ^0}_{ \operatorname{\mathcal{C}}}, \mathscr {F} )$ is a homotopy equivalence.

Choose a Kan complex $Y$ and a natural transformation $\overline{\beta }: \underline{Y}_{ \operatorname{\mathcal{C}}^{\triangleleft } } \rightarrow \overline{\mathscr {F}}$ which exhibits $Y$ as a limit of the diagram $\overline{\mathscr {F}}$ (so that $\beta $ induces a homotopy equivalence $Y \rightarrow \overline{\mathscr {F}}(v)$, where $v$ denotes the cone point of $\operatorname{\mathcal{C}}^{\triangleleft } \simeq \{ v\} \star \operatorname{\mathcal{C}}$). Then $\overline{\beta }$ restricts to a natural transformation $\beta : \underline{Y}_{\operatorname{\mathcal{C}}} \rightarrow \mathscr {F}$. We then have a commutative diagram of Kan complexes

where $\theta $ and $\overline{\theta }$ are induced by composition with $\beta $ and $\overline{\beta }$, respectively. It follows from Proposition 7.4.1.1 that $\overline{\theta }$ is a homotopy equivalence. Moreover, $\overline{\mathscr {F}}$ is a limit diagram if and only if $\beta $ exhibits $Y$ as a limit of $\mathscr {F}$: that is, if and only if $\theta $ is also a homotopy equivalence. Using the commutativity of the diagram, we see that this is equivalent to condition $(2')$. $\square$

Proof. Applying Proposition 7.1.6.12, we see that $F$ is a limit diagram if and only if, for every object $X \in \operatorname{\mathcal{C}}$, the restriction map

is a homotopy equivalence of Kan complexes. Let $\operatorname{\mathcal{E}}$ denote the oriented fiber product $\{ X\} \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}$ and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be given by projection onto the second factor. Note that $U$ is a left fibration (Proposition 4.6.4.11) and that $\theta _{X}$ can be identified with the restriction map

The identity morphism $\operatorname{id}_{X}$ can be viewed as an initial object of $\operatorname{\mathcal{E}}$ satisfying $U( \operatorname{id}_{X} ) = X$ (Proposition 4.6.7.22), so the corepresentable functor $h^{X}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}^{<\kappa }$ is a covariant transport representation for $U$ (Proposition 5.6.6.21). Applying Proposition 7.4.1.16, we see that $\theta _{X}$ is a homotopy equivalence if and only if $h^{X} \circ F$ is a limit diagram in the $\infty $-category $\operatorname{\mathcal{S}}$. $\square$