Kerodon

Proof. Without loss of generality, we may assume that $f$ is a monomorphism. Let us temporarily regard $f$ as fixed, and say that a morphism $g: X \rightarrow Y$ is good if $\nu _{f,g}$ is categorically $(m+n-1)$-connective. We wish to show that if $g$ is categorically $(n-1)$-connective, then it is good. Our proof will make use of the following observations:

$(a)$

Suppose we are given a commutative diagram

\[ \xymatrix { X \ar [r]^{g} \ar [d] & Y \ar [d] \\ X' \ar [r]^{ g' } & Y' } \]

where the vertical maps are categorical equivalences. Since $f$ is a monomorphism, we deduce that the vertical maps in the diagram

\[ \xymatrix { (B \times X) \coprod _{ (A \times X)} (A \times Y) \ar [r]^{\nu _{f,g}} \ar [d] & B \times Y \ar [d] \\ (B \times X') \coprod _{ (A \times X')} (A \times Y') \ar [r]^{\nu _{f,g'}} & B \times Y' } \]

are categorical equivalences. It follows that $g$ is good if and only if $g'$ is good (Remark 4.8.8.4).

$(b)$

The collection of good morphisms of simplicial sets is closed under filtered colimits. This follows from Proposition 4.8.8.10, since the construction $g \mapsto \nu _{f,g}$ preserves filtered colimits.

$(c)$

Let $g: X \rightarrow Z$ be a morphism of simplicial sets which factors as a composition $X \xrightarrow {g'} Y \xrightarrow {g''} Z$, where $g'$ is a monomorphism. Then $\nu _{f,g}$ factors as a composition

\[ (B \times X) \coprod _{ (A \times X)} (A \times Z) \rightarrow (B \times Y) \coprod _{ (A \times Y)} (A \times Z) \xrightarrow { \nu _{f,g''} } B \times Z, \]

where the map on the left is a pushout of the monomorphism $\nu _{f,g'}$. Using Proposition 4.8.8.12 and 4.8.8.6, we see that if $g'$ and $g''$ are good, then $g$ is good.

$(d)$

Let $g: X \hookrightarrow Y$ be a monomorphism of simplicial sets which is a pushout of a monomorphism $g_0: X_0 \hookrightarrow Y_0$. Then $\nu _{f,g}$ is a pushout of $\nu _{f,g_0}$. Using Proposition 4.8.8.12 we see that if $g_0$ is good, then $g$ is good.

Let $g: X \rightarrow Y$ be a categorically $(n-1)$-connective morphism of simplicial sets; we wish to prove that $g$ is good. Using Proposition 4.8.5.20, we can choose a categorical equivalence $Y \xrightarrow {e} Z$, where $Z$ is an $\infty $-category. Applying Corollary 4.5.3.24, we can factor $e \circ g$ as a composition $X \xrightarrow {w} X' \xrightarrow {u} Z$ where $w$ is a categorical equivalence and $u$ is an isofibration of $\infty $-categories. Since $g$ is categorically $(n-1)$-connective, $u$ is also categorically $(n-1)$-connective (Remark 4.8.8.4). Using Proposition 4.8.5.20, we can factor $u$ as a composition $X' \xrightarrow {g'} Y' \xrightarrow {u'} Z$, where $u'$ is a trivial Kan fibration and $g'$ is a monomorphism which is bijective on simplices of dimension smaller than $n$. Applying $(a)$ repeatedly, we see that $g$ is good if and only if $g'$ is good. We may therefore replace $g$ by $g'$ and thereby reduce to the case where $g$ is a monomorphism which is bijective on simplices of dimension smaller than $n$. Using $(b)$, we can reduce to the case where $Y$ is obtained from $X$ by adding finitely many nondegenerate simplices. Using $(c)$, we can reduce to the special case where $Y$ is obtained from $X$ by adjoining a single nondegenerate $n'$-simplex for $n' \geq n$. In this case, we can use $(d)$ (together with Proposition 1.1.4.12) to reduce to the case where $g$ is the inclusion map $\operatorname{\partial \Delta }^{n'} \hookrightarrow \Delta ^{n'}$, for some $n' \geq n$. Applying a similar argument (with the roles of $f$ and $g$ reversed), we may assume that $f$ is the inclusion map $\operatorname{\partial \Delta }^{m'} \hookrightarrow \Delta ^{m}$ for some $m' \geq m$. In this case, Lemma 4.8.8.18 guarantees that $\nu _{f,g}$ is categorically $(m'+n'-1)$-connective, and therefore also categorically $(m+n-1)$-connective (see Remark 4.8.5.7). $\square$