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 that C is idempotent complete, i.e. all idempotents in C split. Other characterisations of idempotent completeness are given by isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent and isIdempotentComplete_iff_idempotents_have_kernels.
• isIdempotentComplete_of_abelian expresses that abelian categories are idempotent complete.
• isIdempotentComplete_iff_ofEquivalence expresses that if two categories C and D are equivalent, then C is idempotent complete iff D is.
• isIdempotentComplete_iff_opposite expresses that Cᵒᵖ is idempotent complete iff C is.

References

• [Stacks: Karoubian categories] https://stacks.math.columbia.edu/tag/09SF

class CategoryTheory.IsIdempotentComplete (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : Prop

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 composition p = e ≫ i with i ≫ e = 𝟙 _

theorem CategoryTheory.Idempotents.isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : CategoryTheory.IsIdempotentComplete C ↔ ∀ (X : C) (p : X ⟶ X), CategoryTheory.CategoryStruct.comp p p = p → CategoryTheory.Limits.HasEqualizer (CategoryTheory.CategoryStruct.id X) p

A category is idempotent complete iff for all idempotent endomorphisms, the equalizer of the identity and this idempotent exists.

theorem CategoryTheory.Idempotents.idem_of_id_sub_idem {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : C} (p : X ⟶ X) (hp : CategoryTheory.CategoryStruct.comp p p = p) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X - p) (CategoryTheory.CategoryStruct.id X - p) = CategoryTheory.CategoryStruct.id X - p

In a preadditive category, when p : X ⟶ X is idempotent, then 𝟙 X - p is also idempotent.

theorem CategoryTheory.Idempotents.isIdempotentComplete_iff_idempotents_have_kernels (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] : CategoryTheory.IsIdempotentComplete C ↔ ∀ (X : C) (p : X ⟶ X), CategoryTheory.CategoryStruct.comp p p = p → CategoryTheory.Limits.HasKernel p

A preadditive category is pseudoabelian iff all idempotent endomorphisms have a kernel.

@[instance 100]

instance CategoryTheory.Idempotents.isIdempotentComplete_of_abelian (D : Type u_2) [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Abelian D] : CategoryTheory.IsIdempotentComplete D

An abelian category is idempotent complete.

theorem CategoryTheory.Idempotents.split_imp_of_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X X' : C} (φ : X ≅ X') (p : X ⟶ X) (p' : X' ⟶ X') (hpp' : CategoryTheory.CategoryStruct.comp p φ.hom = CategoryTheory.CategoryStruct.comp φ.hom p') (h : ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), CategoryTheory.CategoryStruct.comp i e = CategoryTheory.CategoryStruct.id Y ∧ CategoryTheory.CategoryStruct.comp e i = p) : ∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), CategoryTheory.CategoryStruct.comp i' e' = CategoryTheory.CategoryStruct.id Y' ∧ CategoryTheory.CategoryStruct.comp e' i' = p'

theorem CategoryTheory.Idempotents.split_iff_of_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X X' : C} (φ : X ≅ X') (p : X ⟶ X) (p' : X' ⟶ X') (hpp' : CategoryTheory.CategoryStruct.comp p φ.hom = CategoryTheory.CategoryStruct.comp φ.hom p') : (∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), CategoryTheory.CategoryStruct.comp i e = CategoryTheory.CategoryStruct.id Y ∧ CategoryTheory.CategoryStruct.comp e i = p) ↔ ∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), CategoryTheory.CategoryStruct.comp i' e' = CategoryTheory.CategoryStruct.id Y' ∧ CategoryTheory.CategoryStruct.comp e' i' = p'

theorem CategoryTheory.Idempotents.Equivalence.isIdempotentComplete {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] (ε : C ≌ D) (h : CategoryTheory.IsIdempotentComplete C) : CategoryTheory.IsIdempotentComplete D

theorem CategoryTheory.Idempotents.isIdempotentComplete_iff_of_equivalence {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] (ε : C ≌ D) : CategoryTheory.IsIdempotentComplete C ↔ CategoryTheory.IsIdempotentComplete D

If C and D are equivalent categories, that C is idempotent complete iff D is.

theorem CategoryTheory.Idempotents.isIdempotentComplete_of_isIdempotentComplete_opposite {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (h : CategoryTheory.IsIdempotentComplete Cᵒᵖ) : CategoryTheory.IsIdempotentComplete C

theorem CategoryTheory.Idempotents.isIdempotentComplete_iff_opposite {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] : CategoryTheory.IsIdempotentComplete Cᵒᵖ ↔ CategoryTheory.IsIdempotentComplete C

instance CategoryTheory.Idempotents.instIsIdempotentCompleteOpposite {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.IsIdempotentComplete C] : CategoryTheory.IsIdempotentComplete Cᵒᵖ