# Kerodon

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

Theorem 5.2.2.19. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a morphism of simplicial sets. The following conditions are equivalent:

$(1)$

The morphism $U$ is a Kan fibration.

$(2)$

The morphism $U$ is a left fibration and, for every edge $f: C \rightarrow D$ of the simplicial set $\operatorname{\mathcal{C}}$, the covariant transport morphism $[f_{!}]: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ is an isomorphism in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$.

$(3)$

The morphism $U$ is a right fibration and, for every edge $f: C \rightarrow D$ of the simplicial set $\operatorname{\mathcal{C}}$, the contravariant transport morphism $[f^{\ast }]: \operatorname{\mathcal{E}}_{D} \rightarrow \operatorname{\mathcal{E}}_{C}$ is an isomorphism in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$.

Proof. We will show that $(1) \Leftrightarrow (2)$; the proof of the equivalence $(1) \Leftrightarrow (3)$ is similar. The implication $(1) \Rightarrow (2)$ is immediate from Proposition 5.2.2.18. For the converse, assume that $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ is a left fibration of simplicial sets and that, for every edge $f: C \rightarrow D$ of $\operatorname{\mathcal{C}}$, the covariant transport morphism $[f_{!}]$ is an isomorphism in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$. We wish to show that $U$ is a Kan fibration. By virtue of Example 4.2.1.5, it will suffice to show that $U$ is a right fibration. By Proposition 4.2.6.1, this is equivalent to the assertion that the induced map

$\theta : \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}( \{ 1\} , \operatorname{\mathcal{E}}) \times _{ \operatorname{Fun}( \{ 1\} , \operatorname{\mathcal{C}}) } \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}})$

is a trivial Kan fibration. Note that our assumption that $U$ is a left fibration guarantees that $\theta$ is also a left fibration (Proposition 4.2.5.1).

Fix an edge $f: C \rightarrow D$ of the simplicial set $\operatorname{\mathcal{C}}$ and let $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}})_{f}$ denote the fiber $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}}) \times _{ \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) } \{ f\}$. Then evaluation at the vertex $1 \in \Delta ^1$ induces a morphism $\theta _{f}: \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}})_{f} \rightarrow \operatorname{\mathcal{E}}_{D}$. Note that $\theta _{f}$ is a pullback of $\theta$, and is therefore also a left fibration. Since $\operatorname{\mathcal{E}}_{D}$ is a Kan complex (Corollary 4.4.2.3), Corollary 4.4.3.8 guarantees that $\theta _{f}$ is a Kan fibration (so $\operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}})_{f}$ is also a Kan complex). Evaluation at the vertex $0 \in \Delta ^1$ induces another morphism of simplicial sets $u: \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}})_{f} \rightarrow \operatorname{\mathcal{E}}_{C}$. Since $U$ is a left fibration, the morphism $u$ is a trivial Kan fibration. By construction, the homotopy class $[f_{!}]$ can be represented by the morphism of Kan complexes given by the composition

$\operatorname{\mathcal{E}}_{C} \xrightarrow {v} \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{E}})_{f} \xrightarrow { \theta _{f} } \operatorname{\mathcal{E}}_{D},$

where $v$ is a section of $u$ (and therefore a homotopy equivalence). Consequently, our assumption that $[f_{!}]$ is an isomorphism in $\mathrm{h} \mathit{\operatorname{Kan}}$ guarantees that $\theta _{f}$ is a homotopy equivalence of Kan complexes (Remark 3.1.6.16). Applying Corollary 3.2.7.4, we deduce that the fibers of $\theta _{f}$ are contractible Kan complexes. Since every fiber of $\theta$ can also be viewed as a fiber of $\theta _{f}$ for some edge $f$ of the simplicial set $\operatorname{\mathcal{C}}$, it follows that the fibers of $\theta$ are also contractible Kan complexes. Invoking Proposition 4.4.2.14, we conclude that $\theta$ is a trivial Kan fibration, as desired. $\square$