Kerodon

Proof. Combine Theorem 5.2.4.1 with Proposition 4.5.4.11. $\square$

Proof. Let $e$ denote the nondegenerate edge of $\Delta ^1$. By virtue of Proposition 5.2.2.8, we can choose a functor $F': \operatorname{\mathcal{M}}_{0} \rightarrow \operatorname{\mathcal{M}}_{1}$ and a natural transformation $H: \Delta ^1 \times \operatorname{\mathcal{M}}_0 \rightarrow \operatorname{\mathcal{M}}$ which exhibits $F'$ as given by covariant transport along $e$. Let $R: \operatorname{\mathcal{M}}\rightarrow \operatorname{\mathcal{M}}_1$ be a functor satisfying condition $(2)$. Then the composition

can be regarded as a natural transformation from $R \circ H|_{ \{ 0\} \times \operatorname{\mathcal{M}}_0} = F$ to $R \circ H|_{ \{ 1\} \times \operatorname{\mathcal{M}}_1} = F'$. By assumption, this natural transformation carries each object of $\operatorname{\mathcal{M}}_0$ to an isomorphism in the $\infty $-category $\operatorname{\mathcal{M}}_1$, and is therefore an isomorphism of functors (Theorem 4.4.4.4). It follows that the functor $F$ is also given by covariant transport along $e$ (see Proposition 5.2.2.8). This proves the implication $(2) \Rightarrow (1)$.

Now suppose that condition $(1)$ is satisfied. Then we can assume that $F' = F$, so that we have a commutative diagram of simplicial sets

The upper half of the diagram is a pushout square in which the vertical maps are monomorphisms, and therefore a categorical pushout square (Example 4.5.4.12). Theorem 5.2.4.1 guarantees that the outer rectangle is a categorical pushout square, so the lower half of the diagram is also a categorical pushout square (Proposition 4.5.4.8). It follows that the diagram of $\infty $-categories

is a categorical pullback square (Proposition 4.5.4.4). Since the vertical maps are isofibrations (Corollary 4.4.5.3), Corollary 4.5.2.32 implies that composition with $H$ induces an equivalence of $\infty $-categories

It follows that we can choose a functor $R: \operatorname{\mathcal{M}}\rightarrow \operatorname{\mathcal{M}}_1$ such that $R|_{ \operatorname{\mathcal{M}}_0 } = F$, $R|_{ \operatorname{\mathcal{M}}_1} = \operatorname{id}$, and the composition $R \circ H$ is homotopic to the identity (when regarded as a morphism from $F$ to itself in the $\infty $-category $\operatorname{Fun}(\operatorname{\mathcal{M}}_0, \operatorname{\mathcal{M}}_1)$). To complete the proof, it will suffice to show that if $f: X \rightarrow Y$ is a $U$-cocartesian morphism of $\operatorname{\mathcal{M}}$, then $U(f)$ is an isomorphism. We may assume without loss of generality that $X$ belongs to $\operatorname{\mathcal{M}}_0$ and $Y$ belongs to $\operatorname{\mathcal{M}}_1$ (otherwise, $f$ is already an isomorphism and there is nothing to prove). In this case, Remark 5.1.3.8 guarantees that $f$ is isomorphic (as an object of $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{M}})$) to the edge $H|_{ \Delta ^1 \times \{ X\} }$. It will therefore suffice to show that $(R \circ H)|_{ \Delta ^1 \times \{ X\} }$ is an isomorphism in $\operatorname{\mathcal{M}}_1$, which is clear (since it is homotopic to the identity morphism from $F(X)$ to itself). $\square$

Proof. Combine Propositions 5.2.4.5 and 4.5.4.9. $\square$

Proof of Proposition 5.2.4.5. The diagram (5.24) determines a morphism of simplicial sets

