An ordinary category is idempotent complete, aka Karoubi complete or Cauchy complete , if every idempotent splits. Since the splitting of an idempotent is a limit or colimit of that idempotent, any category with all finite limits or all finite colimits is idempotent complete.
In an (∞,1)-category the idea is the same, except that the notion of idempotent is more complicated. Instead of just requiring that , we need an equivalence , together with higher coherence data saying that, for instance, the two derived equivalences are equivalent, and so on up. In particular, being idempotent is no longer a property of a morphism, but structure on it.
It is still true that a splitting of an idempotent in an -category is a limit or colimit of that idempotent (now regarded as a diagram with all its higher coherence data), but this limit is no longer a finite limit; thus an -category can have all finite limits without being idempotent-complete.
Let denote the simplicial subset of , corresponding to those pairs such that . Let denote the simplicial subset corresponding to those pairs such that the quotient has at most one element.
Let C be an -category, incarnated as a quasi-category.
An idempotent morphism in C is a map of simplicial sets . We will refer to as the -category of idempotents in .
A strong retraction diagram in is a map of simplicial sets . We will refer to as the -category of strong retraction diagrams in .
An idempotent is effective if it extends to a map .
By (Lurie, lemma 22.214.171.124).
is called an idempotent complete if every idempotent is effective.
The following properties generalize those of idempotent-complete 1-categories.
This is HTT, 126.96.36.199.
This is HTT, lemma 188.8.131.52.
We may also ask how idempotent-completeness of is related to that of its homotopy category . An idempotent in is an “incoherent idempotent” in , i.e. a map such that , but without any higher coherence conditions. In this case we have:
However, if is not stable, this is false. The following counterexample in ∞Gpd is constructed in Warning 184.108.40.206 of HA. Let be an injective but non-bijective group homomorphism such that and are conjugate. (One such is obtained by letting be the group of endpoint-fixing homeomorphisms of , with acting as a scaled version of on and the identity on . Then for any such that for .)
Then is homotopic to , hence idempotent in the homotopy category. If it could be lifted to a coherent idempotent, then the colimit of the diagram
would be its splitting, and hence the map would have a section. Passing to fundamental groups, would also have a section; but this is impossible as is injective but not surjective.
However, we do have the following:
(HA Lemma 220.127.116.11) A morphism in an -category is idempotent (i.e. extends to ) if and only if there is a homotopy such that .
In other words, an incoherent idempotent can be fully coherentified as soon as it admits one additional coherence datum.
Section 4.4.5 of
Formalization in homotopy type theory: