mathlib3 documentation

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 #

References #

source
@[class]
structure category_theory.is_idempotent_complete (C : Type u_1) [category_theory.category C] :
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
source
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.

source
theorem category_theory.idempotents.idem_of_id_sub_idem {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {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.

source
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.

source
@[protected, instance]
def category_theory.idempotents.is_idempotent_complete_of_abelian (D : Type u_1) [category_theory.category D] [category_theory.abelian D] :
category_theory.is_idempotent_complete D

An abelian category is idempotent complete.

source
theorem category_theory.idempotents.split_imp_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') (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'
source
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') :
(∃ (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'
source
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) :
category_theory.is_idempotent_complete D
source
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) :
category_theory.is_idempotent_complete C ↔ category_theory.is_idempotent_complete D

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

source
theorem category_theory.idempotents.is_idempotent_complete_of_is_idempotent_complete_opposite {C : Type u_1} [category_theory.category C] (h : category_theory.is_idempotent_complete Cᵒᵖ) :
category_theory.is_idempotent_complete C
source
theorem category_theory.idempotents.is_idempotent_complete_iff_opposite {C : Type u_1} [category_theory.category C] :
category_theory.is_idempotent_complete Cᵒᵖ ↔ category_theory.is_idempotent_complete C
source
@[protected, instance]
def category_theory.idempotents.opposite.category_theory.is_idempotent_complete {C : Type u_1} [category_theory.category C] [category_theory.is_idempotent_complete C] :
category_theory.is_idempotent_complete Cᵒᵖ