Background
Basic concepts
equivalences in/of -categories
Universal constructions
Local presentation
Theorems
Extra stuff, structure, properties
Models
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 be the nerve of the free 1-category containing a retraction, with the idempotent, the retraction, and the section (and and ). Let be the similar nerve of the free 1-category containing an idempotent, which is the full sub-simplicial set of spanned by the object . Let be the image in of the 2-simplex exhibiting the composite ; thus is also the quotient of that collapses the 1-face to a point.
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 weak retraction diagram in is a homomorphism of simplicial sets . We refer to as the -category of weak retraction diagrams 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 .
(Lurie, above corollary 4.4.5.14)
An idempotent diagram is effective precisely if it admits an (∞,1)-limit, equivalently if it admits an (∞,1)-colimit.
By (Lurie, lemma 4.3.2.13).
is called an idempotent complete if every idempotent is effective.
(Lurie, above corollary 4.4.5.14)
The following properties generalize those of idempotent-complete 1-categories.
A small (∞,1)-category is idempotent-complete if and only if it is accessible.
This is HTT, 5.4.3.6.
For a small (∞,1)-category and a regular cardinal, the (∞,1)-Yoneda embedding with the full subcategory on -compact objects exhibits as the idempotent completion of .
This is HTT, lemma 5.4.2.4.
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:
(HA Lemma 1.2.4.6) If is stable, then is idempotent-complete (i.e. every coherent idempotent is effective) if and only if is (as a 1-category).
However, if is not stable, this is false. The following counterexample in ∞Gpd is constructed in Warning 1.2.4.8 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 7.3.5.14 in older versions, HTT Proposition 4.4.5.20 in newer versions) 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.
However, there may be multiple inequivialent ways of doing so.
Section 4.4.5 of
Formalization in homotopy type theory:
Last revised on June 22, 2023 at 21:49:41. See the history of this page for a list of all contributions to it.