Kerodon

Proof. Apply Proposition 4.4.5.1 in the special case $\operatorname{\mathcal{D}}= \Delta ^0$. $\square$

Proof. Combine Corollary 4.4.5.3 with Proposition 4.4.3.7. $\square$

Proof. Combine Corollary 4.4.5.3 with Example 4.4.1.14. $\square$

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

Proof. Combine Corollary 4.4.5.6 with Proposition 4.4.3.7. $\square$

Proof. We proceed as in the proof of Lemma 4.4.4.8, with some minor modifications. Let $P$ denote the collection of all pairs $(K, h_ K)$, where $K \subseteq B$ is a simplicial subset containing $A$ and $h_ K: \Delta ^1 \times K \rightarrow \operatorname{\mathcal{C}}$ is a morphism of simplicial sets satisfying

We regard $P$ as partially ordered set, where $(K, h_ K) \leq (K', h_{K'} )$ if $K \subseteq K'$ and $h_ K = h_{K'} |_{\Delta ^1 \times K}$. The partially ordered set $P$ satisfies the hypotheses of Zorn's lemma, and therefore has a maximal element $(K_{\mathrm{max}}, h_{K_{\mathrm{max}}})$. We will complete the proof by showing that $K_{\mathrm{max}} = B$. Assume otherwise. Then there exists some nondegenerate $n$-simplex $\tau : \Delta ^{n} \rightarrow B$ whose image is not contained in $K_{ \mathrm{max} }$. Choosing $n$ as small as possible, we can assume that $\tau $ carries the boundary $\operatorname{\partial \Delta }^{n}$ into $K_{\mathrm{max}}$. Note that, since $A$ contains every vertex of $B$, we must have $n > 0$. Let $K' \subseteq B$ be the union of $K_{\mathrm{max}}$ with the image of $\tau $, so that we have a pushout diagram of simplicial sets

We will complete the proof by showing that the lifting problem

admits a solution, where the dotted arrow carries each edge $\Delta ^1 \times \{ x\} $ to an isomorphism in $\operatorname{\mathcal{C}}$ (contradicting the maximality of the pair $(K_{\mathrm{max}}, h_{K_{\mathrm{max}}} )$). To prove this, we can replace the inclusion $K_{\mathrm{max}} \hookrightarrow K'$ by $\operatorname{\partial \Delta }^ n \hookrightarrow \Delta ^ n$. We are therefore reduced to proving Lemma 4.4.4.8 in the special case where $B = \Delta ^ n$ is a simplex and $A = \operatorname{\partial \Delta }^ n$ is its boundary.

Let

be the sequence of simplicial subsets appearing in the proof of Lemma 3.1.2.12, so that $h_0$ can be identified with a morphism of simplicial sets from $X(0)$ to $\operatorname{\mathcal{C}}$. We will show that, for $0 \leq i \leq n+1$, there exists a morphism of simplicial sets $h_ i: X(i) \rightarrow \operatorname{\mathcal{C}}$ satisfying $h_ i|_{X(0)} = h_0$ and $F \circ h_ i = \overline{h}|_{ X(i)}$ (taking $i = n+1$, this will complete the proof of Proposition 4.4.5.8). We proceed by induction on $i$, the case $i=0$ being vacuous. Assume that $i > 0$ and that we have already constructed a morphism $h_{i-1}: X(i-1) \rightarrow \operatorname{\mathcal{C}}$ satisfying $h_{i-1}|_{X(0)} = h_0$ and $F \circ h_{i-1} = \overline{h}|_{ X(i-1)}$. By virtue of Lemma 3.1.2.12, we have a pushout diagram of simplicial sets

Consequently, to prove the existence of $h_{i}$, it suffices to solve the lifting problem

For $0 < i < n+1$, the existence of the desired solution follows from our assumption that $F$ is an inner fibration. In the case $i = n+1$, the existence follows from Proposition 4.4.2.13, since the map $\sigma : \Delta ^{n+1} \rightarrow \Delta ^1 \times \Delta ^ n$ carries the final edge $\operatorname{N}_{ \bullet }( \{ n < n+1 \} ) \subseteq \Delta ^{n+1}$ to the edge $\Delta ^1 \times \{ n\} \subseteq \Delta ^1 \times \Delta ^ n$, which $h_0$ carries to an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}$ by virtue of assumption $(\ast )$. $\square$

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

Proof of Proposition 4.4.5.1. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be an isofibration of $\infty $-categories, let $B$ be a simplicial set, and let $A \subseteq B$ be a simplicial subset. We wish to show that the restriction map

is an isofibration of $\infty $-categories. We first note that the projection map

is a pullback of the inner fibration $\operatorname{Fun}(B, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}(A, \operatorname{\mathcal{D}})$ (see Corollary 4.1.4.2). Since $\operatorname{Fun}(A, \operatorname{\mathcal{C}})$ is an $\infty $-category (Theorem 1.5.3.7), it follows that $\operatorname{Fun}( A, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(A, \operatorname{\mathcal{D}}) } \operatorname{Fun}(B, \operatorname{\mathcal{D}})$ is also an $\infty $-category (Remark 4.1.1.9). It follows from Proposition 4.1.4.1 that $F'$ is an inner fibration. It will therefore suffice to show that, for every object $Y \in \operatorname{Fun}(B,\operatorname{\mathcal{C}})$, every isomorphism $u: X \rightarrow F'(Y)$ in the $\infty $-category $\operatorname{Fun}( A, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(A, \operatorname{\mathcal{D}}) } \operatorname{Fun}(B, \operatorname{\mathcal{D}})$ can be lifted to an isomorphism $\overline{u}: \overline{X} \rightarrow Y$ in the $\infty $-category $\operatorname{Fun}(B, \operatorname{\mathcal{C}})$. This follows immediately from Corollary 4.4.5.9. $\square$