# Biproducts in the idempotent completion of a preadditive category #

In this file, we define an instance expressing that if C is an additive category (i.e. is preadditive and has finite biproducts), then Karoubi C is also an additive category.

We also obtain that for all P : Karoubi C where C is a preadditive category C, there is a canonical isomorphism P ⊞ P.complement ≅ (toKaroubi C).obj P.X in the category Karoubi C where P.complement is the formal direct factor of P.X corresponding to the idempotent endomorphism 𝟙 P.X - P.p.

@[simp]
theorem CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_pt_X {C : Type u_1} [] {J : Type} [] (F : ) :
= fun (j : J) => (F j).X
@[simp]

The Bicone used in order to obtain the existence of the biproduct of a functor J ⥤ Karoubi C when the category C is additive.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.complement_X {C : Type u_1} [] :
P.complement.X = P.X
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.complement_p {C : Type u_1} [] :
P.complement.p =

P.complement is the formal direct factor of P.X given by the idempotent endomorphism 𝟙 P.X - P.p

Equations
• P.complement = { X := P.X, p := , idem := }
Instances For
def CategoryTheory.Idempotents.Karoubi.decomposition {C : Type u_1} [] :
P P.complement P.X

A formal direct factor P : Karoubi C of an object P.X : C in a preadditive category is actually a direct factor of the image (toKaroubi C).obj P.X of P.X in the category Karoubi C

Equations
• One or more equations did not get rendered due to their size.
Instances For