and we wish to show that $\lambda _{X}$ is a categorical equivalence of simplicial sets (obtained by applying Construction 5.3.4.7 to the diagram $[1] \rightarrow \operatorname{Set_{\Delta }}$ determined by the morphism $f$). We wish to show that $\lambda _{X}$ is a categorical equivalence of simplicial sets (Proposition 4.5.4.11). By virtue of Corollary 4.5.7.3, it will suffice to prove that for every map $\Delta ^{n} \rightarrow Y$, the induced map

is a categorical equivalence. Using Remark 5.2.3.9, we can replace $Y$ by $\Delta ^ n$ and $X$ by the fiber product $\Delta ^ n \times _{Y} X$, and thereby reduce the proof of Proposition 5.2.4.5 to the special case where $Y = \Delta ^ n$ is a standard simplex.

Since the collection of categorical equivalences is closed under the formation of filtered colimits (Corollary 4.5.7.2), we may assume without loss of generality that the simplicial set $X$ is finite (see Remark 3.6.1.8). In particular, $X$ has dimension $\leq m$ for some integer $m \geq -1$. We proceed by induction on $m$. If $m = -1$, then $X$ is empty and the morphism $\lambda _{X}$ is an isomorphism (see Example 5.2.3.4). Assume that $m \geq 0$; we now proceed by induction on the number of nondegenerate $m$-simplices of $X$. If $X$ does not have dimension $\leq m-1$, then a choice of nondegenerate $m$-simplex of $X$ determines a pushout diagram

where the horizontal maps are monomorphisms (Proposition 1.1.4.12). We then obtain a cubical diagram

where the front and back faces are categorical pushout squares (Proposition 4.5.4.11). Our inductive hypothesis guarantees that the morphisms $\lambda _{X'}$ and $\lambda _{\operatorname{\partial \Delta }^ m}$ are categorical equivalences. Consequently, to show that $\lambda _{X}$ is a categorical equivalence, it will suffice to show that $\lambda _{\Delta ^ m}$ is a categorical equivalence. We can therefore replace $X$ by $\Delta ^ m$, and thereby reduce the proof of Proposition 5.2.4.5 to the special case where $f: \Delta ^{m} \rightarrow \Delta ^{n}$ is a morphism between standard simplices.

Suppose that $f(m) < n$. In this case, we can identify $f$ with a morphism from $X = \Delta ^{m}$ to the simplex $\Delta ^{n-1}$ (regarded as a simplicial subset of $\Delta ^{n}$), and we can identify $X \star _{Y} Y$ with the right cone $( X \star _{\Delta ^{n-1} } \Delta ^{n-1} )^{\triangleright }$. Under this identification, $\lambda _{X}$ corresponds to the composition

where $\lambda '$ is a pushout of the map

and is therefore inner anodyne by virtue of Example 4.3.6.5 (since the inclusion $\{ 1\} \times X \hookrightarrow \Delta ^1 \times X$ is right anodyne; see Proposition 4.2.5.3). Consequently, to show that $\lambda _{X}$ is a categorical equivalence, it will suffice to show that $\lambda ''$ is a categorical equivalence. By virtue of Corollary 4.5.8.9, we are reduced to proving Proposition 5.2.4.5 for the map $f: X \rightarrow \Delta ^{n-1}$. Applying this argument repeatedly, we can reduce to the case where $f(m) = n$.

Let $Z(0)$ denote the simplicial subset of $\Delta ^1 \times \Delta ^ m$ given by the union of $\Delta ^1 \times \operatorname{\partial \Delta }^ m$ with $\{ 1\} \times \Delta ^ m$, and let

be the sequence of simplicial subsets appearing in Lemma 3.1.2.12. Note that $\lambda _{X}$ carries $Z(m)$ into the simplicial subset $\operatorname{\partial \Delta }^ m \star _{Y} Y \subseteq X \star _{Y} Y$. We therefore obtain a cubical diagram of simplicial sets

where the front and back faces are pushout squares and the vertical maps are monomorphisms. It follows that the front and back faces are categorical pushout squares (Example 4.5.4.12). Our inductive hypothesis guarantees that $\lambda _{\operatorname{\partial \Delta }^{m}}$ is a categorical equivalence, and the inclusion $Z(0) \hookrightarrow Z(m)$ is inner anodyne by construction (see Lemma 3.1.2.12). Applying Proposition 4.5.4.9, we conclude that $\lambda _{\Delta ^ m}$ is also a categorical equivalence. $\square$

Proof of Theorem 5.2.4.1. Let $U: \operatorname{\mathcal{M}}\rightarrow \Delta ^1$ be a functor of $\infty $-categories and suppose we are given a commutative diagram $\sigma :$

in the category $(\operatorname{Set_{\Delta }})_{/\Delta ^1}$. We wish to show that $\sigma $ is a categorical pushout square if and only if conditions $(1)$ through $(3)$ of Theorem 5.2.4.1 are satisfied.

We first reduce to the case where $\operatorname{\mathcal{C}}$ and $\operatorname{\mathcal{D}}$ are $\infty $-categories. Choose inner anodyne morphisms $\operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{C}}'$ and $\operatorname{\mathcal{D}}\hookrightarrow \operatorname{\mathcal{D}}'$, where $\operatorname{\mathcal{C}}'$ and $\operatorname{\mathcal{D}}'$ are $\infty $-categories (Corollary 4.1.3.3). Since the fiber $\{ 1\} \times _{\Delta ^1} \operatorname{\mathcal{M}}$ is an $\infty $-category, we can extend $g$ to a functor $g': \operatorname{\mathcal{D}}' \rightarrow \{ 1\} \times _{\Delta ^1} \operatorname{\mathcal{M}}$. Similarly, the composition $\operatorname{\mathcal{C}}\xrightarrow {F} \operatorname{\mathcal{D}}\hookrightarrow \operatorname{\mathcal{D}}'$ extends to a functor of $\infty $-categories $F': \operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{D}}'$. Using Exercise 3.1.7.11, we can factor $F'$ as a composition $\operatorname{\mathcal{C}}' \xrightarrow {F''} \operatorname{\mathcal{D}}'' \xrightarrow {v} \operatorname{\mathcal{D}}'$, where $F''$ is a monomorphism and $v$ is a trivial Kan fibration. It follows from Lemma 1.5.7.5 that the inclusion map

