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.

source
def CategoryTheory.Idempotents.Karoubi.Biproducts.bicone {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [Finite J] (F : J → CategoryTheory.Idempotents.Karoubi C) :
CategoryTheory.Limits.Bicone F

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

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

    Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Idempotents.Karoubi.complement_X {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (P : CategoryTheory.Idempotents.Karoubi C) :
      P.complement.X = P.X
      source
      @[simp]
      theorem CategoryTheory.Idempotents.Karoubi.complement_p {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (P : CategoryTheory.Idempotents.Karoubi C) :
      P.complement.p = CategoryTheory.CategoryStruct.id P.X - P.p
      source
      instance CategoryTheory.Idempotents.Karoubi.instHasBinaryBiproductComplement {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (P : CategoryTheory.Idempotents.Karoubi C) :
      CategoryTheory.Limits.HasBinaryBiproduct P P.complement
      Equations
      • ⋯ = ⋯
      source
      def CategoryTheory.Idempotents.Karoubi.decomposition {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (P : CategoryTheory.Idempotents.Karoubi C) :
      P ⊞ P.complement ≅ (CategoryTheory.Idempotents.toKaroubi C).obj 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