Skip to content

Commit

Permalink
Prove some stuff about biproducts + (co)products
Browse files Browse the repository at this point in the history
  • Loading branch information
Reed Mullanix authored and Reed Mullanix committed Feb 22, 2021
1 parent 5d08e16 commit 9e31c06
Showing 1 changed file with 123 additions and 2 deletions.
125 changes: 123 additions & 2 deletions src/Categories/Category/Preadditive/Properties.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,8 @@ open import Categories.Category.Preadditive
open import Categories.Object.Initial
open import Categories.Object.Terminal
open import Categories.Object.Biproduct
open import Categories.Object.Coproduct
open import Categories.Object.Product
open import Categories.Object.Zero

import Categories.Morphism.Reasoning as MR
Expand Down Expand Up @@ -49,8 +51,127 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (preadditive : Preadditive 𝒞) wh
where
open Terminal terminal

Product⇒Biproduct : ∀ {A B} → Product 𝒞 A B → Biproduct 𝒞 A B
Product⇒Biproduct product = record
{ A⊕B = A×B
; π₁ = π₁
; π₂ = π₂
; ⟨_,_⟩ = ⟨_,_⟩
; project₁ = project₁
; project₂ = project₂
; ⟨⟩-unique = unique
; i₁ = ⟨ id , 0H ⟩
; i₂ = ⟨ 0H , id ⟩
; [_,_] = λ f g → (f ∘ π₁) + (g ∘ π₂)
; inject₁ = λ {C} {f} {g} → begin
(f ∘ π₁ + g ∘ π₂) ∘ ⟨ id , 0H ⟩ ≈⟨ +-resp-∘ʳ ⟩
((f ∘ π₁) ∘ ⟨ id , 0H ⟩) + ((g ∘ π₂) ∘ ⟨ id , 0H ⟩) ≈⟨ +-cong (cancelʳ project₁) (pullʳ project₂) ⟩
f + (g ∘ 0H) ≈⟨ +-elimʳ 0-resp-∘ʳ ⟩
f ∎
; inject₂ = λ {C} {f} {g} → begin
(f ∘ π₁ + g ∘ π₂) ∘ ⟨ 0H , id ⟩ ≈⟨ +-resp-∘ʳ ⟩
((f ∘ π₁) ∘ ⟨ 0H , id ⟩) + ((g ∘ π₂) ∘ ⟨ 0H , id ⟩) ≈⟨ +-cong (pullʳ project₁) (cancelʳ project₂) ⟩
(f ∘ 0H) + g ≈⟨ +-elimˡ 0-resp-∘ʳ ⟩
g ∎
; []-unique = λ {X} {h} {f} {g} eq₁ eq₂ → begin
(f ∘ π₁) + (g ∘ π₂) ≈⟨ +-cong (pushˡ (⟺ eq₁)) (pushˡ (⟺ eq₂)) ⟩
(h ∘ ⟨ id , 0H ⟩ ∘ π₁) + (h ∘ ⟨ 0H , id ⟩ ∘ π₂) ≈˘⟨ +-resp-∘ˡ ⟩
h ∘ (⟨ id , 0H ⟩ ∘ π₁ + ⟨ 0H , id ⟩ ∘ π₂) ≈⟨ refl⟩∘⟨ +-cong ∘-distribʳ-⟨⟩ ∘-distribʳ-⟨⟩ ⟩
h ∘ (⟨ id ∘ π₁ , 0H ∘ π₁ ⟩ + ⟨ 0H ∘ π₂ , id ∘ π₂ ⟩) ≈⟨ refl⟩∘⟨ +-cong (⟨⟩-cong₂ identityˡ 0-resp-∘ˡ) (⟨⟩-cong₂ 0-resp-∘ˡ identityˡ) ⟩
h ∘ (⟨ π₁ , 0H ⟩ + ⟨ 0H , π₂ ⟩) ≈⟨ elimʳ (⟺ (unique′ π₁-lemma π₂-lemma)) ⟩
h ∎
; π₁∘i₁≈id = project₁
; π₂∘i₂≈id = project₂
; permute = begin
⟨ id , 0H ⟩ ∘ π₁ ∘ ⟨ 0H , id ⟩ ∘ π₂ ≈⟨ pull-center project₁ ⟩
⟨ id , 0H ⟩ ∘ 0H ∘ π₂ ≈⟨ pullˡ 0-resp-∘ʳ ⟩
0H ∘ π₂ ≈⟨ 0-resp-∘ˡ ⟩
0H ≈˘⟨ 0-resp-∘ˡ ⟩
0H ∘ π₁ ≈⟨ pushˡ (⟺ 0-resp-∘ʳ) ⟩
⟨ 0H , id ⟩ ∘ 0H ∘ π₁ ≈⟨ push-center project₂ ⟩
⟨ 0H , id ⟩ ∘ π₂ ∘ ⟨ id , 0H ⟩ ∘ π₁ ∎
}
where
open Product 𝒞 product

