Kerodon

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

Proposition 7.5.3.12. Let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{QCat}$ be an isofibrant diagram of $\infty $-categories. Then the inclusion map $\iota : \varprojlim ( \mathscr {F} ) \hookrightarrow \underset {\longleftarrow }{\mathrm{holim}}( \mathscr {F} )$ is an equivalence of $\infty $-categories.

Proof. Let $\alpha : \mathscr {F} \hookrightarrow \mathscr {F}^{+}$ be the isofibrant replacement of Construction 7.5.3.3. By virtue of Proposition 7.5.3.7 (and Remark 7.5.3.11), it will suffice to show that the limit $\varprojlim (\alpha ): \varprojlim ( \mathscr {F} ) \hookrightarrow \varprojlim ( \mathscr {F}^{+} )$ is an equivalence of $\infty $-categories. This is a special case of Corollary 4.5.6.17, since $\alpha $ is a levelwise categorical equivalence between isofibrant diagrams (Proposition 7.5.3.4). $\square$