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$