Kerodon

Proof. It follows immediately from the definitions that a diagram in $\operatorname{\mathcal{S}}$ which is a limit (or colimit) diagram in the larger $\infty $-category $\operatorname{\mathcal{QC}}$, then it is already a limit (or colimit) diagram in $\operatorname{\mathcal{S}}$ (see Variant 7.1.3.10). To prove the converse implications, we must show that the inclusion functor $\iota : \operatorname{\mathcal{S}}\rightarrow \operatorname{\mathcal{QC}}$ preserves all limits and colimits. This follows from Corollary 7.1.3.21, since the functor $\iota $ admits both left and right adjoints (Example 6.2.2.16). $\square$

Proof. Since $U$ is a left fibration, Corollary 4.4.2.4 guarantees that the simplicial set $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ is a Kan complex. Note that every edge of $\operatorname{\mathcal{E}}$ is $U$-cocartesian (Example 5.1.1.3), so that $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ coincides with the $\infty $-category $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ of cocartesian sections of $U$. Applying Corollary 7.4.1.9, we see that the Kan complex $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ is a limit of the diagram $\operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ in the $\infty $-category $\operatorname{\mathcal{QC}}$, and therefore also in the full subcategory $\operatorname{\mathcal{S}}\subseteq \operatorname{\mathcal{QC}}$ (Proposition 7.4.5.1). $\square$

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

Proof. Since $U$ is a left fibration, every edge of $\operatorname{\mathcal{E}}$ is $U$-cocartesian (Example 5.1.1.3). Let $W$ be the collection of all $U$-cocartesian edges of $\operatorname{\mathcal{E}}$. By virtue of Corollary 7.4.3.11, an $\infty $-category $X$ is a colimit of $\operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ in the $\infty $-category $\operatorname{\mathcal{QC}}$ if and only if there exists a functor $f: \operatorname{\mathcal{E}}\rightarrow X$ which exhibits $X$ as a localization of $\operatorname{\mathcal{E}}$ with respect to $W$. By virtue of Proposition 6.3.1.20, this is equivalent to the requirement that $X$ is a Kan complex and that $f$ is a weak homotopy equivalence. In this case, $X$ is also a colimit of the diagram $\operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ in the full subcategory $\operatorname{\mathcal{S}}\subseteq \operatorname{\mathcal{QC}}$ (Proposition 7.4.5.1). $\square$

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

Proof. Combine Corollaries 7.4.5.5 and 7.4.5.3 $\square$

Proof. Fix an object $X \in \operatorname{\mathcal{C}}$, and let $h^{X}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa }$ be a functor corepresented by $X$ (Theorem 5.6.6.13). Using Proposition 5.6.6.21, we see that $f \circ h^{X}$ is a covariant transport representation for the left fibration $K \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{X/} \rightarrow K$. Using Corollary 7.4.5.4, we can reformulate condition $(2)$ as follows:

$(2')$

For each object $X \in \operatorname{\mathcal{C}}$, the simplicial set $K \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{X/}$ is weakly contractible.

The equivalence $(1) \Leftrightarrow (2')$ follows from Theorem 7.2.3.1. $\square$

Proof. Combine Corollary 7.4.5.4 with Example 5.6.5.6. $\square$

Proof. Since $\overline{U}$ is a left fibration, every edge of $\overline{\operatorname{\mathcal{E}}}$ is $\overline{U}$-cocartesian (Example 5.1.1.3). We can therefore identify $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} )$ and $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ with the $\infty $-categories $\operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} )$ and $\operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$, respectively. The desired result now follows by combining Theorem 7.4.1.1 with Proposition 7.4.5.1. $\square$

Proof. Assume that condition $(\ast )$ is satisfied; we will show that $e$ is left cofinal (the reverse implication is a special case of Corollary 7.2.2.3). Fix a left fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$; we wish to show that the restriction map

is a homotopy equivalence of Kan complexes. Using Proposition 7.4.1.6 (together with Remark 7.4.1.8), we can extend $U$ to a left fibration $\overline{U}: \overline{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{C}}^{\triangleleft }$ for which the restriction map

is a homotopy equivalence.

Form a pullback diagram of simplicial sets

Let $\overline{F}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{\mathcal{S}}$ be a covariant transport representation for the left fibration $\overline{U}$, so that $\overline{F} \circ e^{\triangleleft }$ is a covariant transport representation for the left fibration $\overline{U}'$. It follows from the criterion of Corollary 7.4.5.13 that $\overline{F}$ is a limit diagram in the $\infty $-category $\operatorname{\mathcal{S}}$. Applying assumption $(\ast )$, we see that $\overline{F} \circ e^{\triangleleft }$ is also a limit diagram in the $\infty $-category $\operatorname{\mathcal{S}}$. We therefore have a commutative diagram of restriction maps

where the horizontal maps are homotopy equivalences (Corollary 7.4.5.13). Consequently, to show that $e^{\ast }$ is a homotopy equivalence, it will suffice to show that $( e^{\triangleleft } )^{\ast }$ is a homotopy equivalence. We now observe that $(e^{\triangleleft } )^{\ast }$ fits into a commutative diagram

