diff options
Diffstat (limited to 'Category')
| -rw-r--r-- | Category/BinaryBiproducts.agda | 110 | ||||
| -rw-r--r-- | Category/Semiadditive.agda | 155 |
2 files changed, 256 insertions, 9 deletions
diff --git a/Category/BinaryBiproducts.agda b/Category/BinaryBiproducts.agda index c96d3bf..5b59df4 100644 --- a/Category/BinaryBiproducts.agda +++ b/Category/BinaryBiproducts.agda @@ -10,6 +10,7 @@ import Categories.Morphism.Reasoning as ⇒-Reasoning open import Categories.Category.BinaryCoproducts 𝒞 using (BinaryCoproducts) open import Categories.Category.BinaryProducts 𝒞 using (BinaryProducts) +open import Categories.Morphism.IsoEquiv 𝒞 using (_≃_; ⌞_⌟) open import Morphism.Zero using (IsZero⇒) open import Object.Biproduct 𝒞 using (Biproduct; Biproduct⇒Product; Biproduct⇒Coproduct) @@ -30,19 +31,21 @@ record BinaryBiproducts : Set (levelOfTerm 𝒞) where _⊕_ : Obj → Obj → Obj A ⊕ B = Biproduct.A⊕B (biproduct {A} {B}) - module _ where + private + binaryProducts : BinaryProducts binaryProducts = record { product = Biproduct⇒Product biproduct } - open BinaryProducts binaryProducts public - hiding (_×_) - renaming (_×₁_ to infixr 10 _×₁_; ×-comm to ⊕-comm; ×-assoc to ⊕-assoc) - module _ where binaryCoproducts : BinaryCoproducts binaryCoproducts = record { coproduct = Biproduct⇒Coproduct biproduct } - open BinaryCoproducts binaryCoproducts public - hiding (_+_) - renaming (_+₁_ to infixr 10 _+₁_; +-comm to ⊕-comm′; +-assoc to ⊕-assoc′) + + open BinaryProducts binaryProducts public + hiding (_×_) + renaming (_×₁_ to infixr 10 _×₁_; ×-comm to ⊕-comm; ×-assoc to ⊕-assoc) + + open BinaryCoproducts binaryCoproducts public + hiding (_+_) + renaming (_+₁_ to infixr 10 _+₁_; +-comm to ⊕-comm′; +-assoc to ⊕-assoc′) private module π₂i₁ {A} {B} = IsZero⇒ (π₂∘i₁-isZero {A} {B}) @@ -94,7 +97,7 @@ record BinaryBiproducts : Set (levelOfTerm 𝒞) where id ∘ 𝟎⇒ ≈⟨ identityˡ ⟩ 𝟎⇒ ∎ - module _ {A B : Obj} (f g : A ⇒ B) where + module _ {A B C D : Obj} (f : A ⇒ B) (g : C ⇒ D) where π₁∘+₁ : π₁ ∘ f +₁ g ≈ f ∘ π₁ π₁∘+₁ = begin @@ -119,6 +122,95 @@ record BinaryBiproducts : Set (levelOfTerm 𝒞) where ×₁-+₁ : f ×₁ g ≈ f +₁ g ×₁-+₁ = ⟨⟩-unique π₁∘+₁ π₂∘+₁ + module _ {A B : Obj} where + + π₁∘+-swap : π₁ ∘ +-swap ≈ π₂ + π₁∘+-swap = begin + π₁ ∘ [ i₂ , i₁ ] ≈⟨ ∘[] ⟩ + [ π₁ ∘ i₂ , π₁ ∘ i₁ ] ≈⟨ []-cong₂ π₁i₂≈π₂i₁ (π₁∘i₁≈id ○ Equiv.sym π₂∘i₂≈id) ⟩ + [ π₂ ∘ i₁ , π₂ ∘ i₂ ] ≈⟨ +-g-η ⟩ + π₂ ∎ + + π₂∘+-swap : π₂ ∘ +-swap ≈ π₁ + π₂∘+-swap = begin + π₂ ∘ [ i₂ , i₁ ] ≈⟨ ∘[] ⟩ + [ π₂ ∘ i₂ , π₂ ∘ i₁ ] ≈⟨ []-cong₂ (π₁∘i₁≈id ○ Equiv.sym π₂∘i₂≈id) π₁i₂≈π₂i₁ ⟨ + [ π₁ ∘ i₁ , π₁ ∘ i₂ ] ≈⟨ +-g-η ⟩ + π₁ ∎ + + swap≈+-swap : swap {A} {B} ≈ +-swap + swap≈+-swap = begin + ⟨ π₂ , π₁ ⟩ ≈⟨ ⟨⟩-unique π₁∘+-swap π₂∘+-swap ⟩ + [ i₂ , i₁ ] ∎ + + ⊕-comm≃ : ⊕-comm {A} {B} ≃ ⊕-comm′ + ⊕-comm≃ = ⌞ swap≈+-swap ⌟ + + module _ {A B C : Obj} where + + private + + lem₁ : π₁ ∘ [ i₂ , π₁ ∘ i₂ ] ≈ π₁ ∘ i₂ + lem₁ = begin + π₁ ∘ [ i₂ , π₁ ∘ i₂ ] ≈⟨ ∘[] ⟩ + [ π₁ ∘ i₂ , π₁ ∘ π₁ ∘ i₂ ] ≈⟨ []-congˡ (π₁i₂-absorbˡ π₁) ⟩ + [ π₁ ∘ i₂ , π₁ ∘ i₂ ] ≈⟨ []-unique (π₁i₂-absorbʳ i₁) (π₁i₂-absorbʳ i₂) ⟩ + π₁ ∘ i₂ ∎ + + lem₂ : π₂ ∘ [ i₂ , π₁ ∘ i₂ ] ≈ π₁ + lem₂ = begin + π₂ ∘ [ i₂ , π₁ ∘ i₂ ] ≈⟨ ∘[] ⟩ + [ π₂ ∘ i₂ , π₂ ∘ π₁ ∘ i₂ ] ≈⟨ []-cong₂ π₂∘i₂≈id (π₁i₂-absorbˡ π₂) ⟩ + [ id , π₁ ∘ i₂ ] ≈⟨ []-congʳ π₁∘i₁≈id ⟨ + [ π₁ ∘ i₁ , π₁ ∘ i₂ ] ≈⟨ +-g-η ⟩ + π₁ ∎ + + lem₃ : ⟨ π₁ , π₁ ∘ π₂ ⟩ ∘ i₁ ≈ i₁ + lem₃ = begin + ⟨ π₁ , π₁ ∘ π₂ ⟩ ∘ i₁ ≈⟨ ⟨⟩∘ ⟩ + ⟨ π₁ ∘ i₁ , (π₁ ∘ π₂) ∘ i₁ ⟩ ≈⟨ ⟨⟩-cong₂ π₁∘i₁≈id assoc ⟩ + ⟨ id , π₁ ∘ π₂ ∘ i₁ ⟩ ≈⟨ ⟨⟩-cong₂ (Equiv.sym π₁∘i₁≈id) (π₂i₁-absorbˡ π₁) ⟩ + ⟨ π₁ ∘ i₁ , π₂ ∘ i₁ ⟩ ≈⟨ g-η ⟩ + i₁ ∎ + + lem₄ : ⟨ π₁ , π₁ ∘ π₂ ⟩ ∘ i₂ ≈ [ i₂ , π₁ ∘ i₂ ] + lem₄ = begin + ⟨ π₁ , π₁ ∘ π₂ ⟩ ∘ i₂ ≈⟨ ⟨⟩∘ ⟩ + ⟨ π₁ ∘ i₂ , (π₁ ∘ π₂) ∘ i₂ ⟩ ≈⟨ ⟨⟩-congˡ (cancelʳ π₂∘i₂≈id) ⟩ + ⟨ π₁ ∘ i₂ , π₁ ⟩ ≈⟨ ⟨⟩-unique lem₁ lem₂ ⟩ + [ i₂ , π₁ ∘ i₂ ] ∎ + + lem₅ : π₁ ∘ [ i₁ ∘ i₁ , [ i₁ ∘ i₂ , i₂ ] ] ≈ ⟨ π₁ , π₁ ∘ π₂ ⟩ + lem₅ = begin + π₁ ∘ [ i₁ ∘ i₁ , [ i₁ ∘ i₂ , i₂ ] ] ≈⟨ ∘[] ⟩ + [ π₁ ∘ i₁ ∘ i₁ , π₁ ∘ [ i₁ ∘ i₂ , i₂ ] ] ≈⟨ []-congˡ ∘[] ⟩ + [ π₁ ∘ i₁ ∘ i₁ , [ π₁ ∘ i₁ ∘ i₂ , π₁ ∘ i₂ ] ] ≈⟨ []-cong₂ (cancelˡ π₁∘i₁≈id) ([]-congʳ (cancelˡ π₁∘i₁≈id)) ⟩ + [ i₁ , [ i₂ , π₁ ∘ i₂ ] ] ≈⟨ []-unique lem₃ lem₄ ⟩ + ⟨ π₁ , π₁ ∘ π₂ ⟩ ∎ + + lem₆ : π₂ ∘ [ i₁ ∘ i₁ , [ i₁ ∘ i₂ , i₂ ] ] ≈ π₂ ∘ π₂ + lem₆ = begin + π₂ ∘ [ i₁ ∘ i₁ , [ i₁ ∘ i₂ , i₂ ] ] ≈⟨ ∘[] ⟩ + [ π₂ ∘ i₁ ∘ i₁ , π₂ ∘ [ i₁ ∘ i₂ , i₂ ] ] ≈⟨ []-cong₂ sym-assoc ∘[] ⟩ + [ (π₂ ∘ i₁) ∘ i₁ , [ π₂ ∘ i₁ ∘ i₂ , π₂ ∘ i₂ ] ] ≈⟨ []-cong₂ (π₂i₁-absorbʳ i₁) ([]-congʳ (sym-assoc ○ π₂i₁-absorbʳ i₂)) ⟩ + [ π₂ ∘ i₁ , [ π₂ ∘ i₁ , π₂ ∘ i₂ ] ] ≈⟨ []-congˡ ([]-congˡ (π₂∘i₂≈id ○ Equiv.sym π₂∘i₂≈id)) ⟩ + [ π₂ ∘ i₁ , [ π₂ ∘ i₁ , π₂ ∘ i₂ ] ] ≈⟨ []-congˡ +-g-η ⟩ + [ π₂ ∘ i₁ , π₂ ] ≈⟨ []-unique (assoc ○ π₂i₁-absorbˡ π₂) (cancelʳ π₂∘i₂≈id) ⟩ + π₂ ∘ π₂ ∎ + + assocʳ≈+-assocʳ : assocʳ ≈ +-assocʳ + assocʳ≈+-assocʳ = begin + ⟨ ⟨ π₁ , π₁ ∘ π₂ ⟩ , π₂ ∘ π₂ ⟩ ≈⟨ ⟨⟩-unique lem₅ lem₆ ⟩ + [ i₁ ∘ i₁ , [ i₁ ∘ i₂ , i₂ ] ] ∎ + + ⊕-assoc≃ : ⊕-assoc {A} {B} {C} ≃ ⊕-assoc′ + ⊕-assoc≃ = ⌞ assocʳ≈+-assocʳ ⌟ + + assocˡ≈+-assocˡ : assocˡ ≈ +-assocˡ + assocˡ≈+-assocˡ = to-≈ ⊕-assoc≃ + where + open _≃_ + ∇-assoc : {A : Obj} → ∇ {A} ∘ ∇ +₁ id ≈ ∇ ∘ id +₁ ∇ ∘ +-assocˡ ∇-assoc = begin ∇ ∘ ∇ +₁ id ≈⟨ ∇∘+₁ ⟩ diff --git a/Category/Semiadditive.agda b/Category/Semiadditive.agda new file mode 100644 index 0000000..e7afc0e --- /dev/null +++ b/Category/Semiadditive.agda @@ -0,0 +1,155 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; levelOfTerm) +open import Categories.Category using (Category) + +module Category.Semiadditive {o ℓ e : Level} (𝒞 : Category o ℓ e) where + +import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning + +open import Algebra using (IsCommutativeMonoid; CommutativeMonoid) +open import Categories.Category.CMonoidEnriched using (CM-Category) +open import Categories.Object.Zero 𝒞 using (Zero) +open import Category.BinaryBiproducts 𝒞 using (BinaryBiproducts) +open import Data.Product using (_,_) + +private module 𝒞 = Category 𝒞 + +-- A semiadditive category has all finite biproducts +record Semiadditive : Set (levelOfTerm 𝒞) where + + field + zero : Zero + biproducts : BinaryBiproducts + + open Zero zero public + open BinaryBiproducts biproducts public + + open 𝒞 + + open HomReasoning + open ⇒-Reasoning + + 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⟩∘⟨ ×₁-cong₂ Equiv.refl identityʳ ⟩∘⟨refl ⟨ + ∇ ∘ ∇ ×₁ id ∘ (x ×₁ y ∘ Δ) ×₁ (z ∘ id) ∘ Δ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (Equiv.sym ×₁∘×₁) ⟩ + ∇ ∘ ∇ ×₁ id ∘ (x ×₁ y) ×₁ z ∘ Δ ×₁ id ∘ Δ ≈⟨ refl⟩∘⟨ ×₁-+₁ ∇ id ⟩∘⟨refl ⟩ + ∇ ∘ ∇ +₁ id ∘ (x ×₁ y) ×₁ z ∘ Δ ×₁ id ∘ Δ ≈⟨ extendʳ ∇-assoc ⟩ + ∇ ∘ (id +₁ ∇ ∘ +-assocˡ) ∘ (x ×₁ y) ×₁ z ∘ Δ ×₁ id ∘ Δ ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ assocˡ≈+-assocˡ) ⟩∘⟨refl ⟨ + ∇ ∘ (id +₁ ∇ ∘ assocˡ) ∘ (x ×₁ y) ×₁ z ∘ Δ ×₁ id ∘ Δ ≈⟨ refl⟩∘⟨ pullʳ (extendʳ assocˡ∘×₁) ⟩ + ∇ ∘ id +₁ ∇ ∘ x ×₁ (y ×₁ z) ∘ assocˡ ∘ Δ ×₁ id ∘ Δ ≈⟨ refl⟩∘⟨ ×₁-+₁ id ∇ ⟩∘⟨ refl⟩∘⟨ Δ-assoc ⟨ + ∇ ∘ id ×₁ ∇ ∘ x ×₁ (y ×₁ z) ∘ id ×₁ Δ ∘ Δ ≈⟨ refl⟩∘⟨ pullˡ second∘×₁ ⟩ + ∇ ∘ x ×₁ (∇ ∘ y ×₁ z) ∘ id ×₁ Δ ∘ Δ ≈⟨ refl⟩∘⟨ pullˡ ×₁∘×₁ ⟩ + ∇ ∘ (x ∘ id) ×₁ ((∇ ∘ y ×₁ z) ∘ Δ) ∘ Δ ≈⟨ refl⟩∘⟨ ×₁-cong₂ identityʳ assoc ⟩∘⟨refl ⟩ + ∇ ∘ 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ʳ (zero-∘ʳ 𝟎⇐) ⟩∘⟨refl ⟨ + ∇ ∘ ⟨ zero⇒ {A} ∘ 𝟎⇐ , id ⟩ ∘ x ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (π₁i₂-absorbˡ zero⇒) (Equiv.sym π₂∘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ˡ (zero-∘ʳ 𝟎⇒) ⟩∘⟨refl ⟨ + ∇ ∘ ⟨ id , zero⇒ {A} ∘ 𝟎⇒ ⟩ ∘ x ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (Equiv.sym π₁∘i₁≈id) (π₂i₁-absorbˡ zero⇒) ⟩∘⟨refl ⟩ + ∇ ∘ ⟨ π₁ ∘ i₁ , π₂ ∘ i₁ ⟩ ∘ x ≈⟨ refl⟩∘⟨ g-η ⟩∘⟨refl ⟩ + ∇ ∘ i₁ ∘ x ≈⟨ cancelˡ ∇-identityʳ ⟩ + x ∎ + + ∇∘+-swap : {A : Obj} → ∇ ∘ +-swap {A} ≈ ∇ + ∇∘+-swap = begin + ∇ ∘ [ i₂ , i₁ ] ≈⟨ ∘[] ⟩ + [ ∇ ∘ i₂ , ∇ ∘ i₁ ] ≈⟨ []-cong₂ inject₂ inject₁ ⟩ + [ id , id ] ∎ + + swap∘Δ : {A : Obj} → swap {A} ∘ Δ ≈ Δ + swap∘Δ = begin + ⟨ π₂ , π₁ ⟩ ∘ Δ ≈⟨ ⟨⟩∘ ⟩ + ⟨ π₂ ∘ Δ , π₁ ∘ Δ ⟩ ≈⟨ ⟨⟩-cong₂ project₂ project₁ ⟩ + ⟨ id , id ⟩ ∎ + + +-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⇒ + isCM = record + { isMonoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = equiv + ; ∙-cong = +-cong + } + ; assoc = +-assoc + } + ; identity = +-identityˡ , +-identityʳ + } + ; comm = +-comm + } + + hom : Obj → Obj → CommutativeMonoid ℓ e + hom A B = record + { 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⟩∘⟨ (×₁-+₁ k k ⟩∘⟨refl) ⟩∘⟨refl ⟨ + ∇ ∘ (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-∘ + } |