# Kerodon

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

Proposition 8.5.5.8 (Uniqueness). Let $H: \operatorname{\mathcal{C}}\rightarrow \widehat{\operatorname{\mathcal{C}}}$ be a functor of $\infty$-categories, where $\widehat{\operatorname{\mathcal{C}}}$ is idempotent complete. The following conditions are equivalent:

$(a)$

The functor $H$ exhibits $\widehat{\operatorname{\mathcal{C}}}$ as an idempotent completion of $\operatorname{\mathcal{C}}$, in the sense of Definition 8.5.5.1.

$(b)$

For every idempotent complete $\infty$-category $\operatorname{\mathcal{D}}$, precomposition with $H$ induces an equivalence of $\infty$-categories $\operatorname{Fun}( \widehat{\operatorname{\mathcal{C}}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$.

$(c)$

For every idempotent complete $\infty$-category $\operatorname{\mathcal{D}}$, precomposition with $H$ induces a homotopy equivalence of Kan complexes $\operatorname{Fun}( \widehat{\operatorname{\mathcal{C}}}, \operatorname{\mathcal{D}})^{\simeq } \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})^{\simeq }$.

$(d)$

For every idempotent complete $\infty$-category $\operatorname{\mathcal{D}}$, precomposition with $H$ induces a bijection $\pi _0( \operatorname{Fun}( \widehat{\operatorname{\mathcal{C}}}, \operatorname{\mathcal{D}})^{\simeq } ) \rightarrow \pi _0( \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})^{\simeq } )$.

Proof of Proposition 8.5.5.8. Let $H: \operatorname{\mathcal{C}}\rightarrow \widehat{\operatorname{\mathcal{C}}}$ be a functor of $\infty$-categories, where $\widehat{\operatorname{\mathcal{C}}}$ is idempotent complete. The implication $(a) \Rightarrow (b)$ follows from Lemma 8.5.5.9, the implication $(b) \Rightarrow (c)$ from Remark 4.5.1.19, and the implication $(c) \Rightarrow (d)$ from Remark 3.1.6.5. We will complete the proof by showing that $(d)$ implies $(a)$.

Using Corollary 8.5.5.6, we can choose an $\infty$-category $\widehat{\operatorname{\mathcal{C}}}'$ and a functor $H': \operatorname{\mathcal{C}}\rightarrow \widehat{\operatorname{\mathcal{C}}}'$ which exhibits $\widehat{\operatorname{\mathcal{C}}'}$ as an idempotent completion of $\operatorname{\mathcal{C}}$. Since the $\infty$-category $\widehat{\operatorname{\mathcal{C}}}'$ is idempotent complete, assumption $(d)$ guarantees that there exists a functor $G: \widehat{\operatorname{\mathcal{C}}} \rightarrow \widehat{\operatorname{\mathcal{C}}}'$ such that $H'$ is isomorphic to $G \circ H$ (as an object of the $\infty$-category $\operatorname{Fun}( \operatorname{\mathcal{C}}, \widehat{\operatorname{\mathcal{C}}}' )$). By virtue of Remark 8.5.5.3, the functor $G \circ H$ also exhibits $\widehat{\operatorname{\mathcal{C}}}'$ as an idempotent completion of $\operatorname{\mathcal{C}}$. To show that $H$ exhibits $\widehat{\operatorname{\mathcal{C}}}$ as an idempotent completion of $\operatorname{\mathcal{C}}$, it will suffice to show that the functor $G$ is an equivalence of $\infty$-categories (Remark 8.5.5.2). This is equivalent to the assertion that the homotopy class $[G]$ is an isomorphism when regarded as a morphism in the homotopy category of idempotent complete $\infty$-categories. Fix an idempotent complete $\infty$-category $\operatorname{\mathcal{D}}$; we wish to show that precomposition with $[G]$ induces a bijection

$\theta : \pi _0( \operatorname{Fun}( \widehat{\operatorname{\mathcal{C}}}', \operatorname{\mathcal{D}})^{\simeq }) \rightarrow \pi _0( \operatorname{Fun}( \widehat{\operatorname{\mathcal{C}}}, \operatorname{\mathcal{D}})^{\simeq } ).$

Invoking assumption $(d)$, this is equivalent to the bijectivity of the composite map

$\pi _0( \operatorname{Fun}( \widehat{\operatorname{\mathcal{C}}}', \operatorname{\mathcal{D}})^{\simeq } ) \xrightarrow { \circ [G]} \pi _0( \operatorname{Fun}( \widehat{\operatorname{\mathcal{C}}}, \operatorname{\mathcal{D}})^{\simeq } ) \xrightarrow { \circ [H]} \pi _0( \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})^{\simeq } ),$

which follows from Lemma 8.5.5.9. $\square$