Kerodon

Proof. By virtue of Corollary 4.4.5.4, the restriction map $\theta : \operatorname{Fun}(B,\operatorname{\mathcal{C}})^{\simeq } \rightarrow \operatorname{Fun}(A, \operatorname{\mathcal{C}})^{\simeq }$ is a Kan fibration. Since the inclusion $A \hookrightarrow B$ is a categorical equivalence, the map $\theta $ is a homotopy equivalence of Kan complexes (Proposition 4.5.3.8). Invoking Proposition 3.3.7.6, we conclude that $\theta $ is a trivial Kan fibration. In particular, it is surjective on vertices. $\square$

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

which is a categorical equivalence by virtue of Corollary 4.5.4.15. 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, the restriction $v|_{A}$ factors through the full subcategory $\operatorname{Isom}(\operatorname{\mathcal{C}})$. Invoking Lemma 4.5.5.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.14), 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$

Proof of Proposition 4.5.5.1. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty $-categories. Assume first that $F$ satisfies condition $(\ast )$ of Proposition 4.5.5.1; we will prove that $F$ is an isofibration. For $0 < i < n$, the inner horn inclusion $\Lambda ^{n}_{i} \hookrightarrow \Delta ^ n$ is a categorical equivalence (Corollary 4.5.3.14), so condition $(\ast )$ guarantees that $F$ is an inner fibration. Fix an object $C \in \operatorname{\mathcal{C}}$ and an isomorphism $u: D \rightarrow F(C)$ in the $\infty $-category $\operatorname{\mathcal{D}}$; we wish to show that $u$ can be lifted to an isomorphism $\overline{u}: \overline{D} \rightarrow C$ in the $\infty $-category $\operatorname{\mathcal{C}}$. By virtue of Corollary 4.4.3.14, we can assume that $u = G(v)$ for some functor $G: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$, where $\operatorname{\mathcal{E}}$ is a contractible Kan complex and $v: X \rightarrow Y$ is a morphism in $\operatorname{\mathcal{E}}$. Since the inclusion $\{ Y\} \hookrightarrow \operatorname{\mathcal{E}}$ is a categorical equivalence (Example 4.5.1.13), condition $(\ast )$ guarantees the existence of a solution to the lifting problem

Then $\overline{u} = \overline{G}(v)$ is an isomorphism of $\operatorname{\mathcal{C}}$ having the desired property.

Now suppose that the functor $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ is an isofibration; we wish to show that condition $(\ast )$ is satisfied. Let $B$ be a simplicial set and $A \subseteq B$ a simplicial subset for which the inclusion $A \hookrightarrow B$ is a categorical equivalence. We wish to show that every lifting problem

admits a solution. Invoking Lemma 4.5.5.2, we see that $f_0$ can be extended to a morphism of simplicial sets $f': B \rightarrow \operatorname{\mathcal{C}}$. Let $\overline{f}'$ denote the composition $B \xrightarrow {f'} \operatorname{\mathcal{C}}\xrightarrow {F} \operatorname{\mathcal{D}}$, so that $\overline{f}|_{A} = \overline{f}'|_{A}$. Invoking Lemma 4.5.5.3, we conclude that there exists an isomorphism $\overline{u}: \overline{f} \rightarrow \overline{f}'$ in the diagram $\infty $-category $\operatorname{Fun}(B, \operatorname{\mathcal{D}})$ whose image in $\operatorname{Fun}(A, \operatorname{\mathcal{D}})$ is the identity transformation $\operatorname{id}_{ \overline{f}|_{A} }$. Applying Corollary 4.4.5.9, we deduce that $\overline{u}$ can be lifted to an isomorphism $u: f \rightarrow f'$ in the diagram $\infty $-category $\operatorname{Fun}(B, \operatorname{\mathcal{C}})$ whose image in $\operatorname{Fun}(A, \operatorname{\mathcal{C}})$ is the identity transformation $\operatorname{id}_{ f_0 }$. The diagram $f: B \rightarrow \operatorname{\mathcal{C}}$ then satisfies $f|_{A} = f_0$ and $F \circ f = \overline{f}$, as desired. $\square$

Proof. Assume that condition $(\ast )$ is satisfied; we will show that the morphism $i: A \hookrightarrow B$ is a categorical equivalence of simplicial sets (the converse follows from Proposition 4.5.5.1). Fix an $\infty $-category $\operatorname{\mathcal{E}}$; we wish to show that precomposition with $i$ induces a bijection $\theta : \pi _0( \operatorname{Fun}(B, \operatorname{\mathcal{E}})^{\simeq } ) \rightarrow \pi _0( \operatorname{Fun}(A, \operatorname{\mathcal{E}})^{\simeq } )$. The surjectivity of $\theta $ follows by applying condition $(\ast )$ to the isofibration $\operatorname{\mathcal{E}}\rightarrow \Delta ^0$, and the injectivity of $\theta $ follows by applying $\theta $ to the isofibration $\operatorname{Isom}(\operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{E}}\times \operatorname{\mathcal{E}}$ of Corollary 4.4.5.5. $\square$

Proof. Let $B'$ be a simplicial set and let $A' \subseteq B'$ be a simplicial subset for which the inclusion $A' \hookrightarrow B'$ is a categorical equivalence. We wish to show that every lifting problem

admits a solution. Unwinding the definitions, we are reduced to the problem of solving an associated lifting problem

The left vertical map in this diagram is a categorical equivalence by virtue of Corollary 4.5.4.15, so the existence of the desired solution follows from our assumption that $q$ is an isofibration. $\square$

Proof. Apply Proposition 4.5.5.14 in the special case $A = \emptyset $. $\square$

Proof. The morphism $\theta $ is a pullback of the isofibration $\operatorname{Fun}(B,X) \rightarrow \operatorname{Fun}(A,X) \times _{ \operatorname{Fun}(A,S) } \operatorname{Fun}(B,S)$ of Proposition 4.5.5.14, and is therefore also an isofibration (Remark 4.5.5.11). We conclude by observing that since $q$ is an inner fibration (Remark 4.5.5.7), the simplicial sets $\operatorname{Fun}_{/S}(B,X)$ and $\operatorname{Fun}_{/S}(A,X)$ are $\infty $-categories (Proposition 4.1.4.6). $\square$

Proof. Let $B'$ be a simplicial set and let $A' \subseteq B'$ be a simplicial subset. We wish to show that every lifting problem

admits a solution. Unwinding the definitions, we are reduced to the problem of solving an associated lifting problem

The left vertical map in this diagram is a categorical equivalence by virtue of Corollary 4.5.4.15, so the existence of the desired solution follows from our assumption that $q$ is an isofibration. $\square$

Proof. Apply Proposition 4.5.5.18 in the special case $S = \Delta ^0$. $\square$

Proof. If $q$ is a trivial Kan fibration, then it is an isofibration by virtue of Example 4.5.5.8 and a categorical equivalence by virtue of Proposition 4.5.3.11. Conversely, suppose that $q$ is both an isofibration and a categorical equivalence. Using Exercise 3.1.7.11, we can write $q$ as a composition $X \xrightarrow {q'} Y \xrightarrow {q''} S$, where $q'$ is a monomorphism and $q''$ is a trivial Kan fibration. Then $q''$ is a categorical equivalence (Proposition 4.5.3.11), so that $q'$ is also a categorical equivalence (Remark 4.5.3.5). Invoking our assumption that $q$ is an isofibration, we conclude that the lifting problem

admits a solution. It follows that $q$ is a retract of the morphism $q''$, and is therefore also a trivial Kan fibration. $\square$