# Kerodon

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

Corollary 4.4.5.9. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be an isofibration of $\infty$-categories, let $B$ be a simplicial set, let $A \subseteq B$ be a simplicial subset, and suppose we are given a lifting problem

$\xymatrix@R =50pt@C=50pt{ (\Delta ^1 \times A) \coprod _{ (\{ 1\} \times A) } (\{ 1 \} \times B) \ar [r]^-{h_0} \ar [d] & \operatorname{\mathcal{C}}\ar [d]^{F} \\ \Delta ^1 \times B \ar [r]^-{ \overline{h} } \ar@ {-->}[ur]^{h} & \operatorname{\mathcal{D}}}$

with the following properties:

• For every vertex $a \in A$, the edge

$\Delta ^1 \simeq \Delta ^1 \times \{ a\} \xrightarrow {h_0} \operatorname{\mathcal{C}}$

is an isomorphism in $\operatorname{\mathcal{C}}$.

• For every vertex $b \in B$, the edge

$\Delta ^1 \simeq \Delta ^1 \times \{ b\} \xrightarrow { \overline{h} } \operatorname{\mathcal{D}}$

is an isomorphism in $\operatorname{\mathcal{D}}$.

Then $h_0$ can be extended to a diagram $h: \Delta ^1 \times B \rightarrow \operatorname{\mathcal{C}}$ satisfying $\overline{h} = F \circ h$. Moreover, we can arrange that for every vertex $b \in B$, the edge $\Delta ^1 \simeq \Delta ^1 \times \{ b\} \xrightarrow {h} \operatorname{\mathcal{C}}$ is an isomorphism in the $\infty$-category $\operatorname{\mathcal{C}}$ (so that $h$ can be regarded as an isomorphism in the diagram $\infty$-category $\operatorname{Fun}(B,\operatorname{\mathcal{C}})$, by virtue of Theorem 4.4.4.4).

Proof. Let $A'$ be the union of $A$ with the $0$-skeleton $\operatorname{sk}_0(B)$, regarded as a simplicial subset of $B$. For each vertex $b \in B$ which does not belong to $A$, our assumption that $F$ is an isofibration allows us to choose an edge $e_{b}: \Delta ^1 \rightarrow \operatorname{\mathcal{C}}$ which is an isomorphism in the $\infty$-category $\operatorname{\mathcal{C}}$ satisfying $e_ b(1) = h_0( 1, b)$ and $F \circ e_{b} = \overline{h}|_{ \Delta ^1 \times \{ b\} }$. The morphism $h_0$ and the edges $e_{b}$ can then be amalgamated to a map $h'_0: (\Delta ^1 \times A') \coprod _{ (\{ 1\} \times A') } (\{ 1 \} \times B) \rightarrow \operatorname{\mathcal{C}}$. The desired result now follows by applying Proposition 4.4.5.8 to the commutative diagram

$\xymatrix@R =50pt@C=50pt{ (\Delta ^1 \times A') \coprod _{ (\{ 1\} \times A') } (\{ 1 \} \times B) \ar [r]^-{h'_0} \ar [d] & \operatorname{\mathcal{C}}\ar [d]^{F} \\ \Delta ^1 \times B \ar [r]^-{ \overline{h} } & \operatorname{\mathcal{D}}. }$
$\square$