module Cat.Diagram.Biproduct where

Biproducts🔗

Recall that, in an -enriched category, products and coproducts automatically coincide: these are called biproducts and are written

Following (Karvonen 2020), we can define what it means to be a biproduct in a general category: we say that a diagram like the one above is a biproduct diagram if is a product diagram, is a coproduct diagram, and the following equations relating the product projections and coproduct injections hold:

  record is-biproduct {A B P}
    (π₁ : Hom P A) (π₂ : Hom P B)
    (ι₁ : Hom A P) (ι₂ : Hom B P)
    : Type (o  ) where
    field
      has-is-product   : is-product C π₁ π₂
      has-is-coproduct : is-coproduct C ι₁ ι₂
      πι₁ : π₁  ι₁  id
      πι₂ : π₂  ι₂  id
      ιπ-comm : ι₁  π₁  ι₂  π₂  ι₂  π₂  ι₁  π₁

  record Biproduct (A B : Ob) : Type (o  ) where
    field
      biapex : Ob
      π₁ : Hom biapex A
      π₂ : Hom biapex B
      ι₁ : Hom A biapex
      ι₂ : Hom B biapex
      has-is-biproduct : is-biproduct π₁ π₂ ι₁ ι₂

Semiadditive categories🔗

Just like terminal objects (resp. initial objects) are 0-ary products (resp. coproducts), zero objects are 0-ary biproducts. A category with a zero object and binary biproducts (hence all finite biproducts) is called semiadditive.

  record is-semiadditive : Type (o  ) where
    field
      has-zero : Zero C
      has-biproducts :  {A B}  Biproduct A B

As the name hints, every additive category is semiadditive. However, quite surprisingly, it turns out that the structure1 of a semiadditive category is already enough to define an enrichment of in commutative monoids!