where the horizontal maps are given by evaluation at the cone points of the simplicial sets $\operatorname{\mathcal{C}}^{\triangleleft }$ and $\operatorname{\mathcal{C}}'^{\triangleleft }$ are are therefore trivial Kan fibrations (Corollary 5.3.1.23). $\square$

Proof. Let ${\bf 1}$ denote the cone point of $\operatorname{\mathcal{C}}^{\triangleright }$, and let $\overline{\operatorname{\mathcal{E}}}_{ {\bf 1} } = \{ {\bf 1} \} \times _{\operatorname{\mathcal{C}}^{\triangleright } } \overline{\operatorname{\mathcal{E}}}$ denote the corresponding fiber of $\overline{\operatorname{\mathcal{E}}}$. Since the inclusion map $\{ {\bf 1} \} \hookrightarrow \operatorname{\mathcal{C}}^{\triangleright }$ is right anodyne (Example 4.3.7.11), the inclusion $\iota : \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} } \hookrightarrow \overline{\operatorname{\mathcal{E}}}$ is also right anodyne (Corollary 7.2.3.13). In particular, $\iota $ is a weak homotopy equivalence of simplicial sets. Let $\mathrm{Rf}: \operatorname{\mathcal{E}}\rightarrow \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ be a covariant refraction diagram (Proposition 7.4.3.3), so that the inclusion map $\operatorname{\mathcal{E}}\hookrightarrow \overline{\operatorname{\mathcal{E}}}$ is homotopic to the composition $\iota \circ \mathrm{Rf}$. It follows that condition $(1)$ can be reformulated as follows:

$(1')$

The covariant refraction diagram $\mathrm{Rf}: \operatorname{\mathcal{E}}\rightarrow \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ is a weak homotopy equivalence.

The equivalence $(1') \Leftrightarrow (3)$ follows by combining Proposition 7.4.5.1, Theorem 7.4.3.6, and Proposition 6.3.1.20.

The implication $(2) \Rightarrow (1)$ follows from Proposition 7.2.1.5. We will complete the proof by showing that $(1')$ implies $(2)$. Choose an inner anodyne monomorphism $\operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{C}}'$, where $K'$ is an $\infty $-category. Then the induced map $\operatorname{\mathcal{C}}^{\triangleright } \rightarrow \operatorname{\mathcal{C}}'^{\triangleright }$ is also inner anodyne (Corollary 4.3.6.6); in particular, it is a categorical equivalence. Using Proposition 5.6.7.2 (and Remark 5.6.7.4), we can assume that $\overline{U}$ is the pullback of a left fibration $\overline{U}': \overline{\operatorname{\mathcal{E}}}' \rightarrow \operatorname{\mathcal{C}}'^{\triangleright }$. Setting $\operatorname{\mathcal{E}}' = \operatorname{\mathcal{C}}' \times _{ \operatorname{\mathcal{C}}'^{\triangleright } } \overline{\operatorname{\mathcal{E}}}'$, we have a commutative diagram of inclusion maps

where the vertical maps are categorical equivalences (Corollary 5.6.7.6). Consequently, to prove that the inclusion map $\operatorname{\mathcal{E}}\hookrightarrow \overline{\operatorname{\mathcal{E}}}$ is left cofinal, it will suffice to show that the inclusion $\operatorname{\mathcal{E}}' \hookrightarrow \overline{\operatorname{\mathcal{E}}}'$ is left cofinal (Corollary 7.2.1.22). We may therefore replace $\overline{U}$ by the left fibration $\overline{U}': \overline{\operatorname{\mathcal{E}}}' \rightarrow \operatorname{\mathcal{C}}'^{\triangleright }$, and thereby reduce to proving the implication $(1') \Rightarrow (2)$ under the assumption that $\operatorname{\mathcal{C}}$ is an $\infty $-category.

Let $\operatorname{\mathcal{E}}\operatorname{\vec{\times }}_{ \overline{\operatorname{\mathcal{E}}} } \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ denote the oriented fiber product of Definition 4.6.4.1, and consider the projection maps

The functor $\pi $ is a trivial Kan fibration, and the refraction functor $\mathrm{Rf}$ is obtained by composing $\pi '$ with a choice of section of $\pi $. Consequently, assumption $(1')$ guarantees that $\pi '$ is a weak homotopy equivalence of simplicial sets. For each vertex $X \in \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$, we have a pullback diagram of simplicial sets

Since $\pi '$ is an isofibration of $\infty $-categories (Corollary 5.3.7.3), the diagram( 7.50 ) is a categorical pullback square (Corollary 4.5.2.27). Because $\overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ is a Kan complex, the diagram ( 7.50) is also a homotopy pullback square (Variant 4.5.2.11). Our assumption that $\pi '$ is a weak homotopy equivalence guarantees that the upper horizontal map is also a weak homotopy equivalence: that is, the simplicial set $\operatorname{\mathcal{E}}\operatorname{\vec{\times }}_{ \overline{\operatorname{\mathcal{E}}} } \{ X\} $ is weakly contractible (Corollary 3.4.1.5). Condition $(2)$ now follows by allowing the object $X$ to vary and applying the criterion of of Theorem 7.2.3.1 (together with Remark 7.2.3.2). $\square$

Proof. Applying Proposition 7.1.5.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}}$ is a covariant transport representation for $U$ (Proposition 5.6.6.21). Applying Corollary 7.4.5.13, 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$