Kerodon

Proof. Let $\sigma $ and $\sigma '$ be $n$-simplices of $\operatorname{N}_{\bullet }^{\mathscr {F}}(A)$ which are isomorphic relative to $\operatorname{\partial \Delta }^ n$; we wish to show that $\sigma = \sigma '$. Note that $\sigma $ and $\sigma '$ have the same image in $\operatorname{N}_{\bullet }(A)$, which we can identify with a nondecreasing sequence $a_0 \leq a_1 \leq \cdots \leq a_ n$ of elements of $A$. Let us identify $\sigma $ with a commutative diagram of simplicial sets

and $\sigma '$ with a commutative diagram

Since $\sigma $ and $\sigma '$ have the same restriction to $\operatorname{\partial \Delta }^ n$, we automatically have $\tau _{i} = \tau '_{i}$ for $i < n$. To complete the proof, it will suffice to show that $\tau _{n} = \tau '_{n}$. Replacing $A$ by the subset $\{ a \in A: a \leq a_ n \} $, we may assume that $a_ n$ is the largest element of $A$. Let $\mathscr {F}': A \rightarrow \operatorname{Set_{\Delta }}$ be the constant functor taking the value $\mathscr {F}(a_ n)$. Then there is a unique natural transformation of functors $\gamma : \mathscr {F} \rightarrow \mathscr {F}'$ which is the identity when evaluated at $a_ n$. Passing to weighted nerves, we obtain a functor of $\infty $-categories

carrying $\sigma $ and $\sigma '$ to $\tau _ n$ and $\tau '_ n$, respectively. Since $\sigma $ and $\sigma '$ are isomorphic relative to $\operatorname{\partial \Delta }^{n}$, the simplices $\tau _ n$ and $\tau '_ n$ are isomorphic relative to $\operatorname{\partial \Delta }^ n$ as $n$-simplices of $\mathscr {F}(a_ n)$. Our assumption that $\mathscr {F}(a_ n)$ is a minimal $\infty $-category then guarantees that $\tau _ n = \tau '_ n$, as desired. $\square$

Proof. Without loss of generality, we may assume that $\operatorname{\mathcal{C}}= [n]$ is a linearly ordered set. In this case, the desired result is a reformulation of Proposition 5.3.8.7 (see Example 5.3.8.3). $\square$

Proof. The equivalence $(1) \Leftrightarrow (2)$ follows from Example 5.3.8.3 and the implication $(3) \Rightarrow (1)$ is a special case of Proposition 5.3.8.7. We will complete the proof by showing that $(1)$ implies $(3)$. Assume that condition $(1)$ is satisfied. For $0 \leq i \leq n$, let $\operatorname{\mathcal{E}}_{i}$ denote the fiber $U^{-1} \{ i\} = \{ i\} \times _{ \Delta ^ n } \operatorname{\mathcal{E}}$. For $1 \leq i \leq n$, choose a functor $T_{i}: \operatorname{\mathcal{E}}_{i-1} \rightarrow \operatorname{\mathcal{E}}_ i$ which is given by covariant transport for the cocartesian fibration $U$. Let $\mathscr {F}: [n] \rightarrow \operatorname{Set_{\Delta }}$ be the diagram given by the sequence of functors

Set $\operatorname{\mathcal{E}}' = \operatorname{N}_{\bullet }^{\mathscr {F} }([n])$, so that we have a canonical isomorphism

Let $\operatorname{Spine}[n]$ denote the spine of the standard $n$-simplex $\Delta ^ n$ (Example 1.5.7.7). Since the functors $T_ i$ are given by covariant transport with respect to $U$, Remark 5.2.4.3 guarantees that we can extend $F_0$ to a morphism

which is an equivalence of cocartesian fibrations over $\operatorname{Spine}[n]$. Since the inclusion map $\operatorname{Spine}[n] \hookrightarrow \Delta ^ n$ is inner anodyne (Example 1.5.7.7), Lemma 5.3.6.5 guarantees that the inclusion $\operatorname{Spine}[n] \times _{\Delta ^ n} \operatorname{\mathcal{E}}\hookrightarrow \operatorname{\mathcal{E}}$ is a categorical equivalence of simplicial sets, so that $F_1$ extends to a functor $F: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}'$. We then have a commutative diagram

