diff --git a/src/Categories/Category/Preadditive.agda b/src/Categories/Category/Preadditive.agda index 2acdbab3f..49517fecb 100644 --- a/src/Categories/Category/Preadditive.agda +++ b/src/Categories/Category/Preadditive.agda @@ -1,36 +1,42 @@ {-# 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 @@ -38,7 +44,7 @@ record Preadditive {o ℓ e} (𝒞 : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) w ; _≈_ = _≈_ ; _∙_ = _+_ ; ε = 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 index fb19fc7a9..d4a5390b8 100644 --- 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) ⟩