Skip to content

Commit

Permalink
More Preadditive Properties
Browse files Browse the repository at this point in the history
  • Loading branch information
@useername @TOTBWF
useername authored and TOTBWF committed Feb 22, 2021
1 parent f08180a commit 56d37bc
Show file tree
Hide file tree
Showing 2 changed files with 92 additions and 36 deletions.
112 changes: 86 additions & 26 deletions src/Categories/Category/Preadditive.agda
View file
Original file line number Diff line number Diff line change
@@ -1,44 +1,50 @@
{-# OPTIONS --without-K --safe #-}

module Categories.Category.Preadditive where
open import Categories.Category

module Categories.Category.Preadditive {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level
open import Function using (_$_)

open import Algebra.Structures
open import Algebra.Bundles
import Algebra.Properties.AbelianGroup as AbGroupₚ renaming (⁻¹-injective to -‿injective)
open import Algebra.Core

open import Categories.Category
open import Categories.Morphism.Reasoning 𝒞

import Categories.Morphism.Reasoning as MR
open Category 𝒞
open HomReasoning

private
variable
A B C D X : Obj
f g h : A ⇒ B

record Preadditive {o ℓ e} (𝒞 : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
open Category 𝒞
open HomReasoning
open MR 𝒞
record Preadditive : Set (o ⊔ ℓ ⊔ e) where

infixl 7 _+_
infixl 6 _-_
infix 8 -_

field
_+_ : ∀ {A B} → Op₂ (A ⇒ B)
0H : ∀ {A B} → A ⇒ B
neg : ∀ {A B} → Op₁ (A ⇒ B)
HomIsAbGroup : ∀ (A B : Obj) → IsAbelianGroup (_≈_ {A} {B}) _+_ 0H neg
-_ : ∀ {A B} → Op₁ (A ⇒ B)
HomIsAbGroup : ∀ (A B : Obj) → IsAbelianGroup (_≈_ {A} {B}) _+_ 0H -_
+-resp-∘ : ∀ {A B C D} {f g : B ⇒ C} {h : A ⇒ B} {k : C ⇒ D} → k ∘ (f + g) ∘ h ≈ (k ∘ f ∘ h) + (k ∘ g ∘ h)

_-_ : ∀ {A B} → Op₂ (A ⇒ B)
f - g = f + neg g
f - g = f + - g

HomAbGroup : ∀ (A B : Obj) → AbelianGroup ℓ e
HomAbGroup A B = record
{ Carrier = A ⇒ B
; _≈_ = _≈_
; _∙_ = _+_
; ε = 0H
; _⁻¹ = neg
; _⁻¹ = -_
; isAbelianGroup = HomIsAbGroup A B
}

Expand All @@ -59,46 +65,100 @@ record Preadditive {o ℓ e} (𝒞 : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) w
module HomAbGroupₚ {A B : Obj} = AbGroupₚ (HomAbGroup A B)

open HomAbGroup public
open HomAbGroupₚ public

--------------------------------------------------------------------------------
-- Reasoning Combinators

+-elimˡ : f ≈ 0H → f + g ≈ g
+-elimˡ {f = f} {g = g} eq = +-congʳ eq ○ +-identityˡ g

+-introˡ : f ≈ 0H → g ≈ f + g
+-introˡ eq = ⟺ (+-elimˡ eq)

+-resp-∘ˡ : ∀ {A B C} {f g : A ⇒ B} {h : B ⇒ C} → h ∘ (f + g) ≈ (h ∘ f) + (h ∘ g)
+-elimʳ : g ≈ 0H → f + g ≈ f
+-elimʳ {g = g} {f = f} eq = +-congˡ eq ○ +-identityʳ f

+-introʳ : g ≈ 0H → f ≈ f + g
+-introʳ eq = ⟺ (+-elimʳ eq)

--------------------------------------------------------------------------------
-- Properties of _+_

+-resp-∘ˡ : ∀ {f g : A ⇒ B} {h : B ⇒ C} → h ∘ (f + g) ≈ (h ∘ f) + (h ∘ g)
+-resp-∘ˡ {f = f} {g = g} {h = h} = begin
h ∘ (f + g) ≈˘⟨ ∘-resp-≈ʳ identityʳ ⟩
h ∘ (f + g) ∘ id ≈⟨ +-resp-∘ ⟩
h ∘ f ∘ id + h ∘ g ∘ id ≈⟨ +-cong (∘-resp-≈ʳ identityʳ) (∘-resp-≈ʳ identityʳ) ⟩
h ∘ f + h ∘ g ∎

+-resp-∘ʳ : ∀ {A B C} {h : A ⇒ B} {f g : B ⇒ C} → (f + g) ∘ h ≈ (f ∘ h) + (g ∘ h)
+-resp-∘ʳ : ∀ {h : A ⇒ B} {f g : B ⇒ C} → (f + g) ∘ h ≈ (f ∘ h) + (g ∘ h)
+-resp-∘ʳ {h = h} {f = f} {g = g} = begin
(f + g) ∘ h ≈˘⟨ identityˡ ⟩
id ∘ (f + g) ∘ h ≈⟨ +-resp-∘ ⟩
id ∘ f ∘ h + id ∘ g ∘ h ≈⟨ +-cong identityˡ identityˡ ⟩
f ∘ h + g ∘ h ∎
f ∘ h + g ∘ h ∎

0-resp-∘ : ∀ {A B C D} {f : C ⇒ D} {g : A ⇒ B} → f ∘ 0H {B} {C} ∘ g ≈ 0H
--------------------------------------------------------------------------------
-- Properties of 0

0-resp-∘ : ∀ {f : C ⇒ D} {g : A ⇒ B} → f ∘ 0H {B} {C} ∘ g ≈ 0H
0-resp-∘ {f = f} {g = g} = begin
f ∘ 0H ∘ g ≈˘⟨ +-identityʳ (f ∘ 0H ∘ g) ⟩
(f ∘ 0H ∘ g + 0H) ≈˘⟨ +-congˡ (-‿inverseʳ (f ∘ 0H ∘ g)) ⟩
(f ∘ 0H ∘ g) + ((f ∘ 0H ∘ g) - (f ∘ 0H ∘ g)) ≈˘⟨ +-assoc (f ∘ 0H ∘ g) (f ∘ 0H ∘ g) (neg (f ∘ 0H ∘ g)) ⟩
(f ∘ 0H ∘ g) + ((f ∘ 0H ∘ g) - (f ∘ 0H ∘ g)) ≈˘⟨ +-assoc (f ∘ 0H ∘ g) (f ∘ 0H ∘ g) (- (f ∘ 0H ∘ g)) ⟩
(f ∘ 0H ∘ g) + (f ∘ 0H ∘ g) - (f ∘ 0H ∘ g) ≈˘⟨ +-congʳ +-resp-∘ ⟩
(f ∘ (0H + 0H) ∘ g) - (f ∘ 0H ∘ g) ≈⟨ +-congʳ (refl⟩∘⟨ +-identityʳ 0H ⟩∘⟨refl) ⟩
(f ∘ 0H ∘ g) - (f ∘ 0H ∘ g) ≈⟨ -‿inverseʳ (f ∘ 0H ∘ g) ⟩
0H ∎
0H ∎

0-resp-∘ˡ : ∀ {A B C} {f : A ⇒ B} → 0H ∘ f ≈ 0H {A} {C}
0-resp-∘ˡ {f = f} = begin
0H ∘ f ≈˘⟨ identityˡ ⟩
id ∘ 0H ∘ f ≈⟨ 0-resp-∘ ⟩
0H ∎
0H ∎

0-resp-∘ʳ : ∀ {A B C} {f : B ⇒ C} → f ∘ 0H ≈ 0H {A} {C}
0-resp-∘ʳ : f ∘ 0H ≈ 0H {A} {C}
0-resp-∘ʳ {f = f} = begin
f ∘ 0H ≈˘⟨ refl⟩∘⟨ identityʳ ⟩
f ∘ 0H ∘ id ≈⟨ 0-resp-∘ ⟩
0H ∎

-- Some helpful reasoning combinators
+-elimˡ : ∀ {X Y} {f g : X ⇒ Y} → f ≈ 0H → f + g ≈ g
+-elimˡ {f = f} {g = g} eq = +-congʳ eq ○ +-identityˡ g
0H ∎

--------------------------------------------------------------------------------
-- Properties of -_

-‿resp-∘ : f ∘ (- g) ∘ h ≈ - (f ∘ g ∘ h)
-‿resp-∘ {f = f} {g = g} {h = h} = inverseˡ-unique (f ∘ (- g) ∘ h) (f ∘ g ∘ h) $ begin
(f ∘ (- g) ∘ h) + (f ∘ g ∘ h) ≈˘⟨ +-resp-∘ ⟩
f ∘ (- g + g) ∘ h ≈⟨ refl⟩∘⟨ -‿inverseˡ g ⟩∘⟨refl ⟩
f ∘ 0H ∘ h ≈⟨ 0-resp-∘ ⟩
0H ∎

-‿resp-∘ˡ : (- f) ∘ g ≈ - (f ∘ g)
-‿resp-∘ˡ {f = f} {g = g} = begin
(- f) ∘ g ≈˘⟨ identityˡ ⟩
id ∘ (- f) ∘ g ≈⟨ -‿resp-∘ ⟩
- (id ∘ f ∘ g) ≈⟨ -‿cong identityˡ ⟩
- (f ∘ g) ∎

-‿resp-∘ʳ : f ∘ (- g) ≈ - (f ∘ g)
-‿resp-∘ʳ {f = f} {g = g} = begin
f ∘ (- g) ≈˘⟨ refl⟩∘⟨ identityʳ ⟩
f ∘ (- g) ∘ id ≈⟨ -‿resp-∘ ⟩
- (f ∘ g ∘ id) ≈⟨ -‿cong (refl⟩∘⟨ identityʳ) ⟩
- (f ∘ g) ∎

-‿idˡ : (- id) ∘ f ≈ - f
-‿idˡ {f = f} = begin
(- id) ∘ f ≈˘⟨ identityˡ ⟩
id ∘ (- id) ∘ f ≈⟨ -‿resp-∘ ⟩
- (id ∘ id ∘ f) ≈⟨ -‿cong (identityˡ ○ identityˡ) ⟩
- f ∎

neg-id-∘ʳ : f ∘ (- id) ≈ - f
neg-id-∘ʳ {f = f} = begin
f ∘ (- id) ≈˘⟨ refl⟩∘⟨ identityʳ ⟩
f ∘ (- id) ∘ id ≈⟨ -‿resp-∘ ⟩
- (f ∘ id ∘ id) ≈⟨ -‿cong (pullˡ identityʳ ○ identityʳ) ⟩
- f ∎

+-elimʳ : ∀ {X Y} {f g : X ⇒ Y} → g ≈ 0H → f + g ≈ f
+-elimʳ {f = f} {g = g} eq = +-congˡ eq ○ +-identityʳ f
16 changes: 6 additions & 10 deletions src/Categories/Category/Preadditive/Properties.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,10 +84,8 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (preadditive : Preadditive 𝒞) wh
; π₂∘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-∘ʳ) ⟩
⟨ id , 0H ⟩ ∘ 0H ∘ π₂ ≈⟨ 0-resp-∘ ⟩
0H ≈˘⟨ 0-resp-∘ ⟩
⟨ 0H , id ⟩ ∘ 0H ∘ π₁ ≈⟨ push-center project₂ ⟩
⟨ 0H , id ⟩ ∘ π₂ ∘ ⟨ id , 0H ⟩ ∘ π₁ ∎
}
Expand Down Expand Up @@ -143,10 +141,8 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (preadditive : Preadditive 𝒞) wh
; π₂∘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 ∘ [ 0H , id ] ≈⟨ 0-resp-∘ ⟩
0H ≈˘⟨ 0-resp-∘ ⟩
i₂ ∘ 0H ∘ [ id , 0H ] ≈⟨ push-center inject₁ ⟩
i₂ ∘ [ 0H , id ] ∘ i₁ ∘ [ id , 0H ] ∎
}
Expand Down Expand Up @@ -231,7 +227,7 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (preadditive : Preadditive 𝒞) wh
p₁∘i₂≈0 = begin
p₁ ∘ i₂ ≈˘⟨ +-identityʳ (p₁ ∘ i₂) ⟩
p₁ ∘ i₂ + 0H ≈˘⟨ +-congˡ (-‿inverseʳ (p₁ ∘ i₂)) ⟩
p₁ ∘ i₂ + (p₁ ∘ i₂ - p₁ ∘ i₂) ≈˘⟨ +-assoc (p₁ ∘ i₂) (p₁ ∘ i₂) (neg (p₁ ∘ i₂)) ⟩
p₁ ∘ i₂ + (p₁ ∘ i₂ - p₁ ∘ i₂) ≈˘⟨ +-assoc (p₁ ∘ i₂) (p₁ ∘ i₂) (- (p₁ ∘ i₂)) ⟩
(p₁ ∘ i₂) + (p₁ ∘ i₂) - p₁ ∘ i₂ ≈⟨ +-congʳ (+-cong (intro-first p₁∘i₁≈id) (intro-last p₂∘i₂≈id)) ⟩
(p₁ ∘ (i₁ ∘ p₁) ∘ i₂) + (p₁ ∘ (i₂ ∘ p₂) ∘ i₂) - (p₁ ∘ i₂) ≈˘⟨ +-congʳ +-resp-∘ ⟩
(p₁ ∘ (i₁ ∘ p₁ + i₂ ∘ p₂) ∘ i₂) - (p₁ ∘ i₂) ≈⟨ +-congʳ (elim-center +-eq) ⟩
Expand All @@ -242,7 +238,7 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (preadditive : Preadditive 𝒞) wh
p₂∘i₁≈0 = begin
(p₂ ∘ i₁) ≈˘⟨ +-identityʳ (p₂ ∘ i₁) ⟩
p₂ ∘ i₁ + 0H ≈˘⟨ +-congˡ (-‿inverseʳ (p₂ ∘ i₁)) ⟩
(p₂ ∘ i₁) + (p₂ ∘ i₁ - p₂ ∘ i₁) ≈˘⟨ +-assoc (p₂ ∘ i₁) (p₂ ∘ i₁) (neg (p₂ ∘ i₁)) ⟩
(p₂ ∘ i₁) + (p₂ ∘ i₁ - p₂ ∘ i₁) ≈˘⟨ +-assoc (p₂ ∘ i₁) (p₂ ∘ i₁) (- (p₂ ∘ i₁)) ⟩
(p₂ ∘ i₁) + (p₂ ∘ i₁) - (p₂ ∘ i₁) ≈⟨ +-congʳ (+-cong (intro-last p₁∘i₁≈id) (intro-first p₂∘i₂≈id)) ⟩
(p₂ ∘ (i₁ ∘ p₁) ∘ i₁) + (p₂ ∘ (i₂ ∘ p₂) ∘ i₁) - (p₂ ∘ i₁) ≈˘⟨ +-congʳ +-resp-∘ ⟩
(p₂ ∘ (i₁ ∘ p₁ + i₂ ∘ p₂) ∘ i₁) - (p₂ ∘ i₁) ≈⟨ +-congʳ (elim-center +-eq) ⟩
Expand Down

0 comments on commit 56d37bc

Please sign in to comment.