# Kerodon

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

Proposition 7.5.4.5. Let $\operatorname{\mathcal{C}}$ be a small category and let $\overline{\mathscr {F}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$ be a diagram of Kan complexes. Then $\overline{\mathscr {F}}$ is a homotopy limit diagram (in the sense of Definition 7.5.4.1) if and only if the induced functor of $\infty$-categories

$\operatorname{N}_{\bullet }^{\operatorname{hc}}( \overline{\mathscr {F}}): \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}^{\triangleleft } ) \rightarrow \operatorname{N}_{\bullet }^{\operatorname{hc}}( \operatorname{Kan}) = \operatorname{\mathcal{S}}$

is a limit diagram (in the sense of Definition 7.1.2.4).

Proof. Let $\operatorname{N}_{\bullet }^{\overline{\mathscr {F}}}(\operatorname{\mathcal{C}}^{\triangleleft })$ be the weighted nerve of the functor $\overline{\mathscr {F}}$ (Definition 5.3.3.1) and let $U: \operatorname{N}_{\bullet }^{\overline{\mathscr {F}}}(\operatorname{\mathcal{C}}^{\triangleleft }) \rightarrow \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}^{\triangleleft } )$ be the projection map. Then $U$ is a left fibration, and $\operatorname{N}_{\bullet }^{\operatorname{hc}}( \overline{\mathscr {F}} )$ is a covariant transport representation for $U$ (Example 5.6.5.6). Set $\mathscr {F} = \overline{\mathscr {F}}|_{\operatorname{\mathcal{C}}}$. Applying Corollary 7.4.5.8, we deduce that $\operatorname{N}_{\bullet }^{\operatorname{hc}}( \overline{\mathscr {F}} )$ is a limit diagram in the $\infty$-category $\operatorname{\mathcal{S}}$ if and only if the restriction map

$\rho : \operatorname{Fun}_{ / \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}^{\triangleleft }) }( \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}^{\triangleleft }), \operatorname{N}_{\bullet }^{\overline{\mathscr {F}}}(\operatorname{\mathcal{C}}^{\triangleleft }) ) \rightarrow \simeq \operatorname{Fun}_{ / \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }( \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}), \operatorname{N}_{\bullet }^{\mathscr {F}}(\operatorname{\mathcal{C}}) )$

is a homotopy equivalence of Kan complexes. We then have a commutative diagram $\rho$ fits into a commutative diagram

$\xymatrix@R =50pt@C=50pt{ \varprojlim ( \overline{ \mathscr {F} } ) \ar [r]^-{\rho '} \ar [d]^{\overline{\iota }} & \varprojlim (\mathscr {F}) \ar [d]^{\iota } \\ \underset {\longleftarrow }{\mathrm{holim}}( \overline{ \mathscr {F} } ) \ar [r]^-{\rho } & \underset {\longleftarrow }{\mathrm{holim}}( \mathscr {F}), }$

where $\iota$ and $\overline{\iota }$ are the comparison maps of Remark 7.5.2.10. Since the category $\operatorname{\mathcal{C}}^{\triangleleft }$ has an initial object, the morphism $\overline{\iota }$ is a homotopy equivalence (Proposition 7.5.2.11). It follows that $\rho$ is a homotopy equivalence if and only if the composition $\rho \circ \overline{\iota } = \iota \circ \rho '$ is a homotopy equivalence. We conclude by observing that the composition $\iota \circ \rho '$ can be identified with the map $\overline{\mathscr {F}}( {\bf 0} ) \rightarrow \underset {\longleftarrow }{\mathrm{holim}}(\mathscr {F})$ appearing in Definition 7.5.4.1. $\square$