# Kerodon

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

Proof of Proposition 5.3.7.1. We will prove assertion $(1)$; the proof of $(2)$ is similar. Note that the oriented fiber product $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{E}}} \operatorname{\mathcal{D}}$ fits into a pullback diagram

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{E}}} \operatorname{\mathcal{D}}\ar [d]^-{\pi } \ar [r] & \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{E}}} \operatorname{\mathcal{E}}\ar [d] \\ \operatorname{\mathcal{D}}\ar [r]^-{G} & \operatorname{\mathcal{E}}. }$

By virtue of Remark 5.1.4.6, we can replace $\operatorname{\mathcal{D}}$ by $\operatorname{\mathcal{E}}$ and thereby reduce to the case where $\operatorname{\mathcal{D}}= \operatorname{\mathcal{E}}$ and $G$ is the identity functor $\operatorname{id}_{\operatorname{\mathcal{D}}}$. It follows from Proposition 4.6.4.2 that the map $(\pi ', \pi ): \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}\times \operatorname{\mathcal{D}}$ is an isofibration of $\infty$-categories, so that $\pi : \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{D}}$ is also an isofibration. Let us say that a morphism $e$ of the $\infty$-category $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ is special if $\pi '(e)$ is an isomorphism in the $\infty$-category $\operatorname{\mathcal{C}}$. Proposition 5.3.7.1 is an immediate consequence of the following three assertions:

$(a)$

For every object $x$ in the $\infty$-category $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ and every morphism $\overline{e}: \pi (x) \rightarrow \overline{y}$ in the $\infty$-category $\operatorname{\mathcal{D}}$, there exists a special morphism $e: x \rightarrow y$ in $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ satisfying $\pi (e) = \overline{e}$.

$(b)$

Every special morphism of $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ is $\pi$-cocartesian.

$(c)$

Every $\pi$-cocartesian morphism of $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ is special.

We begin with the proof of $(a)$. Let $x$ be an object of the $\infty$-category $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$, which we identify with a triple $(\overline{x}', \overline{x}, u)$ where $\overline{x}' = \pi '(x)$ is an object of $\operatorname{\mathcal{C}}$, $\overline{x} = \pi (x)$ is an object of $\operatorname{\mathcal{D}}$, and $u: F( \overline{x}' ) \rightarrow \overline{x}$ is a morphism of $\operatorname{\mathcal{D}}$. Since $\operatorname{\mathcal{D}}$ is an $\infty$-category, we can choose a $2$-simplex $\sigma$ of $\operatorname{\mathcal{E}}$ satisfying $d_0(\sigma ) = \overline{e}$ and $d_2(\sigma ) = f$. Set $g = d_1(\sigma )$. Then the $2$-simplices $\sigma$ and $s_0(g)$ together determine a commutative diagram

$\xymatrix@R =50pt@C=50pt{ F( \overline{x}' ) \ar [d]_-{ \operatorname{id}_{ F( \overline{x}' ) }} \ar [r]^-{f} \ar [dr]_{g} & \overline{x} \ar [d]^-{ \overline{e} } \\ F( \overline{x}' ) \ar [r]^-{g} & \overline{y} }$

in the $\infty$-category $\operatorname{\mathcal{D}}$, which we can identify with an edge $e: x \rightarrow y$ of the $\infty$-category $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ satisfying $\pi '(e) = \operatorname{id}_{ \overline{x}'}$ and $\pi (e) = \overline{e}$.

We now prove $(b)$. Let $n \geq 2$ and suppose that we are given a lifting problem

$\xymatrix@R =50pt@C=50pt{ \Lambda ^{n}_{0} \ar [r]^-{ \tau _0 } \ar [r] \ar [d] & \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}\ar [d]^-{ \pi } \\ \Delta ^{n} \ar [r]^-{ \overline{\tau } } \ar@ {-->}[ur]^{\tau } & \operatorname{\mathcal{D}}}$

for which the composite map

