More Preadditive Properties

TOTBWF · TOTBWF · commit ad98503bd909 · 2021-02-22T07:36:23.000-08:00
diff --git a/src/Categories/Category/Preadditive.agda b/src/Categories/Category/Preadditive.agda
@@ -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
     }
 
@@ -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
diff --git a/src/Categories/Category/Preadditive/Properties.agda b/src/Categories/Category/Preadditive/Properties.agda
@@ -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 ⟩ ∘ π₁ ∎
     }
@@ -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 ] ∎
     }
@@ -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) ⟩
@@ -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) ⟩
