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 π₁ π₂ ι₁ ι₂
open is-biproduct has-is-biproduct public product : Product C A B product = record { apex = biapex ; π₁ = π₁ ; π₂ = π₂ ; has-is-product = has-is-product } coproduct : Coproduct C A B coproduct = record { coapex = biapex ; ι₁ = ι₁ ; ι₂ = ι₂ ; has-is-coproduct = has-is-coproduct } open Product product public hiding (π₁; π₂) renaming (unique₂ to ⟨⟩-unique₂) open Coproduct coproduct public hiding (ι₁; ι₂) renaming (unique₂ to []-unique₂)
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!
open Zero has-zero public module Biprod {A B} = Biproduct (has-biproducts {A} {B}) open Biprod using (πι₁; πι₂; ιπ-comm) open Binary-products C (λ _ _ → Biprod.product) open Binary-coproducts C (λ _ _ → Biprod.coproduct) open Monoidal-category (Cartesian-monoidal (λ _ _ → Biprod.product) terminal) using (associator; module ⊗)
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
Really property, in a univalent category.↩︎
References
- Karvonen, Martti. 2020. “Biproducts Without Pointedness.” https://arxiv.org/abs/1801.06488.