We define the addition of morphisms by the following diagram, where (resp. is the diagonal map (resp. codiagonal map).

    _+→_ :  {x y}  Hom x y  Hom x y  Hom x y
    f +→ g =   (f ⊗₁ g)  δ

We start by noticing a few properties of finite biproducts. First, while we are of course justified in writing without ambiguity for objects, we must prove that so that we can write without ambiguity for morphisms.

To that end, we start by showing that and are zero morphisms.

    π₁-ι₂ :  {a b}  π₁ {a} {b}  ι₂  zero→
    π₂-ι₁ :  {a b}  π₂ {a} {b}  ι₁  zero→
The proofs follow (Karvonen 2020) and are unenlightening.
    π₁-ι₂ = zero-unique λ f g 
      let h =  π₁  ι₂  g , f  in
      (π₁  ι₂)  f                   ≡⟨ insertl πι₁ 
      π₁  ι₁  (π₁  ι₂)  f         ≡˘⟨ refl⟩∘⟨ refl⟩∘⟨ assoc _ _ _  (refl⟩∘⟨ π₂∘⟨⟩) ≡˘
      π₁  ι₁  π₁  ι₂  π₂  h      ≡⟨ refl⟩∘⟨ pulll4 ιπ-comm 
      π₁  (ι₂  π₂  ι₁  π₁)  h    ≡⟨ refl⟩∘⟨ pullr (pullr (pullr π₁∘⟨⟩)) 
      π₁  ι₂  π₂  ι₁  π₁  ι₂  g ≡˘⟨ refl⟩∘⟨ extendl4 ιπ-comm ≡˘
      π₁  ι₁  π₁  ι₂  π₂  ι₂  g ≡⟨ cancell πι₁ 
      π₁  ι₂  π₂  ι₂  g           ≡⟨ pushr (refl⟩∘⟨ cancell πι₂) 
      (π₁  ι₂)  g                   

    π₂-ι₁ = zero-unique λ f g 
      let h =  f , π₂  ι₁  g  in
      (π₂  ι₁)  f                   ≡⟨ insertl πι₂ 
      π₂  ι₂  (π₂  ι₁)  f         ≡˘⟨ refl⟩∘⟨ refl⟩∘⟨ assoc _ _ _  (refl⟩∘⟨ π₁∘⟨⟩) ≡˘
      π₂  ι₂  π₂  ι₁  π₁  h      ≡˘⟨ refl⟩∘⟨ pushl4 ιπ-comm ≡˘
      π₂  (ι₁  π₁  ι₂  π₂)  h    ≡⟨ refl⟩∘⟨ pullr (pullr (pullr π₂∘⟨⟩)) 
      π₂  ι₁  π₁  ι₂  π₂  ι₁  g ≡⟨ refl⟩∘⟨ extendl4 ιπ-comm 
      π₂  ι₂  π₂  ι₁  π₁  ι₁  g ≡⟨ cancell πι₂ 
      π₂  ι₁  π₁  ι₁  g           ≡⟨ pushr (refl⟩∘⟨ cancell πι₁) 
      (π₂  ι₁)  g                   

Next, we note that maps are uniquely determined, thanks to the universal properties of the product and coproduct, by the four components for In other words, admits a unique matrix representation

    unique-matrix
      :  {a b c d} {f g : Hom (a ⊕₀ b) (c ⊕₀ d)}
       (π₁  f  ι₁  π₁  g  ι₁)
       (π₂  f  ι₁  π₂  g  ι₁)
       (π₁  f  ι₂  π₁  g  ι₂)
       (π₂  f  ι₂  π₂  g  ι₂)
       f  g
    unique-matrix p₁₁ p₁₂ p₂₁ p₂₂ = Biprod.[]-unique₂
      (Biprod.⟨⟩-unique₂ p₁₁ p₁₂ refl refl)
      (Biprod.⟨⟩-unique₂ p₂₁ p₂₂ refl refl)
      refl refl

This implies that and are equal, as they both have the same matrix representation:

    ⊕₁≡⊗₁ :  {a b c d} {f : Hom a b} {g : Hom c d}  f ⊕₁ g  f ⊗₁ g
    ⊕₁≡⊗₁ = unique-matrix
      ((refl⟩∘⟨ []∘ι₁)  cancell πι₁  sym (pulll π₁∘⟨⟩  cancelr πι₁))
      ((refl⟩∘⟨ []∘ι₁)  pulll π₂-ι₁  zero-∘r _  sym (pulll π₂∘⟨⟩  pullr π₂-ι₁  zero-∘l _))
      ((refl⟩∘⟨ []∘ι₂)  pulll π₁-ι₂  zero-∘r _  sym (pulll π₁∘⟨⟩  pullr π₁-ι₂  zero-∘l _))
      ((refl⟩∘⟨ []∘ι₂)  cancell πι₂  sym (pulll π₂∘⟨⟩  cancelr πι₂))

Similarly, we show that the associators and braidings for products and coproducts coincide.

    coassoc≡assoc :  {a b c}  ⊕-assoc {a} {b} {c}  ×-assoc
    coswap≡swap :  {a b}  coswap {a} {b}  swap
    coassoc≡assoc = unique-matrix
      ((refl⟩∘⟨ []∘ι₁)  cancell πι₁  sym (pulll π₁∘⟨⟩  Biprod.⟨⟩-unique₂
        (pulll π₁∘⟨⟩  πι₁)
        (pulll π₂∘⟨⟩  pullr π₂-ι₁  zero-∘l _)
        πι₁ π₂-ι₁))
      ((refl⟩∘⟨ []∘ι₁)  pulll π₂-ι₁  zero-∘r _  sym (pulll π₂∘⟨⟩  pullr π₂-ι₁  zero-∘l _))
      ((refl⟩∘⟨ []∘ι₂)  unique-matrix
        ((refl⟩∘⟨ pullr []∘ι₁  cancell πι₁)  π₁-ι₂  sym (pulll (pulll π₁∘⟨⟩)  (π₁-ι₂ ⟩∘⟨refl)  zero-∘r _))
        ((refl⟩∘⟨ pullr []∘ι₁  cancell πι₁)  πι₂  sym (pulll (pulll π₂∘⟨⟩)  (cancelr πι₂ ⟩∘⟨refl)  πι₁))
        ((refl⟩∘⟨ pullr []∘ι₂  π₁-ι₂)  zero-∘l _  sym (pulll (pulll π₁∘⟨⟩)  (π₁-ι₂ ⟩∘⟨refl)  zero-∘r _))
        ((refl⟩∘⟨ pullr []∘ι₂  π₁-ι₂)  zero-∘l _  sym (pulll (pulll π₂∘⟨⟩)  (cancelr πι₂ ⟩∘⟨refl)  π₁-ι₂))
       sym (pulll π₁∘⟨⟩))
      ((refl⟩∘⟨ []∘ι₂)  Biprod.[]-unique₂
        (pullr []∘ι₁  pulll π₂-ι₁  zero-∘r _)
        (pullr []∘ι₂  πι₂)
        ((cancelr πι₂ ⟩∘⟨refl)  π₂-ι₁)
        ((cancelr πι₂ ⟩∘⟨refl)  πι₂)
       sym (pulll π₂∘⟨⟩))

    coswap≡swap = ⟨⟩-unique
      (Biprod.[]-unique₂
        (pullr []∘ι₁  π₁-ι₂) (pullr []∘ι₂  πι₁)
        π₂-ι₁ πι₂)
      (Biprod.[]-unique₂
        (pullr []∘ι₁  πι₂) (pullr []∘ι₂  π₂-ι₁)
        πι₁ π₁-ι₂)

We are finally ready to show that addition of morphisms is associative, commutative and unital. These properties essentially follow from the corresponding properties of biproducts. For associativity, we use the following diagram:

    +-assoc :  {x y} {f g h : Hom x y}  f +→ (g +→ h)  (f +→ g) +→ h
    +-assoc {f = f} {g} {h} =
        (f ⊗₁ (  (g ⊗₁ h)  δ))  δ                           ≡˘⟨ refl⟩∘⟨ ⊗.pulll3 (idl _  idr _ ,ₚ refl) 
        (id ⊗₁ )  (f ⊗₁ (g ⊗₁ h))  (id ⊗₁ δ)  δ             ≡˘⟨ refl⟩∘⟨ ⊕₁≡⊗₁ ⟩∘⟨refl 
        (id ⊕₁ )  (f ⊗₁ (g ⊗₁ h))  (id ⊗₁ δ)  δ             ≡˘⟨ pushl ∇-assoc 
      (  ( ⊕₁ id)  ⊕-assoc)  (f ⊗₁ (g ⊗₁ h))  (id ⊗₁ δ)  δ ≡⟨ (refl⟩∘⟨ ⊕₁≡⊗₁ ⟩∘⟨refl) ⟩∘⟨refl 
      (  ( ⊗₁ id)  ⊕-assoc)  (f ⊗₁ (g ⊗₁ h))  (id ⊗₁ δ)  δ ≡⟨ pullr (pullr (coassoc≡assoc ⟩∘⟨refl)) 
        ( ⊗₁ id)  ×-assoc  (f ⊗₁ (g ⊗₁ h))  (id ⊗₁ δ)  δ   ≡⟨ refl⟩∘⟨ refl⟩∘⟨ extendl (associator .Isoⁿ.from .is-natural _ _ _) 
        ( ⊗₁ id)  ((f ⊗₁ g) ⊗₁ h)  ×-assoc  (id ⊗₁ δ)  δ   ≡⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ assoc-δ 
        ( ⊗₁ id)  ((f ⊗₁ g) ⊗₁ h)  (δ ⊗₁ id)  δ             ≡⟨ refl⟩∘⟨ ⊗.pulll3 (refl ,ₚ idl _  idr _) 
        ((  (f ⊗₁ g)  δ) ⊗₁ h)  δ                           

Commutativity follows from the following diagram, where is the braiding:

    +-comm :  {x y} {f g : Hom x y}  f +→ g  g +→ f
    +-comm {f = f} {g} =
        (f ⊗₁ g)  δ          ≡˘⟨ pulll ∇-coswap 
        coswap  (f ⊗₁ g)  δ ≡⟨ refl⟩∘⟨ coswap≡swap ⟩∘⟨refl 
        swap  (f ⊗₁ g)  δ   ≡˘⟨ refl⟩∘⟨ extendl (swap-natural _) 
        (g ⊗₁ f)  swap  δ   ≡⟨ refl⟩∘⟨ refl⟩∘⟨ swap-δ 
        (g ⊗₁ f)  δ          

Since addition is commutative, it suffices to show that the zero morphism is a left unit. We again use the analogous property of biproducts, which is that the zero object is a left unit for

    ∇-¡l :  {a}   {a}  (¡ ⊕₁ id)  π₂
    ∇-¡l = Biprod.[]-unique₂
      (¡-unique₂ _ _) (pullr []∘ι₂  cancell []∘ι₂)
      refl πι₂

    +-idl :  {x y} {f : Hom x y}  zero→ +→ f  f
    +-idl {f = f} =
        (zero→ ⊗₁ f)  δ         ≡⟨ refl⟩∘⟨ ⊗.pushl (refl ,ₚ sym (idl _)) 
        (¡ ⊗₁ id)  (! ⊗₁ f)  δ ≡˘⟨ refl⟩∘⟨ ⊕₁≡⊗₁ ⟩∘⟨refl 
        (¡ ⊕₁ id)  (! ⊗₁ f)  δ ≡⟨ pulll ∇-¡l 
      π₂  (! ⊗₁ f)  δ            ≡⟨ pulll π₂∘⟨⟩ 
      (f  π₂)  δ                 ≡⟨ cancelr π₂∘⟨⟩ 
      f                            

    +-idr :  {x y} {f : Hom x y}  f +→ zero→  f
    +-idr = +-comm  +-idl

Naturality of the (co)diagonals implies that composition is bilinear with respect to our defined addition.

    ∘-linear-l
      :  {a b c} {f g : Hom b c} {h : Hom a b}
       f  h +→ g  h  (f +→ g)  h
    ∘-linear-l {f = f} {g} {h} =
        ((f  h) ⊗₁ (g  h))  δ ≡⟨ refl⟩∘⟨ ⊗.pushl refl 
        (f ⊗₁ g)  (h ⊗₁ h)  δ  ≡˘⟨ pullr (pullr (δ-natural _ _ _)) 
      (  (f ⊗₁ g)  δ)  h       

    ∘-linear-r
      :  {a b c} {f g : Hom a b} {h : Hom b c}
       h  f +→ h  g  h  (f +→ g)
    ∘-linear-r {f = f} {g} {h} =
        ((h  f) ⊗₁ (h  g))  δ ≡⟨ refl⟩∘⟨ ⊗.pushl refl 
        (h ⊗₁ h)  (f ⊗₁ g)  δ  ≡˘⟨ refl⟩∘⟨ ⊕₁≡⊗₁ ⟩∘⟨refl 
        (h ⊕₁ h)  (f ⊗₁ g)  δ  ≡⟨ extendl (∇-natural _ _ _) 
      h    (f ⊗₁ g)  δ         

This provides an alternative route to defining additive categories: instead of starting with an -enriched category and requiring finite (co)products, we can start with a semiadditive category and require that every be a group.

In order to construct a semiadditive category from a category with a zero object, binary products and coproducts, it suffices to require that the map defined by the matrix representation

is invertible.

  record make-semiadditive : Type (o  ) where
    field
      has-zero : Zero C
      has-coprods :  a b  Coproduct C a b
      has-prods :  a b  Product C a b

    open Zero has-zero
    open Binary-products C has-prods
    open Binary-coproducts C has-coprods

    coproduct→product :  {a b}  Hom (a ⊕₀ b) (a ⊗₀ b)
    coproduct→product =  [ id , zero→ ]
                        , [ zero→ , id ] 

    field
      coproduct≅product :  {a b}  is-invertible (coproduct→product {a} {b})

If that is the case, then the coproduct is a biproduct when equipped with the projections and

    has-biproducts :  {a b}  Biproduct a b
    has-biproducts {a} {b} .Biproduct.biapex = a ⊕₀ b
    has-biproducts .Biproduct.π₁ = [ id , zero→ ]
    has-biproducts .Biproduct.π₂ = [ zero→ , id ]
    has-biproducts .Biproduct.ι₁ = ι₁
    has-biproducts .Biproduct.ι₂ = ι₂
    has-biproducts .Biproduct.has-is-biproduct .is-biproduct.has-is-product =
        is-product-iso-apex coproduct≅product π₁∘⟨⟩ π₂∘⟨⟩ has-is-product
    has-biproducts .Biproduct.has-is-biproduct .is-biproduct.has-is-coproduct = has-is-coproduct
    has-biproducts .Biproduct.has-is-biproduct .is-biproduct.πι₁ = []∘ι₁
    has-biproducts .Biproduct.has-is-biproduct .is-biproduct.πι₂ = []∘ι₂
    has-biproducts .Biproduct.has-is-biproduct .is-biproduct.ιπ-comm =
      ι₁  [ id , zero→ ]  ι₂  [ zero→ , id ] ≡⟨ refl⟩∘⟨ pulll []∘ι₂ 
      ι₁  zero→  [ zero→ , id ]               ≡⟨ pulll (zero-∘l _)  zero-∘r _ 
      zero→                                     ≡˘⟨ pulll (zero-∘l _)  zero-∘r _ 
      ι₂  zero→  [ id , zero→ ]               ≡˘⟨ refl⟩∘⟨ pulll []∘ι₁ 
      ι₂  [ zero→ , id ]  ι₁  [ id , zero→ ] 

  open make-semiadditive

  to-semiadditive : make-semiadditive  is-semiadditive
  to-semiadditive mk .is-semiadditive.has-zero = has-zero mk
  to-semiadditive mk .is-semiadditive.has-biproducts = has-biproducts mk

  1. Really property, in a univalent category.↩︎


References