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 C
expresses thatC
is idempotent complete, i.e. all idempotents inC
split. Other characterisations of idempotent completeness are given byis_idempotent_complete_iff_has_equalizer_of_id_and_idempotent
andis_idempotent_complete_iff_idempotents_have_kernels
.is_idempotent_complete_of_abelian
expresses that abelian categories are idempotent complete.is_idempotent_complete_iff_of_equivalence
expresses that if two categoriesC
andD
are equivalent, thenC
is idempotent complete iffD
is.is_idempotent_complete_iff_opposite
expresses thatCᵒᵖ
is idempotent complete iffC
is.
References #
- [Stacks: Karoubian categories] https://stacks.math.columbia.edu/tag/09SF
@[class]
- idempotents_split : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → (∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p)
A category is idempotent complete iff all idempotent endomorphisms p
split as a composition p = e ≫ i
with i ≫ e = 𝟙 _
Instances of this typeclass
- category_theory.idempotents.is_idempotent_complete_of_abelian
- category_theory.idempotents.opposite.category_theory.is_idempotent_complete
- category_theory.idempotents.karoubi.category_theory.is_idempotent_complete
- category_theory.idempotents.functor_category_is_idempotent_complete
- category_theory.idempotents.category_theory.simplicial_object.category_theory.is_idempotent_complete
- category_theory.idempotents.category_theory.cosimplicial_object.category_theory.is_idempotent_complete
- category_theory.idempotents.homological_complex.category_theory.is_idempotent_complete
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 idempotent endomorphisms, the equalizer of the identity and this idempotent exists.
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.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]