# Kerodon

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

Proposition 6.3.5.4. Suppose we are given a pullback diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [d]^{U} \ar [r]^{F} & \operatorname{\mathcal{E}}' \ar [d]^{U'} \\ \operatorname{\mathcal{C}}\ar [r]^{\overline{F}} & \operatorname{\mathcal{C}}', }$

where $U$ and $U'$ are cocartesian fibrations. Suppose that $\overline{F}$ exhibits $\operatorname{\mathcal{C}}'$ as a localization of $\operatorname{\mathcal{C}}$ with respect to some collection of edges $\overline{W}$, and let $W$ denote the collection of $U$-cocartesian edges $e$ of $\operatorname{\mathcal{E}}$ which satisfy $U(e) \in \overline{W}$. Then $F$ exhibits $\operatorname{\mathcal{E}}'$ as a localization of $\operatorname{\mathcal{E}}$ with respect to $W$.

Proof. Using Corollary 4.1.3.3, we can choose an inner anodyne map $\operatorname{\mathcal{C}}' \hookrightarrow \operatorname{\mathcal{C}}''$, where $\operatorname{\mathcal{C}}''$ is an $\infty$-category. By virtue of Proposition 5.6.7.2, we can assume that $U'$ is the pullback of a cocartesian fibration of simplicial sets $U'': \operatorname{\mathcal{E}}'' \rightarrow \operatorname{\mathcal{C}}''$. Applying Proposition 5.3.6.1, we deduce that the inclusion map $\operatorname{\mathcal{E}}' \hookrightarrow \operatorname{\mathcal{E}}''$ is a categorical equivalence of simplicial sets. We may therefore replace $U'$ by $U''$, and thereby reduce to proving Proposition 6.3.5.4 in the special case where $\operatorname{\mathcal{C}}'$ is an $\infty$-category.

Fix an $\infty$-category $\operatorname{\mathcal{D}}$. We wish to show that the functor $F^{\ast }: \operatorname{Fun}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{D}})$ is fully faithful and that its essential image is the full subcategory $\operatorname{Fun}( \operatorname{\mathcal{E}}[W^{-1} ], \operatorname{\mathcal{D}}) \subseteq \operatorname{Fun}(\operatorname{\mathcal{E}}, \operatorname{\mathcal{D}})$. Let $\operatorname{\mathcal{B}}' = \operatorname{Fun}( \operatorname{\mathcal{E}}' / \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ and $\pi ': \operatorname{\mathcal{B}}' \rightarrow \operatorname{\mathcal{C}}$ be as in the proof of Proposition 6.3.5.2, so that we have canonical isomorphisms

$\operatorname{Fun}(\operatorname{\mathcal{E}}', \operatorname{\mathcal{D}}) \simeq \operatorname{Fun}_{ / \operatorname{\mathcal{C}}'}(\operatorname{\mathcal{C}}', \operatorname{\mathcal{B}}') \quad \quad \operatorname{Fun}(\operatorname{\mathcal{E}}, \operatorname{\mathcal{D}}) \simeq \operatorname{Fun}_{ / \operatorname{\mathcal{C}}'}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{B}}')$

Note that a morphism $G: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ carries each edge of $W$ to an isomorphism in $\operatorname{\mathcal{D}}$ if and only if the corresponding object $g \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}'}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{B}}')$ carries each element $\overline{e} \in \overline{W}$ to a $\pi '$-cartesian edge of $\operatorname{\mathcal{B}}'$ (see Corollary 5.3.6.8). Since $\overline{F}$ carries each edge $\overline{e} \in \overline{W}$ to an isomorphism in $\operatorname{\mathcal{C}}'$, this is equivalent to the requirement that $g( \overline{e} )$ is an isomorphism in $\operatorname{\mathcal{B}}'$ (Proposition 5.1.1.8). We are therefore reduced to showing that composition with $\overline{F}$ induces a fully faithful functor $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}' }( \operatorname{\mathcal{C}}', \operatorname{\mathcal{B}}' ) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}' }( \operatorname{\mathcal{C}}, \operatorname{\mathcal{B}}' )$, whose essential image is spanned by those functors $g \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}' }( \operatorname{\mathcal{C}}, \operatorname{\mathcal{B}}' )$ which carry each edge of $\overline{W}$ to an isomorphism in $\operatorname{\mathcal{B}}'$. This is a special case of Remark 6.3.1.15. $\square$