Idempotent complete categories #
In this file, we define the notion of idempotent complete categories (also known as Karoubian categories, or pseudoabelian in the case of preadditive categories).
Main definitions #
IsIdempotentComplete C
expresses thatC
is idempotent complete, i.e. all idempotents inC
split. Other characterisations of idempotent completeness are given byisIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent
andisIdempotentComplete_iff_idempotents_have_kernels
.isIdempotentComplete_of_abelian
expresses that abelian categories are idempotent complete.isIdempotentComplete_iff_ofEquivalence
expresses that if two categoriesC
andD
are equivalent, thenC
is idempotent complete iffD
is.isIdempotentComplete_iff_opposite
expresses thatCᵒᵖ
is idempotent complete iffC
is.
References #
- [Stacks: Karoubian categories] https://stacks.math.columbia.edu/tag/09SF
A category is idempotent complete iff all idempotent endomorphisms p
split as a composition p = e ≫ i
with i ≫ e = 𝟙 _
- idempotents_split : ∀ (X : C) (p : X ⟶ X), CategoryTheory.CategoryStruct.comp p p = p → ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), CategoryTheory.CategoryStruct.comp i e = CategoryTheory.CategoryStruct.id Y ∧ CategoryTheory.CategoryStruct.comp e i = p
A category is idempotent complete iff all idempotent endomorphisms
p
split as a compositionp = e ≫ i
withi ≫ e = 𝟙 _
Instances
A category is idempotent complete iff for all idempotent endomorphisms, the equalizer of the identity and this idempotent exists.
In a preadditive category, when p : X ⟶ X
is idempotent,
then 𝟙 X - p
is also idempotent.
A preadditive category is pseudoabelian iff all idempotent endomorphisms have a kernel.
An abelian category is idempotent complete.
If C
and D
are equivalent categories, that C
is idempotent complete iff D
is.