# Kerodon

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

Proposition 6.3.5.6. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a morphism of simplicial sets which exhibits $\operatorname{\mathcal{D}}$ as a localization of $\operatorname{\mathcal{C}}$ with respect to a collection of edges $W$. Let $K$ be any simplicial set, and let $W_{K}$ denote the collection of edges $e = (e', e'')$ of the product $K \times \operatorname{\mathcal{C}}$ for which $e'$ is a degenerate edge of $K$ and $e''$ belongs to $W$. Then the induced map $F_{K}: K \times \operatorname{\mathcal{C}}\rightarrow K \times \operatorname{\mathcal{D}}$ exhibits $K \times \operatorname{\mathcal{D}}$ as the localization of $K \times \operatorname{\mathcal{C}}$ with respect to $W_{K}$.

Proof. Let $\operatorname{\mathcal{E}}$ be an $\infty$-category, and let

$\theta : \operatorname{Fun}( K \times \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}(K \times \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$

be the functor given by precomposition with $F_ K$. We wish to show that $F_{K}$ is fully faithful, and that its essential image is the full subcategory $\operatorname{Fun}( (K \times \operatorname{\mathcal{C}})[W_{K}^{-1}], \operatorname{\mathcal{E}})$ of Notation 6.3.1.1. Unwinding the definitions, we can identify $\theta$ with the functor

$\theta ': \operatorname{Fun}( \operatorname{\mathcal{D}}, \operatorname{Fun}(K,\operatorname{\mathcal{E}}) ) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{Fun}(K, \operatorname{\mathcal{E}}))$

given by precomposition with $F$. Under this identification $\operatorname{Fun}( (K \times \operatorname{\mathcal{C}})[W_{K}^{-1}], \operatorname{\mathcal{E}})$ corresponds to the full subcategory $\operatorname{Fun}( \operatorname{\mathcal{C}}[W^{-1}], \operatorname{Fun}(K,\operatorname{\mathcal{E}}) ) \subseteq \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{Fun}(K,\operatorname{\mathcal{E}}) )$ (see Theorem 4.4.4.4), so that the desired result follows from our assumption on the functor $F$. $\square$