# Kerodon

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

Proposition 7.1.7.12. Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty$-categories and let $\overline{f}: K^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$. Then $\overline{f}$ is a $U$-limit diagram if and only if, for every object $C \in \operatorname{\mathcal{C}}$, the diagram of morphism spaces

7.4
$$\begin{gathered}\label{equation:U-colimit-by-morphism-space} \xymatrix@R =50pt@C=50pt{ \operatorname{Hom}_{\operatorname{Fun}(K^{\triangleleft }, \operatorname{\mathcal{C}}) }( \underline{C}, \overline{f} ) \ar [r] \ar [d] & \operatorname{Hom}_{\operatorname{Fun}(K, \operatorname{\mathcal{C}}) }( \underline{C}|_{K}, \overline{f}|_{K} ) \ar [d] \\ \operatorname{Hom}_{\operatorname{Fun}(K^{\triangleleft }, \operatorname{\mathcal{D}}) }( U \circ \underline{C}, U \circ \overline{f} ) \ar [r] & \operatorname{Hom}_{\operatorname{Fun}(K, \operatorname{\mathcal{D}}) }( U \circ \underline{C}|_{K}, U \circ \overline{f}|_{K} ) } \end{gathered}$$

is a homotopy pullback square; here we let $\underline{C} \in \operatorname{Fun}( K^{\triangleleft }, \operatorname{\mathcal{C}})$ denote the constant diagram taking the value $C$.

Proof. Set $f = \overline{f}|_{K}$. Note that the restriction maps

$\operatorname{\mathcal{C}}_{/\overline{f}} \rightarrow \operatorname{\mathcal{C}}_{/f } \quad \quad \operatorname{\mathcal{C}}_{/f} \rightarrow \operatorname{\mathcal{C}}\quad \quad \operatorname{\mathcal{D}}_{ / (U \circ \overline{f} )} \rightarrow \operatorname{\mathcal{E}}_{/(U \circ f) }$

are right fibrations of simplicial sets (Corollary 4.3.6.11). It follows that we can regard the map

$U': \operatorname{\mathcal{C}}_{ / \overline{f} } \rightarrow \operatorname{\mathcal{C}}_{/f} \times _{ \operatorname{\mathcal{D}}_{/(U \circ f)}} \operatorname{\mathcal{D}}_{ / (U \circ \overline{f} ) }$

of Remark 7.1.7.8 as a functor between $\infty$-categories which are right-fibered over $\operatorname{\mathcal{C}}$. Combining Remark 7.1.7.8 with the criterion of Corollary 5.1.5.4, we see that $\overline{f}$ is a $U$-colimit diagram if and only if, for every object $C \in \operatorname{\mathcal{C}}$, the induced map

$U'_{C}: \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{ / \overline{f} } \rightarrow \{ C\} \times _{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/f} \times _{ \operatorname{\mathcal{D}}_{/(U \circ f)}} \operatorname{\mathcal{D}}_{ / (U \circ \overline{f} ) }$

is a homotopy equivalence of Kan complexes.

To complete the proof, it will suffice to show that $U'_{C}$ is a homotopy equivalence if and only if the diagram (7.4) is a homotopy pullback square. To see this, we note that Theorem 3.4.1.5 supplies a termwise homotopy equivalence of (7.4) with the diagram

7.5
$$\begin{gathered}\label{equation:U-colimit-by-morphism-space2} \xymatrix@R =50pt@C=50pt{ \{ C\} \times _{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{ / \overline{f} } \ar [r] \ar [d] & \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/f} \ar [d] \\ \{ U(C) \} \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}_{ / (U \circ \overline{f} )} \ar [r] & \{ U(C) \} \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}_{ / (U \circ f) }. } \end{gathered}$$

It will therefore suffice to show that (7.5) is a homotopy pullback square if and only if $U'_{C}$ is a homotopy equivalence (Corollary 3.4.1.10). This is a special case of Example 3.4.1.5, since the horizontal maps in the diagram (7.5) are Kan fibrations (combine Corollaries 4.3.6.11 and 4.4.3.8). $\square$