Documentation

Mathlib.CategoryTheory.Idempotents.Biproducts

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.

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.Biproducts.bicone_ι_f {C : Type u_1} [Category.{v, u_1} C] [Preadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (F : JKaroubi C) (j : J) :
    ((bicone F) j).f = CategoryStruct.comp (Limits.biproduct.ι (fun (j : J) => (F j).X) j) (Limits.biproduct.map fun (j : J) => (F j).p)
    @[simp]
    theorem CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_pt_X {C : Type u_1} [Category.{v, u_1} C] [Preadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (F : JKaroubi C) :
    (bicone F).pt.X = fun (j : J) => (F j).X
    @[simp]
    theorem CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_π_f {C : Type u_1} [Category.{v, u_1} C] [Preadditive C] [Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (F : JKaroubi C) (j : J) :
    ((bicone F) j).f = CategoryStruct.comp (Limits.biproduct.map fun (j : J) => (F j).p) ((Limits.biproduct.bicone fun (j : J) => (F j).X) j)

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

    Equations
    Instances For
      @[simp]
      theorem CategoryTheory.Idempotents.Karoubi.complement_X {C : Type u_1} [Category.{v, u_1} C] [Preadditive C] (P : Karoubi C) :
      P.complement.X = 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