is inner anodyne, so that we can extend $h$ to a functor $h': \Delta ^1 \times \operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{M}}$ satisfying $h'|_{ \{ 1\} \times \operatorname{\mathcal{C}}'} = g' \circ F'$. By virtue of Proposition 4.5.4.9, $\sigma $ is a categorical pushout square if and only if the diagram $\sigma :$

is a categorical pushout square. We may therefore replace $\operatorname{\mathcal{C}}$ and $\operatorname{\mathcal{D}}$ by $\operatorname{\mathcal{C}}'$ and $\operatorname{\mathcal{D}}''$, and thereby reduce to the case where $\operatorname{\mathcal{C}}$ and $\operatorname{\mathcal{D}}$ are $\infty $-categories and $F$ is a monomorphism.

The assumption that $F$ is a monomorphism guarantees that the natural map

is also a monomorphism, and Proposition 5.2.4.5 guarantees that $\iota $ is a categorical equivalence of simplicial sets. Since $\operatorname{\mathcal{M}}$ is an $\infty $-category, Lemma 4.5.5.2 guarantees the existence of a functor $G: \operatorname{\mathcal{C}}\star _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{M}}$ satisfying $G|_{ \Delta ^1 \times \operatorname{\mathcal{C}}} = h$ and $G|_{\operatorname{\mathcal{D}}} = g$. By virtue of Proposition 4.5.4.9, the diagram $\sigma $ is a categorical pushout square if and only if the functor $G$ is an equivalence of $\infty $-categories.

Note that the functor $G$ fits into a commutative diagram

where $U'$ is the cocartesian fibration of Proposition 5.2.3.15, and the functor $U$ is an isofibration (Example 4.4.1.6). The desired result now follows by applying the criterion of Theorem 5.1.6.1 (and invoking Remark 5.1.6.8). $\square$