# Kerodon

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

Lemma 4.5.6.3. Let $\operatorname{\mathcal{C}}$ be an $\infty$-category, let $B$ be a simplicial set, let $A \subseteq B$ be a simplicial subset, and suppose we are given a pair of diagrams $f,g: B \rightarrow \operatorname{\mathcal{C}}$ together with a natural transformation $u_0: f|_{A} \rightarrow f'|_{A}$. If the inclusion $A \hookrightarrow B$ is a categorical equivalence, then $u_0$ can be lifted to a natural transformation $u: f \rightarrow f'$. Moreover, if $u_0$ is a natural isomorphism, then $u$ is automatically a natural isomorphism.

Proof. The existence of the natural isomorphism $u$ follows by applying Lemma 4.5.6.2 to the inclusion of simplicial sets

$(\Delta ^1 \times A) \coprod _{ (\operatorname{\partial \Delta }^1 \times A)} (\operatorname{\partial \Delta }^1 \times B) \hookrightarrow \Delta ^1 \times B,$

which is a categorical equivalence by virtue of Corollary 4.5.3.10. We will complete the proof by showing that if $u_0$ is a natural isomorphism, then $u$ is a natural isomorphism.

Let us identify $u$ with a morphism of simplicial sets $v: B \rightarrow \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}})$, and let $\operatorname{Isom}(\operatorname{\mathcal{C}})$ denote the full subcategory of $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}})$ spanned by the isomorphisms in $\operatorname{\mathcal{C}}$. Since $u_0$ is a natural isomorphism, then restriction $v|_{A}$ factors through the full subcategory $\operatorname{Isom}(\operatorname{\mathcal{C}})$. Invoking Lemma 4.5.6.2, we conclude that $v|_{A}$ extends to a diagram $v': B \rightarrow \operatorname{Isom}(\operatorname{\mathcal{C}})$. Since the inclusion $A \hookrightarrow B$ is a categorical equivalence, the equality $v|_{A} = v'|_{A}$ guarantees that $v$ and $v'$ are isomorphic as objects of the $\infty$-category $\operatorname{Fun}(B, \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}}) )$. Since the full subcategory $\operatorname{Isom}(\operatorname{\mathcal{C}}) \subseteq \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}})$ is replete (Example 4.4.1.13), we conclude that $v$ also factors through $\operatorname{Isom}(\operatorname{\mathcal{C}})$, so that $u$ is a natural isomorphism by virtue of Theorem 4.4.4.4. $\square$