# mathlib3documentation

category_theory.idempotents.karoubi

# The Karoubi envelope of a category #

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

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.
• to_karoubi C : C ⥤ karoubi C is a fully faithful functor, which is an equivalence (to_karoubi_is_equivalence) when C is idempotent complete.
@[nolint]
structure category_theory.idempotents.karoubi (C : Type u_1)  :
Type (max u_1 u_2)
• X : C
• p : self.X self.X
• idem : self.p self.p = self.p

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 enveloppe of C. It makes sense for any category C.

Instances for category_theory.idempotents.karoubi
@[simp]
theorem category_theory.idempotents.karoubi.idem_assoc {C : Type u_1} (self : category_theory.idempotents.karoubi C) {X' : C} (f' : self.X X') :
self.p self.p f' = self.p f'
@[ext]
theorem category_theory.idempotents.karoubi.ext {C : Type u_1} (h_X : P.X = Q.X) (h_p : = ) :
P = Q
theorem category_theory.idempotents.karoubi.hom.ext {C : Type u_1} {_inst_1 : category_theory.category C} (x y : P.hom Q) (h : x.f = y.f) :
x = y
theorem category_theory.idempotents.karoubi.hom.ext_iff {C : Type u_1} {_inst_1 : category_theory.category C} (x y : P.hom Q) :
x = y x.f = y.f
@[ext]
structure category_theory.idempotents.karoubi.hom {C : Type u_1}  :
Type u_2

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 category_theory.idempotents.karoubi.hom
@[protected, instance]
Equations
@[simp]
theorem category_theory.idempotents.karoubi.hom_ext {C : Type u_1} {f g : P.hom Q} :
f = g f.f = g.f
@[simp]
theorem category_theory.idempotents.karoubi.p_comp {C : Type u_1} (f : P.hom Q) :
P.p f.f = f.f
@[simp]
theorem category_theory.idempotents.karoubi.p_comp_assoc {C : Type u_1} (f : P.hom Q) {X' : C} (f' : Q.X X') :
P.p f.f f' = f.f f'
@[simp]
theorem category_theory.idempotents.karoubi.comp_p {C : Type u_1} (f : P.hom Q) :
f.f Q.p = f.f
@[simp]
theorem category_theory.idempotents.karoubi.comp_p_assoc {C : Type u_1} (f : P.hom Q) {X' : C} (f' : Q.X X') :
f.f Q.p f' = f.f f'
theorem category_theory.idempotents.karoubi.p_comm {C : Type u_1} (f : P.hom Q) :
P.p f.f = f.f Q.p
theorem category_theory.idempotents.karoubi.comp_proof {C : Type u_1} {P Q R : category_theory.idempotents.karoubi C} (g : Q.hom R) (f : P.hom Q) :
f.f g.f = P.p (f.f g.f) R.p
@[protected, instance]

The category structure on the karoubi envelope of a category.

Equations
@[simp]
theorem category_theory.idempotents.karoubi.comp_f {C : Type u_1} {P Q R : category_theory.idempotents.karoubi C} (f : P Q) (g : Q R) :
(f g).f = f.f g.f
@[simp]
theorem category_theory.idempotents.karoubi.id_eq {C : Type u_1}  :
𝟙 P = {f := P.p, comm := _}
@[protected, instance]

It is possible to coerce an object of C into an object of karoubi C. See also the functor to_karoubi.

Equations
@[simp]
theorem category_theory.idempotents.karoubi.coe_X {C : Type u_1} (X : C) :
X.X = X
@[simp]
theorem category_theory.idempotents.karoubi.coe_p {C : Type u_1} (X : C) :
X.p = 𝟙 X
@[simp]
theorem category_theory.idempotents.karoubi.eq_to_hom_f {C : Type u_1} (h : P = Q) :
@[simp]
theorem category_theory.idempotents.to_karoubi_map_f (C : Type u_1) (X Y : C) (f : X Y) :
= f

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

Equations
Instances for category_theory.idempotents.to_karoubi
@[simp]
theorem category_theory.idempotents.to_karoubi_obj_X (C : Type u_1) (X : C) :
= X
@[simp]
theorem category_theory.idempotents.to_karoubi_obj_p (C : Type u_1) (X : C) :
= 𝟙 X
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[simp]
theorem category_theory.idempotents.quiver.hom.add_comm_group_sub {C : Type u_1} (ᾰ ᾰ_1 : P Q) :
- ᾰ_1 = add_group.sub._default (λ (f g : P Q), {f := f.f + g.f, comm := _}) category_theory.idempotents.quiver.hom.add_comm_group._proof_11 {f := 0, comm := _} category_theory.idempotents.quiver.hom.add_comm_group._proof_12 category_theory.idempotents.quiver.hom.add_comm_group._proof_13 (add_group.nsmul._default {f := 0, comm := _} (λ (f g : P Q), {f := f.f + g.f, comm := _}) category_theory.idempotents.quiver.hom.add_comm_group._proof_6 category_theory.idempotents.quiver.hom.add_comm_group._proof_7) category_theory.idempotents.quiver.hom.add_comm_group._proof_14 category_theory.idempotents.quiver.hom.add_comm_group._proof_15 (λ (f : P Q), {f := -f.f, comm := _}) ᾰ_1
@[simp]
theorem category_theory.idempotents.quiver.hom.add_comm_group_zsmul {C : Type u_1} (ᾰ : ) (ᾰ_1 : P Q) :
ᾰ_1 = add_group.zsmul._default (λ (f g : P Q), {f := f.f + g.f, comm := _}) category_theory.idempotents.quiver.hom.add_comm_group._proof_17 {f := 0, comm := _} category_theory.idempotents.quiver.hom.add_comm_group._proof_18 category_theory.idempotents.quiver.hom.add_comm_group._proof_19 (add_group.nsmul._default {f := 0, comm := _} (λ (f g : P Q), {f := f.f + g.f, comm := _}) category_theory.idempotents.quiver.hom.add_comm_group._proof_6 category_theory.idempotents.quiver.hom.add_comm_group._proof_7) category_theory.idempotents.quiver.hom.add_comm_group._proof_20 category_theory.idempotents.quiver.hom.add_comm_group._proof_21 (λ (f : P Q), {f := -f.f, comm := _}) ᾰ_1
@[simp]
theorem category_theory.idempotents.quiver.hom.add_comm_group_add_f {C : Type u_1} (f g : P Q) :
(f + g).f = f.f + g.f
@[simp]
theorem category_theory.idempotents.quiver.hom.add_comm_group_nsmul {C : Type u_1} (ᾰ : ) (ᾰ_1 : P Q) :
ᾰ_1 = add_group.nsmul._default {f := 0, comm := _} (λ (f g : P Q), {f := f.f + g.f, comm := _}) category_theory.idempotents.quiver.hom.add_comm_group._proof_6 category_theory.idempotents.quiver.hom.add_comm_group._proof_7 ᾰ_1
@[simp]
theorem category_theory.idempotents.karoubi.hom_eq_zero_iff {C : Type u_1} {f : P.hom Q} :
f = 0 f.f = 0

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

Equations
@[simp]
theorem category_theory.idempotents.karoubi.sum_hom {C : Type u_1} {α : Type u_3} (s : finset α) (f : α (P Q)) :
(s.sum (λ (x : α), f x)).f = s.sum (λ (x : α), (f x).f)
@[protected, instance]

The category karoubi C is preadditive if C is.

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]

If C is idempotent complete, the functor to_karoubi : C ⥤ karoubi C is an equivalence.

Equations

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

Equations
@[protected, instance]

The split mono which appears in the factorisation decomp_id P.

Equations

The split epi which appears in the factorisation decomp_id P.

Equations

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 category_theory.idempotents.karoubi.zsmul_hom {C : Type u_1} (n : ) (f : P Q) :
(n f).f = n f.f