From 7cb4f160835178d06e0c0bf9802c3cad6d48a9d0 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sun, 11 Oct 2026 22:59:21 -0700 Subject: Add hom-set addition to semiadditive record --- Category/Semiadditive.agda | 256 ++++++++++++++++++++++++++++++++------------- 1 file changed, 185 insertions(+), 71 deletions(-) (limited to 'Category/Semiadditive.agda') diff --git a/Category/Semiadditive.agda b/Category/Semiadditive.agda index 7d34fbf..30f84e6 100644 --- a/Category/Semiadditive.agda +++ b/Category/Semiadditive.agda @@ -18,7 +18,10 @@ open import Categories.Object.Zero 𝒞 using (Zero) open import Category.BinaryBiproducts 𝒞 using (BinaryBiproducts) open import Data.Product using (_,_) -private module 𝒞 = Category 𝒞 +private + module 𝒞 = Category 𝒞 + variable + A B C D : 𝒞.Obj -- A semiadditive category has all finite biproducts record Semiadditive : Set (levelOfTerm 𝒞) where @@ -32,9 +35,43 @@ record Semiadditive : Set (levelOfTerm 𝒞) where open 𝒞 + infix 8 _+_ + + field + 𝟎 : A ⇒ B + 𝟎-resp-∘ : {h : A ⇒ B} {k : C ⇒ D} → k ∘ 𝟎 ∘ h ≈ 𝟎 + _+_ : A ⇒ B → A ⇒ B → A ⇒ B + +-resp-≈ : {x y u v : A ⇒ B} → x ≈ y → u ≈ v → x + u ≈ y + v + +-resp-∘ : {f g : B ⇒ C} {h : A ⇒ B} {k : C ⇒ D} → k ∘ (f + g) ∘ h ≈ k ∘ f ∘ h + k ∘ g ∘ h + +-identityˡ : (f : A ⇒ B) → 𝟎 + f ≈ f + +-identityʳ : (f : A ⇒ B) → f + 𝟎 ≈ f + open HomReasoning open ⇒-Reasoning + +-cong : {x y u v : A ⇒ B} → x ≈ y → u ≈ v → x + u ≈ y + v + +-cong = +-resp-≈ + + +-resp-∘ˡ + : {A B C : Obj} + {f g : A ⇒ B} + {k : B ⇒ C} + → k ∘ (f + g) ≈ k ∘ f + k ∘ g + +-resp-∘ˡ {f = f} {g} {h} = begin + h ∘ (f + g) ≈⟨ refl⟩∘⟨ identityʳ ⟨ + h ∘ (f + g) ∘ id ≈⟨ +-resp-∘ ⟩ + h ∘ f ∘ id + h ∘ g ∘ id ≈⟨ +-resp-≈ (refl⟩∘⟨ identityʳ) (refl⟩∘⟨ identityʳ) ⟩ + h ∘ f + h ∘ g ∎ + + 𝟎-resp-∘ˡ + : {A B C : Obj} + {f : B ⇒ C} + → f ∘ 𝟎 {A} {B} ≈ 𝟎 + 𝟎-resp-∘ˡ {f = f} = begin + f ∘ 𝟎 ≈⟨ refl⟩∘⟨ identityʳ ⟨ + f ∘ 𝟎 ∘ id ≈⟨ 𝟎-resp-∘ ⟩ + 𝟎 ∎ + module _ {A B : Obj} where π₁∘i₂≈0 : π₁ {A} {B} ∘ i₂ ≈ zero⇒ @@ -49,6 +86,38 @@ record Semiadditive : Set (levelOfTerm 𝒞) where zero⇒ {A} ∘ π₂ ∘ i₁ ≈⟨ zero-∘ʳ (π₂ ∘ i₁) ⟩ zero⇒ ∎ + 𝟎≈zero⇒ : 𝟎 {A} {B} ≈ zero⇒ + 𝟎≈zero⇒ = begin + 𝟎 ≈⟨ 𝟎-resp-∘ˡ ⟨ + zero⇒ ∘ 𝟎 ≈⟨ zero-∘ʳ {A} {B} 𝟎 ⟩ + zero⇒ ∎ + + module _ {A B : Obj} where + + +-∇∘⟨⟩ : {f g : A ⇒ B} → f + g ≈ ∇ ∘ ⟨ f , g ⟩ + +-∇∘⟨⟩ {f} {g} = begin + f + g ≈⟨ +-resp-≈ (insertˡ inject₁) (insertˡ inject₂) ⟩ + ∇ ∘ i₁ ∘ f + ∇ ∘ i₂ ∘ g ≈⟨ +-resp-∘ˡ ⟨ + ∇ ∘ (i₁ ∘ f + i₂ ∘ g) ≈⟨ refl⟩∘⟨ ⟨⟩-unique left right ⟨ + ∇ ∘ ⟨ f , g ⟩ ∎ + where + left : π₁ ∘ (i₁ ∘ f + i₂ ∘ g) ≈ f + left = begin + π₁ ∘ (i₁ ∘ f + i₂ ∘ g) ≈⟨ +-resp-∘ˡ ⟩ + π₁ ∘ i₁ ∘ f + π₁ ∘ i₂ ∘ g ≈⟨ +-resp-≈ (cancelˡ π₁∘i₁≈id) (pullˡ π₁∘i₂≈0) ⟩ + f + zero⇒ ∘ g ≈⟨ +-resp-≈ Equiv.refl (zero-∘ʳ g) ⟩ + f + zero⇒ ≈⟨ +-resp-≈ Equiv.refl 𝟎≈zero⇒ ⟨ + f + 𝟎 ≈⟨ +-identityʳ f ⟩ + f ∎ + right : π₂ ∘ (i₁ ∘ f + i₂ ∘ g) ≈ g + right = begin + π₂ ∘ (i₁ ∘ f + i₂ ∘ g) ≈⟨ +-resp-∘ˡ ⟩ + π₂ ∘ i₁ ∘ f + π₂ ∘ i₂ ∘ g ≈⟨ +-resp-≈ (pullˡ π₂∘i₁≈0) (cancelˡ π₂∘i₂≈id) ⟩ + zero⇒ ∘ f + g ≈⟨ +-resp-≈ (zero-∘ʳ f) Equiv.refl ⟩ + zero⇒ + g ≈⟨ +-resp-≈ 𝟎≈zero⇒ Equiv.refl ⟨ + 𝟎 + g ≈⟨ +-identityˡ g ⟩ + g ∎ + Δ-⊕ : {X Y : Obj} → Δ {X ⊕ Y} ≈ σ₂₃ ∘ Δ ×₁ Δ Δ-⊕ {X} {Y} = begin ⟨ id , id ⟩ ≈⟨ ⟨⟩-cong₂ id×₁id id×₁id ⟨ @@ -69,45 +138,17 @@ record Semiadditive : Set (levelOfTerm 𝒞) where module _ {A B : Obj} where - _+_ _+′_ : A ⇒ B → A ⇒ B → A ⇒ B - f + g = ∇ ∘ f ×₁ g ∘ Δ - f +′ g = ∇ ∘ f +₁ g ∘ Δ - - infix 8 _+_ - - +-cong : {x y u v : A ⇒ B} → x ≈ y → u ≈ v → x + u ≈ y + v - +-cong eq₁ eq₂ = refl⟩∘⟨ ×₁-cong₂ eq₁ eq₂ ⟩∘⟨refl - +-assoc : (x y z : A ⇒ B) → (x + y) + z ≈ x + (y + z) +-assoc x y z = begin - ∇ ∘ (∇ ∘ x ×₁ y ∘ Δ) ×₁ z ∘ Δ ≈⟨ refl⟩∘⟨ pushˡ (Equiv.sym first∘×₁) ⟩ - ∇ ∘ ∇ ×₁ id ∘ (x ×₁ y ∘ Δ) ×₁ z ∘ Δ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (Equiv.sym ×₁∘first) ⟩ - ∇ ∘ ∇ ×₁ id ∘ (x ×₁ y) ×₁ z ∘ Δ ×₁ id ∘ Δ ≈⟨ extendʳ ∇-assoc-×₁ ⟩ - ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ (x ×₁ y) ×₁ z ∘ Δ ×₁ id ∘ Δ ≈⟨ refl⟩∘⟨ pullʳ (extendʳ assocˡ∘×₁) ⟩ - ∇ ∘ id ×₁ ∇ ∘ x ×₁ y ×₁ z ∘ assocˡ ∘ Δ ×₁ id ∘ Δ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ Δ-assoc ⟨ - ∇ ∘ id ×₁ ∇ ∘ x ×₁ y ×₁ z ∘ id ×₁ Δ ∘ Δ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ ×₁∘second ⟩ - ∇ ∘ id ×₁ ∇ ∘ x ×₁ (y ×₁ z ∘ Δ) ∘ Δ ≈⟨ refl⟩∘⟨ pullˡ second∘×₁ ⟩ - ∇ ∘ x ×₁ (∇ ∘ y ×₁ z ∘ Δ) ∘ Δ ∎ - - +-identityˡ : (x : A ⇒ B) → zero⇒ + x ≈ x - +-identityˡ x = begin - ∇ ∘ zero⇒ ×₁ x ∘ Δ ≈⟨ refl⟩∘⟨ ×₁∘Δ ⟩ - ∇ ∘ ⟨ zero⇒ , x ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (zero-∘ʳ x) identityˡ ⟨ - ∇ ∘ ⟨ zero⇒ ∘ x , id ∘ x ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟨ - ∇ ∘ ⟨ zero⇒ , id ⟩ ∘ x ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ π₁∘i₂≈0 π₂∘i₂≈id ⟩∘⟨refl ⟨ - ∇ ∘ ⟨ π₁ ∘ i₂ , π₂ ∘ i₂ ⟩ ∘ x ≈⟨ refl⟩∘⟨ g-η ⟩∘⟨refl ⟩ - ∇ ∘ i₂ ∘ x ≈⟨ cancelˡ ∇-identityˡ ⟩ - x ∎ - - +-identityʳ : (x : A ⇒ B) → x + zero⇒ ≈ x - +-identityʳ x = begin - ∇ ∘ x ×₁ zero⇒ ∘ Δ ≈⟨ refl⟩∘⟨ ×₁∘Δ ⟩ - ∇ ∘ ⟨ x , zero⇒ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ identityˡ (zero-∘ʳ x) ⟨ - ∇ ∘ ⟨ id ∘ x , zero⇒ ∘ x ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟨ - ∇ ∘ ⟨ id , zero⇒ ⟩ ∘ x ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ π₁∘i₁≈id π₂∘i₁≈0 ⟩∘⟨refl ⟨ - ∇ ∘ ⟨ π₁ ∘ i₁ , π₂ ∘ i₁ ⟩ ∘ x ≈⟨ refl⟩∘⟨ g-η ⟩∘⟨refl ⟩ - ∇ ∘ i₁ ∘ x ≈⟨ cancelˡ ∇-identityʳ ⟩ - x ∎ + (x + y) + z ≈⟨ +-∇∘⟨⟩ ⟩ + ∇ ∘ ⟨ x + y , z ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ +-∇∘⟨⟩ ⟩ + ∇ ∘ ⟨ ∇ ∘ ⟨ x , y ⟩ , z ⟩ ≈⟨ refl⟩∘⟨ first∘⟨⟩ ⟨ + ∇ ∘ ∇ ×₁ id ∘ ⟨ ⟨ x , y ⟩ , z ⟩ ≈⟨ extendʳ ∇-assoc-×₁ ⟩ + ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ ⟨ x , y ⟩ , z ⟩ ≈⟨ refl⟩∘⟨ pullʳ assocˡ∘⟨⟩ ⟩ + ∇ ∘ id ×₁ ∇ ∘ ⟨ x , ⟨ y , z ⟩ ⟩ ≈⟨ refl⟩∘⟨ second∘⟨⟩ ⟩ + ∇ ∘ ⟨ x , ∇ ∘ ⟨ y , z ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ +-∇∘⟨⟩ ⟨ + ∇ ∘ ⟨ x , y + z ⟩ ≈⟨ +-∇∘⟨⟩ ⟨ + x + (y + z) ∎ ∇∘+-swap : {A : Obj} → ∇ ∘ +-swap {A} ≈ ∇ ∇∘+-swap = begin @@ -123,19 +164,20 @@ record Semiadditive : Set (levelOfTerm 𝒞) where +-comm : (x y : A ⇒ B) → x + y ≈ y + x +-comm x y = begin - ∇ ∘ x ×₁ y ∘ Δ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ swap∘Δ ⟨ - ∇ ∘ x ×₁ y ∘ swap ∘ Δ ≈⟨ refl⟩∘⟨ extendʳ swap∘×₁ ⟨ - ∇ ∘ swap ∘ y ×₁ x ∘ Δ ≈⟨ refl⟩∘⟨ swap≈+-swap ⟩∘⟨refl ⟩ - ∇ ∘ +-swap ∘ y ×₁ x ∘ Δ ≈⟨ pullˡ ∇∘+-swap ⟩ - ∇ ∘ y ×₁ x ∘ Δ ∎ - - isCM : IsCommutativeMonoid (_≈_ {A} {B}) _+_ zero⇒ + x + y ≈⟨ +-∇∘⟨⟩ ⟩ + ∇ ∘ ⟨ x , y ⟩ ≈⟨ refl⟩∘⟨ swap∘⟨⟩ ⟨ + ∇ ∘ swap ∘ ⟨ y , x ⟩ ≈⟨ refl⟩∘⟨ swap≈+-swap ⟩∘⟨refl ⟩ + ∇ ∘ +-swap ∘ ⟨ y , x ⟩ ≈⟨ pullˡ ∇∘+-swap ⟩ + ∇ ∘ ⟨ y , x ⟩ ≈⟨ +-∇∘⟨⟩ ⟨ + y + x ∎ + + isCM : IsCommutativeMonoid (_≈_ {A} {B}) _+_ 𝟎 isCM = record { isMonoid = record { isSemigroup = record { isMagma = record { isEquivalence = equiv - ; ∙-cong = +-cong + ; ∙-cong = +-resp-≈ } ; assoc = +-assoc } @@ -149,39 +191,16 @@ record Semiadditive : Set (levelOfTerm 𝒞) where { Carrier = A ⇒ B ; _≈_ = _≈_ ; _∙_ = _+_ - ; ε = zero⇒ + ; ε = 𝟎 ; isCommutativeMonoid = isCM } - +-resp-∘ - : {A B C D : Obj} - {f g : B ⇒ C} - {h : A ⇒ B} - {k : C ⇒ D} - → k ∘ (f + g) ∘ h ≈ k ∘ f ∘ h + k ∘ g ∘ h - +-resp-∘ {f = f} {g} {h} {k} = begin - k ∘ (∇ ∘ f ×₁ g ∘ Δ) ∘ h ≈⟨ extendʳ (extendʳ ⇒∇-×₁) ⟩ - ∇ ∘ (k ×₁ k ∘ f ×₁ g ∘ Δ) ∘ h ≈⟨ refl⟩∘⟨ pullʳ (pullʳ ⇒Δ) ⟩ - ∇ ∘ k ×₁ k ∘ f ×₁ g ∘ h ×₁ h ∘ Δ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ ×₁∘×₁ ⟩ - ∇ ∘ k ×₁ k ∘ (f ∘ h) ×₁ (g ∘ h) ∘ Δ ≈⟨ refl⟩∘⟨ pullˡ ×₁∘×₁ ⟩ - ∇ ∘ (k ∘ f ∘ h) ×₁ (k ∘ g ∘ h) ∘ Δ ∎ - - 0-resp-∘ - : {A C D : Obj} - {h : A ⇒ C} - {k : C ⇒ D} - → k ∘ zero⇒ ∘ h ≈ zero⇒ - 0-resp-∘ {h = h} {k} = begin - k ∘ zero⇒ ∘ h ≈⟨ pullˡ (zero-∘ˡ k) ⟩ - zero⇒ ∘ h ≈⟨ zero-∘ʳ h ⟩ - zero⇒ ∎ - cm-category : CM-Category o ℓ e cm-category = record { 𝒞 ; Hom = hom ; +-resp-∘ = +-resp-∘ - ; 0-resp-∘ = 0-resp-∘ + ; 0-resp-∘ = 𝟎-resp-∘ } cartesian : Cartesian @@ -195,3 +214,98 @@ record Semiadditive : Set (levelOfTerm 𝒞) where { initial = initial ; coproducts = binaryCoproducts } + +record SemiadditiveHelper : Set (levelOfTerm 𝒞) where + + field + zero : Zero + biproducts : BinaryBiproducts + + open Zero zero + open BinaryBiproducts biproducts + open 𝒞 + open HomReasoning + open ⇒-Reasoning + + module _ {A B : Obj} where + + π₁∘i₂≈0 : π₁ {A} {B} ∘ i₂ ≈ zero⇒ + π₁∘i₂≈0 = begin + π₁ ∘ i₂ ≈⟨ π₁i₂-absorbˡ zero⇒ ⟨ + zero⇒ {A} ∘ π₁ ∘ i₂ ≈⟨ zero-∘ʳ (π₁ ∘ i₂) ⟩ + zero⇒ ∎ + + π₂∘i₁≈0 : π₂ {A} {B} ∘ i₁ ≈ zero⇒ + π₂∘i₁≈0 = begin + π₂ ∘ i₁ ≈⟨ π₂i₁-absorbˡ zero⇒ ⟨ + zero⇒ {A} ∘ π₂ ∘ i₁ ≈⟨ zero-∘ʳ (π₂ ∘ i₁) ⟩ + zero⇒ ∎ + +-- Construct hom-set addition from biproduct +semiadditveHelper : SemiadditiveHelper → Semiadditive +semiadditveHelper sh = record + { zero = zero + ; biproducts = biproducts + ; 𝟎 = zero⇒ + ; 𝟎-resp-∘ = 𝟎-resp-∘ + ; _+_ = _+_ + ; +-resp-≈ = +-cong + ; +-resp-∘ = +-resp-∘ + ; +-identityˡ = +-identityˡ + ; +-identityʳ = +-identityʳ + } + where + open SemiadditiveHelper sh + open Zero zero + open BinaryBiproducts biproducts + open 𝒞 + open HomReasoning + open ⇒-Reasoning + + 𝟎-resp-∘ + : {A B C D : Obj} + {h : A ⇒ B} + {k : C ⇒ D} + → k ∘ zero⇒ ∘ h ≈ zero⇒ + 𝟎-resp-∘ {h = h} {k} = begin + k ∘ zero⇒ ∘ h ≈⟨ pullˡ (zero-∘ˡ k) ⟩ + zero⇒ ∘ h ≈⟨ zero-∘ʳ h ⟩ + zero⇒ ∎ + + infix 8 _+_ + + _+_ : A ⇒ B → A ⇒ B → A ⇒ B + f + g = ∇ ∘ ⟨ f , g ⟩ + + +-cong : {x y u v : A ⇒ B} → x ≈ y → u ≈ v → x + u ≈ y + v + +-cong eq₁ eq₂ = refl⟩∘⟨ ⟨⟩-cong₂ eq₁ eq₂ + + +-resp-∘ + : {A B C D : Obj} + {f g : B ⇒ C} + {h : A ⇒ B} + {k : C ⇒ D} + → k ∘ (f + g) ∘ h ≈ k ∘ f ∘ h + k ∘ g ∘ h + +-resp-∘ {f = f} {g} {h} {k} = begin + k ∘ (∇ ∘ ⟨ f , g ⟩) ∘ h ≈⟨ refl⟩∘⟨ pullʳ ⟨⟩∘ ⟩ + k ∘ ∇ ∘ ⟨ f ∘ h , g ∘ h ⟩ ≈⟨ extendʳ ⇒∇-×₁ ⟩ + ∇ ∘ k ×₁ k ∘ ⟨ f ∘ h , g ∘ h ⟩ ≈⟨ refl⟩∘⟨ ×₁∘⟨⟩ ⟩ + ∇ ∘ ⟨ k ∘ f ∘ h , k ∘ g ∘ h ⟩ ∎ + + +-identityˡ : (x : A ⇒ B) → zero⇒ + x ≈ x + +-identityˡ x = begin + ∇ ∘ ⟨ zero⇒ , x ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (zero-∘ʳ x) identityˡ ⟨ + ∇ ∘ ⟨ zero⇒ ∘ x , id ∘ x ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟨ + ∇ ∘ ⟨ zero⇒ , id ⟩ ∘ x ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ π₁∘i₂≈0 π₂∘i₂≈id ⟩∘⟨refl ⟨ + ∇ ∘ ⟨ π₁ ∘ i₂ , π₂ ∘ i₂ ⟩ ∘ x ≈⟨ refl⟩∘⟨ g-η ⟩∘⟨refl ⟩ + ∇ ∘ i₂ ∘ x ≈⟨ cancelˡ ∇-identityˡ ⟩ + x ∎ + + +-identityʳ : (x : A ⇒ B) → x + zero⇒ ≈ x + +-identityʳ x = begin + ∇ ∘ ⟨ x , zero⇒ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ identityˡ (zero-∘ʳ x) ⟨ + ∇ ∘ ⟨ id ∘ x , zero⇒ ∘ x ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟨ + ∇ ∘ ⟨ id , zero⇒ ⟩ ∘ x ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ π₁∘i₁≈id π₂∘i₁≈0 ⟩∘⟨refl ⟨ + ∇ ∘ ⟨ π₁ ∘ i₁ , π₂ ∘ i₁ ⟩ ∘ x ≈⟨ refl⟩∘⟨ g-η ⟩∘⟨refl ⟩ + ∇ ∘ i₁ ∘ x ≈⟨ cancelˡ ∇-identityʳ ⟩ + x ∎ -- cgit v1.2.3