# Kerodon

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

Corollary 7.1.6.6. Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be an inner fibration of $\infty$-categories, let $B$ and $K$ be simplicial sets, and let $A \subseteq B$ be a simplicial subset which contains every vertex of $B$. Suppose we are given a lifting problem

7.4
$$\begin{gathered}\label{equation:relative-colimit-pointwise-existence-strong} \xymatrix@R =50pt@C=50pt{ (B \times K) \coprod _{ (A \times K ) } (A \times K^{\triangleright }) \ar [r]^-{ f } \ar [d] & \operatorname{\mathcal{C}}\ar [d]^{U} \\ B \times K^{\triangleright } \ar [r] \ar@ {-->}[ur]^{ \overline{f} } & \operatorname{\mathcal{D}}} \end{gathered}$$

which satisfies the following condition:

$(\ast )$

Let $\sigma : \Delta ^ n \rightarrow B$ be an $n$-simplex which does not belong to $A$, and let $a = \sigma (0)$ be the initial vertex. Then the restriction

$f_{a} = f|_{ \{ a\} \times K^{\triangleright } }: K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$

is a $U$-colimit diagram.

Then the lifting problem (7.4) admits a solution $\overline{f}: B \times K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$.

Proof. Set $\operatorname{\mathcal{C}}' = \operatorname{Fun}(K^{\triangleright }, \operatorname{\mathcal{C}})$ and $\operatorname{\mathcal{D}}' = \operatorname{Fun}(K,\operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(K, \operatorname{\mathcal{D}}) } \operatorname{Fun}(K^{\triangleright }, \operatorname{\mathcal{D}})$, so that $U$ induces an inner fibration $U': \operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{D}}'$ (Proposition 4.1.4.1). We can then rewrite (7.4) as a lifting problem

$\xymatrix@R =50pt@C=50pt{ A \ar [r]^-{g} \ar [d] & \operatorname{\mathcal{C}}' \ar [d]^{U'} \\ B \ar@ {-->}[ur] \ar [r]^-{g_0} & \operatorname{\mathcal{D}}'. }$

Let $P$ be the partially ordered set of pairs $(A', g')$, where $A' \subseteq B$ is a simplicial subset containing $A$, and $g': A' \rightarrow \operatorname{\mathcal{C}}'$ is a morphism satisfying $g'|_{A} = g$ and $U' \circ g' = g_0|_{A'}$. The partially ordered set $P$ satisfies the hypotheses of Zorn's lemma and therefore contains a maximal element $(A_{\mathrm{max}}, g_{\mathrm{max}})$. To complete the proof, it will suffice to show that $A_{\mathrm{max}} = B$. Assume otherwise: then there exists some $n$-simplex $\sigma : \Delta ^ n \rightarrow B$ which is not contained in $A_{\mathrm{max}}$. Choose $n$ as small as possible, so that $\sigma$ carries the boundary $\operatorname{\partial \Delta }^ n$ into $A_{\mathrm{max}}$. Since every vertex of $A$ is contained in $B$, we must have $n > 0$. Moreover, it follows from $(\ast )$ together with Proposition 7.1.6.3 that the vertex $a = \sigma (0)$ is a $U'$-initial object of $\operatorname{\mathcal{C}}'$. Applying Corollary 7.1.4.17, we deduce that the lifting problem

$\xymatrix@R =50pt@C=50pt{ \operatorname{\partial \Delta }^{n} \ar [r]^-{ g_{\mathrm{max}} \circ \sigma } \ar [d] & \operatorname{\mathcal{C}}' \ar [d]^{U'} \\ \Delta ^{n} \ar@ {-->}[ur] \ar [r]^-{ g_0 \circ \sigma } & \operatorname{\mathcal{D}}' }$

has a solution, which contradicts the maximality of $(A_{\mathrm{max}}, g_{\mathrm{max}} )$. $\square$