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.
Section 4.4.5 of
Formalization in homotopy type theory:
Last revised on March 13, 2020 at 02:11:04. See the history of this page for a list of all contributions to it.