Kerodon

Proof. Using the well-ordering theorem (Theorem 4.7.1.34), we can choose an ordinal $\alpha $ and a bijection $\ell : S \rightarrow \mathrm{Ord}_{ < \alpha }$. Let $Q$ denote the disjoint union $(S \times [1]) \coprod \mathrm{Ord}_{\leq \alpha }$. For elements $q,q' \in Q$, we write $q \leq q'$ if (exactly) one of the following conditions holds:

• There exist an element $s \in S$ such that $q = (s,i)$ and $q' = (s, i' )$, where $i \leq i'$.

• We have $q = \beta $ and $q' = \beta '$ for ordinals $\beta , \beta ' \in \mathrm{Ord}_{\leq \alpha }$ satisfying $\beta \leq \beta '$ (for the usual ordering of $\mathrm{Ord}_{\leq \alpha }$).

• We have $q = (s,0)$ for some $s \in S$ and $q' = \beta $ for some $\beta \in \mathrm{Ord}_{\leq \alpha }$.

• We have $q = (s,1)$ and $q' = \beta $ for some $\beta \in \mathrm{Ord}_{\leq \alpha }$ satisfying $\ell (s) < \beta $.

Let $Q_0 = (S \times [1]) \coprod \{ 0 \} $, which we regard as a partially ordered subset of $Q$. By construction, the nerve $\operatorname{N}_{\bullet }( Q_{0} )$ can be identified with the pushout $(S \times \Delta ^1) \coprod _{ S \times \{ 0\} } S^{\triangleright }$. Consequently, the collections $\{ e_ s \} _{s \in S}$ and $\{ w_ s \} _{s \in S}$ determine a diagram $F_0: \operatorname{N}_{\bullet }( Q_{\leq 0 } ) \rightarrow \operatorname{\mathcal{C}}$. Since $\operatorname{\mathcal{C}}$ admits small colimits, the diagram $F_0$ admits a left Kan extension $F: \operatorname{N}_{\bullet }( Q ) \rightarrow \operatorname{\mathcal{C}}$ (Proposition 7.6.6.13). Then $D = F( \alpha )$ is a colimit of the diagram $F_{0}$, and we can identify $u$ with the morphism obtained by evaluating the functor $F$ on the edge of $\operatorname{N}_{\bullet }( Q )$ given by the pair $(0 \leq \alpha )$. We will show that the restriction $F|_{ \operatorname{N}_{\bullet }( \mathrm{Ord}_{\leq \alpha } )}$ exhibits $u$ as a transfinite pushout of morphisms belonging to $\{ w_ s \} _{s \in S}$.

We first claim that that if $\beta \leq \alpha $ is a nonzero limit ordinal, then the restriction $F|_{ \operatorname{N}_{\bullet }( \mathrm{Ord}_{ \leq \beta } ) }$ is a colimit diagram in $\operatorname{\mathcal{C}}$. Set $Q_{\leq \beta } = \{ q \in Q: q \leq \beta \} $ and $Q_{ < \beta } = \{ q \in Q: q < \beta \} $. Since the functor $F$ is left Kan extended from $\operatorname{N}_{\bullet }(Q_0)$, it is also left Kan extended from larger $\infty $-category $\operatorname{N}_{\bullet }( (S \times [1]) \coprod \mathrm{Ord}_{ < \beta } )$ (see Corollary 7.3.8.8). It follows that $F|_{ \operatorname{N}_{\bullet }( Q_{\leq \beta } ) }$ is a colimit diagram in $\operatorname{\mathcal{C}}$. It will therefore suffice to show that $\operatorname{N}_{\bullet }(\iota )$ is right cofinal, where $\iota $ denotes the inclusion map $\mathrm{Ord}_{< \beta } \hookrightarrow Q_{ < \beta }$ (Corollary 7.2.2.2). This is a special case of Corollary 7.2.3.7, since $\iota $ admits a left adjoint (given on $S \times [1]$ by the construction $(s,0) \mapsto 0$ and $(s,1) \mapsto \ell (s) + 1$).

Now suppose that $\beta = \gamma +1$ is a successor ordinal. Let $s \in S$ be the unique element satisfying $\ell (s) = \gamma $. We will complete the proof by showing that the morphism $F(\gamma ) \rightarrow F(\beta )$ in $\operatorname{\mathcal{C}}$ can be realized as a pushout of $w_ s$. More precisely, we will show that the functor $F$ carries the diagram

in $\operatorname{N}_{\bullet }( Q )$ to a pushout diagram in the $\infty $-category $\operatorname{\mathcal{C}}$. Arguing as above, we see that the restriction $F|_{ Q_{\leq \beta } }$ is a colimit diagram. Using Corollary 7.2.2.2 again, we are reduced to showing that $\operatorname{N}_{\bullet }( \iota )$ is right cofinal, where $\iota $ denotes the inclusion of partially ordered sets $\{ (s,1) > (s,0) < \beta \} \hookrightarrow Q_{< \beta }$. This again follows from Corollary 7.2.3.7, since $\iota $ admits a left adjoint given by the construction