where the horizontal maps are categorical equivalences by Lemma 5.3.6.5 and the left vertical map is a categorical equivalence by Proposition 5.1.7.5. It follows that $F$ is an equivalence of $\infty $-categories. The $\infty $-category $\operatorname{\mathcal{E}}$ is minimal by assumption, and the $\infty $-category $\operatorname{\mathcal{E}}'$ is minimal by virtue of Proposition 5.3.8.7. Applying Proposition 4.7.6.13, we conclude that $F$ is an isomorphism of simplicial sets. $\square$

Proof. We will show that $(1)$ implies $(2)$; the reverse implication is immediate from the definitions. Assume that $U$ is minimal and fix an $n$-simplex $\sigma : \Delta ^ n \rightarrow \operatorname{\mathcal{C}}$. Applying Corollary 5.3.8.9, we deduce that there is an isomorphism of simplicial sets $\operatorname{\mathcal{E}}_{\sigma } \simeq \operatorname{N}_{\bullet }^{\mathscr {F}}([n])$, for some diagram $\mathscr {F}: [n] \rightarrow \operatorname{Set_{\Delta }}$ which carries each integer $i \in [n]$ to a minimal Kan complex $\mathscr {F}(i)$. For $i \leq j$, the map of Kan complexes $e: \mathscr {F}(i) \rightarrow \mathscr {F}(j)$ is given by covariant transport along the corresponding edge of $\operatorname{\mathcal{C}}$ (Remark 5.3.3.22), and is therefore a homotopy equivalence (Example 5.2.5.9). Since $\mathscr {F}(i)$ and $\mathscr {F}(j)$ are minimal Kan complexes, it follows that $e$ is an isomorphism of simplicial sets (Proposition 4.7.6.13). It follows that $\mathscr {F}$ is isomorphic to the constant diagram $\underline{X}$ (where $X = \mathscr {F}(0)$ is a minimal Kan complex), so that $\operatorname{\mathcal{E}}_{\sigma }$ is isomorphic to $\operatorname{N}_{\bullet }^{\underline{X}}([n]) = \Delta ^ n \times X$. $\square$

Proof of Proposition 5.3.8.11. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a inner fibration of simplicial sets and let $A$ be the collection of all pairs $(\operatorname{\mathcal{C}}', \operatorname{\mathcal{E}}')$, where $\operatorname{\mathcal{C}}' \subseteq \operatorname{\mathcal{C}}$ and $\operatorname{\mathcal{E}}' \subseteq \operatorname{\mathcal{E}}$ are simplicial subsets satisfying the following conditions:

