Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Proof. Let $K$ be a small simplicial set; we wish to show that $\operatorname{\mathcal{C}}$ admits $K$-indexed limits. For each $n \geq 0$, let $\operatorname{sk}_{n}(K)$ denote the $n$-skeleton of $K$ (Construction 1.1.3.5), so that $K = \bigcup _{n} \operatorname{sk}_ n(K)$. It follows from Proposition 7.6.6.16 that $\operatorname{\mathcal{C}}$ admits sequential limits. Consequently, to show that $\operatorname{\mathcal{C}}$ admits $K$-indexed limits, it will suffice to show that it admits $\operatorname{sk}_ n(K)$-indexed limits, for each $n \geq 0$ (Corollary 7.6.6.14). We may therefore assume without loss of generality that the simplicial set $K$ has finite dimension. We proceed by induction on the dimension $n$ of $K$. If $n=-1$, then $K$ is empty and the desired result is immediate (see Example 7.6.1.8). Assume that $n \geq 0$ and let $S$ denote the collection of nondegenerate $n$-simplices of $K$, so that Proposition 1.1.3.13 supplies a pushout diagram of simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ \underset { \sigma \in S }{\coprod } \operatorname{\partial \Delta }^{n} \ar [r] \ar [d] & \underset { \sigma \in S }{\coprod } \Delta ^{n} \ar [d] \\ \operatorname{sk}_{n-1}(K) \ar [r] & \operatorname{sk}_{n}(K ). } \]

Since the horizontal maps in this diagram are monomorphisms, it is also a categorical pushout square (Example 4.5.4.12). By virtue of Proposition 7.6.3.17, it will suffice to show that $\operatorname{\mathcal{C}}$ admits limits indexed by the simplicial sets $\operatorname{sk}_{n-1}(K)$, $S \times \operatorname{\partial \Delta }^{n}$, and $S \times \Delta ^ n$. In the first two cases, this follows from our inductive hypothesis. To handle the third case, we can use Corollary 7.6.1.19 to reduce to showing that the $\infty $-category $\operatorname{\mathcal{C}}$ admits $\Delta ^{n}$-indexed limits. This is clear, since the simplicial set $\Delta ^ n$ is an $\infty $-category containing an initial object (see Corollary 7.2.2.12). $\square$