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 #
is_idempotent_complete Cexpresses thatCis idempotent complete, i.e. all idempotents inCsplit. Other caracterisations of idempotent completeness are given byis_idempotent_complete_iff_has_equalizer_of_id_and_idempotentandis_idempotent_complete_iff_idempotents_have_kernels.is_idempotent_complete_of_abelianexpresses that abelian categories are idempotent complete.is_idempotent_complete_iff_of_equivalenceexpresses that if two categoriesCandDare equivalent, thenCis idempotent complete iffDis.is_idempotent_complete_iff_oppositeexpresses thatCᵒᵖis idempotent complete iffCis.
References #
- [Stacks: Karoubian categories] https://stacks.math.columbia.edu/tag/09SF
theorem
category_theory.idempotents.is_idempotent_complete_iff_has_equalizer_of_id_and_idempotent
(C : Type u_1)
[category_theory.category C] :
category_theory.is_idempotent_complete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → category_theory.limits.has_equalizer (𝟙 X) p
A category is idempotent complete iff for all idempotents endomorphisms, the equalizer of the identity and this idempotent exists.
theorem
category_theory.idempotents.idempotence_of_id_sub_idempotent
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : C}
(p : X ⟶ X)
(hp : p ≫ p = p) :
In a preadditive category, when p : X ⟶ X is idempotent,
then 𝟙 X - p is also idempotent.
theorem
category_theory.idempotents.is_idempotent_complete_iff_idempotents_have_kernels
(C : Type u_1)
[category_theory.category C]
[category_theory.preadditive C] :
category_theory.is_idempotent_complete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → category_theory.limits.has_kernel p
A preadditive category is pseudoabelian iff all idempotent endomorphisms have a kernel.
@[protected, instance]
def
category_theory.idempotents.is_idempotent_complete_of_abelian
(D : Type u_1)
[category_theory.category D]
[category_theory.abelian D] :
An abelian category is idempotent complete.
theorem
category_theory.idempotents.split_iff_of_iso
{C : Type u_1}
[category_theory.category C]
{X X' : C}
(φ : X ≅ X')
(p : X ⟶ X)
(p' : X' ⟶ X')
(hpp' : p ≫ φ.hom = φ.hom ≫ p') :
theorem
category_theory.idempotents.equivalence.is_idempotent_complete
{C : Type u_1}
[category_theory.category C]
{D : Type u_3}
[category_theory.category D]
(ε : C ≌ D)
(h : category_theory.is_idempotent_complete C) :
theorem
category_theory.idempotents.is_idempotent_complete_iff_of_equivalence
{C : Type u_1}
[category_theory.category C]
{D : Type u_3}
[category_theory.category D]
(ε : C ≌ D) :
If C and D are equivalent categories, that C is idempotent complete iff D is.
@[protected, instance]