Kerodon

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

Proposition 9.2.8.6. Suppose we are given a categorical pushout diagram of $\infty $-categories

9.5
\begin{equation} \begin{gathered}\label{equation:categorical-pushout-essentially-finite} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}\ar [r] \ar [d]& \operatorname{\mathcal{C}}_0 \ar [d] \\ \operatorname{\mathcal{C}}_1 \ar [r] & \operatorname{\mathcal{C}}_{01}. } \end{gathered} \end{equation}

If $\operatorname{\mathcal{C}}$, $\operatorname{\mathcal{C}}_0$, and $\operatorname{\mathcal{C}}_1$ are essentially finite, then $\operatorname{\mathcal{C}}_{01}$ is essentially finite.

Proof. Using Lemma 9.2.8.2, we can construct a commutative diagram of simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ K_0 \ar [d] & K \ar [l] \ar [r] \ar [d] & K_1 \ar [d] \\ \operatorname{\mathcal{C}}_0 & \operatorname{\mathcal{C}}\ar [l] \ar [r] & \operatorname{\mathcal{C}}_1 } \]

where the vertical maps are categorical equivalences, the upper horizontal maps are monomorphisms, and the simplicial sets $K_0$, $K$, and $K_1$ are finite. Our assumption that (9.5) is a categorical pushout square then guarantees that the induced map $K_0 \amalg _{K} K_1 \rightarrow \operatorname{\mathcal{C}}_{01}$ is a categorical equivalence (Proposition 4.5.4.9), so that the $\infty $-category $\operatorname{\mathcal{C}}_{01}$ is also essentially finite. $\square$