# Kerodon

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

Proposition 6.3.5.2. Suppose we are given a commutative diagram of simplicial sets

6.12
$$\begin{gathered}\label{equation:cocartesian-fiberwise-localization} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [rr]^{F} \ar [dr]^{U} & & \operatorname{\mathcal{E}}' \ar [dl]_{U'} \\ & \operatorname{\mathcal{C}}& } \end{gathered}$$

with the following properties:

$(1)$

The morphisms $U$ and $U'$ are cocartesian fibrations.

$(2)$

The morphism $F$ carries $U$-cocartesian edges of $\operatorname{\mathcal{E}}$ to $U'$-cocartesian edges of $\operatorname{\mathcal{E}}'$.

$(3)$

For every vertex $C \in \operatorname{\mathcal{C}}$, the induced functor of $\infty$-categories $F_{C}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}'_{C}$ exhibits $\operatorname{\mathcal{E}}'_{C}$ as the localization of $\operatorname{\mathcal{E}}_{C}$ with respect to some collection of morphisms $W_{C}$.

Set $W = \bigcup _{C \in \operatorname{\mathcal{C}}} W_{C}$, which we regard as a collection of edges of the simplicial set $\operatorname{\mathcal{E}}$. Then $F$ exhibits $\operatorname{\mathcal{E}}'$ as a localization of $\operatorname{\mathcal{E}}$ with respect to $W$.

Proof. Let $\operatorname{\mathcal{D}}$ be an $\infty$-category, so that precomposition with $F$ induces a functor $F^{\ast }: \operatorname{Fun}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}(\operatorname{\mathcal{E}}, \operatorname{\mathcal{D}})$. We wish to show that the functor $F^{\ast }$ 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 $\operatorname{\mathcal{B}}' = \operatorname{Fun}(\operatorname{\mathcal{E}}'/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ be the relative exponentials of Construction 4.5.9.1, and let $\pi : \operatorname{\mathcal{B}}\rightarrow \operatorname{\mathcal{C}}$ and $\pi ': \operatorname{\mathcal{B}}' \rightarrow \operatorname{\mathcal{C}}$ denote the projection maps. Combining assumption $(1)$ with Corollary 5.3.6.8, we see that $\pi$ and $\pi '$ are cartesian fibrations.

For each vertex $C \in \operatorname{\mathcal{C}}$, let us identify the fibers $\operatorname{\mathcal{B}}_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{B}}$ and $\operatorname{\mathcal{B}}'_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{B}}'$ with the $\infty$-categories $\operatorname{Fun}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{D}})$ and $\operatorname{Fun}( \operatorname{\mathcal{E}}'_{C}, \operatorname{\mathcal{D}})$, respectively. Precomposition with $F$ induces a morphism of simplicial sets $G: \operatorname{\mathcal{B}}' \rightarrow \operatorname{\mathcal{B}}$ satisfying $\pi \circ G = \pi '$, given on each fiber by the functor

$\operatorname{\mathcal{B}}'_{C} = \operatorname{Fun}( \operatorname{\mathcal{E}}'_{C},\operatorname{\mathcal{D}}) \xrightarrow { \circ F_ C } \operatorname{Fun}( \operatorname{\mathcal{E}}_ C, \operatorname{\mathcal{D}}) = \operatorname{\mathcal{B}}_{C}.$

Combining assumption $(2)$ with Corollary 5.3.6.8, we see that $G$ carries $\pi '$-cartesian edges of $\operatorname{\mathcal{B}}'$ to $\pi$-cartesian edges of $\operatorname{\mathcal{B}}$. In particular, for every edge $e: X \rightarrow Y$ of $\operatorname{\mathcal{C}}$, the diagram of $\infty$-categories

6.13
$$\begin{gathered}\label{equation:proposition:cocartesian-fiberwise-localization} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{B}}'_{Y} \ar [r]^-{e^{\ast }} \ar [d]^{ G_{Y} } & \operatorname{\mathcal{B}}'_{X} \ar [d]^{ G_{X}} \\ \operatorname{\mathcal{B}}_{Y} \ar [r]^-{ e^{\ast } } & \operatorname{\mathcal{B}}_{X} } \end{gathered}$$

commutes up to isomorphism, where the horizontal functors are given by contravariant transport along $e$ (see Remark 5.2.8.5).

Let us identify the vertices of $\operatorname{\mathcal{B}}$ with pairs $(C, \rho )$, where $C$ is a vertex of $\operatorname{\mathcal{C}}$ and $\rho : \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{D}}$ is a functor of $\infty$-categories. Let $\operatorname{\mathcal{B}}^{0} \subseteq \operatorname{\mathcal{B}}$ denote the full simplicial subset spanned by those vertices $(C,\rho )$ for which the functor $\rho$ carries each edge of $W_{C}$ to an isomorphism in the $\infty$-category $\operatorname{\mathcal{D}}$. It follows from assumption $(3)$ that for every vertex $C$, the functor $G_{C}: \operatorname{\mathcal{B}}'_{C} \rightarrow \operatorname{\mathcal{B}}_{C}$ is fully faithful, and its essential image can be identified with the full subcategory $\operatorname{\mathcal{B}}^{0}_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{B}}^{0} \subseteq \operatorname{\mathcal{B}}_{C}$. Combining this observation with the homotopy commutativity of the diagram (6.13), we see that for every edge $e: X \rightarrow Y$ in $\operatorname{\mathcal{E}}$, the contravariant transport functor $e^{\ast }: \operatorname{\mathcal{B}}_{Y} \rightarrow \operatorname{\mathcal{B}}_{X}$ carries $\operatorname{\mathcal{B}}^{0}_{Y}$ into $\operatorname{\mathcal{B}}^{0}_{X}$. It follows that $\pi$ restricts to a cartesian fibration of simplicial sets $\pi ^{0}: \operatorname{\mathcal{B}}^{0} \rightarrow \operatorname{\mathcal{C}}$, and that an edge of $\operatorname{\mathcal{B}}^{0}$ is $\pi ^{0}$-cartesian if and only if it is $\pi$-cartesian when viewed as an edge of $\operatorname{\mathcal{B}}$ (Proposition 5.1.4.16). In particular, the morphism $G: \operatorname{\mathcal{B}}' \rightarrow \operatorname{\mathcal{B}}^{0} \subseteq \operatorname{\mathcal{B}}$ carries $\pi '$-cartesian edges of $\operatorname{\mathcal{B}}'$ to $\pi ^{0}$-cartesian edges of $\operatorname{\mathcal{B}}^{0}$, and therefore induces an equivalence $\operatorname{\mathcal{B}}' \rightarrow \operatorname{\mathcal{B}}^{0}$ of cartesian fibrations over $\operatorname{\mathcal{C}}$ (Proposition 5.1.7.14). We complete the proof by observing that $F^{\ast }: \operatorname{Fun}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}(\operatorname{\mathcal{E}}[W^{-1}], \operatorname{\mathcal{D}})$ can be identified with the functor

$\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{B}}' ) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{B}}^{0} )$

given by precomposition with $G$, and is therefore an equivalence of $\infty$-categories. $\square$