$\Delta ^1 \simeq \operatorname{N}_{\bullet }( \{ 0 < 1 \} ) \hookrightarrow \Lambda ^{n}_0 \xrightarrow { \tau _0 } \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$

is a special edge of $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$. Then $\pi ' \circ \tau _0$ carries the initial edge of $\Lambda ^{n}_0$ to an isomorphism in the $\infty$-category $\operatorname{\mathcal{C}}$, and can therefore be extended to an $n$-simplex $\rho : \Delta ^ n \rightarrow \operatorname{\mathcal{C}}$. Let $X(0)$ denote the simplicial subset of $\Delta ^1 \times \Delta ^ n$ given by the union of $\{ 0 \} \times \Delta ^ n$, $\{ 1\} \times \Delta ^ n$, and $\Delta ^1 \times \Lambda ^{n}_0$. The morphisms $\rho$, $\overline{\tau }$, and $\tau _0$ can then be amalgamated to a morphism of simplicial sets $h_0: X(0) \rightarrow \operatorname{\mathcal{D}}$. We wish to show that $h_0$ can be extended to a map $h: \Delta ^1 \times \Delta ^ n \rightarrow \operatorname{\mathcal{D}}$. Choose a filtration

$X(0) \subset X(1) \subset X(2) \subset \cdots \subset X(t) = \Delta ^{1} \times \Delta ^{n}$

satisfying the requirements of Lemma 4.4.4.7. We will complete the proof of $(b)$ by showing that, for each $s \leq t$, the morphism $h_0$ admits an extension $h_ s: X(s) \rightarrow \operatorname{\mathcal{D}}$. The proof proceeds by induction on $s$, the case $s = 0$ being vacuous. Let us therefore assume that $0 < s \leq t$ and that $h_0$ has already been extended to a morphism of simplicial sets $h_{s-1}: X(s-1) \rightarrow \operatorname{\mathcal{D}}$. By construction, we have a pushout diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ \Lambda ^{q}_{p} \ar [r]^-{\varphi } \ar [d] & X(s-1) \ar [d] \\ \Delta ^{q} \ar [r] & X(s) }$

for some $q \geq 2$ and $0 \leq p < q$. Consequently, to prove the existence of $h_ s$, it will suffice to show that $h_{s-1} \circ \varphi$ can be extended to a $q$-simplex of $\operatorname{\mathcal{D}}$. For $p \neq 0$, the existence of this extension follows from our assumption that $\operatorname{\mathcal{D}}$ is an $\infty$-category. In the case $p = 0$, Lemma 4.4.4.7 guarantees that the morphism $\varphi$ carries the initial edge of $\Delta ^{q}$ to the edge $(0,0) \rightarrow (0,1)$ of $\Delta ^{1} \times \Delta ^ n$, so that $h_{s-1} \circ \varphi$ carries the initial edge of $\Delta ^ q$ to an isomorphism in $\operatorname{\mathcal{D}}$. In this case, the existence of the desired extension follows from Theorem 4.4.2.6.

We now prove $(c)$. Let $e: x \rightarrow z$ be a $\pi$-cocartesian morphism in the $\infty$-category $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$; we wish to show that $e$ is special. By virtue of $(a)$, there exists a special morphism $e': x \rightarrow y$ of $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ satisfying $\pi (e) = \pi (e')$. It follows from $(b)$ that $e'$ is also $\pi$-cocartesian. Applying Remark 5.1.3.8, we deduce that there exists a commutative diagram

$\xymatrix@R =50pt@C=50pt{ & y \ar [dr]^{ e'' } & \\ x \ar [ur]^{e'} \ar [rr]^-{e} & & z }$

in the $\infty$-category $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$, where $e''$ is an isomorphism. Then $\pi '(e')$ and $\pi '(e'')$ are isomorphisms in the $\infty$-category $\operatorname{\mathcal{C}}$, so that $\pi '(e)$ is also an isomorphism in $\operatorname{\mathcal{C}}$ (Remark 1.3.6.3). It follows that $e$ is a special morphism of $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$, as desired. $\square$