# Kerodon

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

Lemma 5.6.4.1. Suppose we are given a commutative diagram of simplicial sets

5.52
$$\begin{gathered}\label{equation:isomorphism-extension-small-diagram} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}_0 \ar [r]^-{G_0} \ar [d]^{U_0} & \operatorname{\mathcal{E}}' \ar [d]^{V} \\ \operatorname{\mathcal{C}}_0 \ar [r] & \operatorname{\mathcal{C}}} \end{gathered}$$

where the vertical maps are inner fibrations, the bottom horizontal map exhibits $\operatorname{\mathcal{C}}_0$ as a simplicial subset of $\operatorname{\mathcal{C}}$, and $G_0$ induces an equivalence $\operatorname{\mathcal{E}}_0 \rightarrow \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}'$ of inner fibrations over $\operatorname{\mathcal{C}}_0$. Then (5.52) can be extended to a commutative diagram

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}_0 \ar [r] \ar [d]^{U_0} & \operatorname{\mathcal{E}}\ar [d]^{U} \ar [r]^-{G} & \operatorname{\mathcal{E}}' \ar [d]^{V} \\ \operatorname{\mathcal{C}}_0 \ar [r] & \operatorname{\mathcal{C}}\ar@ {=}[r] & \operatorname{\mathcal{C}}, }$

where $U$ is an inner fibration, $G$ is an equivalence of inner fibrations over $\operatorname{\mathcal{C}}$, and the square on the left induces an isomorphism of simplicial sets $\operatorname{\mathcal{E}}_0 \simeq \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$.

Proof. Choose a monomorphism of simplicial sets $\operatorname{\mathcal{E}}_0 \hookrightarrow \operatorname{\mathcal{Q}}$, where $\operatorname{\mathcal{Q}}$ is a contractible Kan complex (see Exercise 3.1.7.11). Replacing $\operatorname{\mathcal{E}}'$ with the product $\operatorname{\mathcal{E}}' \times \operatorname{\mathcal{Q}}$, we can reduce to the case where $G_0$ is a monomorphism of simplicial sets. Let $\operatorname{\mathcal{E}}$ denote the simplicial subset of $\operatorname{\mathcal{E}}'$ consisting of those simplices $\sigma : \Delta ^ m \rightarrow \operatorname{\mathcal{E}}'$ for which the induced map $\operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \Delta ^ m \rightarrow \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}'$ factors through $G_0$. To complete the proof, it will suffice to verify the following:

$(a)$

The morphism $U = V|_{\operatorname{\mathcal{E}}}$ is an inner fibration from $\operatorname{\mathcal{E}}$ to $\operatorname{\mathcal{C}}$.

$(b)$

The inclusion $\operatorname{\mathcal{E}}\hookrightarrow \operatorname{\mathcal{E}}'$ is an equivalence of inner fibrations over $\operatorname{\mathcal{C}}$.

By virtue of Remark 4.1.1.13 and Proposition 5.1.6.9, it suffices to prove $(a)$ and $(b)$ in the special case where $\operatorname{\mathcal{C}}= \Delta ^ n$ is a standard simplex. In this case, the morphism $V: \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$ is an isofibration (Example 4.4.1.6).

Let $\operatorname{\mathcal{E}}'_{0}$ denote the fiber product $\operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}'$. Applying Lemma 5.1.6.12 to the morphism $G_0: \operatorname{\mathcal{E}}_0 \rightarrow \operatorname{\mathcal{E}}'_0$ (which is an equivalence of inner fibrations over $\operatorname{\mathcal{C}}_{0}$), we deduce that there exists a morphism $R_0: \operatorname{\mathcal{E}}'_{0} \rightarrow \operatorname{\mathcal{E}}_0$ in the category $(\operatorname{Set_{\Delta }})_{/\operatorname{\mathcal{C}}_0}$ such that $R_0 \circ G_0 = \operatorname{id}_{\operatorname{\mathcal{E}}_0}$, and an isomorphism $\alpha _0: \operatorname{id}_{ \operatorname{\mathcal{E}}'_0 } \rightarrow G_0 \circ R_0$ in the $\infty$-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0}( \operatorname{\mathcal{E}}'_0, \operatorname{\mathcal{E}}'_0 )$ whose image in $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{E}}'_0 )$ is degenerate. Applying Proposition 4.4.5.8 (and the criterion of Proposition 4.4.4.9), we can choose a morphism $R: \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{E}}'$ in $(\operatorname{Set_{\Delta }})_{/\operatorname{\mathcal{C}}}$ such that $R|_{\operatorname{\mathcal{E}}'_0} = G_0 \circ R_0$ and an isomorphism $\alpha : \operatorname{id}_{\operatorname{\mathcal{E}}'} \rightarrow R$ in the $\infty$-category $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}')$ whose image in $\operatorname{Fun}_{/\operatorname{\mathcal{C}}_0}(\operatorname{\mathcal{E}}'_0, \operatorname{\mathcal{E}}'_0)$ is equal to $\alpha _0$.

We now prove $(a)$. Suppose we are given a lifting problem

$\xymatrix@R =50pt@C=50pt{ A \ar [d] \ar [r]^-{f_0} & \operatorname{\mathcal{E}}\ar [d]^{U} \\ B \ar [r]^-{\overline{f}} \ar@ {-->}[ur]^{f} & \operatorname{\mathcal{C}}, }$

where the left vertical map is inner anodyne. Since $V: \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}$ is an inner fibration, we can extend $f_0$ to a morphism $f': B \rightarrow \operatorname{\mathcal{E}}$ satisfying $V \circ f' = \overline{f}$. Set $B_0 = \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} B$ and $A_0 = \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} A$, and define

$f_{1}: (A \coprod _{A_0} B_0) \rightarrow \operatorname{\mathcal{E}}$

by the formula $f_1|_{A} = f_0$ and $f_1|_{B_0} = R \circ f'|_{B_0}$. Note that there is an isomorphism

$\beta : f'|_{ A \coprod _{A_0} B_0} \rightarrow f_{1}$

in the $\infty$-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( A \coprod _{A_0} B_0, \operatorname{\mathcal{E}}' )$, whose image in $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}( A, \operatorname{\mathcal{E}}')$ is degenerate and whose image in $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}( B_0, \operatorname{\mathcal{E}}' )$ is the restriction of $\alpha$. Applying Proposition 4.4.5.8, we deduce that $f_{1}$ admits an extension $f: B \rightarrow \operatorname{\mathcal{C}}$ satisfying $U \circ f = \overline{f}$.

To prove $(b)$, we observe that the morphism $R: \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{E}}$ is a homotopy inverse of the inclusion $\iota : \operatorname{\mathcal{E}}\hookrightarrow \operatorname{\mathcal{E}}'$ relative to $\operatorname{\mathcal{C}}$. By construction, $\alpha$ determines an isomorphism from $\operatorname{id}_{\operatorname{\mathcal{E}}'}$ to the composition $\iota \circ R$ in the $\infty$-category $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}')$, and the restriction of $\alpha$ determines an isomorphism from $\operatorname{id}_{\operatorname{\mathcal{E}}}$ to $R \circ \iota$ in the $\infty$-category $\operatorname{Fun}_{/\operatorname{\mathcal{C}}}(\operatorname{\mathcal{E}}, \operatorname{\mathcal{E}})$. $\square$