# Kerodon

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

Proposition 7.2.2.1. Let $F: A \rightarrow B$ be a morphism of simplicial sets. The following conditions are equivalent:

$(1)$

The morphism $F$ is left cofinal (in the sense of Definition 7.2.1.1).

$(2)$

For every $\infty$-category $\operatorname{\mathcal{C}}$ and every diagram $G: B \rightarrow \operatorname{\mathcal{C}}$, the restriction map $\operatorname{\mathcal{C}}_{/G} \rightarrow \operatorname{\mathcal{C}}_{ / (G \circ F) }$ is an equivalence of $\infty$-categories.

$(3)$

For every $\infty$-category $\operatorname{\mathcal{C}}$ and every diagram $G: B \rightarrow \operatorname{\mathcal{C}}$, composition with $F$ induces an equivalence of $\infty$-categories

$\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(B, \operatorname{\mathcal{C}}) } \{ G\} \rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(A, \operatorname{\mathcal{C}}) } \{ G \circ F \} .$
$(4)$

For every $\infty$-category $\operatorname{\mathcal{C}}$, every diagram $G: B \rightarrow \operatorname{\mathcal{C}}$, and every object $X \in \operatorname{\mathcal{C}}$, precomposition with $F$ induces a homotopy equivalence of Kan complexes

$\operatorname{Hom}_{\operatorname{Fun}(B,\operatorname{\mathcal{C}})}( \underline{X}, G ) \rightarrow \operatorname{Hom}_{ \operatorname{Fun}(A, \operatorname{\mathcal{C}})}( \underline{X} \circ F, G \circ F);$

here $\underline{X}: B \rightarrow \operatorname{\mathcal{C}}$ denotes the constant diagram taking the value $X$.

$(5)$

For every $\infty$-category $\operatorname{\mathcal{C}}$, every diagram $G: B \rightarrow \operatorname{\mathcal{C}}$, and every object $X \in \operatorname{\mathcal{C}}$, precomposition with $F$ induces a homotopy equivalence of Kan complexes

$\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( B, \operatorname{\mathcal{C}}_{X/} ) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}} (A, \operatorname{\mathcal{C}}_{X/} ).$