π₁-lemma : π₁ ∘ id ≈ π₁ ∘ (⟨ π₁ , 0H ⟩ + ⟨ 0H , π₂ ⟩)
π₁-lemma = begin
π₁ ∘ id ≈⟨ identityʳ ⟩
π₁ ≈˘⟨ +-identityʳ π₁ ⟩
π₁ + 0H ≈⟨ +-cong (⟺ project₁) (⟺ project₁) ⟩
(π₁ ∘ ⟨ π₁ , 0H ⟩) + (π₁ ∘ ⟨ 0H , π₂ ⟩) ≈˘⟨ +-resp-∘ˡ ⟩
π₁ ∘ (⟨ π₁ , 0H ⟩ + ⟨ 0H , π₂ ⟩) ∎

π₂-lemma : π₂ ∘ id ≈ π₂ ∘ (⟨ π₁ , 0H ⟩ + ⟨ 0H , π₂ ⟩)
π₂-lemma = begin
π₂ ∘ id ≈⟨ identityʳ ⟩
π₂ ≈˘⟨ +-identityˡ π₂ ⟩
0H + π₂ ≈⟨ +-cong (⟺ project₂) (⟺ project₂) ⟩
(π₂ ∘ ⟨ π₁ , 0H ⟩) + (π₂ ∘ ⟨ 0H , π₂ ⟩) ≈˘⟨ +-resp-∘ˡ ⟩
π₂ ∘ (⟨ π₁ , 0H ⟩ + ⟨ 0H , π₂ ⟩) ∎

Coproduct⇒Biproduct : ∀ {A B} → Coproduct 𝒞 A B → Biproduct 𝒞 A B
Coproduct⇒Biproduct coproduct = record
{ A⊕B = A+B
; π₁ = [ id , 0H ]
; π₂ = [ 0H , id ]
; ⟨_,_⟩ = λ f g → (i₁ ∘ f) + (i₂ ∘ g)
; project₁ = λ {C} {f} {g} → begin
[ id , 0H ] ∘ (i₁ ∘ f + i₂ ∘ g) ≈⟨ +-resp-∘ˡ ⟩
([ id , 0H ] ∘ i₁ ∘ f) + ([ id , 0H ] ∘ i₂ ∘ g) ≈⟨ +-cong (cancelˡ inject₁) (pullˡ inject₂) ⟩
f + (0H ∘ g) ≈⟨ +-elimʳ 0-resp-∘ˡ ⟩
f ∎
; project₂ = λ {C} {f} {g} → begin
[ 0H , id ] ∘ (i₁ ∘ f + i₂ ∘ g) ≈⟨ +-resp-∘ˡ ⟩
([ 0H , id ] ∘ i₁ ∘ f) + ([ 0H , id ] ∘ i₂ ∘ g) ≈⟨ +-cong (pullˡ inject₁) (cancelˡ inject₂) ⟩
(0H ∘ f) + g ≈⟨ +-elimˡ 0-resp-∘ˡ ⟩
g ∎
; ⟨⟩-unique = λ {X} {h} {f} {g} eq₁ eq₂ → begin
(i₁ ∘ f) + (i₂ ∘ g) ≈⟨ +-cong (pushʳ (⟺ eq₁)) (pushʳ (⟺ eq₂)) ⟩
(i₁ ∘ [ id , 0H ]) ∘ h + (i₂ ∘ [ 0H , id ]) ∘ h ≈˘⟨ +-resp-∘ʳ ⟩
(i₁ ∘ [ id , 0H ] + i₂ ∘ [ 0H , id ]) ∘ h ≈⟨ +-cong ∘-distribˡ-[] ∘-distribˡ-[] ⟩∘⟨refl ⟩
([ i₁ ∘ id , i₁ ∘ 0H ] + [ i₂ ∘ 0H , i₂ ∘ id ]) ∘ h ≈⟨ +-cong ([]-cong₂ identityʳ 0-resp-∘ʳ) ([]-cong₂ 0-resp-∘ʳ identityʳ) ⟩∘⟨refl ⟩
([ i₁ , 0H ] + [ 0H , i₂ ]) ∘ h ≈⟨ elimˡ (⟺ (unique′ i₁-lemma i₂-lemma)) ⟩
h ∎
; i₁ = i₁
; i₂ = i₂
; [_,_] = [_,_]
; inject₁ = inject₁
; inject₂ = inject₂
; []-unique = unique
; π₁∘i₁≈id = inject₁
; π₂∘i₂≈id = inject₂
; permute = begin
i₁ ∘ [ id , 0H ] ∘ i₂ ∘ [ 0H , id ] ≈⟨ pull-center inject₂ ⟩
i₁ ∘ 0H ∘ [ 0H , id ] ≈⟨ pullˡ 0-resp-∘ʳ ⟩
0H ∘ [ 0H , id ] ≈⟨ 0-resp-∘ˡ ⟩
0H ≈˘⟨ 0-resp-∘ˡ ⟩
0H ∘ [ id , 0H ] ≈⟨ pushˡ (⟺ 0-resp-∘ʳ) ⟩
i₂ ∘ 0H ∘ [ id , 0H ] ≈⟨ push-center inject₁ ⟩
i₂ ∘ [ 0H , id ] ∘ i₁ ∘ [ id , 0H ] ∎
}
where
open Coproduct coproduct

