Kerodon

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

Proposition 6.2.1.13. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ and $G: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be functors of $\infty$-categories and let

$\eta : \operatorname{id}_{\operatorname{\mathcal{C}}} \rightarrow G \circ F \quad \quad \epsilon : F \circ G \rightarrow \operatorname{id}_{\operatorname{\mathcal{D}}}$

be natural transformations which are compatible up to homotopy. Let $\operatorname{\mathcal{C}}' \subseteq \operatorname{\mathcal{C}}$ be the full subcategory spanned by those objects $C \in \operatorname{\mathcal{C}}$ for which the unit $\eta _{C}: C \rightarrow (G \circ F)(C)$ is an isomorphism, and let $\operatorname{\mathcal{D}}' \subseteq \operatorname{\mathcal{D}}$ be the full subcategory spanned by those objects $D \in \operatorname{\mathcal{D}}$ for which the counit $\epsilon _ D: (F \circ G)(D) \rightarrow D$ is an isomorphism. Then $F$ and $G$ restrict to functors $F': \operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{D}}'$ and $G': \operatorname{\mathcal{D}}' \rightarrow \operatorname{\mathcal{C}}'$ which are homotopy inverse to one another.

Proof. Let $C$ be an object of $\operatorname{\mathcal{C}}'$, so that $\eta _{C}: C \rightarrow (G \circ F)(C)$ is an isomorphism. Since $\eta$ and $\epsilon$ are compatible up to homotopy, the identity morphism $\operatorname{id}_{ F(C) }$ is a composition of $F(\eta _ C): F(C) \rightarrow (F \circ G \circ F)(C)$ with $\epsilon _{F(C)}: (F \circ G \circ F)(C) \rightarrow F(C)$ in the $\infty$-category $\operatorname{\mathcal{D}}$. It follows that $\epsilon _{F(C)}$ is an isomorphism in $\operatorname{\mathcal{D}}$ (Remark 1.3.6.3), so that $F(C)$ belongs to the full subcategory $\operatorname{\mathcal{D}}' \subseteq \operatorname{\mathcal{D}}$. Setting $F' = F|_{\operatorname{\mathcal{C}}'}$, we obtain a functor $F': \operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{D}}'$. A similar argument shows that we can regard $G' = G|_{\operatorname{\mathcal{D}}'}$ as a functor from $\operatorname{\mathcal{D}}'$ to $\operatorname{\mathcal{C}}'$. The unit morphism $\eta$ restricts to a natural transformation of functors $\eta ': \operatorname{id}_{\operatorname{\mathcal{C}}'} \rightarrow G' \circ F'$. By construction, $\eta '$ carries each object $C \in \operatorname{\mathcal{C}}'$ to an isomorphism, and is therefore an isomorphism in the functor $\infty$-category $\operatorname{Fun}( \operatorname{\mathcal{C}}', \operatorname{\mathcal{C}}' )$ (Theorem 4.4.4.4). Similarly, the counit $\epsilon$ restricts to a natural isomorphism $\epsilon ': F' \circ G' \rightarrow \operatorname{id}_{\operatorname{\mathcal{D}}'}$, so that $F'$ and $G'$ are homotopy inverse to one another. $\square$