Kerodon

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

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

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

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

Proof. For each vertex $C \in \operatorname{\mathcal{C}}$, let $W_{C}$ be the collection of all morphisms in the $\infty $-category $\operatorname{\mathcal{E}}_{C}$. Since $\operatorname{\mathcal{E}}_{C}$ is weakly contractible, the projection map $\operatorname{\mathcal{E}}_{C} \rightarrow \{ C\} $ exhibits $\{ C\} $ as a localization of $\operatorname{\mathcal{E}}_{C}$ with respect to $W_{C}$ (Proposition 6.3.1.20). The desired result now follows by applying Proposition 6.3.5.2 to the commutative diagram

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

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$

Proof. Combine Proposition 6.3.5.4 with Proposition 5.1.4.14. $\square$

Proof of Theorem 6.3.5.1. Suppose we are given a commutative diagram of simplicial sets

which satisfies the hypotheses of Theorem 6.3.5.1. Fix an $\infty $-category $\operatorname{\mathcal{D}}$. We wish to show that precomposition with $F$ induces a fully faithful functor $F^{\ast }: \operatorname{Fun}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}(\operatorname{\mathcal{E}}, \operatorname{\mathcal{D}})$, whose essential image consists of those morphisms $G: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ which carry each edge of $W_{-} \cup W_{+}$ to an isomorphism in $\operatorname{\mathcal{D}}$. Let $\pi : \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{C}}'} \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{E}}'$ be given by projection onto the second factor. Note that the pair $(U, F)$ determines a morphism of simplicial sets $\widetilde{F}: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{C}}'} \operatorname{\mathcal{E}}'$ satisfying $\pi \circ \widetilde{F} = F$, so that $F^{\ast }$ factors as a composition

Let $W'$ be the collection of all edges of $\operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{C}}'} \operatorname{\mathcal{E}}'$ of the form $( \overline{e}, f)$, where $\overline{e}$ belongs to $\overline{W}$ and $f$ is a $U'$-cocartesian edge of $\operatorname{\mathcal{E}}'$. It follows from Proposition 6.3.5.4 that the functor $\pi ^{\ast }$ is fully faithful, and that its essential image consists of those morphisms $G': \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{C}}'} \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{D}}$ which carry each edge of $W'$ to an isomorphism in $\operatorname{\mathcal{D}}$. Applying Proposition 6.3.5.2, we see that the functor $\widetilde{F}^{\ast }$ is also fully faithful, and that its essential image consists of those morphisms $G: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ which carry each edge of $W_{-}$ to an isomorphism in $\operatorname{\mathcal{D}}$. To complete the proof, it will suffice to show the following:

$(\ast )$

A morphism of simplicial sets $G': \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{C}}'} \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{D}}$ carries each edge of $W'$ to an isomorphism in $\operatorname{\mathcal{D}}$ if and only if $G' \circ \widetilde{F}$ carries each edge of $W_{+}$ to an isomorphism in $\operatorname{\mathcal{D}}$.

The “only if” assertion is immediate (since $\widetilde{F}(W_{+} )$ is contained in $W'$). The converse follows from the observation that every edge $(\overline{e}, f)$ is isomorphic, when viewed as an object of the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \Delta ^1, \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{C}}'} \operatorname{\mathcal{E}}')$, to $\widetilde{F}(e)$, where $e: X \rightarrow Y$ is any $U$-cocartesian edge of $\operatorname{\mathcal{E}}$ for which $U(e) = \overline{e}$ and $F(X)$ is isomorphic to the domain of $f$ as an object of the $\infty $-category $\{ X\} \times _{\operatorname{\mathcal{C}}'} \operatorname{\mathcal{E}}'$. $\square$

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

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

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$