Documentation

TauCeti.CategoryTheory.Products.Preadditive

Products of preadditive categories #

This file equips product categories with componentwise binary biproducts and, when the factors are preadditive, a componentwise preadditive structure and additive projection and product functors. These constructions let additive invariants, including split Grothendieck groups, compare a product category with its factors. Every object of such a product is the biproduct of its two zero-padded components (CategoryTheory.prod.biprodComponentsIso).

source
@[instance_reducible]
instance TauCeti.instPreadditiveProd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] :
CategoryTheory.Preadditive (C × D)

The componentwise preadditive structure on a product category.

Equations
  • One or more equations did not get rendered due to their size.
source
instance TauCeti.instHasBinaryBiproductsProd_tauCeti {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts D] :
CategoryTheory.Limits.HasBinaryBiproducts (C × D)

Binary biproducts in a product category are computed componentwise.

source
instance TauCeti.instAdditiveProdFst_tauCeti {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] :
(CategoryTheory.Prod.fst C D).Additive

The first projection from a product of preadditive categories is additive.

source
instance TauCeti.instAdditiveProdSnd_tauCeti {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] :
(CategoryTheory.Prod.snd C D).Additive

The second projection from a product of preadditive categories is additive.

source
instance TauCeti.instAdditiveProdSectLOfNat_tauCeti {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] :
(CategoryTheory.Prod.sectL C 0).Additive

Inserting a zero object in the second coordinate is an additive functor.

source
instance TauCeti.instAdditiveProdSectROfNat_tauCeti {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] :
(CategoryTheory.Prod.sectR 0 D).Additive

Inserting a zero object in the first coordinate is an additive functor.

source
instance TauCeti.instAdditiveProdProd_tauCeti {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] {C' : Type u_1} [CategoryTheory.Category.{v_1, u_1} C'] [CategoryTheory.Preadditive C'] {D' : Type u_2} [CategoryTheory.Category.{v_2, u_2} D'] [CategoryTheory.Preadditive D'] (F : CategoryTheory.Functor C C') (G : CategoryTheory.Functor D D') [F.Additive] [G.Additive] :
(F.prod G).Additive

The product of two additive functors is additive.

source
noncomputable def CategoryTheory.prod.biprodComponentsIso {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasBinaryBiproducts C] [Limits.HasBinaryBiproducts D] (X : C × D) :
(X.1, 0) ⊞ (0, X.2) ≅ X

An object of a product of categories with zero morphisms and zero objects is the biproduct of its two components, each padded by a zero object in the other coordinate.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.prod.biprodComponentsIso_hom {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasBinaryBiproducts C] [Limits.HasBinaryBiproducts D] (X : C × D) :
    (biprodComponentsIso X).hom = Limits.biprod.desc (CategoryStruct.id X.1, 0) (0, CategoryStruct.id X.2)

    The forward map of biprodComponentsIso is induced by the two coordinate inclusions.

    source
    @[simp]
    theorem CategoryTheory.prod.biprodComponentsIso_inv {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasBinaryBiproducts C] [Limits.HasBinaryBiproducts D] (X : C × D) :
    (biprodComponentsIso X).inv = Limits.biprod.lift (CategoryStruct.id X.1, 0) (0, CategoryStruct.id X.2)

    The inverse of biprodComponentsIso is induced by the two coordinate projections.