i₁-lemma : id ∘ i₁ ≈ ([ i₁ , 0H ] + [ 0H , i₂ ]) ∘ i₁
i₁-lemma = begin
id ∘ i₁ ≈⟨ identityˡ ⟩
i₁ ≈˘⟨ +-identityʳ i₁ ⟩
i₁ + 0H ≈⟨ +-cong (⟺ inject₁) (⟺ inject₁) ⟩
[ i₁ , 0H ] ∘ i₁ + [ 0H , i₂ ] ∘ i₁ ≈˘⟨ +-resp-∘ʳ ⟩
([ i₁ , 0H ] + [ 0H , i₂ ]) ∘ i₁ ∎

i₂-lemma : id ∘ i₂ ≈ ([ i₁ , 0H ] + [ 0H , i₂ ]) ∘ i₂
i₂-lemma = begin
id ∘ i₂ ≈⟨ identityˡ ⟩
i₂ ≈˘⟨ +-identityˡ i₂ ⟩
0H + i₂ ≈⟨ +-cong (⟺ inject₂) (⟺ inject₂) ⟩
[ i₁ , 0H ] ∘ i₂ + [ 0H , i₂ ] ∘ i₂ ≈˘⟨ +-resp-∘ʳ ⟩
([ i₁ , 0H ] + [ 0H , i₂ ]) ∘ i₂ ∎

-- FIXME: Show the other direction, and bundle up all of this junk into a record
-- Our version of biproducts coincide with those found in CWM, VIII.2
-- Our version of biproducts coincide with those found in Maclane's "Categories For the Working Mathematician", VIII.2,
-- and Borceux's "Handbook of Categorical Algebra, Volume 2", 1.2.4
Biproduct⇒Preadditive : ∀ {A B X} {p₁ : X ⇒ A} {p₂ : X ⇒ B} {i₁ : A ⇒ X} {i₂ : B ⇒ X}
→ p₁ ∘ i₁ ≈ id
→ p₂ ∘ i₂ ≈ id
Expand Down Expand Up @@ -93,7 +214,7 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (preadditive : Preadditive 𝒞) wh
(f ∘ p₁) + (g ∘ p₂) ≈⟨ +-cong (pushˡ (⟺ eq₁)) (pushˡ (⟺ eq₂)) ⟩
(h ∘ i₁ ∘ p₁) + (h ∘ i₂ ∘ p₂) ≈˘⟨ +-resp-∘ˡ ⟩
h ∘ (i₁ ∘ p₁ + i₂ ∘ p₂) ≈⟨ elimʳ +-eq ⟩
h ∎
h ∎
; π₁∘i₁≈id = p₁∘i₁≈id
; π₂∘i₂≈id = p₂∘i₂≈id
; permute = begin
Expand Down

0 comments on commit 9e31c06

Please sign in to comment.