Kerodon

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

Corollary 7.2.1.16. Suppose we are given a categorical pushout diagram of simplicial sets

7.9
\begin{equation} \begin{gathered}\label{equation:categorical-pushout-cofinal} \xymatrix@R =50pt@C=50pt{ X \ar [r]^-{f} \ar [d] & Z \ar [d] \\ X' \ar [r]^-{f'} & Z'. } \end{gathered} \end{equation}

If $f$ is left cofinal, then $f'$ is also left cofinal.

Proof. By virtue of Corollary 7.2.1.15, we may assume that $f$ factors as a composition $X \xrightarrow {g} Y \xrightarrow {h} Z$, where $g$ is left anodyne and $h$ is a trivial Kan fibration. Setting $Y' = Y {\coprod }_{X} X'$, we can expand (7.9) to a commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ X \ar [r]^-{g} \ar [d] & Y \ar [r]^-{h} \ar [d] & Z \ar [d] \\ X' \ar [r]^-{g'} & Y' \ar [r]^-{h'} & Z'. } \]

Note that the square on the left is a pushout diagram in which the horizontal maps are monomorphisms, and therefore a categorical pushout diagram (Example 4.5.4.12). Applying Proposition 4.5.4.8, we deduce that the square on the right is also a categorical pushout diagram. Since $h$ is a categorical equivalence (Proposition 4.5.3.11), it follows that $h'$ is also a categorical equivalence (Proposition 4.5.4.10). In particular, $h'$ is left cofinal (Corollary 7.2.1.13). The morphism $g'$ is left anodyne (since it is a pushout of $g$), and is therefore also left cofinal (Proposition 7.2.1.3). Applying Proposition 7.2.1.6, we deduce that $f' = h' \circ g'$ is also left cofinal. $\square$