Kerodon

Proof of Proposition 8.5.6.4. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category. We wish to show that the restriction functor

has a left homotopy inverse. Using Corollary 8.5.5.3, we can choose a fully faithful functor $H: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}'$, where $\operatorname{\mathcal{C}}'$ is idempotent complete. Replacing $\operatorname{\mathcal{C}}$ by the essential image of $H$, we may assume without loss of generality that $\operatorname{\mathcal{C}}$ is a full subcategory of $\operatorname{\mathcal{C}}'$ (and $H$ is the inclusion functor). Then $R$ is the restriction of a functor $R': \operatorname{Fun}( \operatorname{N}_{\bullet }( \operatorname{Idem}), \operatorname{\mathcal{C}}' ) \rightarrow \operatorname{End}_{\operatorname{\mathcal{C}}'}^{\mathrm{idm}}$. Since $\operatorname{\mathcal{C}}'$ is idempotent complete, every idempotent endomorphism in $\operatorname{\mathcal{C}}'$ is split, and therefore weakly split. Applying Proposition 8.5.6.19, we deduce that the composition

admits a left homotopy inverse. The restriction map $\operatorname{Fun}( \operatorname{N}_{\bullet }( \operatorname{Ret}), \operatorname{\mathcal{C}}' ) \rightarrow \operatorname{Fun}( \operatorname{N}_{\bullet }( \operatorname{Idem}), \operatorname{\mathcal{C}}' )$ is an equivalence of $\infty $-categories (Remark 8.5.4.8), so $R'$ admits a left homotopy inverse $S': \operatorname{End}_{\operatorname{\mathcal{C}}'}^{\mathrm{idm}} \rightarrow \operatorname{Fun}( \operatorname{N}_{\bullet }( \operatorname{Idem}), \operatorname{\mathcal{C}}' )$. Restricting to the full subcategory $\operatorname{End}_{\operatorname{\mathcal{C}}}^{\mathrm{idm}} \subseteq \operatorname{End}_{\operatorname{\mathcal{C}}'}^{\mathrm{idm}}$, we obtain a functor $S: \operatorname{End}_{\operatorname{\mathcal{C}}}^{\mathrm{idm}} \rightarrow \operatorname{Fun}( \operatorname{N}_{\bullet }( \operatorname{Idem}), \operatorname{\mathcal{C}})$ which is left homotopy inverse to $R$. $\square$