# Kerodon

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

Lemma 5.7.8.10. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets. Let $\operatorname{\mathcal{C}}_0$ be a simplicial subset of $\operatorname{\mathcal{C}}$ and set $\operatorname{\mathcal{E}}_0 = \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$. Then:

$(1)$

The restriction map $\theta : \operatorname{TW}(\operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}) \rightarrow \operatorname{TW}( \operatorname{\mathcal{E}}_0/ \operatorname{\mathcal{C}}_0 )$ of Notation 5.7.8.9 is a Kan fibration between Kan complexes.

$(2)$

If the inclusion $\operatorname{\mathcal{C}}_0 \hookrightarrow \operatorname{\mathcal{C}}$ is inner anodyne, then $\theta$ is a trivial Kan fibration.

Proof. We first prove $(1)$. Since the simplicial set $\operatorname{TW}( \operatorname{\mathcal{E}}_0 / \operatorname{\mathcal{C}}_0 )$ is a Kan complex (Lemma 5.7.8.7), it will suffice to show that $\theta$ is an isofibration. Define fiber products

$\operatorname{\mathcal{M}}= \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{QC}}) \times _{ \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}}) } \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} )$

$\operatorname{\mathcal{M}}_0 = \operatorname{Fun}(\operatorname{\mathcal{C}}_0, \operatorname{\mathcal{QC}}) \times _{ \operatorname{Fun}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{QC}}) } \operatorname{Fun}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{QC}}_{\operatorname{Obj}}),$

so that we have a commutative diagram

5.63
$$\begin{gathered}\label{equation:classifier-infinity5} \xymatrix@R =50pt@C=50pt{ \operatorname{TW}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}) \ar [r] \ar [d]^{\theta } & \operatorname{\mathcal{M}}\ar [d]^{\overline{\theta }} \\ \operatorname{TW}(\operatorname{\mathcal{E}}_0 / \operatorname{\mathcal{C}}_0) \ar [r] & \operatorname{\mathcal{M}}_0. } \end{gathered}$$

It follows from Lemma 5.7.8.6 that $\operatorname{TW}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}})$ is a replete subcategory of $\operatorname{\mathcal{M}}$, and therefore also a replete subcategory of the fiber product $\operatorname{TW}( \operatorname{\mathcal{E}}_0 / \operatorname{\mathcal{C}}_0 ) \times _{ \operatorname{\mathcal{M}}_0 } \operatorname{\mathcal{M}}$. It will therefore suffice to show that the projection map $\operatorname{TW}( \operatorname{\mathcal{E}}_0 / \operatorname{\mathcal{C}}_0 ) \times _{ \operatorname{\mathcal{M}}_0 } \operatorname{\mathcal{M}}\rightarrow \operatorname{TW}( \operatorname{\mathcal{E}}_0 / \operatorname{\mathcal{C}}_0 )$ is an isofibration of $\infty$-categories. Since the collection of isofibrations is stable under pullback, we are reduced to showing that the map $\overline{\theta }: \operatorname{\mathcal{M}}\rightarrow \operatorname{\mathcal{M}}_0$ is an isofibration. We now observe that $\overline{\theta }$ factors as a composition

\begin{eqnarray*} \operatorname{\mathcal{M}}& = & \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{QC}}) \times _{ \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}})} \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} ) \\ & \xrightarrow {\overline{\theta }'} & \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{QC}}) \times _{ \operatorname{Fun}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{QC}}) } \operatorname{Fun}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} ) \\ & \xrightarrow {\overline{\theta }''} & \operatorname{Fun}( \operatorname{\mathcal{C}}_0, \operatorname{\mathcal{QC}}) \times _{ \operatorname{Fun}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{QC}}) } \operatorname{Fun}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} ) \\ & = & \operatorname{\mathcal{M}}_0, \end{eqnarray*}

where $\overline{\theta }''$ is a pullback of the restriction map

$\psi '': \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} ) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} ) \times _{ \operatorname{Fun}( \operatorname{\mathcal{E}}_0, \operatorname{\mathcal{QC}}) } \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}}).$

Since the forgetful functor $V: \operatorname{\mathcal{QC}}_{\operatorname{Obj}} \rightarrow \operatorname{\mathcal{QC}}$ is an isofibration, $\psi ''$ is also an isofibration (Propositions 4.4.5.1). Similarly, $\overline{\theta }'$ is a pullback of the restriction map $\psi ': \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{QC}}) \rightarrow \operatorname{Fun}(\operatorname{\mathcal{C}}_0, \operatorname{\mathcal{QC}})$, which is an isofibration by virtue of Corollary 4.4.5.3. It follows that $\overline{\theta } = \overline{\theta }'' \circ \overline{\theta }'$ is also an isofibration. This completes the proof of $(1)$.

We now prove $(2)$. Suppose that the inclusion map $\operatorname{\mathcal{C}}_0 \hookrightarrow \operatorname{\mathcal{C}}$ is inner anodyne; we wish to show that $\theta$ is a trivial Kan fibration. Applying Proposition 1.4.7.6, we deduce that $\psi '$ is a trivial Kan fibration of simplicial sets. Since $U$ is a cocartesian fibration, the inclusion map $\operatorname{\mathcal{E}}_0 \hookrightarrow \operatorname{\mathcal{E}}$ is a categorical equivalence (Lemma 5.3.6.5). Applying Proposition 4.5.5.18, we deduce that $\psi ''$ is a trivial Kan fibration. It follows that the morphisms $\overline{\theta }'$ and $\overline{\theta }''$ are also trivial Kan fibrations, so that $\overline{\theta } = \overline{\theta }'' \circ \overline{\theta }'$ is a trivial Kan fibration. Applying Lemma 5.7.8.5, we see that the diagram (5.63) is a pullback square, so that $\theta$ is also a trivial Kan fibration. $\square$