$(1')$

The inner fibration $U$ carries $\operatorname{\mathcal{E}}'$ into $\operatorname{\mathcal{C}}'$, and the restriction $U|_{\operatorname{\mathcal{E}}'}: \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}'$ is a minimal inner fibration.

$(2')$

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

We regard $A$ as a partially ordered set, where $(\operatorname{\mathcal{C}}', \operatorname{\mathcal{E}}') \leq (\operatorname{\mathcal{C}}'', \operatorname{\mathcal{E}}'' )$ if $\operatorname{\mathcal{C}}'$ is contained in $\operatorname{\mathcal{C}}''$ and $\operatorname{\mathcal{E}}'$ is contained in $\operatorname{\mathcal{E}}''$ (in this case, Lemma 4.7.6.11 guarantees that $\operatorname{\mathcal{E}}'$ coincides with the inverse image $\operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}''} \operatorname{\mathcal{E}}''$). The partially ordered set $A$ satisfies the hypotheses of Zorn's Lemma, and therefore contains a maximal element $( \operatorname{\mathcal{C}}^{0}, \operatorname{\mathcal{E}}^{0} )$. To prove Proposition 5.3.8.11, it will suffice to show that $\operatorname{\mathcal{C}}^{0} = \operatorname{\mathcal{C}}$. Suppose otherwise, so that there is an $n$-simplex $\sigma : \Delta ^ n \rightarrow \operatorname{\mathcal{C}}$ which is not contained in $\operatorname{\mathcal{C}}^{0}$. Choose $n$ as small as possible, so that $\sigma |_{\operatorname{\partial \Delta }^{n}}$ factors through $\operatorname{\mathcal{C}}^{0}$.

Let $\operatorname{\mathcal{E}}_{\sigma }$ denote the $\infty $-category $\Delta ^{n} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$. Using Proposition 4.7.6.15, we can choose an equivalence of $\infty $-categories $F_{\sigma }: \operatorname{\mathcal{D}}_{\sigma } \rightarrow \operatorname{\mathcal{E}}_{\sigma }$ where $\operatorname{\mathcal{D}}_{\sigma }$ is minimal, so that the composite map $\operatorname{\mathcal{D}}_{\sigma } \rightarrow \operatorname{\mathcal{E}}_{\sigma } \rightarrow \Delta ^ n$ is a minimal inner fibration (Example 5.3.8.2). Set $\operatorname{\mathcal{D}}_{\partial \sigma } = \operatorname{\partial \Delta }^{n} \times _{\Delta ^ n} \operatorname{\mathcal{D}}_{\sigma }$ and $\operatorname{\mathcal{E}}_{\partial \sigma } = \operatorname{\partial \Delta }^{n} \times _{ \Delta ^ n} \operatorname{\mathcal{E}}_{\sigma }$, so that $F_{\sigma }$ restricts to an equivalence $F_{ \partial \sigma }: \operatorname{\mathcal{D}}_{ \partial \sigma } \rightarrow \operatorname{\mathcal{E}}_{\partial \sigma }$ of inner fibrations over $\operatorname{\partial \Delta }^ n$. Applying Remark 5.3.8.12, we see that there exists an isomorphism of simplicial sets $G_{\partial \sigma }: \operatorname{\mathcal{D}}_{\partial \sigma } \rightarrow \operatorname{\partial \Delta }^ n \times _{\operatorname{\mathcal{C}}^{0} } \operatorname{\mathcal{E}}^{0}$ and an isomorphism $\alpha _{\partial \sigma }: F_{\partial \sigma } \rightarrow G_{\partial \sigma }$ in the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\partial \Delta }^ n }( \operatorname{\mathcal{D}}_{\partial \sigma }, \operatorname{\mathcal{E}}_{\partial \sigma } )$. Using Corollary 4.4.5.9, we can lift $\alpha _{\partial \sigma }$ to an isomorphism $\alpha : F_{\sigma } \rightarrow G_{\sigma }$ in the $\infty $-category $\operatorname{Fun}_{ / \Delta ^ n}( \operatorname{\mathcal{D}}_{\sigma }, \operatorname{\mathcal{E}}_{\sigma } )$, so that $G_{\sigma }: \operatorname{\mathcal{D}}_{\sigma } \rightarrow \operatorname{\mathcal{E}}_{\sigma }$ is also an equivalence of $\infty $-categories. Let $\operatorname{\mathcal{C}}^{1} \subseteq \operatorname{\mathcal{C}}$ be the simplicial subset generated by $\operatorname{\mathcal{C}}^{0}$ together with $\sigma $, and let $\operatorname{\mathcal{E}}^{1} \subseteq \operatorname{\mathcal{E}}$ be the simplicial subset generated by $\operatorname{\mathcal{E}}^{0}$ together with the image of the composite map $\operatorname{\mathcal{D}}_{\sigma } \xrightarrow { G_{\sigma } } \operatorname{\mathcal{E}}_{\sigma } \rightarrow \operatorname{\mathcal{E}}$. Then the pair $( \operatorname{\mathcal{C}}^{1}, \operatorname{\mathcal{E}}^{1} )$ is an element of the partially ordered set $A$, contradicting the maximality of $( \operatorname{\mathcal{C}}^{0}, \operatorname{\mathcal{E}}^{0} )$. $\square$