# 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)

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 : XX 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.

• X : C

an object of the underlying category

• p : self.X self.X

an endomorphism of the object

• idem : CategoryTheory.CategoryStruct.comp self.p self.p = self.p

the condition that the given endomorphism is an idempotent

Instances For
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.idem {C : Type u_1} [] (self : ) :

the condition that the given endomorphism is an idempotent

@[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_iff {C : Type u_1} :
∀ {inst : } {P Q : } (x y : P.Hom Q), x = y x.f = y.f
theorem CategoryTheory.Idempotents.Karoubi.Hom.ext {C : Type u_1} :
∀ {inst : } {P Q : } (x y : P.Hom Q), x.f = y.fx = y

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.

• f : P.X Q.X

a morphism between the underlying objects

• comm : self.f =

compatibility of the given morphism with the given idempotents

Instances For
theorem CategoryTheory.Idempotents.Karoubi.Hom.comm {C : Type u_1} [] (self : P.Hom Q) :
self.f =

compatibility of the given morphism with the given idempotents

Equations
• P.instInhabitedHomOfPreadditive Q = { default := { f := 0, comm := } }
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.p_comp_assoc {C : Type u_1} [] (f : P.Hom Q) {Z : C} (h : Q.X Z) :
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.p_comp {C : Type u_1} [] (f : P.Hom Q) :
= f.f
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.comp_p_assoc {C : Type u_1} [] (f : P.Hom Q) {Z : C} (h : Q.X Z) :
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.comp_p {C : Type u_1} [] (f : P.Hom Q) :
= f.f
theorem CategoryTheory.Idempotents.Karoubi.p_comm_assoc {C : Type u_1} [] (f : P.Hom Q) {Z : C} (h : Q.X Z) :
theorem CategoryTheory.Idempotents.Karoubi.p_comm {C : Type u_1} [] (f : P.Hom Q) :
theorem CategoryTheory.Idempotents.Karoubi.comp_proof {C : Type u_1} [] (g : Q.Hom R) (f : P.Hom Q) :

The category structure on the karoubi envelope of a category.

Equations
• CategoryTheory.Idempotents.Karoubi.instCategory =
@[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]
theorem CategoryTheory.Idempotents.Karoubi.id_eq {C : Type u_1} [] :
= { f := P.p, comm := }

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

Equations
• CategoryTheory.Idempotents.Karoubi.coe = { coe := fun (X : C) => { X := X, p := , idem := } }
theorem CategoryTheory.Idempotents.Karoubi.coe_X {C : Type u_1} [] (X : C) :
{ X := X, p := , idem := }.X = X
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.coe_p {C : Type u_1} [] (X : C) :
{ X := X, p := , idem := }.p =
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.eqToHom_f {C : Type u_1} [] (h : P = Q) :
@[simp]
theorem CategoryTheory.Idempotents.toKaroubi_obj_X (C : Type u_1) [] (X : C) :
( X).X = X
@[simp]
theorem CategoryTheory.Idempotents.toKaroubi_map_f (C : Type u_1) [] :
∀ {X Y : C} (f : X Y), ( f).f = f
@[simp]
theorem CategoryTheory.Idempotents.toKaroubi_obj_p (C : Type u_1) [] (X : C) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• =
Equations
• =
@[simp]
theorem CategoryTheory.Idempotents.instAdd_add {C : Type u_1} [] (f : P Q) (g : P Q) :
f + g = { f := f.f + g.f, comm := }
instance CategoryTheory.Idempotents.instAdd {C : Type u_1} [] :
Equations
• CategoryTheory.Idempotents.instAdd = { add := fun (f g : P Q) => { f := f.f + g.f, comm := } }
@[simp]
theorem CategoryTheory.Idempotents.instNeg_neg {C : Type u_1} [] (f : P Q) :
-f = { f := -f.f, comm := }
instance CategoryTheory.Idempotents.instNeg {C : Type u_1} [] :
Neg (P Q)
Equations
• CategoryTheory.Idempotents.instNeg = { neg := fun (f : P Q) => { f := -f.f, comm := } }
@[simp]
theorem CategoryTheory.Idempotents.instZero_zero {C : Type u_1} [] :
0 = { f := 0, comm := }
instance CategoryTheory.Idempotents.instZero {C : Type u_1} [] :
Zero (P Q)
Equations
• CategoryTheory.Idempotents.instZero = { zero := { f := 0, comm := } }
Equations
theorem CategoryTheory.Idempotents.Karoubi.hom_eq_zero_iff {C : Type u_1} [] {f : P Q} :
f = 0 f.f = 0
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.inclusionHom_apply {C : Type u_1} [] (f : P Q) :
(P.inclusionHom Q) f = f.f

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

Equations
• P.inclusionHom Q = { toFun := fun (f : P Q) => f.f, map_zero' := , map_add' := }
Instances For
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.sum_hom {C : Type u_1} [] {α : Type u_2} (s : ) (f : α(P Q)) :
(xs, f x).f = xs, (f x).f

The category Karoubi C is preadditive if C is.

Equations
• CategoryTheory.Idempotents.instPreadditiveKaroubi = { homGroup := fun (P Q : ) => inferInstance, add_comp := , comp_add := }
Equations
• =
Equations
• =
Equations
• =
instance CategoryTheory.Idempotents.toKaroubi_isEquivalence (C : Type u_1) [] :
.IsEquivalence

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

Equations
• =

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

Equations
Instances For
Equations
• =
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.decompId_i_f {C : Type u_1} [] :
P.decompId_i.f = P.p
def CategoryTheory.Idempotents.Karoubi.decompId_i {C : Type u_1} [] :
P { X := P.X, p := , idem := }

The split mono which appears in the factorisation decompId P.

Equations
• P.decompId_i = { f := P.p, comm := }
Instances For
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.decompId_p_f {C : Type u_1} [] :
P.decompId_p.f = P.p
def CategoryTheory.Idempotents.Karoubi.decompId_p {C : Type u_1} [] :
{ X := P.X, p := , idem := } P

The split epi which appears in the factorisation decompId P.

Equations
• P.decompId_p = { f := P.p, comm := }
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.

theorem CategoryTheory.Idempotents.Karoubi.decompId_i_toKaroubi {C : Type u_1} [] (X : C) :
( X).decompId_i =
theorem CategoryTheory.Idempotents.Karoubi.decompId_p_toKaroubi {C : Type u_1} [] (X : C) :
( X).decompId_p = CategoryTheory.CategoryStruct.id { X := ( X).X, p := , idem := }
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.zsmul_hom {C : Type u_1} [] (n : ) (f : P Q) :
(n f).f = n f.f