# Kerodon

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

Lemma 5.1.7.12. Let $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ be an isofibration of simplicial sets and $F: \operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{D}}$ be a monomorphism of simplicial sets. The following conditions are equivalent:

$(1)$

The restriction $(U \circ F): \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{E}}$ is an inner fibration and $F$ is an equivalence of inner fibrations over $\operatorname{\mathcal{E}}$.

$(2)$

There exists a morphism $G: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ in $(\operatorname{Set_{\Delta }})_{/\operatorname{\mathcal{E}}}$ satisfying $G \circ F = \operatorname{id}_{\operatorname{\mathcal{C}}}$ and an isomorphism $u: \operatorname{id}_{\operatorname{\mathcal{D}}} \rightarrow F \circ G$ in the $\infty$-category $\operatorname{Fun}_{/\operatorname{\mathcal{E}}}(\operatorname{\mathcal{D}}, \operatorname{\mathcal{D}})$ whose image in $\operatorname{Fun}_{/\operatorname{\mathcal{E}}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ is the identity morphism $\operatorname{id}_{F}: F \rightarrow F \circ G \circ F = F$.

Proof. We first show that $(2)$ implies $(1)$. Suppose that there exists a morphism $G: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ satisfying $G \circ F = \operatorname{id}_{\operatorname{\mathcal{C}}}$. Then $F$ and $G$ exhibit $\operatorname{\mathcal{C}}$ as a retract of $\operatorname{\mathcal{D}}$ in the category $(\operatorname{Set_{\Delta }})_{/\operatorname{\mathcal{E}}}$. Since $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ is an isofibration, it follows that $(U \circ F): \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{E}}$ is an isofibration (Remark 4.5.5.10). In particular, $U \circ F$ is an inner fibration (Remark 4.5.5.7). If there exists an isomorphism $u: \operatorname{id}_{\operatorname{\mathcal{D}}} \rightarrow F \circ G$ in the $\infty$-category $\operatorname{Fun}_{/\operatorname{\mathcal{E}}}(\operatorname{\mathcal{D}}, \operatorname{\mathcal{D}})$, then $G$ is a homotopy inverse of $F$ relative to $\operatorname{\mathcal{E}}$, so that $F$ is an equivalence of inner fibrations over $\operatorname{\mathcal{E}}$.

We now show that $(1)$ implies $(2)$. Assume that $U \circ F$ is an inner fibration and that $F$ is an equivalence of inner fibrations over $\operatorname{\mathcal{E}}$. Let $G': \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be a homotopy inverse of $F$ relative to $\operatorname{\mathcal{E}}$, so that there exists an isomorphism $e: \operatorname{id}_{\operatorname{\mathcal{C}}} \rightarrow G' \circ F$ in the $\infty$-category $\operatorname{Fun}_{/\operatorname{\mathcal{E}}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{C}})$. Applying Proposition 4.4.5.8, we can lift $e$ to an isomorphism $\widetilde{e}: G \rightarrow G'$ in the $\infty$-category $\operatorname{Fun}_{/\operatorname{\mathcal{E}}}(\operatorname{\mathcal{D}}, \operatorname{\mathcal{C}})$, where $G: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ satisfies $G \circ F = \operatorname{id}_{\operatorname{\mathcal{C}}}$. Note that $F$ is a categorical equivalence of simplicial sets (Proposition 5.1.7.5), and therefore induces a categorical equivalence

$(\Delta ^1 \times \operatorname{\mathcal{C}}) \coprod _{ (\operatorname{\partial \Delta }^1 \times \operatorname{\mathcal{C}})} (\operatorname{\partial \Delta }^1 \times \operatorname{\mathcal{D}}) \hookrightarrow \Delta ^1 \times \operatorname{\mathcal{D}}.$

Since $U$ is an isofibration, every lifting problem

$\xymatrix@R =50pt@C=50pt{ (\Delta ^1 \times \operatorname{\mathcal{C}}) \coprod _{ (\operatorname{\partial \Delta }^1 \times \operatorname{\mathcal{C}})} (\operatorname{\partial \Delta }^1 \times \operatorname{\mathcal{D}}) \ar [r] \ar [d] & \operatorname{\mathcal{D}}\ar [d]^{U} \\ \Delta ^1 \times \operatorname{\mathcal{D}}\ar [r] \ar@ {-->}[ur] & \operatorname{\mathcal{E}}}$

admits a solution. In particular, there exists a morphism $u: \operatorname{id}_{\operatorname{\mathcal{D}}} \rightarrow F \circ G$ in the $\infty$-category $\operatorname{Fun}_{ / \operatorname{\mathcal{E}}}( \operatorname{\mathcal{D}}, \operatorname{\mathcal{D}})$ whose image in $\operatorname{Fun}_{/\operatorname{\mathcal{E}}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ is the identity map $\operatorname{id}_{F}$. We will complete the proof by showing that $u$ is an isomorphism in the $\infty$-category $\operatorname{Fun}_{/\operatorname{\mathcal{E}}}(\operatorname{\mathcal{D}}, \operatorname{\mathcal{D}})$. Using the criterion of Proposition 4.4.4.9, we are reduced to checking that, for each vertex $D \in \operatorname{\mathcal{D}}$ having image $E = U(D) \in \operatorname{\mathcal{E}}$, the induced map $u_{D}: D \rightarrow (F \circ G)(D)$ is an isomorphism in the $\infty$-category $\operatorname{\mathcal{D}}_{E} = \{ E\} \times _{\operatorname{\mathcal{E}}} \operatorname{\mathcal{D}}$. This is clear, since $D$ is isomorphic (in the $\infty$-category $\operatorname{\mathcal{D}}_{E}$) to an object of the form $F(C)$ for $C \in \operatorname{\mathcal{C}}_{E}$, and the morphism $u_{F(C)}$ is equal to the identity $\operatorname{id}_{F(C)}$. $\square$