Kerodon

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

Proposition 7.2.4.8. Let $\operatorname{\mathcal{C}}$ be a filtered $\infty$-category and let $f: K \rightarrow \operatorname{\mathcal{C}}$ be a diagram, where $K$ is a finite simplicial set. Then the $\infty$-category $\operatorname{\mathcal{C}}_{f/}$ is also filtered.

Proof. By virtue of Remark 7.2.4.7, it will suffice to show that for every finite simplicial set $L$ and every morphism $g: L \rightarrow \operatorname{\mathcal{C}}_{f/}$, the $\infty$-category $(\operatorname{\mathcal{C}}_{f/} )_{g/}$ is nonempty. Unwinding the definitions, we can identify $g$ with a morphism of simplicial sets $\overline{f}: K \star L \rightarrow \operatorname{\mathcal{C}}$ satisfying $\overline{f}|_{K} = f$. This identification supplies an isomorphism $(\operatorname{\mathcal{C}}_{f/} )_{g/} \simeq \operatorname{\mathcal{C}}_{ \overline{f} / }$. We are therefore reduced to showing that the coslice $\infty$-category $\operatorname{\mathcal{C}}_{ \overline{f} / }$ is nonempty. This follows from Remark 7.2.4.7, since the simplicial set $K \star L$ is finite (Remark 4.3.3.16). $\square$