Proof. We first show that $(1)$ implies $(2)$. Let $F: A \rightarrow B$ be a left cofinal morphism of simplicial sets, let $\operatorname{\mathcal{C}}$ be an $\infty$-category, and let $G: B \rightarrow \operatorname{\mathcal{C}}$ be a diagram; we wish to show that precomposition with $F$ induces an equivalence of $\infty$-categories $\theta : \operatorname{\mathcal{C}}_{/G} \rightarrow \operatorname{\mathcal{C}}_{ / (G \circ F) }$. By virtue of Corollary 7.2.1.15, we may assume without loss of generality that $F$ is either left anodyne or a trivial Kan fibration. In the first case, the functor $\theta$ is a trivial Kan fibration (Corollary 4.3.6.13). In the second case, the morphism $F$ admits a section $s: B \hookrightarrow A$. The morphism $s$ is then a categorical equivalence, which is automatically left cofinal (Proposition 7.2.1.21) and therefore left anodyne ( (Remark 4.5.3.5) and therefore left cofinal (Proposition 7.2.1.3). Corollary 4.3.6.13 then implies that the map $\theta ': \operatorname{\mathcal{C}}_{ / (G \circ F) } \rightarrow \operatorname{\mathcal{C}}_{ / (G \circ F \circ s) } = \operatorname{\mathcal{C}}_{/G}$ is a trivial Kan fibration. The morphism $\theta$ is a section of $\theta '$, and is therefore an equivalence of $\infty$-categories by virtue of Remark 4.5.1.18.

We next prove the equivalences $(2) \Leftrightarrow (3) \Leftrightarrow (4) \Leftrightarrow (5)$. Let $G: B \rightarrow \operatorname{\mathcal{C}}$ be as above. Applying Construction 4.6.4.13, we obtain a commutative diagram of $\infty$-categories

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}_{/G} \ar [r] \ar [d]^{\theta } & \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(B, \operatorname{\mathcal{C}}) } \{ G\} \ar [d]^{\theta '} \\ \operatorname{\mathcal{C}}_{ / (G \circ F)} \ar [r] & \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(A, \operatorname{\mathcal{C}}) } \{ G \circ F \} , }$

where the horizontal maps are equivalences of $\infty$-categories (Theorem 4.6.4.17). It follows that $\theta$ is an equivalence of $\infty$-categories if and only if $\theta '$ is an equivalence of $\infty$-categories. This proves the equivalence $(2) \Leftrightarrow (3)$. Note that the functor $\theta '$ fits into a commutative diagram

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(B, \operatorname{\mathcal{C}}) } \{ G\} \ar [dr] \ar [rr]^{\theta '} & & \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(A, \operatorname{\mathcal{C}}) } \{ G \circ F \} \ar [dl] \\ & \operatorname{\mathcal{C}}, & }$

where the vertical maps are right fibrations (Corollary 4.6.4.12). Applying Corollary 5.1.6.15 and Proposition 5.1.6.5, we see that $\theta '$ is an equivalence of $\infty$-categories if and only if it induces a homotopy equivalence

$\theta '_{X}: \{ \underline{X} \} \operatorname{\vec{\times }}_{ \operatorname{Fun}(B, \operatorname{\mathcal{C}}) } \{ G\} \rightarrow \{ \underline{X} \circ F \} \operatorname{\vec{\times }}_{ \operatorname{Fun}(A, \operatorname{\mathcal{C}}) } \{ G \circ F \}$

for each object $X \in \operatorname{\mathcal{C}}$, which proves the equivalence $(3) \Leftrightarrow (4)$. Unwinding the definitions, we can identify $\theta '$ with the lower horizontal map appearing in the diagram

$\xymatrix@R =50pt@C=50pt{ \operatorname{Fun}_{/\operatorname{\mathcal{C}}}( B, \operatorname{\mathcal{C}}_{X/} ) \ar [r]^-{\theta ''_{X}} \ar [d] & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( A, \operatorname{\mathcal{C}}_{X/} ) \ar [d] \\ \operatorname{Fun}_{/\operatorname{\mathcal{C}}}( B, \{ X\} \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}) \ar [r]^-{\theta '_{X}} & \operatorname{Fun}_{/\operatorname{\mathcal{C}}}( A, \{ X\} \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}), }$

where the vertical maps are given by postcomposition with the coslice diagonal morphism $\rho : \operatorname{\mathcal{C}}_{X/} \rightarrow \{ X\} \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}$. Theorem 4.6.4.17 guarantees that $\rho$ is an equivalence of $\infty$-categories. It is therefore also an an equivalence of left fibrations over $\operatorname{\mathcal{C}}$ (Proposition 5.1.6.5), so that the vertical maps are homotopy equivalences. It follows that $\theta '_{X}$ is a homotopy equivalence if and only if $\theta ''_{X}$ is a homotopy equivalence, which proves the equivalence $(4) \Leftrightarrow (5)$.

We now complete the proof by showing that $(5)$ implies $(1)$. Assume that condition $(5)$ is satisfied; we wish to show that $F$ is left cofinal. Let $q: \widetilde{B} \rightarrow B$ be a left fibration; we must show that composition with $F$ induces a homotopy equivalence $\operatorname{Fun}_{/B}( B, \widetilde{B} ) \rightarrow \operatorname{Fun}_{/B}(A, \widetilde{B} )$. To prove this, we are free to replace $q: \widetilde{B} \rightarrow B$ by any other left fibration which is equivalent to it (in the sense of Definition 5.1.6.1). We may therefore assume without loss of generality that there exists a pullback diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ \widetilde{B} \ar [r] \ar [d]^{q} & \operatorname{\mathcal{S}}_{\ast } \ar [d]^{q_{\mathrm{univ}}} \\ B \ar [r]^-{G} & \operatorname{\mathcal{S}}, }$

where $q_{\mathrm{univ}}: \operatorname{\mathcal{S}}_{\ast } \rightarrow \operatorname{\mathcal{S}}$ is the universal left fibration of Corollary 5.7.0.6. We are then reduced to proving that $F$ induces a homotopy equivalence $\operatorname{Fun}_{ / \operatorname{\mathcal{S}}}( B, \operatorname{\mathcal{S}}_{\ast } ) \rightarrow \operatorname{Fun}_{ \operatorname{\mathcal{S}}}( A, \operatorname{\mathcal{S}}_{\ast } )$, which is a special case of $(5)$ (applied to the $\infty$-category $\operatorname{\mathcal{C}}= \operatorname{\mathcal{S}}$ and the object $X = \Delta ^0$). $\square$