Kerodon

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

Proposition 4.4.3.21. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $X$ be a Kan complex. Then the canonical map

\[ \theta : \operatorname{Fun}(X, \operatorname{\mathcal{C}}^{\simeq } ) \hookrightarrow \operatorname{Fun}( X, \operatorname{\mathcal{C}})^{\simeq } \]

is an isomorphism of simplicial sets.

Proof of Proposition 4.4.3.21. Let $\sigma : Y \rightarrow \operatorname{Fun}(X, \operatorname{\mathcal{C}})^{\simeq }$ be a morphism of simplicial sets, which we identify with a diagram $F: X \times Y \rightarrow \operatorname{\mathcal{C}}$. To show that $\sigma $ factors through the monomorphism $\theta $, it will suffice to show that $F$ factors through the core $\operatorname{\mathcal{C}}^{\simeq } \subseteq \operatorname{\mathcal{C}}$. Equivalently, we wish to show that for every edge $(u,v): (x,y) \rightarrow (x',y')$ in the product simplicial set $X \times Y$, the morphism $F(u,v): F(x,y) \rightarrow F(x',y')$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}$. Note that $F(u,v)$ can be identified with a composition of morphisms

\[ F(x,y) \xrightarrow { F(u,\operatorname{id}_ y)} F(x', y) \xrightarrow { F( \operatorname{id}_{x'}, v) } F(x',y') \]

in the $\infty $-category $\operatorname{\mathcal{C}}$. Since the collection of isomorphisms in $\operatorname{\mathcal{C}}$ is closed under composition (Remark 1.3.6.3), it will suffice to show that $F(u,\operatorname{id}_{y} )$ and $F( \operatorname{id}_{x'}, v)$ are isomorphsms in $\operatorname{\mathcal{C}}$. In the first case, this follows from Proposition 4.4.3.16 (applied to the morphism $F|_{ X \times \{ y\} }$), since $X$ is a Kan complex. In the second case, it follows from our assumption that $\sigma $ factors through the core $\operatorname{Fun}(X, \operatorname{\mathcal{C}})^{\simeq } \subseteq \operatorname{Fun}(X,\operatorname{\mathcal{C}})$ (and therefore carries the edge $v: y \rightarrow y'$ to an isomorphism in the diagram $\infty $-category $\operatorname{Fun}(X,\operatorname{\mathcal{C}})$). $\square$