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
- category_theory.idempotents.karoubi.biproducts.bicone F = {X := {X := ⨁ λ (j : J), (F j).X, p := category_theory.limits.biproduct.map (λ (j : J), (F j).p), idem := _}, π := λ (j : J), {f := category_theory.limits.biproduct.map (λ (j : J), (F j).p) ≫ (category_theory.limits.biproduct.bicone (λ (j : J), (F j).X)).π j, comm := _}, ι := λ (j : J), {f := (category_theory.limits.biproduct.bicone (λ (j : J), (F j).X)).ι j ≫ category_theory.limits.biproduct.map (λ (j : J), (F j).p), comm := _}, ι_π := _}
P.complement is the formal direct factor of P.X given by the idempotent
endomorphism 𝟙 P.X - P.p
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