Kerodon

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

Proposition 7.5.7.6. Let $\operatorname{\mathcal{C}}$ be a category and let $\overline{\mathscr {F}}: \operatorname{\mathcal{C}}^{\triangleright } \rightarrow \operatorname{Set_{\Delta }}$ be a diagram of simplicial sets. Then $\overline{\mathscr {F}}$ is a homotopy colimit diagram if and only if, for every Kan complex $X$, the functor

\[ X^{\overline{\mathscr {F}}}: ( \operatorname{\mathcal{C}}^{\triangleright } )^{\operatorname{op}} \rightarrow \operatorname{Kan}\quad \quad C \mapsto \operatorname{Fun}( \overline{\mathscr {F}}(C), X) \]

is a homotopy limit diagram.

Proof. Set $\mathscr {F} = \overline{\mathscr {F}}|_{\operatorname{\mathcal{C}}}$, let ${\bf 1}$ denote the final object of $\operatorname{\mathcal{C}}^{\triangleright }$, and let $\theta : \underset { \longrightarrow }{\mathrm{holim}}( \mathscr {F} ) \rightarrow \overline{\mathscr {F}}({\bf 1})$ be the map appearing in Definition 7.5.7.3. Then $\overline{\mathscr {F}}$ is a homotopy colimit diagram if and only if, for every Kan complex $X$, precomposition with $\theta $ induces a homotopy equivalence of Kan complexes

\[ \theta ^{\ast }: \operatorname{Fun}( \overline{\mathscr {F}}({\bf 1}), X) \rightarrow \operatorname{Fun}( \underset { \longrightarrow }{\mathrm{holim}}( \mathscr {F} ), X). \]

Setting $\mathscr {G} = \mathscr {F}^{\operatorname{op}}$, $\overline{\mathscr {G}} = \overline{\mathscr {F}}^{\operatorname{op}}$, and $Y = X^{\operatorname{op}}$, Example 7.5.1.7 identifies $\theta ^{\ast }$ with the opposite of the restriction map $Y^{ \overline{\mathscr {G}} }( {\bf 1} ) \rightarrow \underset {\longleftarrow }{\mathrm{holim}}( Y^{\mathscr {G}} )$ appearing in Definition 7.5.4.1. In particular, $\theta ^{\ast }$ is a homotopy equivalence if and only if $Y^{ \overline{\mathscr {G}} }$ is a homotopy limit diagram of Kan complexes. By virtue of Corollary 7.5.4.12, this is equivalent to the requirement that $X^{\overline{\mathscr {F}}}$ is a homotopy limit diagram. $\square$