Kerodon

Proof of Proposition 4.4.3.22. 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

in the $\infty $-category $\operatorname{\mathcal{C}}$. Since the collection of isomorphisms in $\operatorname{\mathcal{C}}$ is closed under composition (Remark 1.4.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.17 (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$