Kerodon

Proof. Let $U: \operatorname{\mathcal{C}}_{/C} \rightarrow \operatorname{\mathcal{C}}$ be the projection map and let $f: X \rightarrow Y$ be a morphism of $\operatorname{\mathcal{C}}$ which can be written as a transfinite composition of morphisms of $\operatorname{\mathcal{C}}$. Suppose we are given a morphism $X \rightarrow C$ in $\operatorname{\mathcal{C}}$, which we identify with an object $\widetilde{X} \in \operatorname{\mathcal{C}}_{/C}$ satisfying $U( \widetilde{X} ) = X$. We wish to show that there is a morphism $\widetilde{f}: \widetilde{X} \rightarrow \widetilde{Y}$ of $\operatorname{\mathcal{C}}_{/C}$ satisfying $U( \widetilde{f} ) = f$.

Choose an ordinal $\alpha $ and a functor $F: \operatorname{N}_{\bullet }( \mathrm{Ord}_{ \leq \alpha } ) \rightarrow \operatorname{\mathcal{C}}$ which exhibits $f$ as a transfinite composition of morphisms of $W$. Let $Q$ be the collection of all ordered pairs $(\beta , \widetilde{F}_{\leq \beta } )$, where $\beta \leq \alpha $ is an ordinal and $\widetilde{F}_{\leq \beta }: \operatorname{N}_{\bullet }( \mathrm{Ord}_{\leq \beta } ) \rightarrow \operatorname{\mathcal{C}}_{/C}$ is a functor satisfying $\widetilde{F}_{\leq \beta }(0) = \widetilde{X}$ and $U \circ \widetilde{F}_{\leq \beta } = F|_{ \operatorname{N}_{\bullet }( \mathrm{Ord}_{\leq \beta } ) }$. We regard $Q$ as a partially ordered set, where $(\beta , \widetilde{F}_{\leq \beta } ) \leq (\beta ', \widetilde{F}'|_{\leq \beta '})$ if $\beta \leq \beta '$ and $\widetilde{F}_{\leq \beta } = \widetilde{F}'_{\leq \beta '} |_{ \operatorname{N}_{\bullet }( \mathrm{Ord}_{\leq \beta } ) }$.

We first claim that $Q$ satisfies the hypotheses of Zorn's lemma. Let $Q_0 \subseteq Q$ be a linearly ordered subset of $Q$; we wish to show that $Q_0$ admits an upper bound. If $Q_0$ is empty, we can take this upper bound be the pair $(0, \widetilde{F}_{\leq 0} )$, where $\widetilde{F}_{\leq 0}$ is the constant functor taking the value $\widetilde{X}$. Without loss of generality, we may assume that $Q_0$ does not contain a maximal element (otherwise, there is nothing to prove). Write $Q_0 = \{ ( \beta _ i, \widetilde{F}_{\leq \beta _ i} ) \} _{i \in I}$ and let $\beta \leq \alpha $ be the supremum of the set $\{ \beta _ i \} _{i \in I}$. The functors $\widetilde{F}_{\leq \beta _ i}$ can then be amalgamated to a single functor $\widetilde{F}_{< \beta }: \operatorname{N}_{\bullet }( \mathrm{Ord}_{< \beta } ) \rightarrow \operatorname{\mathcal{C}}_{/C}$. To find an upper bound for $Q_0$, it will suffice to show that the lifting problem

admits a solution. This follows immediately from our assumption that $F|_{ \operatorname{N}_{\bullet }( \mathrm{Ord}_{\leq \beta } ) }$ is a colimit diagram in $\operatorname{\mathcal{C}}$.

Applying Zorn's lemma, we deduce that $Q$ contains a maximal element $(\beta , \widetilde{F}_{\leq \beta } )$. To complete the proof, it will suffice to show that $\beta = \alpha $; we can then take $\widetilde{f}$ to be obtained by applying the functor $\widetilde{F}$ to the edge of $\operatorname{N}_{\bullet }( \mathrm{Ord}_{\leq \alpha } )$ given by the pair $(0, \alpha )$. Assume otherwise, let $F_{\leq \beta }$ denote the restriction $F|_{ \operatorname{N}_{\bullet }( \mathrm{Ord}_{\leq \beta } )}$, and let $\operatorname{\mathcal{D}}$ denote the coslice $\infty $-category $\operatorname{\mathcal{C}}_{ F_{\leq \beta } / }$. Then $F_{\leq \beta +1}$ and $\widetilde{F}_{\leq \beta }$ can be identified with objects $D,D' \in \operatorname{\mathcal{D}}$, and the maximality of $(\beta , \widetilde{F}_{\leq \beta } )$ guarantees that $\operatorname{Hom}_{\operatorname{\mathcal{D}}}( D, D' ) = \emptyset $. Since the inclusion map $\{ \beta \} \hookrightarrow \operatorname{N}_{\bullet }( \mathrm{Ord}_{\leq \beta } )$ is right anodyne (Corollary 4.6.7.24), the restriction map $V: \operatorname{\mathcal{D}}= \operatorname{\mathcal{C}}_{ F_{\leq \beta } / } \rightarrow \operatorname{\mathcal{C}}_{ F(\beta ) / }$ is a trivial Kan fibration (Corollary 4.3.6.14). It follows that the mapping space $\operatorname{Hom}_{\operatorname{\mathcal{C}}_{ F(\beta ) / } }( V(D), V(D') )$ is also empty: that is, there is no $2$-simplex of $\operatorname{\mathcal{C}}$ with boundary indicated in the diagram

This contradicts our assumption that the morphism $F(\beta ) \rightarrow F(\beta +1)$ belongs to $W$. $\square$