# Kerodon

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

Corollary 5.2.6.22. Let $\pi : \operatorname{\mathcal{C}}\rightarrow \Delta ^ n$ be a cocartesian fibration of $\infty$-categories and let $\operatorname{\mathcal{C}}(0)$ denote the fiber $\{ 0\} \times _{\Delta ^ n} \operatorname{\mathcal{C}}$. Then there exists a functor $V: \Delta ^ n \times \operatorname{\mathcal{C}}(0) \rightarrow \operatorname{\mathcal{C}}$ with the following properties:

$(1)$

The composition $\Delta ^ n \times \operatorname{\mathcal{C}}(0) \rightarrow \operatorname{\mathcal{C}}\xrightarrow {\pi } \Delta ^ n$ is given by projection onto the first factor (that is, $V$ is a morphism in the category $(\operatorname{Set_{\Delta }})_{/\Delta ^ n}$).

$(2)$

The restriction $V|_{ \{ 0\} \times \operatorname{\mathcal{C}}(0) }$ is equal to the identity map $\operatorname{id}_{\operatorname{\mathcal{C}}(0)}$.

$(3)$

For each object $C \in \operatorname{\mathcal{C}}(0)$, the restriction $V|_{ \Delta ^ n \times \{ C\} }: \Delta ^ n \rightarrow \operatorname{\mathcal{C}}$ carries each edge of $\Delta ^ n$ to a $\pi$-cocartesian morphism of $\operatorname{\mathcal{C}}$.

$(4)$

The diagram

$\xymatrix@R =50pt@C=50pt{ \operatorname{\partial \Delta }^ n \times \operatorname{\mathcal{C}}(0) \ar [r] \ar [d] & \operatorname{\partial \Delta }^ n \times _{\Delta ^ n} \operatorname{\mathcal{C}}\ar [d] \\ \Delta ^ n \times \operatorname{\mathcal{C}}(0) \ar [r]^-{V} & \operatorname{\mathcal{C}}}$

is a categorical pushout square of simplicial sets.

Proof. For $0 \leq i \leq n$, let $\operatorname{\mathcal{C}}(i)$ denote the fiber $\{ i\} \times _{\Delta ^ n} \operatorname{\mathcal{C}}$. By virtue of Proposition 5.2.6.18, there exists a sequence of functors

$\operatorname{\mathcal{C}}(0) \xrightarrow {F(1)} \operatorname{\mathcal{C}}(1) \xrightarrow {F(2)} \operatorname{\mathcal{C}}(2) \rightarrow \cdots \xrightarrow {F(n)} \operatorname{\mathcal{C}}(n)$

and a morphism $U: M \rightarrow \operatorname{\mathcal{C}}$ which is a scaffold of $\pi$, where $M = M( \operatorname{\mathcal{C}}(0) \rightarrow \operatorname{\mathcal{C}}(1) \rightarrow \cdots \rightarrow \operatorname{\mathcal{C}}(n) )$ is the mapping simplex of Construction 5.2.6.3. Let $V$ denote the composite map

$\Delta ^ n \times \operatorname{\mathcal{C}}(0) \rightarrow M \xrightarrow {U} \operatorname{\mathcal{C}}.$

It follows immediately from the definitions that $V$ satisfies conditions $(1)$, $(2)$, and $(3)$. To prove $(4)$, we observe that there is a commutative diagram

$\xymatrix@R =50pt@C=50pt{ \operatorname{\partial \Delta }^{n} \times \operatorname{\mathcal{C}}(0) \ar [r] \ar [d] & \operatorname{\partial \Delta }^ n \times _{\Delta ^ n} M \ar [r] \ar [d] & \operatorname{\partial \Delta }^ n \times _{\Delta ^ n} \operatorname{\mathcal{C}}\ar [d] \\ \Delta ^ n \times \operatorname{\mathcal{C}}(0) \ar [r] & M \ar [r]^-{U} & \operatorname{\mathcal{C}}. }$

Note that the square on the left is a pushout diagram in which the vertical maps are monomorphisms, hence a categorical pushout diagram (Example 4.5.3.9). Corollary 5.2.6.21 implies that both of the horizontal maps on the right are categorical equivalences, so that the right square is also a categorical pushout diagram (Proposition 4.5.3.7). Applying Proposition 4.5.3.5, we deduce that the outer rectangle is also a categorical pushout square. $\square$