# Kerodon

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

Corollary 4.5.6.19. Let $\operatorname{\mathcal{C}}$ be a small category, let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{Set_{\Delta }}$ be an isofibrant diagram, and define $\mathscr {F}^{\simeq }: \operatorname{\mathcal{C}}\rightarrow \operatorname{Set_{\Delta }}$ by the formula $\mathscr {F}^{\simeq }(C) = \mathscr {F}(C)^{\simeq }$. Then $\mathscr {F}^{\simeq }$ is also an isofibrant diagram. Moreover, the inclusion map $\varprojlim ( \mathscr {F}^{\simeq } ) \hookrightarrow \varprojlim ( \mathscr {F} )$ restricts to an isomorphism of $\varprojlim ( \mathscr {F}^{\simeq } )$ with the core of the $\infty$-category $\varprojlim ( \mathscr {F} )$.

Proof. We first show that the diagram $\mathscr {F}^{\simeq }$ is isofibrant. Let $\mathscr {E}: \operatorname{\mathcal{C}}\rightarrow \operatorname{Set_{\Delta }}$ be a functor and let $\mathscr {E}_0 \subseteq \mathscr {E}$ be a subfunctor for which the inclusion $\mathscr {E}_0 \hookrightarrow \mathscr {E}$ is a levelwise categorical equivalence. Suppose we are given a natural transformation $\alpha _0: \mathscr {E}_0 \rightarrow \mathscr {F}^{\simeq }$. Our assumption that $\mathscr {F}$ is isofibrant guarantees that $\alpha _0$ can be extended to a natural transformation $\alpha : \mathscr {E} \rightarrow \mathscr {F}$. We claim that $\alpha$ automatically factors through the functor $\mathscr {F}^{\simeq }$: that is, for every object $C \in \operatorname{\mathcal{C}}$, the map $\alpha _{C}: \mathscr {E}(C) \rightarrow \mathscr {F}(C)$ factors through the core of $\mathscr {F}(C)$. This follows from the observation that the lifting problem

$\xymatrix@R =50pt@C=50pt{ \mathscr {E}_0(C) \ar [d] \ar [r]^-{ \alpha _0} & \mathscr {F}(C)^{\simeq } \ar [d] \\ \mathscr {E}(C) \ar [r]^-{ \alpha } \ar@ {-->}[ur] & \mathscr {F}(C) }$

has a (unique) solution, since the inclusion $\mathscr {F}(C)^{\simeq } \hookrightarrow \mathscr {F}(C)$ is an isofibration (Proposition 4.4.3.6).

We now prove the second assertion. Let $X$ denote the core of the $\infty$-category $\varprojlim ( \mathscr {F} )$. For every object $C \in \operatorname{\mathcal{C}}$, the projection map $\varprojlim ( \mathscr {F} ) \rightarrow \mathscr {F}(C)$ carries $X$ into the core of $\mathscr {F}(C)$. It follows that $X$ is contained in the inverse limit $\varprojlim ( \mathscr {F}^{\simeq } )$. The reverse inclusion follows from Corollary 4.4.3.17, since the simplicial set $\varprojlim ( \mathscr {F}^{\simeq } )$ is a Kan complex (Corollary 4.5.6.18). $\square$