# mathlib3documentation

category_theory.idempotents.basic

# Idempotent complete categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 that C is idempotent complete, i.e. all idempotents in C split. Other characterisations of idempotent completeness are given by is_idempotent_complete_iff_has_equalizer_of_id_and_idempotent and is_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 categories C and D are equivalent, then C is idempotent complete iff D is.
• is_idempotent_complete_iff_opposite expresses that Cᵒᵖ is idempotent complete iff C is.

## References #

@[class]
structure category_theory.is_idempotent_complete (C : Type u_1)  :
Prop

A category is idempotent complete iff all idempotent endomorphisms p split as a composition p = e ≫ i with i ≫ e = 𝟙 _

Instances of this typeclass

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

theorem category_theory.idempotents.idem_of_id_sub_idem {C : Type u_1} {X : C} (p : X X) (hp : p p = p) :
(𝟙 X - p) (𝟙 X - p) = 𝟙 X - p

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.

@[protected, instance]

An abelian category is idempotent complete.

theorem category_theory.idempotents.split_imp_of_iso {C : Type u_1} {X X' : C} (φ : X X') (p : X X) (p' : X' X') (hpp' : p φ.hom = φ.hom p') (h : (Y : C) (i : Y X) (e : X Y), i e = 𝟙 Y e i = p) :
(Y' : C) (i' : Y' X') (e' : X' Y'), i' e' = 𝟙 Y' e' i' = p'
theorem category_theory.idempotents.split_iff_of_iso {C : Type u_1} {X X' : C} (φ : X X') (p : X X) (p' : X' X') (hpp' : p φ.hom = φ.hom p') :
( (Y : C) (i : Y X) (e : X Y), i e = 𝟙 Y e i = p) (Y' : C) (i' : Y' X') (e' : X' Y'), i' e' = 𝟙 Y' e' i' = p'

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

@[protected, instance]