Lemma 6.2.5.13. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $S$ be a class of short morphisms of $\operatorname{\mathcal{C}}$, and suppose we are given a $2$-simplex
6.3
\begin{equation} \begin{gathered}\label{equation:S-length-decrease} \xymatrix@R =50pt@C=50pt{ & Y \ar [dr]^{s} & \\ X \ar [ur]^{g} \ar [rr]^{f} & & Z, } \end{gathered} \end{equation}
of $\operatorname{\mathcal{C}}$, where $s$ belongs to $S$. Then:
- $(a)$
If $\ell (f) \geq 1$, then $\ell (g) \leq \ell (f)$.
- $(b)$
If $\ell (f) \geq 2$ and the factorization (6.3) is $S$-optimal, then $\ell (g) = \ell (f) - 1$.
Proof.
We prove $(a)$ and $(b)$ by simultaneous induction on the length $n = \ell (f)$. If $n = 1$, then assertion $(a)$ follows from condition $(2)$ of Definition 6.2.5.4 and assertion $(b)$ is vacuous. We therefore assume that $n \geq 2$. We first prove $(b)$. Choose a factorization
\[ \xymatrix@R =50pt@C=50pt{ & Y' \ar [dr]^{s'} & \\ X \ar [ur]^{g'} \ar [rr]^{f} & & Z, } \]
where $s' \in S$ and $\ell (g') = n-1$. If the factorization (6.3) is $S$-optimal, then we can choose a $3$-simplex
\[ \xymatrix@R =50pt@C=50pt{ & Y \ar [dd]^{h} \ar [dr]^{s} & \\ X \ar [ur]^{g} \ar [dr]^{g'} & & Z \\ & Y'. \ar [ur]^{s'} & } \]
Condition $(2)$ of Definition 6.2.5.4 guarantees that $h$ belongs to $S$. Our inductive hypothesis guarantees that the left half of the diagram satisfies assertion $(a)$; so that $\ell (g) \leq \ell (g') = \ell (f) - 1$. The reverse inequality follows immediately from the definition.
We now prove $(a)$. Choose an $S$-optimal factorization
\[ \xymatrix@R =50pt@C=50pt{ & Y'' \ar [dr]^{s''} & \\ X \ar [ur]^{g''} \ar [rr]^{f} & & Z. } \]
It follows from the preceding argument that $\ell (g'') = n-1$. We then have a commutative diagram
\[ \xymatrix@R =50pt@C=50pt{ & Y'' \ar [dd]^{j} \ar [dr]^{s''} & \\ X \ar [ur]^{g''} \ar [dr]^{g} & & Z \\ & Y, \ar [ur]^{s} & } \]
and condition $(2)$ of Definition 6.2.5.4 guarantees that $j$ belongs to $S$. We therefore obtain $\ell (g) \leq \ell (g'') + \ell (j) \leq (n-1) + 1 = n$, as desired.
$\square$