# Documentation

Mathlib.CategoryTheory.Idempotents.Karoubi

# The Karoubi envelope of a category #

In this file, we define the Karoubi envelope Karoubi C of a category C.

## Main constructions and definitions #

• Karoubi C is the Karoubi envelope of a category C: it is an idempotent complete category. It is also preadditive when C is preadditive.
• toKaroubi C : C ⥤ Karoubi C is a fully faithful functor, which is an equivalence (toKaroubiIsEquivalence) when C is idempotent complete.
structure CategoryTheory.Idempotents.Karoubi (C : Type u_1) [] :
Type (max u_1 u_2)
• X : C

an object of the underlying category

• p : s.X s.X

an endomorphism of the object

• idem : = s.p

the condition that the given endomorphism is an idempotent

In a preadditive category C, when an object X decomposes as X ≅ P ⨿ Q, one may consider P as a direct factor of X and up to unique isomorphism, it is determined by the obvious idempotent X ⟶ P ⟶ X which is the projection onto P with kernel Q. More generally, one may define a formal direct factor of an object X : C : it consists of an idempotent p : X ⟶ X which is thought as the "formal image" of p. The type Karoubi C shall be the type of the objects of the karoubi envelope of C. It makes sense for any category C.

Instances For
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.idem_assoc {C : Type u_1} [] (self : ) {Z : C} (h : self.X Z) :
theorem CategoryTheory.Idempotents.Karoubi.ext {C : Type u_1} [] (h_X : P.X = Q.X) (h_p : ) :
P = Q
theorem CategoryTheory.Idempotents.Karoubi.Hom.ext {C : Type u_1} :
∀ {inst : } {P Q : } (x y : ), x.f = y.fx = y
theorem CategoryTheory.Idempotents.Karoubi.Hom.ext_iff {C : Type u_1} :
∀ {inst : } {P Q : } (x y : ), x = y x.f = y.f
• f : P.X Q.X

a morphism between the underlying objects

• comm : s.f =

compatibility of the given morphism with the given idempotents

A morphism P ⟶ Q in the category Karoubi C is a morphism in the underlying category C which satisfies a relation, which in the preadditive case, expresses that it induces a map between the corresponding "formal direct factors" and that it vanishes on the complement formal direct factor.

Instances For
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.p_comp_assoc {C : Type u_1} [] {Z : C} (h : Q.X Z) :
@[simp]
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.comp_p_assoc {C : Type u_1} [] {Z : C} (h : Q.X Z) :
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.p_comm_assoc {C : Type u_1} [] {Z : C} (h : Q.X Z) :

The category structure on the karoubi envelope of a category.

@[simp]
theorem CategoryTheory.Idempotents.Karoubi.hom_ext_iff {C : Type u_1} [] {f : P Q} {g : P Q} :
f = g f.f = g.f
theorem CategoryTheory.Idempotents.Karoubi.hom_ext {C : Type u_1} [] (f : P Q) (g : P Q) (h : f.f = g.f) :
f = g
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.comp_f {C : Type u_1} [] (f : P Q) (g : Q R) :
@[simp]

It is possible to coerce an object of C into an object of Karoubi C. See also the functor toKaroubi.

@[simp]
theorem CategoryTheory.Idempotents.Karoubi.coe_p {C : Type u_1} [] (X : C) :
@[simp]
theorem CategoryTheory.Idempotents.toKaroubi_obj_p (C : Type u_1) [] (X : C) :
@[simp]
theorem CategoryTheory.Idempotents.toKaroubi_map_f (C : Type u_1) [] :
∀ {X Y : C} (f : X Y), (().map f).f = f
@[simp]
theorem CategoryTheory.Idempotents.toKaroubi_obj_X (C : Type u_1) [] (X : C) :
(().obj X).X = X

The obvious fully faithful functor toKaroubi sends an object X : C to the obvious formal direct factor of X given by 𝟙 X.

Instances For
@[simp]
@[simp]
@[simp]
theorem CategoryTheory.Idempotents.instAddCommGroupHom_add {C : Type u_1} [] (f : P Q) (g : P Q) :
f + g =
theorem CategoryTheory.Idempotents.Karoubi.hom_eq_zero_iff {C : Type u_1} [] {f : P Q} :
f = 0 f.f = 0
@[simp]

The map sending f : P ⟶ Q to f.f : P.X ⟶ Q.X is additive.

Instances For
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.sum_hom {C : Type u_1} [] {α : Type u_2} (s : ) (f : α → (P Q)) :
(Finset.sum s fun x => f x).f = Finset.sum s fun x => (f x).f

The category Karoubi C is preadditive if C is.

If C is idempotent complete, the functor toKaroubi : C ⥤ Karoubi C is an equivalence.

Instances For

The equivalence C ≅ Karoubi C when C is idempotent complete.

Instances For

The split mono which appears in the factorisation decompId P.

Instances For

The split epi which appears in the factorisation decompId P.

Instances For

The formal direct factor of P.X given by the idempotent P.p in the category C is actually a direct factor in the category Karoubi C.

@[simp]
theorem CategoryTheory.Idempotents.Karoubi.zsmul_hom {C : Type u_1} [] (n : ) (f : P Q) :
(n f).f = n f.f