mathlib3 documentation

category_theory.idempotents.biproducts

Biproducts in the idempotent completion of a preadditive category #

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

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 ≅ (to_karoubi 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.

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

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

Equations
Instances for category_theory.idempotents.karoubi.complement

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 (to_karoubi C).obj P.X of P.X in the category karoubi C

Equations