# Kerodon

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

Corollary 7.4.5.11. Let $e: \operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{C}}$ be a morphism of simplicial sets. Then $e$ is left cofinal if and only if it satisfies the following condition:

$(\ast )$

For every limit diagram $\overline{F}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{\mathcal{S}}$, the composition $(\overline{F} \circ e^{\triangleleft }): \operatorname{\mathcal{C}}'^{\triangleleft } \rightarrow \operatorname{\mathcal{S}}$ is also a limit diagram.

Proof. Assume that condition $(\ast )$ is satisfied; we will show that $e$ is left cofinal (the reverse implication is a special case of Corollary 7.2.2.3). Fix a left fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$; we wish to show that the restriction map

$e^{\ast }: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}} ( \operatorname{\mathcal{C}}', \operatorname{\mathcal{E}})$

is a homotopy equivalence of Kan complexes. Using Proposition 7.4.1.6 (together with Remark 7.4.1.8), we can extend $U$ to a left fibration $\overline{U}: \overline{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{C}}^{\triangleleft }$ for which the restriction map

$T: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} ) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$

is a homotopy equivalence.

Form a pullback diagram of simplicial sets

$\xymatrix { \overline{\operatorname{\mathcal{E}}}' \ar [r] \ar [d]^{ \overline{U}' } & \overline{\operatorname{\mathcal{E}}} \ar [d]^{U} \\ \operatorname{\mathcal{C}}'^{\triangleleft } \ar [r]^-{e} & \operatorname{\mathcal{C}}^{\triangleleft }. }$

Let $\overline{F}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{\mathcal{S}}$ be a covariant transport representation for the left fibration $\overline{U}$, so that $\overline{F} \circ e^{\triangleleft }$ is a covariant transport representation for the left fibration $\overline{U}'$. It follows from the criterion of Corollary 7.4.5.10 that $\overline{F}$ is a limit diagram in the $\infty$-category $\operatorname{\mathcal{S}}$. Applying assumption $(\ast )$, we see that $\overline{F} \circ e^{\triangleleft }$ is also a limit diagram in the $\infty$-category $\operatorname{\mathcal{S}}$. We therefore have a commutative diagram of restriction maps

$\xymatrix { \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }( \operatorname{\mathcal{C}}'^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} ) \ar [r]^{T'} \ar [d]^{(e^{\triangleleft })^{\ast }} & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}', \operatorname{\mathcal{E}}) \ar [d]^{ e^{\ast } } \\ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} ) \ar [r]^{T} & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}), }$

where the horizontal maps are homotopy equivalences (Corollary 7.4.5.10). Consequently, to show that $e^{\ast }$ is a homotopy equivalence, it will suffice to show that $( e^{\triangleleft } )^{\ast }$ is a homotopy equivalence. We now observe that $(e^{\triangleleft } )^{\ast }$ fits into a commutative diagram

$\xymatrix { \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }( \operatorname{\mathcal{C}}'^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} ) \ar [dd]^{(e^{\triangleleft } )^{\ast } } \ar [dr] & \\ & \{ {\bf 0} \} \times _{ \operatorname{\mathcal{C}}^{\triangleleft } } \overline{\operatorname{\mathcal{E}}} \\ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} ), \ar [ur] & }$

where the horizontal maps are given by evaluation at the cone points of the simplicial sets $\operatorname{\mathcal{C}}^{\triangleleft }$ and $\operatorname{\mathcal{C}}'^{\triangleleft }$ are are therefore trivial Kan fibrations (Corollary 5.3.1.23). $\square$