diff --git a/src/Categories/Category/Preadditive.agda b/src/Categories/Category/Preadditive.agda new file mode 100644 index 000000000..49517fecb --- /dev/null +++ b/src/Categories/Category/Preadditive.agda @@ -0,0 +1,164 @@ +{-# OPTIONS --without-K --safe #-} + +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.Morphism.Reasoning 𝒞 + +open Category 𝒞 +open HomReasoning + +private + variable + A B C D X : Obj + f g h : A ⇒ B + +record Preadditive : Set (o ⊔ ℓ ⊔ e) where + + infixl 7 _+_ + infixl 6 _-_ + infix 8 -_ + + field + _+_ : ∀ {A B} → Op₂ (A ⇒ B) + 0H : ∀ {A B} → A ⇒ B + -_ : ∀ {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 + - g + + HomAbGroup : ∀ (A B : Obj) → AbelianGroup ℓ e + HomAbGroup A B = record + { Carrier = A ⇒ B + ; _≈_ = _≈_ + ; _∙_ = _+_ + ; ε = 0H + ; _⁻¹ = -_ + ; isAbelianGroup = HomIsAbGroup A B + } + + module HomAbGroup {A B : Obj} = IsAbelianGroup (HomIsAbGroup A B) + using () + renaming + (assoc to +-assoc + ; identityˡ to +-identityˡ + ; identityʳ to +-identityʳ + ; inverseˡ to -‿inverseˡ + ; inverseʳ to -‿inverseʳ + ; comm to +-comm + ; ∙-cong to +-cong + ; ∙-congˡ to +-congˡ + ; ∙-congʳ to +-congʳ + ; ⁻¹-cong to -‿cong + ) + 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) + + +-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-∘ʳ : ∀ {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 ∎ + + -------------------------------------------------------------------------------- + -- 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) (- (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 ∎ + + 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 ∎ + + 0-resp-∘ʳ : f ∘ 0H ≈ 0H {A} {C} + 0-resp-∘ʳ {f = f} = begin + f ∘ 0H ≈˘⟨ refl⟩∘⟨ identityʳ ⟩ + f ∘ 0H ∘ id ≈⟨ 0-resp-∘ ⟩ + 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 ∎ + diff --git a/src/Categories/Category/Preadditive/Properties.agda b/src/Categories/Category/Preadditive/Properties.agda new file mode 100644 index 000000000..2609b08a4 --- /dev/null +++ b/src/Categories/Category/Preadditive/Properties.agda @@ -0,0 +1,251 @@ +{-# OPTIONS --without-K --safe #-} + +module Categories.Category.Preadditive.Properties where + +open import Categories.Category +open import Categories.Category.Preadditive + +open import Categories.Object.Initial +open import Categories.Object.Terminal +open import Categories.Object.Biproduct +open import Categories.Object.Coproduct +open import Categories.Object.Product +open import Categories.Object.Zero + +import Categories.Morphism.Reasoning as MR + +module _ {o ℓ e} {𝒞 : Category o ℓ e} (preadditive : Preadditive 𝒞) where + open Category 𝒞 + open HomReasoning + open Preadditive preadditive + + open MR 𝒞 + + Initial⇒Zero : Initial 𝒞 → Zero 𝒞 + Initial⇒Zero initial = record + { 𝟘 = ⊥ + ; isZero = record + { isInitial = ⊥-is-initial + ; isTerminal = record + { ! = 0H + ; !-unique = λ f → begin + 0H ≈˘⟨ 0-resp-∘ˡ ⟩ + 0H ∘ f ≈⟨ !-unique₂ 0H id ⟩∘⟨refl ⟩ + id ∘ f ≈⟨ identityˡ ⟩ + f ∎ + } + } + } + where + open Initial initial + + Terminal⇒Zero : Terminal 𝒞 → Zero 𝒞 + Terminal⇒Zero terminal = record + { 𝟘 = ⊤ + ; isZero = record + { isInitial = record + { ! = 0H + ; !-unique = λ f → begin + 0H ≈˘⟨ 0-resp-∘ʳ ⟩ + f ∘ 0H ≈⟨ refl⟩∘⟨ !-unique₂ ⟩ + f ∘ id ≈⟨ identityʳ ⟩ + f ∎ + } + ; isTerminal = ⊤-is-terminal + } + } + where + open Terminal terminal + + Product⇒Biproduct : ∀ {A B} → Product 𝒞 A B → Biproduct 𝒞 A B + Product⇒Biproduct product = record + { i₁ = ⟨ id , 0H ⟩ + ; i₂ = ⟨ 0H , id ⟩ + ; isBiproduct = record + { isCoproduct = record + { [_,_] = λ f g → (f ∘ π₁) + (g ∘ π₂) + ; inject₁ = λ {C} {f} {g} → begin + (f ∘ π₁ + g ∘ π₂) ∘ ⟨ id , 0H ⟩ ≈⟨ +-resp-∘ʳ ⟩ + ((f ∘ π₁) ∘ ⟨ id , 0H ⟩) + ((g ∘ π₂) ∘ ⟨ id , 0H ⟩) ≈⟨ +-cong (cancelʳ project₁) (pullʳ project₂) ⟩ + f + (g ∘ 0H) ≈⟨ +-elimʳ 0-resp-∘ʳ ⟩ + f ∎ + ; inject₂ = λ {C} {f} {g} → begin + (f ∘ π₁ + g ∘ π₂) ∘ ⟨ 0H , id ⟩ ≈⟨ +-resp-∘ʳ ⟩ + ((f ∘ π₁) ∘ ⟨ 0H , id ⟩) + ((g ∘ π₂) ∘ ⟨ 0H , id ⟩) ≈⟨ +-cong (pullʳ project₁) (cancelʳ project₂) ⟩ + (f ∘ 0H) + g ≈⟨ +-elimˡ 0-resp-∘ʳ ⟩ + g ∎ + ; unique = λ {X} {h} {f} {g} eq₁ eq₂ → begin + (f ∘ π₁) + (g ∘ π₂) ≈⟨ +-cong (pushˡ (⟺ eq₁)) (pushˡ (⟺ eq₂)) ⟩ + (h ∘ ⟨ id , 0H ⟩ ∘ π₁) + (h ∘ ⟨ 0H , id ⟩ ∘ π₂) ≈˘⟨ +-resp-∘ˡ ⟩ + h ∘ (⟨ id , 0H ⟩ ∘ π₁ + ⟨ 0H , id ⟩ ∘ π₂) ≈⟨ refl⟩∘⟨ +-cong ∘-distribʳ-⟨⟩ ∘-distribʳ-⟨⟩ ⟩ + h ∘ (⟨ id ∘ π₁ , 0H ∘ π₁ ⟩ + ⟨ 0H ∘ π₂ , id ∘ π₂ ⟩) ≈⟨ refl⟩∘⟨ +-cong (⟨⟩-cong₂ identityˡ 0-resp-∘ˡ) (⟨⟩-cong₂ 0-resp-∘ˡ identityˡ) ⟩ + h ∘ (⟨ π₁ , 0H ⟩ + ⟨ 0H , π₂ ⟩) ≈⟨ elimʳ (⟺ (unique′ π₁-lemma π₂-lemma)) ⟩ + h ∎ + } + ; isProduct = Product⇒IsProduct 𝒞 product + ; π₁∘i₁≈id = project₁ + ; π₂∘i₂≈id = project₂ + ; permute = begin + ⟨ id , 0H ⟩ ∘ π₁ ∘ ⟨ 0H , id ⟩ ∘ π₂ ≈⟨ pull-center project₁ ⟩ + ⟨ id , 0H ⟩ ∘ 0H ∘ π₂ ≈⟨ 0-resp-∘ ⟩ + 0H ≈˘⟨ 0-resp-∘ ⟩ + ⟨ 0H , id ⟩ ∘ 0H ∘ π₁ ≈⟨ push-center project₂ ⟩ + ⟨ 0H , id ⟩ ∘ π₂ ∘ ⟨ id , 0H ⟩ ∘ π₁ ∎ + } + } + where + open Product 𝒞 product + + π₁-lemma : π₁ ∘ id ≈ π₁ ∘ (⟨ π₁ , 0H ⟩ + ⟨ 0H , π₂ ⟩) + π₁-lemma = begin + π₁ ∘ id ≈⟨ identityʳ ⟩ + π₁ ≈˘⟨ +-identityʳ π₁ ⟩ + π₁ + 0H ≈⟨ +-cong (⟺ project₁) (⟺ project₁) ⟩ + (π₁ ∘ ⟨ π₁ , 0H ⟩) + (π₁ ∘ ⟨ 0H , π₂ ⟩) ≈˘⟨ +-resp-∘ˡ ⟩ + π₁ ∘ (⟨ π₁ , 0H ⟩ + ⟨ 0H , π₂ ⟩) ∎ + + π₂-lemma : π₂ ∘ id ≈ π₂ ∘ (⟨ π₁ , 0H ⟩ + ⟨ 0H , π₂ ⟩) + π₂-lemma = begin + π₂ ∘ id ≈⟨ identityʳ ⟩ + π₂ ≈˘⟨ +-identityˡ π₂ ⟩ + 0H + π₂ ≈⟨ +-cong (⟺ project₂) (⟺ project₂) ⟩ + (π₂ ∘ ⟨ π₁ , 0H ⟩) + (π₂ ∘ ⟨ 0H , π₂ ⟩) ≈˘⟨ +-resp-∘ˡ ⟩ + π₂ ∘ (⟨ π₁ , 0H ⟩ + ⟨ 0H , π₂ ⟩) ∎ + + Coproduct⇒Biproduct : ∀ {A B} → Coproduct 𝒞 A B → Biproduct 𝒞 A B + Coproduct⇒Biproduct coproduct = record + { π₁ = [ id , 0H ] + ; π₂ = [ 0H , id ] + ; isBiproduct = record + { isCoproduct = Coproduct⇒IsCoproduct 𝒞 coproduct + ; isProduct = record + { ⟨_,_⟩ = λ f g → (i₁ ∘ f) + (i₂ ∘ g) + ; project₁ = λ {C} {f} {g} → begin + [ id , 0H ] ∘ (i₁ ∘ f + i₂ ∘ g) ≈⟨ +-resp-∘ˡ ⟩ + ([ id , 0H ] ∘ i₁ ∘ f) + ([ id , 0H ] ∘ i₂ ∘ g) ≈⟨ +-cong (cancelˡ inject₁) (pullˡ inject₂) ⟩ + f + (0H ∘ g) ≈⟨ +-elimʳ 0-resp-∘ˡ ⟩ + f ∎ + ; project₂ = λ {C} {f} {g} → begin + [ 0H , id ] ∘ (i₁ ∘ f + i₂ ∘ g) ≈⟨ +-resp-∘ˡ ⟩ + ([ 0H , id ] ∘ i₁ ∘ f) + ([ 0H , id ] ∘ i₂ ∘ g) ≈⟨ +-cong (pullˡ inject₁) (cancelˡ inject₂) ⟩ + (0H ∘ f) + g ≈⟨ +-elimˡ 0-resp-∘ˡ ⟩ + g ∎ + ; unique = λ {X} {h} {f} {g} eq₁ eq₂ → begin + (i₁ ∘ f) + (i₂ ∘ g) ≈⟨ +-cong (pushʳ (⟺ eq₁)) (pushʳ (⟺ eq₂)) ⟩ + (i₁ ∘ [ id , 0H ]) ∘ h + (i₂ ∘ [ 0H , id ]) ∘ h ≈˘⟨ +-resp-∘ʳ ⟩ + (i₁ ∘ [ id , 0H ] + i₂ ∘ [ 0H , id ]) ∘ h ≈⟨ +-cong ∘-distribˡ-[] ∘-distribˡ-[] ⟩∘⟨refl ⟩ + ([ i₁ ∘ id , i₁ ∘ 0H ] + [ i₂ ∘ 0H , i₂ ∘ id ]) ∘ h ≈⟨ +-cong ([]-cong₂ identityʳ 0-resp-∘ʳ) ([]-cong₂ 0-resp-∘ʳ identityʳ) ⟩∘⟨refl ⟩ + ([ i₁ , 0H ] + [ 0H , i₂ ]) ∘ h ≈⟨ elimˡ (⟺ (unique′ i₁-lemma i₂-lemma)) ⟩ + h ∎ + } + ; π₁∘i₁≈id = inject₁ + ; π₂∘i₂≈id = inject₂ + ; permute = begin + i₁ ∘ [ id , 0H ] ∘ i₂ ∘ [ 0H , id ] ≈⟨ pull-center inject₂ ⟩ + i₁ ∘ 0H ∘ [ 0H , id ] ≈⟨ 0-resp-∘ ⟩ + 0H ≈˘⟨ 0-resp-∘ ⟩ + i₂ ∘ 0H ∘ [ id , 0H ] ≈⟨ push-center inject₁ ⟩ + i₂ ∘ [ 0H , id ] ∘ i₁ ∘ [ id , 0H ] ∎ + } + } + where + open Coproduct coproduct + + i₁-lemma : id ∘ i₁ ≈ ([ i₁ , 0H ] + [ 0H , i₂ ]) ∘ i₁ + i₁-lemma = begin + id ∘ i₁ ≈⟨ identityˡ ⟩ + i₁ ≈˘⟨ +-identityʳ i₁ ⟩ + i₁ + 0H ≈⟨ +-cong (⟺ inject₁) (⟺ inject₁) ⟩ + [ i₁ , 0H ] ∘ i₁ + [ 0H , i₂ ] ∘ i₁ ≈˘⟨ +-resp-∘ʳ ⟩ + ([ i₁ , 0H ] + [ 0H , i₂ ]) ∘ i₁ ∎ + + i₂-lemma : id ∘ i₂ ≈ ([ i₁ , 0H ] + [ 0H , i₂ ]) ∘ i₂ + i₂-lemma = begin + id ∘ i₂ ≈⟨ identityˡ ⟩ + i₂ ≈˘⟨ +-identityˡ i₂ ⟩ + 0H + i₂ ≈⟨ +-cong (⟺ inject₂) (⟺ inject₂) ⟩ + [ i₁ , 0H ] ∘ i₂ + [ 0H , i₂ ] ∘ i₂ ≈˘⟨ +-resp-∘ʳ ⟩ + ([ i₁ , 0H ] + [ 0H , i₂ ]) ∘ i₂ ∎ + + -- FIXME: Show the other direction, and bundle up all of this junk into a record + -- Our version of biproducts coincide with those found in Maclane's "Categories For the Working Mathematician", VIII.2, + -- and Borceux's "Handbook of Categorical Algebra, Volume 2", 1.2.4 + Biproduct⇒Preadditive : ∀ {A B X} {p₁ : X ⇒ A} {p₂ : X ⇒ B} {i₁ : A ⇒ X} {i₂ : B ⇒ X} + → p₁ ∘ i₁ ≈ id + → p₂ ∘ i₂ ≈ id + → (i₁ ∘ p₁) + (i₂ ∘ p₂) ≈ id + → Biproduct 𝒞 A B + Biproduct⇒Preadditive {A} {B} {X} {p₁} {p₂} {i₁} {i₂} p₁∘i₁≈id p₂∘i₂≈id +-eq = record + { π₁ = p₁ + ; π₂ = p₂ + ; i₁ = i₁ + ; i₂ = i₂ + ; isBiproduct = record + { isCoproduct = record + { [_,_] = λ f g → (f ∘ p₁) + (g ∘ p₂) + ; inject₁ = λ {C} {f} {g} → begin + (f ∘ p₁ + g ∘ p₂) ∘ i₁ ≈⟨ +-resp-∘ʳ ⟩ + ((f ∘ p₁) ∘ i₁) + ((g ∘ p₂) ∘ i₁) ≈⟨ +-cong (cancelʳ p₁∘i₁≈id) (pullʳ p₂∘i₁≈0) ⟩ + f + (g ∘ 0H) ≈⟨ +-elimʳ 0-resp-∘ʳ ⟩ + f ∎ + ; inject₂ = λ {C} {f} {g} → begin + (f ∘ p₁ + g ∘ p₂) ∘ i₂ ≈⟨ +-resp-∘ʳ ⟩ + ((f ∘ p₁) ∘ i₂) + ((g ∘ p₂) ∘ i₂) ≈⟨ +-cong (pullʳ p₁∘i₂≈0) (cancelʳ p₂∘i₂≈id) ⟩ + (f ∘ 0H) + g ≈⟨ +-elimˡ 0-resp-∘ʳ ⟩ + g ∎ + ; unique = λ {X} {h} {f} {g} eq₁ eq₂ → begin + (f ∘ p₁) + (g ∘ p₂) ≈⟨ +-cong (pushˡ (⟺ eq₁)) (pushˡ (⟺ eq₂)) ⟩ + (h ∘ i₁ ∘ p₁) + (h ∘ i₂ ∘ p₂) ≈˘⟨ +-resp-∘ˡ ⟩ + h ∘ (i₁ ∘ p₁ + i₂ ∘ p₂) ≈⟨ elimʳ +-eq ⟩ + h ∎ + } + ; isProduct = record + { ⟨_,_⟩ = λ f g → (i₁ ∘ f) + (i₂ ∘ g) + ; project₁ = λ {C} {f} {g} → begin + p₁ ∘ (i₁ ∘ f + i₂ ∘ g) ≈⟨ +-resp-∘ˡ ⟩ + (p₁ ∘ i₁ ∘ f) + (p₁ ∘ i₂ ∘ g) ≈⟨ +-cong (cancelˡ p₁∘i₁≈id) (pullˡ p₁∘i₂≈0) ⟩ + f + (0H ∘ g) ≈⟨ +-elimʳ 0-resp-∘ˡ ⟩ + f ∎ + ; project₂ = λ {C} {f} {g} → begin + p₂ ∘ (i₁ ∘ f + i₂ ∘ g) ≈⟨ +-resp-∘ˡ ⟩ + (p₂ ∘ i₁ ∘ f) + (p₂ ∘ i₂ ∘ g) ≈⟨ +-cong (pullˡ p₂∘i₁≈0) (cancelˡ p₂∘i₂≈id) ⟩ + (0H ∘ f) + g ≈⟨ +-elimˡ 0-resp-∘ˡ ⟩ + g ∎ + ; unique = λ {X} {h} {f} {g} eq₁ eq₂ → begin + (i₁ ∘ f) + (i₂ ∘ g) ≈⟨ +-cong (pushʳ (⟺ eq₁)) (pushʳ (⟺ eq₂)) ⟩ + ((i₁ ∘ p₁) ∘ h) + ((i₂ ∘ p₂) ∘ h) ≈˘⟨ +-resp-∘ʳ ⟩ + (i₁ ∘ p₁ + i₂ ∘ p₂) ∘ h ≈⟨ elimˡ +-eq ⟩ + h ∎ + } + ; π₁∘i₁≈id = p₁∘i₁≈id + ; π₂∘i₂≈id = p₂∘i₂≈id + ; permute = begin + i₁ ∘ p₁ ∘ i₂ ∘ p₂ ≈⟨ pull-center p₁∘i₂≈0 ⟩ + i₁ ∘ 0H ∘ p₂ ≈⟨ 0-resp-∘ ⟩ + 0H ≈˘⟨ 0-resp-∘ ⟩ + i₂ ∘ 0H ∘ p₁ ≈⟨ push-center p₂∘i₁≈0 ⟩ + i₂ ∘ p₂ ∘ i₁ ∘ p₁ ∎ + } + } + where + p₁∘i₂≈0 : p₁ ∘ i₂ ≈ 0H + 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₂) (- (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) ⟩ + (p₁ ∘ i₂) - (p₁ ∘ i₂) ≈⟨ -‿inverseʳ (p₁ ∘ i₂) ⟩ + 0H ∎ + + p₂∘i₁≈0 : p₂ ∘ i₁ ≈ 0H + 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₁) (- (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) ⟩ + (p₂ ∘ i₁) - (p₂ ∘ i₁) ≈⟨ -‿inverseʳ (p₂ ∘ i₁) ⟩ + 0H ∎ diff --git a/src/Categories/Morphism/Normal.agda b/src/Categories/Morphism/Normal.agda index 37c5fcfc1..9a30a55f5 100644 --- a/src/Categories/Morphism/Normal.agda +++ b/src/Categories/Morphism/Normal.agda @@ -10,6 +10,7 @@ module Categories.Morphism.Normal {o ℓ e} (𝒞 : Category o ℓ e) (𝒞-Zero open import Level open import Categories.Object.Kernel 𝒞-Zero +open import Categories.Object.Cokernel 𝒞-Zero open import Categories.Object.Kernel.Properties 𝒞-Zero open import Categories.Morphism 𝒞 @@ -32,3 +33,18 @@ record NormalMonomorphism (K A : Obj) : Set (o ⊔ ℓ ⊔ e) where isNormalMonomorphism : IsNormalMonomorphism mor open IsNormalMonomorphism isNormalMonomorphism public + +record IsNormalEpimorphism {B K : Obj} (k : B ⇒ K) : Set (o ⊔ ℓ ⊔ e) where + field + {A} : Obj + arr : A ⇒ B + isCokernel : IsCokernel arr k + + open IsCokernel isCokernel public + +record NormalEpimorphism (B K : Obj) : Set (o ⊔ ℓ ⊔ e) where + field + mor : B ⇒ K + isNormalEpimorphism : IsNormalEpimorphism mor + + open IsNormalEpimorphism isNormalEpimorphism public diff --git a/src/Categories/Object/Biproduct/Properties.agda b/src/Categories/Object/Biproduct/Properties.agda new file mode 100644 index 000000000..024fd56e6 --- /dev/null +++ b/src/Categories/Object/Biproduct/Properties.agda @@ -0,0 +1,36 @@ +{-# OPTIONS --without-K --safe #-} + +module Categories.Object.Biproduct.Properties where + +open import Categories.Category +open import Categories.Object.Biproduct +open import Categories.Object.Coproduct +open import Categories.Object.Product + +module _ {o ℓ e} (𝒞 : Category o ℓ e) where + + Biproduct⇒Product : ∀ {A B} → Biproduct 𝒞 A B → Product 𝒞 A B + Biproduct⇒Product biproduct = record + { A×B = A⊕B + ; π₁ = π₁ + ; π₂ = π₂ + ; ⟨_,_⟩ = ⟨_,_⟩ + ; project₁ = project₁ + ; project₂ = project₂ + ; unique = ⟨⟩-unique + } + where + open Biproduct biproduct + + Biproduct⇒Coproduct : ∀ {A B} → Biproduct 𝒞 A B → Coproduct 𝒞 A B + Biproduct⇒Coproduct biproduct = record + { A+B = A⊕B + ; i₁ = i₁ + ; i₂ = i₂ + ; [_,_] = [_,_] + ; inject₁ = inject₁ + ; inject₂ = inject₂ + ; unique = []-unique + } + where + open Biproduct biproduct diff --git a/src/Categories/Object/Coproduct.agda b/src/Categories/Object/Coproduct.agda index c2071b2cb..1dac01bc3 100644 --- a/src/Categories/Object/Coproduct.agda +++ b/src/Categories/Object/Coproduct.agda @@ -43,6 +43,9 @@ record Coproduct (A B : Obj) : Set (o ⊔ ℓ ⊔ e) where ∘-distribˡ-[] : ∀ {f : A ⇒ C} {g : B ⇒ C} {q : C ⇒ D} → q ∘ [ f , g ] ≈ [ q ∘ f , q ∘ g ] ∘-distribˡ-[] = ⟺ $ unique (pullʳ inject₁) (pullʳ inject₂) + unique′ : f ∘ i₁ ≈ g ∘ i₁ → f ∘ i₂ ≈ g ∘ i₂ → f ≈ g + unique′ eq₁ eq₂ = ⟺ (unique eq₁ eq₂) ○ g-η + record IsCoproduct {A B A+B : Obj} (i₁ : A ⇒ A+B) (i₂ : B ⇒ A+B) : Set (o ⊔ ℓ ⊔ e) where field [_,_] : A ⇒ C → B ⇒ C → A+B ⇒ C diff --git a/src/Categories/Object/Kernel/Properties.agda b/src/Categories/Object/Kernel/Properties.agda index 571132d01..1d84b2de5 100644 --- a/src/Categories/Object/Kernel/Properties.agda +++ b/src/Categories/Object/Kernel/Properties.agda @@ -13,6 +13,8 @@ open import Categories.Diagram.Pullback.Properties 𝒞 open import Categories.Object.Kernel 𝒞-Zero open import Categories.Object.Terminal 𝒞 +open import Categories.Object.Zero.Properties + open import Categories.Morphism 𝒞 open import Categories.Morphism.Reasoning 𝒞 @@ -108,6 +110,19 @@ module _ (K : Kernel f) where universal universal-∘ ≈˘⟨ unique eq ⟩ g₂ ∎ + kernel-mono-zero : Mono f → kernel⇒ ≈ zero⇒ + kernel-mono-zero mono-f = zero-mono-factor 𝒞-Zero f kernel⇒ mono-f $ begin + f ∘ kernel⇒ ≈⟨ commute ⟩ + zero⇒ ∎ + +isKernel-zero-id : ∀ {A B} → IsKernel id (zero⇒ {A} {B}) +isKernel-zero-id = record + { commute = zero-∘ʳ id + ; universal = λ {_} {h} _ → h + ; factors = ⟺ (identityˡ) + ; unique = λ eq → ⟺ identityˡ ○ ⟺ eq + } + module _ (has-kernels : ∀ {A B} → (f : A ⇒ B) → Kernel f) where -- The kernel of a kernel is isomorphic to the zero object. diff --git a/src/Categories/Object/Zero/Properties.agda b/src/Categories/Object/Zero/Properties.agda new file mode 100644 index 000000000..19d58f7c6 --- /dev/null +++ b/src/Categories/Object/Zero/Properties.agda @@ -0,0 +1,21 @@ +{-# OPTIONS --without-K --safe #-} + + + +module Categories.Object.Zero.Properties where + +open import Categories.Category +open import Categories.Object.Zero + +import Categories.Morphism as Mor +import Categories.Morphism.Reasoning as MR + +module _ {o ℓ e} {𝒞 : Category o ℓ e} (∅ : Zero 𝒞) where + open Category 𝒞 + open HomReasoning + open Mor 𝒞 + open MR 𝒞 + open Zero ∅ + + zero-mono-factor : ∀ {X Y Z} → (f : Y ⇒ Z) → (g : X ⇒ Y) → Mono f → f ∘ g ≈ zero⇒ → g ≈ zero⇒ + zero-mono-factor f g f-mono eq = f-mono g zero⇒ (eq ○ ⟺ (zero-∘ˡ f)) diff --git a/src/Experiments/Additive.agda b/src/Experiments/Additive.agda new file mode 100644 index 000000000..d39eaa4a3 --- /dev/null +++ b/src/Experiments/Additive.agda @@ -0,0 +1,37 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category + +module Experiments.Additive {o ℓ e} (𝒞 : Category o ℓ e) where + +open import Data.Nat +open import Data.Fin +open import Data.Vec + +open import Categories.Category.Additive 𝒞 +-- open import Categories.Object.Biproduct.Indexed 𝒞 + +-- open Category 𝒞 +-- open HomReasoning +-- open Equiv + + +-- module _ {j k} {J : Set j} {K : Set k} {P : J → Obj} {Q : K → Obj} (A : IndexedBiproductOf P) (B : IndexedBiproductOf Q) where +-- private +-- module A = IndexedBiproductOf A +-- module B = IndexedBiproductOf B + +-- decompose : (A.X ⇒ B.X) → (∀ (j : J) → (k : K) → P j ⇒ Q k) +-- decompose f j k = B.π k ∘ f ∘ A.i j + +-- collect : (∀ (j : J) → (k : K) → P j ⇒ Q k) → (A.X ⇒ B.X) +-- collect f[_,_] = A.[ (λ j → B.⟨ (λ k → f[ j , k ]) ⟩) ] + +-- -- collect∘decompose : ∀ {f : A.X ⇒ B.X} → collect (decompose f) ≈ f +-- -- collect∘decompose {f = f} = B.⟨⟩-unique _ _ λ k → ⟺ (A.[]-unique _ _ λ j → assoc) + +-- -- pointwise : ∀ {f g : A.X ⇒ B.X} → (∀ (j : J) → (k : K) → B.π k ∘ f ∘ A.i j ≈ B.π k ∘ g ∘ A.i j) → f ≈ g +-- -- pointwise {f = f} {g = g} pointwise-eq = begin +-- -- f ≈˘⟨ collect∘decompose ⟩ +-- -- B.⟨ (λ k → A.[ (λ j → B.π k ∘ f ∘ A.i j) ]) ⟩ ≈⟨ B.⟨⟩-unique g _ (λ k → ⟺ (A.[]-unique _ _ (λ j → assoc ○ ⟺ (pointwise-eq j k)))) ⟩ +-- -- g ∎ diff --git a/src/Experiments/Category/Abelian.agda b/src/Experiments/Category/Abelian.agda new file mode 100644 index 000000000..7b33e9355 --- /dev/null +++ b/src/Experiments/Category/Abelian.agda @@ -0,0 +1,37 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category + +module Experiments.Category.Abelian {o ℓ e} (𝒞 : Category o ℓ e) where + +open import Level + +open import Data.Product using (Σ-syntax; _,_) + +open import Experiments.Category.Additive +open import Experiments.Category.PreAbelian + +open import Categories.Object.Zero +open import Categories.Object.Kernel +open import Categories.Object.Cokernel + +open import Categories.Morphism 𝒞 +open import Categories.Morphism.Normal 𝒞 + +open Category 𝒞 +open HomReasoning + +private + variable + A B C : Obj + f g k : A ⇒ B + +record Abelian : Set (o ⊔ ℓ ⊔ e) where + field + preAbelian : PreAbelian 𝒞 + + open PreAbelian preAbelian public + + field + mono-is-normal : ∀ {A K} {k : K ⇒ A} → Mono k → IsNormalMonomorphism 𝟎 k + epi-is-normal : ∀ {B K} {k : B ⇒ K} → Epi k → IsNormalEpimorphism 𝟎 k diff --git a/src/Experiments/Category/Abelian/Embedding/Faithful.agda b/src/Experiments/Category/Abelian/Embedding/Faithful.agda new file mode 100644 index 000000000..a70ec8eae --- /dev/null +++ b/src/Experiments/Category/Abelian/Embedding/Faithful.agda @@ -0,0 +1,154 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category +open import Experiments.Category.Abelian + +-- The Faithful Embedding Theorem for Abelian Categories +module Experiments.Category.Abelian.Embedding.Faithful {o ℓ e} {𝒜 : Category o ℓ e} (abelian : Abelian 𝒜) where + +open import Level +open import Data.Product using (_,_) + +import Relation.Binary.Reasoning.Setoid as SR + +open import Categories.Category.SubCategory +open import Categories.Category.Construction.Functors + +open import Categories.Functor +open import Categories.NaturalTransformation +open import Categories.Yoneda + +import Categories.Morphism.Reasoning as MR + +open import Categories.Category.Preadditive +open import Experiments.Category.Additive +open import Experiments.Category.Instance.AbelianGroups + +open import Experiments.Functor.Exact + +open AbelianGroupHomomorphism +open AbelianGroup + +Lex : ∀ (c′ ℓ′ : Level) → Category (o ⊔ ℓ ⊔ e ⊔ suc c′ ⊔ suc ℓ′) (o ⊔ ℓ ⊔ c′ ⊔ ℓ′) (o ⊔ c′ ⊔ ℓ′) +Lex c′ ℓ′ = FullSubCategory′ (Functors 𝒜 (AbelianGroups c′ ℓ′)) LeftExact + + +-- NOTE: I think I can do this with any functor, not just a lex functor... +LexPreadditive : ∀ (c′ ℓ′ : Level) → Preadditive (Lex c′ ℓ′) +LexPreadditive c′ ℓ′ = record + { _+_ = λ { {F , F-Lex} {G , G-Lex} α β → + let module F = Functor F + module G = Functor G + module α = NaturalTransformation α + module β = NaturalTransformation β + in ntHelper record + { η = λ A → + let open SR (setoid (G.F₀ A)) + -- Why do all of this work when we can get the combinators for freeeee + open MR (Delooping (G.F₀ A)) + in record + { ⟦_⟧ = λ fa → G.F₀ A [ ⟦ α.η A ⟧ fa ∙ ⟦ β.η A ⟧ fa ] + ; cong = λ {fa} {fb} eq → begin + G.F₀ A [ ⟦ α.η A ⟧ fa ∙ ⟦ β.η A ⟧ fa ] ≈⟨ ∙-cong (G.F₀ A) (cong (α.η A) eq) (cong (β.η A) eq) ⟩ + G.F₀ A [ ⟦ α.η A ⟧ fb ∙ ⟦ β.η A ⟧ fb ] ∎ + ; homo = λ x y → begin + G.F₀ A [ (⟦ α.η A ⟧ (F.F₀ A [ x ∙ y ])) ∙ ⟦ β.η A ⟧ (F.F₀ A [ x ∙ y ]) ] ≈⟨ ∙-cong (G.F₀ A) (homo (α.η A) x y) (homo (β.η A) x y) ⟩ + G.F₀ A [ G.F₀ A [ ⟦ α.η A ⟧ x ∙ ⟦ α.η A ⟧ y ] ∙ G.F₀ A [ ⟦ β.η A ⟧ x ∙ ⟦ β.η A ⟧ y ] ] ≈⟨ center (comm (G.F₀ A) _ _) ⟩ + G.F₀ A [ ⟦ α.η A ⟧ x ∙ G.F₀ A [ G.F₀ A [ ⟦ β.η A ⟧ x ∙ ⟦ α.η A ⟧ y ] ∙ ⟦ β.η A ⟧ y ] ] ≈⟨ pull-first (refl (G.F₀ A)) ⟩ + G.F₀ A [ G.F₀ A [ ⟦ α.η A ⟧ x ∙ ⟦ β.η A ⟧ x ] ∙ G.F₀ A [ ⟦ α.η A ⟧ y ∙ ⟦ β.η A ⟧ y ] ] ∎ + } + ; commute = λ {X} {Y} f fx → + let open SR (setoid (G.F₀ Y)) + in begin + G.F₀ Y [ ⟦ α.η Y ⟧ (⟦ F.F₁ f ⟧ fx) ∙ ⟦ β.η Y ⟧ (⟦ F.F₁ f ⟧ fx) ] ≈⟨ ∙-cong (G.F₀ Y) (α.commute f fx) (β.commute f fx) ⟩ + G.F₀ Y [ ⟦ G.F₁ f ⟧ (⟦ α.η X ⟧ fx) ∙ ⟦ G.F₁ f ⟧ (⟦ β.η X ⟧ fx) ] ≈˘⟨ homo (G.F₁ f) (⟦ α.η X ⟧ fx) (⟦ β.η X ⟧ fx) ⟩ + ⟦ G.F₁ f ⟧ (G.F₀ X [ ⟦ α.η X ⟧ fx ∙ ⟦ β.η X ⟧ fx ]) ∎ + }} + ; 0H = λ { {F , F-Lex} {G , G-Lex} → + let module F = Functor F + module G = Functor G + in ntHelper record + { η = λ A → + let open SR (setoid (G.F₀ A)) + in record + { ⟦_⟧ = λ _ → ε (G.F₀ A) + ; cong = λ _ → refl (G.F₀ A) + ; homo = λ _ _ → sym (G.F₀ A) (identityʳ (G.F₀ A) _) + } + ; commute = λ {X} {Y} f x → sym (G.F₀ Y) (ε-homo (G.F₁ f)) + }} + ; -_ = λ { {F , F-Lex} {G , G-Lex} α → + let module F = Functor F + module G = Functor G + module α = NaturalTransformation α + in ntHelper record + { η = λ A → + let open SR (setoid (G.F₀ A)) + in record + { ⟦_⟧ = λ fa → G.F₀ A [ ⟦ α.η A ⟧ fa ⁻¹] + ; cong = λ {fa} {fb} eq → begin + (G.F₀ A [ ⟦ α.η A ⟧ fa ⁻¹]) ≈⟨ ⁻¹-cong (G.F₀ A) (cong (α.η A) eq) ⟩ + (G.F₀ A [ ⟦ α.η A ⟧ fb ⁻¹]) ∎ + ; homo = λ x y → begin + G.F₀ A [ ⟦ α.η A ⟧ (F.F₀ A [ x ∙ y ]) ⁻¹] ≈⟨ ⁻¹-cong (G.F₀ A) (homo (α.η A) x y) ⟩ + (G.F₀ A [ G.F₀ A [ ⟦ α.η A ⟧ x ∙ ⟦ α.η A ⟧ y ] ⁻¹] ) ≈⟨ ⁻¹-distrib-∙ (G.F₀ A) (⟦ α.η A ⟧ x) (⟦ α.η A ⟧ y) ⟩ + G.F₀ A [ G.F₀ A [ ⟦ α.η A ⟧ x ⁻¹] ∙ G.F₀ A [ ⟦ α.η A ⟧ y ⁻¹] ] ∎ + } + ; commute = λ {X} {Y} f fx → + let open SR (setoid (G.F₀ Y)) + in begin + G.F₀ Y [ ⟦ α.η Y ⟧ (⟦ F.F₁ f ⟧ fx) ⁻¹] ≈⟨ ⁻¹-cong (G.F₀ Y) (α.commute f fx) ⟩ + G.F₀ Y [ ⟦ G.F₁ f ⟧ (⟦ α.η X ⟧ fx) ⁻¹] ≈˘⟨ ⁻¹-homo (G.F₁ f) (⟦ α.η X ⟧ fx) ⟩ + ⟦ G.F₁ f ⟧ (G.F₀ X [ ⟦ α.η X ⟧ fx ⁻¹]) ∎ + }} + ; HomIsAbGroup = λ { (F , F-Lex) (G , G-Lex) → + let module F = Functor F + module G = Functor G + in record + { isGroup = record + { isMonoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = record + { refl = λ {_} {A} _ → refl (G.F₀ A) + ; sym = λ eq {A} fx → sym (G.F₀ A) (eq fx) + ; trans = λ eq₁ eq₂ {A} fx → trans (G.F₀ A) (eq₁ fx) (eq₂ fx) + } + ; ∙-cong = λ eq₁ eq₂ {A} fx → ∙-cong (G.F₀ A) (eq₁ fx) (eq₂ fx) + } + ; assoc = λ _ _ _ {A} _ → assoc (G.F₀ A) _ _ _ + } + ; identity = (λ _ {A} _ → identityˡ (G.F₀ A) _) , (λ _ {A} _ → identityʳ (G.F₀ A) _) + } + ; inverse = (λ _ {A} _ → inverseˡ (G.F₀ A) _) , (λ _ {A} _ → inverseʳ (G.F₀ A) _) + ; ⁻¹-cong = λ eq {A} fx → ⁻¹-cong (G.F₀ A) (eq fx) + } + ; comm = λ _ _ {A} _ → comm (G.F₀ A) _ _ + }} + ; +-resp-∘ = λ { {F , F-Lex} {G , G-Lex} {H , H-Lex} {I , I-Lex} {α} {β} {γ} {δ} {A} x → + let module α = NaturalTransformation α + module β = NaturalTransformation β + module γ = NaturalTransformation γ + module δ = NaturalTransformation δ + in homo (δ.η A) (⟦ α.η A ⟧ (⟦ γ.η A ⟧ x)) (⟦ β.η A ⟧ (⟦ γ.η A ⟧ x)) + } + } + +LexAdditive : ∀ (c′ ℓ′ : Level) → Additive (Lex c′ ℓ′) +LexAdditive c′ ℓ′ = record + { preadditive = LexPreadditive c′ ℓ′ + ; 𝟎 = record + { 𝟘 = + -- This will just map to the zero object + let 𝟘F = record + { F₀ = λ _ → {!!} + ; F₁ = {!!} + ; identity = {!!} + ; homomorphism = {!!} + ; F-resp-≈ = {!!} + } + in 𝟘F , {!!} + ; isZero = {!!} + } + ; biproduct = {!!} + } diff --git a/src/Experiments/Category/Additive.agda b/src/Experiments/Category/Additive.agda new file mode 100644 index 000000000..90a274a92 --- /dev/null +++ b/src/Experiments/Category/Additive.agda @@ -0,0 +1,32 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category +open import Categories.Category.Preadditive + +module Experiments.Category.Additive {o ℓ e} (𝒞 : Category o ℓ e) where + +open import Level + +open import Categories.Object.Biproduct 𝒞 +open import Categories.Object.Zero 𝒞 + +open Category 𝒞 + +record Additive : Set (o ⊔ ℓ ⊔ e) where + + infixr 7 _⊕_ + + field + preadditive : Preadditive 𝒞 + 𝟎 : Zero + biproduct : ∀ {A B} → Biproduct A B + + open Preadditive preadditive public + + open Zero 𝟎 public + module biproduct {A} {B} = Biproduct (biproduct {A} {B}) + + _⊕_ : Obj → Obj → Obj + A ⊕ B = Biproduct.A⊕B (biproduct {A} {B}) + + open biproduct public diff --git a/src/Experiments/Category/Instance/AbelianGroups.agda b/src/Experiments/Category/Instance/AbelianGroups.agda new file mode 100644 index 000000000..c3cf908e3 --- /dev/null +++ b/src/Experiments/Category/Instance/AbelianGroups.agda @@ -0,0 +1,323 @@ +{-# OPTIONS --without-K --safe #-} +module Experiments.Category.Instance.AbelianGroups where + +open import Level +open import Function using (_$_) + +open import Data.Product using (Σ; _,_; proj₁) +open import Data.Unit using (⊤) + +open import Algebra.Core +open import Algebra.Bundles using (AbelianGroup) public +open import Algebra.Structures using (IsAbelianGroup) public +open import Algebra.Properties.AbelianGroup + +import Algebra.Definitions as Define +open import Algebra.Morphism.Structures +import Algebra.Morphism.Definitions as MorDefine + +open import Relation.Binary +import Relation.Binary.Reasoning.Setoid as SR + +open import Categories.Category +open import Categories.Functor +open import Categories.Morphism +open import Categories.Morphism.Notation + +import Categories.Morphism.Reasoning as MR + + +-- FIXME: Where should this live???? +Delooping : ∀ {c ℓ} → AbelianGroup c ℓ → Category 0ℓ c ℓ +Delooping G = record + { Obj = ⊤ + ; _⇒_ = λ _ _ → Carrier + ; _≈_ = _≈_ + ; id = ε + ; _∘_ = _∙_ + ; assoc = assoc _ _ _ + ; sym-assoc = sym (assoc _ _ _) + ; identityˡ = identityˡ _ + ; identityʳ = identityʳ _ + ; identity² = identityʳ _ + ; equiv = isEquivalence + ; ∘-resp-≈ = ∙-cong + } + where + open AbelianGroup G + + +-- FIXME: Random group properties +_[_∙_] : ∀ {c′ ℓ′} → (G : AbelianGroup c′ ℓ′) → AbelianGroup.Carrier G → AbelianGroup.Carrier G → AbelianGroup.Carrier G +_[_∙_] = AbelianGroup._∙_ + +_[_⁻¹] : ∀ {c′ ℓ′} → (G : AbelianGroup c′ ℓ′) → AbelianGroup.Carrier G → AbelianGroup.Carrier G +_[_⁻¹] = AbelianGroup._⁻¹ + +module _ {c ℓ} (G : AbelianGroup c ℓ) where + open AbelianGroup G + open SR setoid + open MR (Delooping G) + + ⁻¹-distrib-∙ : ∀ x y → (x ∙ y) ⁻¹ ≈ x ⁻¹ ∙ y ⁻¹ + ⁻¹-distrib-∙ x y = sym $ uniqueˡ-⁻¹ (x ⁻¹ ∙ y ⁻¹) (x ∙ y) $ begin + (x ⁻¹ ∙ y ⁻¹) ∙ (x ∙ y) ≈⟨ ∙-congˡ (comm x y) ⟩ + (x ⁻¹ ∙ y ⁻¹) ∙ (y ∙ x) ≈⟨ cancelInner (inverseˡ y) ⟩ + x ⁻¹ ∙ x ≈⟨ inverseˡ x ⟩ + ε ∎ + +-- The stdlib provides an annoying version of group homomorphisms, so it's easier to roll our own bundled form +record AbelianGroupHomomorphism {c c′ ℓ ℓ′} (G : AbelianGroup c ℓ) (H : AbelianGroup c′ ℓ′) : Set (c ⊔ c′ ⊔ ℓ ⊔ ℓ′) where + private + module G = AbelianGroup G + module H = AbelianGroup H + open MorDefine G.Carrier H.Carrier H._≈_ + open G using () renaming (_∙_ to _∙ᴳ_; ε to εᴳ; _⁻¹ to _⁻¹ᴳ; _≈_ to _≈ᴳ_) + open H using () renaming (_∙_ to _∙ᴴ_; ε to εᴴ; _⁻¹ to _⁻¹ᴴ; _≈_ to _≈ᴴ_) + open SR H.setoid + + field + ⟦_⟧ : G.Carrier → H.Carrier + cong : ∀ {x y} → x ≈ᴳ y → ⟦ x ⟧ ≈ᴴ ⟦ y ⟧ + homo : Homomorphic₂ ⟦_⟧ _∙ᴳ_ _∙ᴴ_ + + ε-homo : ⟦ εᴳ ⟧ ≈ᴴ εᴴ + ε-homo = begin + ⟦ εᴳ ⟧ ≈˘⟨ H.identityˡ ⟦ εᴳ ⟧ ⟩ + εᴴ ∙ᴴ ⟦ εᴳ ⟧ ≈˘⟨ H.∙-congʳ (H.inverseˡ ⟦ εᴳ ⟧) ⟩ + ⟦ εᴳ ⟧ ⁻¹ᴴ ∙ᴴ ⟦ εᴳ ⟧ ∙ᴴ ⟦ εᴳ ⟧ ≈⟨ H.assoc (⟦ εᴳ ⟧ ⁻¹ᴴ) ⟦ εᴳ ⟧ ⟦ εᴳ ⟧ ⟩ + ⟦ εᴳ ⟧ ⁻¹ᴴ ∙ᴴ (⟦ εᴳ ⟧ ∙ᴴ ⟦ εᴳ ⟧) ≈˘⟨ H.∙-congˡ (homo εᴳ εᴳ) ⟩ + ⟦ εᴳ ⟧ ⁻¹ᴴ ∙ᴴ ⟦ εᴳ ∙ᴳ εᴳ ⟧ ≈⟨ H.∙-congˡ (cong (G.identityʳ εᴳ)) ⟩ + ⟦ εᴳ ⟧ ⁻¹ᴴ ∙ᴴ ⟦ εᴳ ⟧ ≈⟨ H.inverseˡ ⟦ εᴳ ⟧ ⟩ + εᴴ ∎ + + ⁻¹-homo : ∀ x → ⟦ x ⁻¹ᴳ ⟧ ≈ᴴ ⟦ x ⟧ ⁻¹ᴴ + ⁻¹-homo x = begin + ⟦ x ⁻¹ᴳ ⟧ ≈˘⟨ H.identityˡ ⟦ x ⁻¹ᴳ ⟧ ⟩ + εᴴ ∙ᴴ ⟦ x ⁻¹ᴳ ⟧ ≈˘⟨ H.∙-congʳ (H.inverseˡ ⟦ x ⟧) ⟩ + ⟦ x ⟧ ⁻¹ᴴ ∙ᴴ ⟦ x ⟧ ∙ᴴ ⟦ x ⁻¹ᴳ ⟧ ≈⟨ H.assoc (⟦ x ⟧ ⁻¹ᴴ) ⟦ x ⟧ ⟦ x ⁻¹ᴳ ⟧ ⟩ + ⟦ x ⟧ ⁻¹ᴴ ∙ᴴ (⟦ x ⟧ ∙ᴴ ⟦ x ⁻¹ᴳ ⟧) ≈˘⟨ H.∙-congˡ (homo x (x ⁻¹ᴳ)) ⟩ + ⟦ x ⟧ ⁻¹ᴴ ∙ᴴ ⟦ x ∙ᴳ x ⁻¹ᴳ ⟧ ≈⟨ H.∙-congˡ (cong (G.inverseʳ x)) ⟩ + ⟦ x ⟧ ⁻¹ᴴ ∙ᴴ ⟦ εᴳ ⟧ ≈⟨ H.∙-congˡ ε-homo ⟩ + ⟦ x ⟧ ⁻¹ᴴ ∙ᴴ εᴴ ≈⟨ H.identityʳ (⟦ x ⟧ ⁻¹ᴴ) ⟩ + ⟦ x ⟧ ⁻¹ᴴ ∎ + +open AbelianGroupHomomorphism + +AbelianGroups : ∀ c ℓ → Category (suc c ⊔ suc ℓ) (c ⊔ ℓ) (c ⊔ ℓ) +AbelianGroups c ℓ = record + { Obj = AbelianGroup c ℓ + ; _⇒_ = AbelianGroupHomomorphism + ; _≈_ = λ {G} {H} f g → ∀ x → AbelianGroup._≈_ H (⟦ f ⟧ x) (⟦ g ⟧ x) + ; id = λ {G} → record + { ⟦_⟧ = λ x → x + ; cong = λ eq → eq + ; homo = λ x y → AbelianGroup.refl G + } + ; _∘_ = λ {G} {H} {I} f g → + let module G = AbelianGroup G + module H = AbelianGroup H + module I = AbelianGroup I + module f = AbelianGroupHomomorphism f + module g = AbelianGroupHomomorphism g + open SR I.setoid + in record + { ⟦_⟧ = λ x → f.⟦ g.⟦ x ⟧ ⟧ + ; cong = λ eq → f.cong (g.cong eq) + ; homo = λ x y → begin + f.⟦ g.⟦ x G.∙ y ⟧ ⟧ ≈⟨ f.cong (g.homo x y) ⟩ + f.⟦ g.⟦ x ⟧ H.∙ g.⟦ y ⟧ ⟧ ≈⟨ f.homo g.⟦ x ⟧ g.⟦ y ⟧ ⟩ + f.⟦ g.⟦ x ⟧ ⟧ I.∙ f.⟦ g.⟦ y ⟧ ⟧ ∎ + } + ; assoc = λ {G} {H} {I} {J} {f} {g} {h} x → AbelianGroup.refl J + ; sym-assoc = λ {G} {H} {I} {J} {f} {g} {h} x → AbelianGroup.refl J + ; identityˡ = λ {A} {B} {f} x → AbelianGroup.refl B + ; identityʳ = λ {A} {B} {f} x → AbelianGroup.refl B + ; identity² = λ {A} x → AbelianGroup.refl A + ; equiv = λ {A} {B} → record + { refl = λ x → AbelianGroup.refl B + ; sym = λ eq x → AbelianGroup.sym B (eq x) + ; trans = λ eq₁ eq₂ x → AbelianGroup.trans B (eq₁ x) (eq₂ x) + } + ; ∘-resp-≈ = λ {A} {B} {C} {f} {g} {h} {i} eq₁ eq₂ x → + let module C = AbelianGroup C + module f = AbelianGroupHomomorphism f + module g = AbelianGroupHomomorphism g + module h = AbelianGroupHomomorphism h + module i = AbelianGroupHomomorphism i + open SR C.setoid + in begin + f.⟦ h.⟦ x ⟧ ⟧ ≈⟨ f.cong (eq₂ x) ⟩ + f.⟦ i.⟦ x ⟧ ⟧ ≈⟨ eq₁ i.⟦ x ⟧ ⟩ + g.⟦ i.⟦ x ⟧ ⟧ ∎ + } + +-------------------------------------------------------------------------------- +-- Helper for creating abelian groups + +private + + record IsAbelianGroupHelper {c ℓ} {A : Set c} (_≈_ : Rel A ℓ) (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (c ⊔ ℓ) where + open Define _≈_ + + field + isEquivalence : IsEquivalence _≈_ + ∙-cong : Congruent₂ _∙_ + ⁻¹-cong : Congruent₁ _⁻¹ + assoc : Associative _∙_ + identityˡ : LeftIdentity ε _∙_ + inverseˡ : LeftInverse ε _⁻¹ _∙_ + comm : Commutative _∙_ + + record AbelianGroupHelper (c ℓ : Level) : Set (suc (c ⊔ ℓ)) where + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∙_ : Op₂ Carrier + ε : Carrier + _⁻¹ : Op₁ Carrier + + open Define _≈_ + + field + isEquivalence : IsEquivalence _≈_ + ∙-cong : Congruent₂ _∙_ + ⁻¹-cong : Congruent₁ _⁻¹ + assoc : Associative _∙_ + identityˡ : LeftIdentity ε _∙_ + inverseˡ : LeftInverse ε _⁻¹ _∙_ + comm : Commutative _∙_ + +isAbGroupHelper : ∀ {c ℓ} {A : Set c} {_≈_ : Rel A ℓ} {_∙_ : Op₂ A} {ε : A} {_⁻¹ : Op₁ A} + → IsAbelianGroupHelper _≈_ _∙_ ε _⁻¹ + → IsAbelianGroup _≈_ _∙_ ε _⁻¹ +isAbGroupHelper {_≈_ = _≈_} {_∙_ = _∙_} {ε = ε} {_⁻¹ = _⁻¹} helper = record + { isGroup = record + { isMonoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = isEquivalence + ; ∙-cong = ∙-cong + } + ; assoc = assoc + } + ; identity = identityˡ , (λ x → trans (comm x ε) (identityˡ x)) + } + ; inverse = inverseˡ , (λ x → trans (comm x (x ⁻¹)) (inverseˡ x)) + ; ⁻¹-cong = ⁻¹-cong + } + ; comm = comm + } + where + open IsAbelianGroupHelper helper + open IsEquivalence isEquivalence + +abGroupHelper : ∀ {c ℓ} → AbelianGroupHelper c ℓ → AbelianGroup c ℓ +abGroupHelper helper = record + { Carrier = Carrier + ; _≈_ = _≈_ + ; _∙_ = _∙_ + ; ε = ε + ; _⁻¹ = _⁻¹ + ; isAbelianGroup = record + { isGroup = record + { isMonoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = isEquivalence + ; ∙-cong = ∙-cong + } + ; assoc = assoc + } + ; identity = identityˡ , (λ x → trans (comm x ε) (identityˡ x)) + } + ; inverse = inverseˡ , (λ x → trans (comm x (x ⁻¹)) (inverseˡ x)) + ; ⁻¹-cong = ⁻¹-cong + } + ; comm = comm + } + } + where + open AbelianGroupHelper helper + open IsEquivalence isEquivalence + +module _ {c ℓ} (G : AbelianGroup c ℓ) where + open AbelianGroup G + + subgroup : ∀ {p} + → (P : Carrier → Set p) + → (∀ x y → P x → P y → P (x ∙ y)) + → P ε + → (∀ x → P x → P (x ⁻¹)) + → AbelianGroup (c ⊔ p) ℓ + subgroup P ∙-closed ε-closed ⁻¹-closed = abGroupHelper record + { Carrier = Σ Carrier P + ; _≈_ = λ { (x , _) (y , _) → x ≈ y } + ; _∙_ = λ { (x , px) (y , py) → (x ∙ y) , (∙-closed x y px py) } + ; ε = ε , ε-closed + ; _⁻¹ = λ { (x , px) → x ⁻¹ , ⁻¹-closed x px } + ; isEquivalence = record + { refl = refl + ; sym = sym + ; trans = trans + } + ; ∙-cong = ∙-cong + ; ⁻¹-cong = ⁻¹-cong + ; assoc = λ { (x , _) (y , _) (z , _) → assoc x y z } + ; identityˡ = λ { (x , _) → identityˡ x } + ; inverseˡ = λ { (x , _) → inverseˡ x } + ; comm = λ { (x , _) (y , _) → comm x y } + } + + -- TODO This is mono/injective + subgroup-inj : ∀ {p} + → {P : Carrier → Set p} + → {∙-closed : ∀ x y → P x → P y → P (x ∙ y)} + → {ε-closed : P ε} + → {⁻¹-closed : ∀ x → P x → P (x ⁻¹)} + → AbelianGroupHomomorphism (subgroup P ∙-closed ε-closed ⁻¹-closed) G + subgroup-inj = record + { ⟦_⟧ = proj₁ + ; cong = λ eq → eq + ; homo = λ x y → refl + } + +-- FIXME: Finish this stuff + + -- We don't ever want these proofs about quotient equality expanding, as they cause + -- goals to balloon in size + -- abstract + -- quot-refl : ∀ {x} → ⟦⟧ + -- quot-refl : ∀ {x} → Quot x x + -- quot-refl {x = x} = quot H.ε $ begin + -- ⟦ inj ⟧ H.ε ≈⟨ ε-homo inj ⟩ + -- G.ε ≈˘⟨ G.inverseʳ x ⟩ + -- x G.∙ x G.⁻¹ ∎ + + -- quot-sym : ∀ {x y} → Quot x y → Quot y x + -- quot-sym {x = x} {y = y} (quot witness element) = quot (witness H.⁻¹) $ begin + -- ⟦ inj ⟧ (witness H.⁻¹) ≈⟨ ⁻¹-homo inj witness ⟩ + -- ⟦ inj ⟧ witness G.⁻¹ ≈⟨ G.⁻¹-cong element ⟩ + -- (x G.∙ y G.⁻¹) G.⁻¹ ≈⟨ ⁻¹-anti-homo-∙ G x (y G.⁻¹) ⟩ + -- (y G.⁻¹) G.⁻¹ G.∙ x G.⁻¹ ≈⟨ {!!} ⟩ + -- y G.∙ x G.⁻¹ ∎ + + -- quotient : AbelianGroup c (c ⊔ ℓ) + -- quotient = abGroupHelper record + -- { Carrier = G.Carrier + -- ; _≈_ = Quot + -- ; _∙_ = G._∙_ + -- ; ε = G.ε + -- ; _⁻¹ = G._⁻¹ + -- ; isEquivalence = record + -- { refl = {!!} + -- ; sym = {!!} + -- ; trans = {!!} + -- } + -- ; ∙-cong = {!!} + -- ; ⁻¹-cong = {!!} + -- ; assoc = {!!} + -- ; identityˡ = {!!} + -- ; inverseˡ = {!!} + -- ; comm = {!!} + -- } diff --git a/src/Experiments/Category/Instance/AbelianGroups/Abelian.agda b/src/Experiments/Category/Instance/AbelianGroups/Abelian.agda new file mode 100644 index 000000000..0319fb39a --- /dev/null +++ b/src/Experiments/Category/Instance/AbelianGroups/Abelian.agda @@ -0,0 +1,143 @@ +{-# OPTIONS --without-K --safe #-} + +module Experiments.Category.Instance.AbelianGroups.Abelian where + +open import Level +open import Function using (_$_) +open import Data.Unit.Polymorphic +open import Data.Product using (Σ-syntax; _,_; _×_; proj₁; proj₂) + +import Algebra.Construct.DirectProduct as DirectProduct +open import Algebra.Properties.AbelianGroup + +import Relation.Binary.Reasoning.Setoid as SR + +open import Categories.Category.Core + +open import Categories.Object.Zero +open import Categories.Object.Kernel +open import Categories.Object.Cokernel + +import Categories.Morphism as Mor +import Categories.Morphism.Normal as NormalMor +import Categories.Morphism.Reasoning as MR + +open import Categories.Category.Preadditive +open import Categories.Category.Additive +open import Experiments.Category.PreAbelian +open import Experiments.Category.Abelian + +open import Experiments.Category.Instance.AbelianGroups +open import Experiments.Category.Instance.AbelianGroups.Preadditive +open import Experiments.Category.Instance.AbelianGroups.Additive +open import Experiments.Category.Instance.AbelianGroups.Preabelian + +private + variable + c ℓ : Level + +open AbelianGroup +open AbelianGroupHomomorphism + +module _ {c ℓ} {A K : AbelianGroup (c ⊔ ℓ) (c ⊔ ℓ)} where + private + module A = AbelianGroup A + module K = AbelianGroup K + + open Mor (AbelianGroups (c ⊔ ℓ) (c ⊔ ℓ)) + open NormalMor (AbelianGroups (c ⊔ ℓ) (c ⊔ ℓ)) + + mono-is-normal : ∀ {k : AbelianGroupHomomorphism K A} → Mono k → IsNormalMonomorphism 𝟎 k + mono-is-normal {k = k} k-mono = + let coker = cokernels {ℓ = c ⊔ ℓ} k + open Zero (𝟎 {c = c ⊔ ℓ} {ℓ = c ⊔ ℓ}) + module coker = Cokernel coker + in record + { B = coker.cokernel + ; arr = coker.cokernel⇒ + ; isKernel = record + { commute = coker.commute + ; universal = λ { {X} {h} eq → + let module X = AbelianGroup X + open SR A.setoid + open MR (Delooping A) + in record + { ⟦_⟧ = λ x → proj₁ (eq (x X.⁻¹)) + ; cong = λ {x} {y} x≈y → mono-injective {c = c ⊔ ℓ} {ℓ = c ⊔ ℓ} k k-mono $ begin + ⟦ k ⟧ (proj₁ (eq (x X.⁻¹))) ≈⟨ insertˡ (A.inverseˡ (⟦ h ⟧ (x X.⁻¹))) ⟩ + ⟦ h ⟧ (x X.⁻¹) A.⁻¹ A.∙ (⟦ h ⟧ (x X.⁻¹) A.∙ ⟦ k ⟧ (proj₁ (eq (x X.⁻¹)))) ≈⟨ elimʳ (proj₂ (eq (x X.⁻¹))) ⟩ + ⟦ h ⟧ (x X.⁻¹) A.⁻¹ ≈⟨ A.⁻¹-cong (cong h (X.⁻¹-cong x≈y)) ⟩ + ⟦ h ⟧ (y X.⁻¹) A.⁻¹ ≈⟨ introʳ (proj₂ (eq (y X.⁻¹))) ⟩ + ⟦ h ⟧ (y X.⁻¹) A.⁻¹ A.∙ (⟦ h ⟧ (y X.⁻¹) A.∙ ⟦ k ⟧ (proj₁ (eq (y X.⁻¹)))) ≈⟨ cancelˡ (A.inverseˡ (⟦ h ⟧ (y X.⁻¹))) ⟩ + ⟦ k ⟧ (proj₁ (eq (y X.⁻¹))) ∎ + ; homo = λ x y → mono-injective {c = c ⊔ ℓ} {ℓ = c ⊔ ℓ} k k-mono $ begin + ⟦ k ⟧ (proj₁ (eq ((x X.∙ y) X.⁻¹))) ≈⟨ insertˡ (A.inverseˡ (⟦ h ⟧ ((x X.∙ y) X.⁻¹))) ⟩ + ⟦ h ⟧ ((x X.∙ y) X.⁻¹) A.⁻¹ A.∙ (⟦ h ⟧ ((x X.∙ y) X.⁻¹) A.∙ ⟦ k ⟧ (proj₁ (eq ((x X.∙ y) X.⁻¹)))) ≈⟨ elimʳ (proj₂ (eq ((x X.∙ y) X.⁻¹))) ⟩ + ⟦ h ⟧ ((x X.∙ y) X.⁻¹) A.⁻¹ ≈⟨ A.⁻¹-cong (⁻¹-homo h (x X.∙ y)) ⟩ + (⟦ h ⟧ (x X.∙ y) A.⁻¹) A.⁻¹ ≈⟨ ⁻¹-involutive A (⟦ h ⟧ (x X.∙ y)) ⟩ + ⟦ h ⟧ (x X.∙ y) ≈⟨ homo h x y ⟩ + ⟦ h ⟧ x A.∙ ⟦ h ⟧ y ≈⟨ introʳ (proj₂ (eq (y X.⁻¹))) ⟩ + ⟦ h ⟧ x A.∙ ⟦ h ⟧ y A.∙ (⟦ h ⟧ (y X.⁻¹) A.∙ ⟦ k ⟧ (proj₁ (eq (y X.⁻¹)))) ≈⟨ cancelInner (A.trans (A.∙-congˡ (⁻¹-homo h y)) (A.inverseʳ (⟦ h ⟧ y))) ⟩ + ⟦ h ⟧ x A.∙ ⟦ k ⟧ (proj₁ (eq (y X.⁻¹))) ≈⟨ pushʳ (introˡ (proj₂ (eq (x X.⁻¹)))) ⟩ + ⟦ h ⟧ x A.∙ (⟦ h ⟧ (x X.⁻¹) A.∙ ⟦ k ⟧ (proj₁ (eq (x X.⁻¹)))) A.∙ ⟦ k ⟧ (proj₁ (eq (y X.⁻¹))) ≈⟨ A.∙-congʳ (cancelˡ (A.trans (A.∙-congˡ (⁻¹-homo h x)) (A.inverseʳ (⟦ h ⟧ x)))) ⟩ + ⟦ k ⟧ (proj₁ (eq (x X.⁻¹))) A.∙ ⟦ k ⟧ (proj₁ (eq (y X.⁻¹))) ≈˘⟨ homo k (proj₁ (eq (x X.⁻¹))) (proj₁ (eq (y X.⁻¹))) ⟩ + ⟦ k ⟧ (proj₁ (eq (x X.⁻¹)) K.∙ proj₁ (eq (y X.⁻¹))) ∎ + }} + ; factors = λ {X} {h} {eq} x → + let module X = AbelianGroup X + open SR A.setoid + open MR (Delooping A) + in begin + ⟦ h ⟧ x ≈⟨ insertˡ (proj₂ (eq (x X.⁻¹))) ⟩ + ⟦ h ⟧ (x X.⁻¹) A.∙ (⟦ k ⟧ (proj₁ (eq (x X.⁻¹))) A.∙ ⟦ h ⟧ x) ≈⟨ A.∙-cong (⁻¹-homo h x) (A.comm (⟦ k ⟧ (proj₁ (eq (x X.⁻¹)))) (⟦ h ⟧ x)) ⟩ + ⟦ h ⟧ x A.⁻¹ A.∙ (⟦ h ⟧ x A.∙ ⟦ k ⟧ (proj₁ (eq (x X.⁻¹)))) ≈⟨ cancelˡ (A.inverseˡ (⟦ h ⟧ x)) ⟩ + ⟦ k ⟧ (proj₁ (eq (x X.⁻¹))) ∎ + ; unique = λ {X} {h} {i} {eq} eq-hki x → + let module X = AbelianGroup X + open SR A.setoid + open MR (Delooping A) + -- FIXME: This is factors, so factor (ayoooo) this out + in mono-injective {c = c ⊔ ℓ} {ℓ = c ⊔ ℓ} k k-mono $ begin + ⟦ k ⟧ (⟦ i ⟧ x) ≈˘⟨ eq-hki x ⟩ + ⟦ h ⟧ x ≈⟨ insertˡ (proj₂ (eq (x X.⁻¹))) ⟩ + ⟦ h ⟧ (x X.⁻¹) A.∙ (⟦ k ⟧ (proj₁ (eq (x X.⁻¹))) A.∙ ⟦ h ⟧ x) ≈⟨ A.∙-cong (⁻¹-homo h x) (A.comm (⟦ k ⟧ (proj₁ (eq (x X.⁻¹)))) (⟦ h ⟧ x)) ⟩ + ⟦ h ⟧ x A.⁻¹ A.∙ (⟦ h ⟧ x A.∙ ⟦ k ⟧ (proj₁ (eq (x X.⁻¹)))) ≈⟨ cancelˡ (A.inverseˡ (⟦ h ⟧ x)) ⟩ + ⟦ k ⟧ (proj₁ (eq (x X.⁻¹))) ∎ + } + } + + epi-is-normal : ∀ {k : AbelianGroupHomomorphism A K} → Epi k → IsNormalEpimorphism 𝟎 k + epi-is-normal {k = k} k-epi = + let ker = kernels {c = c ⊔ ℓ} k + open Zero (𝟎 {c = c ⊔ ℓ} {ℓ = c ⊔ ℓ}) + module ker = Kernel ker + in record + { arr = ker.kernel⇒ + ; isCokernel = record + { commute = ker.commute + ; universal = λ {X} {h} eq → + let module X = AbelianGroup X + open SR X.setoid + -- Pick an element out of the preimage + preimage = λ x → proj₁ (epi-surjective {c = c} {ℓ = ℓ} k k-epi x) + preimage-eq = λ x → proj₂ (epi-surjective {c = c} {ℓ = ℓ} k k-epi x) + in record + { ⟦_⟧ = λ x → ⟦ h ⟧ (preimage x) + ; cong = λ {x} {y} x≈y → cong h {!!} + -- begin + -- ⟦ h ⟧ (proj₁ (epi-surjective {c = c} {ℓ = ℓ} k k-epi x)) ≈⟨ {! eq (? , ?)!} ⟩ + -- {!!} ≈⟨ {!!} ⟩ + -- ⟦ h ⟧ (proj₁ (epi-surjective {c = c} {ℓ = ℓ} k k-epi y)) ∎ + ; homo = {!!} + } + ; factors = {!!} + ; unique = {!!} + } + } + +AbelianGroupsAbelian : Abelian (AbelianGroups (c ⊔ ℓ) (c ⊔ ℓ)) +AbelianGroupsAbelian {c = c} {ℓ = ℓ} = record + { preAbelian = AbelianGroupsPreAbelian {c = c} {ℓ = ℓ} + ; mono-is-normal = mono-is-normal {c = c} {ℓ = ℓ} + ; epi-is-normal = {!!} + } diff --git a/src/Experiments/Category/Instance/AbelianGroups/Additive.agda b/src/Experiments/Category/Instance/AbelianGroups/Additive.agda new file mode 100644 index 000000000..32ba2b5d2 --- /dev/null +++ b/src/Experiments/Category/Instance/AbelianGroups/Additive.agda @@ -0,0 +1,152 @@ +{-# OPTIONS --without-K --safe #-} +module Experiments.Category.Instance.AbelianGroups.Additive where + +open import Level +open import Function using (_$_) +open import Data.Unit.Polymorphic +open import Data.Product using (Σ-syntax; _,_; _×_; proj₁; proj₂) + +import Algebra.Construct.DirectProduct as DirectProducts +import Algebra.Construct.Zero as Zeros +open import Algebra.Properties.AbelianGroup + +import Relation.Binary.Reasoning.Setoid as SR + +open import Categories.Category +open import Categories.Object.Initial +open import Categories.Object.Zero +open import Categories.Object.Biproduct + +import Categories.Morphism as Mor +import Categories.Morphism.Reasoning as MR + +open import Categories.Category.Preadditive +open import Categories.Category.Additive + +open import Experiments.Category.Instance.AbelianGroups +open import Experiments.Category.Instance.AbelianGroups.Preadditive + +private + variable + c ℓ : Level + +open AbelianGroup +open AbelianGroupHomomorphism + +𝟎 : Zero (AbelianGroups c ℓ) +𝟎 = record + { 𝟘 = Zeros.abelianGroup + ; isZero = record + { isInitial = record + { ! = λ {A} → record + { ⟦_⟧ = λ _ → ε A + ; cong = λ _ → refl A + ; homo = λ _ _ → sym A (identityʳ A (ε A)) + } + ; !-unique = λ {A} f tt → sym A (ε-homo f) + } + } + } + +module _ {G : AbelianGroup c ℓ} where + private + module G = AbelianGroup G + open SR G.setoid + open Mor (AbelianGroups c ℓ) + open Category (AbelianGroups c ℓ) + + -- All zero objects in Ab are trivial. + zero-trivial : IsZero (AbelianGroups c ℓ) G → (x y : G.Carrier) → x G.≈ y + zero-trivial is-zero x y = begin + x ≈˘⟨ iso.isoʳ x ⟩ + G.ε ≈⟨ iso.isoʳ y ⟩ + y ∎ + where + module is-zero = IsZero is-zero + module 𝟎 = Zero 𝟎 + module iso = _≅_ (up-to-iso (AbelianGroups c ℓ) 𝟎.initial is-zero.initial) + +biproduct : ∀ {A B} → Biproduct (AbelianGroups c ℓ) A B +biproduct {A = A} {B = B} = record + { A⊕B = DirectProducts.abelianGroup A B + ; π₁ = record + { ⟦_⟧ = proj₁ + ; cong = proj₁ + ; homo = λ _ _ → refl A + } + ; π₂ = record + { ⟦_⟧ = proj₂ + ; cong = proj₂ + ; homo = λ _ _ → refl B + } + ; i₁ = record + { ⟦_⟧ = λ x → x , B.ε + ; cong = λ eq → eq , B.refl + ; homo = λ _ _ → A.refl , B.sym (B.identityʳ _) + } + ; i₂ = record + { ⟦_⟧ = λ x → A.ε , x + ; cong = λ eq → A.refl , eq + ; homo = λ _ _ → A.sym (A.identityʳ _) , B.refl + } + ; isBiproduct = record + { isCoproduct = record + { [_,_] = λ {C} f g → + let module C = AbelianGroup C + open SR (C.setoid) + open MR (Delooping C) + in record + { ⟦_⟧ = λ { (a , b) → ⟦ f ⟧ a C.∙ ⟦ g ⟧ b } + ; cong = λ { (eqa , eqb) → C.∙-cong (cong f eqa) (cong g eqb) } + ; homo = λ { (a₁ , b₁) (a₂ , b₂) → begin + ⟦ f ⟧ (a₁ A.∙ a₂) C.∙ ⟦ g ⟧ (b₁ B.∙ b₂) ≈⟨ C.∙-cong (homo f a₁ a₂) (homo g b₁ b₂) ⟩ + ⟦ f ⟧ a₁ C.∙ ⟦ f ⟧ a₂ C.∙ (⟦ g ⟧ b₁ C.∙ ⟦ g ⟧ b₂) ≈⟨ center (C.comm (⟦ f ⟧ a₂) (⟦ g ⟧ b₁)) ⟩ + ⟦ f ⟧ a₁ C.∙ (⟦ g ⟧ b₁ C.∙ ⟦ f ⟧ a₂ C.∙ ⟦ g ⟧ b₂) ≈⟨ pull-first C.refl ⟩ + ⟦ f ⟧ a₁ C.∙ ⟦ g ⟧ b₁ C.∙ (⟦ f ⟧ a₂ C.∙ ⟦ g ⟧ b₂) ∎ + } + } + ; inject₁ = λ {C} {f} {g} x → + let open MR (Delooping C) + in elimʳ (ε-homo g) + ; inject₂ = λ {C} {f} {g} x → + let open MR (Delooping C) + in elimˡ (ε-homo f) + ; unique = λ { {C} {h} {f} {g} eq₁ eq₂ (a , b) → + let module C = AbelianGroup C + open SR (C.setoid) + in begin + ⟦ f ⟧ a C.∙ ⟦ g ⟧ b ≈˘⟨ C.∙-cong (eq₁ a) (eq₂ b) ⟩ + ⟦ h ⟧ (a , B.ε) C.∙ ⟦ h ⟧ (A.ε , b) ≈˘⟨ homo h (a , B.ε) (A.ε , b) ⟩ + ⟦ h ⟧ (a A.∙ A.ε , B.ε B.∙ b) ≈⟨ cong h ((A.identityʳ a) , (B.identityˡ b)) ⟩ + ⟦ h ⟧ (a , b) ∎ + } + } + ; isProduct = record + { ⟨_,_⟩ = λ {C} f g → + let module C = AbelianGroup C + open SR (C.setoid) + open MR (Delooping C) + in record + { ⟦_⟧ = λ x → (⟦ f ⟧ x) , (⟦ g ⟧ x) + ; cong = λ eq → cong f eq , cong g eq + ; homo = λ x y → (homo f x y) , (homo g x y) + } + ; project₁ = λ _ → A.refl + ; project₂ = λ _ → B.refl + ; unique = λ {C} {h} {f} {g} eq₁ eq₂ x → (A.sym (eq₁ x)) , (B.sym (eq₂ x)) + } + ; π₁∘i₁≈id = λ _ → A.refl + ; π₂∘i₂≈id = λ _ → B.refl + ; permute = λ _ → A.refl , B.refl + } + } + where + module A = AbelianGroup A + module B = AbelianGroup B + +AbelianGroupsAdditive : Additive (AbelianGroups c ℓ) +AbelianGroupsAdditive = record + { 𝟎 = 𝟎 + ; biproduct = biproduct + ; preadditive = AbelianGroupsPreadditive + } diff --git a/src/Experiments/Category/Instance/AbelianGroups/Image.agda b/src/Experiments/Category/Instance/AbelianGroups/Image.agda new file mode 100644 index 000000000..d056bbe9f --- /dev/null +++ b/src/Experiments/Category/Instance/AbelianGroups/Image.agda @@ -0,0 +1,32 @@ +{-# OPTIONS --without-K --safe #-} + +-- The image of a homomorphism +module Experiments.Category.Instance.AbelianGroups.Image where + +open import Data.Product using (Σ-syntax; _,_; _×_; proj₁; proj₂) + +open import Level + +open import Algebra.Properties.AbelianGroup +open import Experiments.Category.Instance.AbelianGroups + +open AbelianGroupHomomorphism + +Image : ∀ {c ℓ} {G H : AbelianGroup c ℓ} → AbelianGroupHomomorphism G H → AbelianGroup (c ⊔ ℓ) ℓ +Image {c = c} {ℓ = ℓ} {G = G} {H = H} f = + subgroup H in-image in-image-∙-closed in-image-ε-closed in-image-⁻¹-closed + where + module G = AbelianGroup G + module H = AbelianGroup H + + in-image : H.Carrier → Set (c ⊔ ℓ) + in-image h = Σ[ g ∈ G.Carrier ] (⟦ f ⟧ g H.≈ h) + + in-image-∙-closed : ∀ h₁ h₂ → in-image h₁ → in-image h₂ → in-image (h₁ H.∙ h₂) + in-image-∙-closed h₁ h₂ (g₁ , eq₁) (g₂ , eq₂) = (g₁ G.∙ g₂) , {!!} + + in-image-ε-closed : in-image H.ε + in-image-ε-closed = {!!} + + in-image-⁻¹-closed : ∀ h → in-image h → in-image (h H.⁻¹) + in-image-⁻¹-closed h (g , eq) = {!!} diff --git a/src/Experiments/Category/Instance/AbelianGroups/Kernels.agda b/src/Experiments/Category/Instance/AbelianGroups/Kernels.agda new file mode 100644 index 000000000..319fd8e1c --- /dev/null +++ b/src/Experiments/Category/Instance/AbelianGroups/Kernels.agda @@ -0,0 +1,85 @@ +{-# OPTIONS --without-K --safe #-} + +-- Proofs about the kernels of abelian groups +module Experiments.Category.Instance.AbelianGroups.Kernels where + +open import Level +open import Function using (_$_) + +open import Data.Unit.Polymorphic +open import Data.Product using (Σ-syntax; _,_; _×_; proj₁; proj₂) + +import Algebra.Construct.DirectProduct as DirectProduct +open import Algebra.Properties.AbelianGroup + +import Relation.Binary.Reasoning.Setoid as SR + +open import Categories.Category.Core +open import Categories.Object.Zero +open import Categories.Object.Kernel +open import Categories.Object.Cokernel + +open import Categories.Morphism.Notation +import Categories.Morphism as Mor +import Categories.Morphism.Reasoning as MR + +open import Categories.Category.Preadditive +open import Categories.Category.Additive +open import Experiments.Category.PreAbelian + +open import Experiments.Category.Instance.AbelianGroups +open import Experiments.Category.Instance.AbelianGroups.Preadditive +open import Experiments.Category.Instance.AbelianGroups.Additive + +private + variable + c ℓ : Level + +open AbelianGroup +open AbelianGroupHomomorphism + +-- The category of abelian groups has all kernels +kernels : ∀ {A B : AbelianGroup (c ⊔ ℓ) ℓ} (f : AbelianGroupHomomorphism A B) → Kernel 𝟎 f +kernels {A = A} {B = B} f = record + { kernel = subgroup A P ∙-closed ε-closed ⁻¹-closed + ; kernel⇒ = record + { ⟦_⟧ = proj₁ + ; cong = λ eq → eq + ; homo = λ _ _ → A.refl + } + ; isKernel = record + { commute = proj₂ + ; universal = λ {X} {h} eq → record + { ⟦_⟧ = λ x → (⟦ h ⟧ x) , (eq x) + ; cong = cong h + ; homo = homo h + } + ; factors = λ _ → A.refl + ; unique = λ eq x → A.sym (eq x) + } + } + where + module A = AbelianGroup A + module B = AbelianGroup B + + open SR B.setoid + + P : A.Carrier → Set _ + P x = ⟦ f ⟧ x B.≈ B.ε + + ∙-closed : ∀ x y → P x → P y → P (x A.∙ y) + ∙-closed x y px py = begin + ⟦ f ⟧ (x A.∙ y) ≈⟨ homo f x y ⟩ + ⟦ f ⟧ x B.∙ ⟦ f ⟧ y ≈⟨ B.∙-cong px py ⟩ + B.ε B.∙ B.ε ≈⟨ B.identityˡ B.ε ⟩ + B.ε ∎ + + ε-closed : P A.ε + ε-closed = ε-homo f + + ⁻¹-closed : ∀ x → P x → P (x A.⁻¹) + ⁻¹-closed x px = begin + ⟦ f ⟧ (x A.⁻¹) ≈⟨ ⁻¹-homo f x ⟩ + ⟦ f ⟧ x B.⁻¹ ≈⟨ B.⁻¹-cong px ⟩ + B.ε B.⁻¹ ≈⟨ ε⁻¹≈ε B ⟩ + B.ε ∎ diff --git a/src/Experiments/Category/Instance/AbelianGroups/Preabelian.agda b/src/Experiments/Category/Instance/AbelianGroups/Preabelian.agda new file mode 100644 index 000000000..7132a0efd --- /dev/null +++ b/src/Experiments/Category/Instance/AbelianGroups/Preabelian.agda @@ -0,0 +1,378 @@ +{-# OPTIONS --without-K --safe #-} +module Experiments.Category.Instance.AbelianGroups.Preabelian where + +open import Level +open import Function using (_$_) + +open import Data.Unit.Polymorphic +open import Data.Product using (Σ-syntax; _,_; _×_; proj₁; proj₂) + +import Algebra.Construct.DirectProduct as DirectProduct +open import Algebra.Properties.AbelianGroup + +import Relation.Binary.Reasoning.Setoid as SR + +open import Categories.Category.Core +open import Categories.Object.Zero +open import Categories.Object.Kernel +open import Categories.Object.Cokernel + +open import Categories.Morphism.Notation +import Categories.Morphism as Mor +import Categories.Morphism.Reasoning as MR + +open import Categories.Category.Preadditive +open import Categories.Category.Additive +open import Experiments.Category.PreAbelian + +open import Experiments.Category.Instance.AbelianGroups +open import Experiments.Category.Instance.AbelianGroups.Preadditive +open import Experiments.Category.Instance.AbelianGroups.Additive + +private + variable + c ℓ : Level + +open AbelianGroup +open AbelianGroupHomomorphism + + +kernels : ∀ {A B : AbelianGroup (c ⊔ ℓ) ℓ} (f : AbelianGroupHomomorphism A B) → Kernel 𝟎 f +kernels {A = A} {B = B} f = record + { kernel = subgroup A P ∙-closed ε-closed ⁻¹-closed + ; kernel⇒ = record + { ⟦_⟧ = proj₁ + ; cong = λ eq → eq + ; homo = λ _ _ → A.refl + } + ; isKernel = record + { commute = proj₂ + ; universal = λ {X} {h} eq → record + { ⟦_⟧ = λ x → (⟦ h ⟧ x) , (eq x) + ; cong = cong h + ; homo = homo h + } + ; factors = λ _ → A.refl + ; unique = λ eq x → A.sym (eq x) + } + } + where + module A = AbelianGroup A + module B = AbelianGroup B + + open SR B.setoid + + P : A.Carrier → Set _ + P x = ⟦ f ⟧ x B.≈ B.ε + + ∙-closed : ∀ x y → P x → P y → P (x A.∙ y) + ∙-closed x y px py = begin + ⟦ f ⟧ (x A.∙ y) ≈⟨ homo f x y ⟩ + ⟦ f ⟧ x B.∙ ⟦ f ⟧ y ≈⟨ B.∙-cong px py ⟩ + B.ε B.∙ B.ε ≈⟨ B.identityˡ B.ε ⟩ + B.ε ∎ + + ε-closed : P A.ε + ε-closed = ε-homo f + + ⁻¹-closed : ∀ x → P x → P (x A.⁻¹) + ⁻¹-closed x px = begin + ⟦ f ⟧ (x A.⁻¹) ≈⟨ ⁻¹-homo f x ⟩ + ⟦ f ⟧ x B.⁻¹ ≈⟨ B.⁻¹-cong px ⟩ + B.ε B.⁻¹ ≈⟨ ε⁻¹≈ε B ⟩ + B.ε ∎ + + +cokernels : ∀ {A B : AbelianGroup c (c ⊔ ℓ)} (f : AbelianGroupHomomorphism A B) → Cokernel 𝟎 f +cokernels {A = A} {B = B} f = record + { cokernel = abGroupHelper record + { Carrier = B.Carrier + ; _≈_ = λ b₁ b₂ → Σ[ a ∈ A.Carrier ] (b₁ B.∙ ⟦ f ⟧ a B.≈ b₂) + ; _∙_ = B._∙_ + ; ε = B.ε + ; _⁻¹ = B._⁻¹ + ; isEquivalence = record + { refl = A.ε , quot-refl + ; sym = λ { {b₁} {b₂} (a , eq) → (a A.⁻¹) , quot-sym eq } + ; trans = λ { {b₁} {b₂} {b₃} (a₁ , eq₁) (a₂ , eq₂) → (a₁ A.∙ a₂) , quot-trans eq₁ eq₂ } + } + ; ∙-cong = λ { (a₁ , eq₁) (a₂ , eq₂) → (a₁ A.∙ a₂) , quot-∙-cong eq₁ eq₂ } + ; ⁻¹-cong = λ { (a , eq) → (a A.⁻¹) , quot-inv-cong eq } + ; assoc = λ x y z → A.ε , lift-quot (B.assoc x y z) + ; identityˡ = λ x → A.ε , lift-quot (B.identityˡ x) + ; inverseˡ = λ x → A.ε , lift-quot (B.inverseˡ x) + ; comm = λ x y → A.ε , lift-quot (B.comm x y) + } + ; cokernel⇒ = record + { ⟦_⟧ = λ x → x + ; cong = λ { eq → A.ε , lift-quot eq } + ; homo = λ x y → A.ε , quot-refl + } + ; isCokernel = record + { commute = λ a → (a A.⁻¹) , quot-commute + ; universal = λ {X} {h} eq → + let module X = AbelianGroup X + open SR X.setoid + open MR (Delooping X) + in record + { ⟦_⟧ = λ x → ⟦ h ⟧ x + ; cong = λ { {x} {y} (a , eq-a) → begin + ⟦ h ⟧ x ≈˘⟨ cong h (quot-sym eq-a) ⟩ + ⟦ h ⟧ (y B.∙ ⟦ f ⟧ (a A.⁻¹)) ≈⟨ homo h y (⟦ f ⟧ (a A.⁻¹)) ⟩ + ⟦ h ⟧ y X.∙ ⟦ h ⟧ (⟦ f ⟧ (a A.⁻¹)) ≈⟨ elimʳ (eq (a A.⁻¹)) ⟩ + ⟦ h ⟧ y ∎ + } + ; homo = λ x y → homo h x y + } + ; factors = λ {X} {h} {eq} x → X .refl + ; unique = λ {X} {h} {i} {eq} eq x → X .sym (eq x) + } + } + where + module A = AbelianGroup A + module B = AbelianGroup B + + abstract + quot-refl : ∀ {b} → (b B.∙ ⟦ f ⟧ A.ε) B.≈ b + quot-refl {b} = begin + b B.∙ ⟦ f ⟧ A.ε ≈⟨ elimʳ (ε-homo f) ⟩ + b ∎ + where + open SR B.setoid + open MR (Delooping B) + + quot-sym : ∀ {b₁ b₂} {a} → b₁ B.∙ ⟦ f ⟧ a B.≈ b₂ → b₂ B.∙ ⟦ f ⟧ (a A.⁻¹) B.≈ b₁ + quot-sym {b₁ = b₁} {b₂ = b₂} {a = a} eq = begin + b₂ B.∙ ⟦ f ⟧ (a A.⁻¹) ≈⟨ B.∙-congˡ (⁻¹-homo f a) ⟩ + b₂ B.∙ ⟦ f ⟧ a B.⁻¹ ≈˘⟨ B.∙-congʳ eq ⟩ + b₁ B.∙ ⟦ f ⟧ a B.∙ ⟦ f ⟧ a B.⁻¹ ≈⟨ cancelʳ (B.inverseʳ (⟦ f ⟧ a)) ⟩ + b₁ ∎ + where + open SR B.setoid + open MR (Delooping B) + + quot-trans : ∀ {b₁ b₂ b₃} {a₁ a₂} → b₁ B.∙ ⟦ f ⟧ a₁ B.≈ b₂ → b₂ B.∙ ⟦ f ⟧ a₂ B.≈ b₃ → b₁ B.∙ ⟦ f ⟧ (a₁ A.∙ a₂) B.≈ b₃ + quot-trans {b₁ = b₁} {b₂ = b₂} {b₃ = b₃} {a₁ = a₁} {a₂ = a₂} eq₁ eq₂ = begin + b₁ B.∙ ⟦ f ⟧ (a₁ A.∙ a₂) ≈⟨ B.∙-congˡ (homo f a₁ a₂) ⟩ + b₁ B.∙ (⟦ f ⟧ a₁ B.∙ ⟦ f ⟧ a₂) ≈⟨ pullˡ eq₁ ⟩ + b₂ B.∙ ⟦ f ⟧ a₂ ≈⟨ eq₂ ⟩ + b₃ ∎ + where + open SR B.setoid + open MR (Delooping B) + + quot-∙-cong : ∀ {b₁ b₂ b₃ b₄} {a₁ a₂} → b₁ B.∙ ⟦ f ⟧ a₁ B.≈ b₂ → b₃ B.∙ ⟦ f ⟧ a₂ B.≈ b₄ → b₁ B.∙ b₃ B.∙ ⟦ f ⟧ (a₁ A.∙ a₂) B.≈ b₂ B.∙ b₄ + quot-∙-cong {b₁ = b₁} {b₂ = b₂} {b₃ = b₃} {b₄ = b₄} {a₁ = a₁} {a₂ = a₂} eq₁ eq₂ = begin + b₁ B.∙ b₃ B.∙ ⟦ f ⟧ (a₁ A.∙ a₂) ≈⟨ B.∙-congˡ (homo f a₁ a₂) ⟩ + b₁ B.∙ b₃ B.∙ (⟦ f ⟧ a₁ B.∙ ⟦ f ⟧ a₂) ≈⟨ B.∙-congˡ (B.comm (⟦ f ⟧ a₁) (⟦ f ⟧ a₂)) ⟩ + b₁ B.∙ b₃ B.∙ (⟦ f ⟧ a₂ B.∙ ⟦ f ⟧ a₁) ≈⟨ center eq₂ ⟩ + b₁ B.∙ (b₄ B.∙ ⟦ f ⟧ a₁) ≈⟨ B.∙-congˡ (B.comm b₄ (⟦ f ⟧ a₁)) ⟩ + b₁ B.∙ (⟦ f ⟧ a₁ B.∙ b₄) ≈⟨ pullˡ eq₁ ⟩ + b₂ B.∙ b₄ ∎ + where + open SR B.setoid + open MR (Delooping B) + + quot-inv-cong : ∀ {b₁ b₂} {a} → b₂ B.∙ ⟦ f ⟧ a B.≈ b₁ → (b₂ B.⁻¹) B.∙ ⟦ f ⟧ (a A.⁻¹) B.≈ (b₁ B.⁻¹) + quot-inv-cong {b₁ = b₁} {b₂ = b₂} {a = a} eq = begin + b₂ B.⁻¹ B.∙ ⟦ f ⟧ (a A.⁻¹) ≈⟨ B.∙-congˡ (⁻¹-homo f a) ⟩ + b₂ B.⁻¹ B.∙ ⟦ f ⟧ a B.⁻¹ ≈⟨ ⁻¹-∙-comm B b₂ (⟦ f ⟧ a) ⟩ + (b₂ B.∙ ⟦ f ⟧ a) B.⁻¹ ≈⟨ B.⁻¹-cong eq ⟩ + b₁ B.⁻¹ ∎ + where + open SR B.setoid + open MR (Delooping B) + + lift-quot : ∀ {b₁ b₂} → b₁ B.≈ b₂ → b₁ B.∙ ⟦ f ⟧ A.ε B.≈ b₂ + lift-quot {b₁} {b₂} eq = begin + b₁ B.∙ ⟦ f ⟧ A.ε ≈⟨ elimʳ (ε-homo f) ⟩ + b₁ ≈⟨ eq ⟩ + b₂ ∎ + where + open SR B.setoid + open MR (Delooping B) + + quot-commute : ∀ {a} → ⟦ f ⟧ a B.∙ ⟦ f ⟧ (a A.⁻¹) B.≈ B.ε + quot-commute {a = a} = begin + ⟦ f ⟧ a B.∙ ⟦ f ⟧ (a A.⁻¹) ≈⟨ B.∙-congˡ (⁻¹-homo f a) ⟩ + ⟦ f ⟧ a B.∙ ⟦ f ⟧ a B.⁻¹ ≈⟨ B.inverseʳ (⟦ f ⟧ a) ⟩ + B.ε ∎ + where + open SR B.setoid + open MR (Delooping B) + +-- Some facts about morphisms in Ab +module _ {A B : AbelianGroup (c ⊔ ℓ) (c ⊔ ℓ)} (f : AbelianGroupHomomorphism A B) where + private + module A = AbelianGroup A + module B = AbelianGroup B + + module ker = Kernel (kernels {c = c ⊔ ℓ} f) + module coker = Cokernel (cokernels {ℓ = c ⊔ ℓ} f) + + open Mor (AbelianGroups (c ⊔ ℓ) (c ⊔ ℓ)) + open Zero (𝟎 {c = (c ⊔ ℓ)} {ℓ = (c ⊔ ℓ)}) + open Category (AbelianGroups (c ⊔ ℓ) (c ⊔ ℓ)) + + mono-trivial-kernel : Mono f → IsZero (AbelianGroups (c ⊔ ℓ) (c ⊔ ℓ)) ker.kernel + mono-trivial-kernel f-mono = record + { isInitial = record + { ! = zero⇒ + ; !-unique = λ { {X} g (x , eq) → + let module X = AbelianGroup X + open SR X.setoid + in begin + X.ε ≈˘⟨ ε-homo g ⟩ + ⟦ g ⟧ (A.ε , _) ≈˘⟨ cong g (f-mono ker.kernel⇒ zero⇒ (λ { (x′ , eq′) → B.trans eq′ (B.sym (ε-homo f)) }) (x , eq)) ⟩ + ⟦ g ⟧ (x , eq) ∎ + } + } + ; isTerminal = record + { ! = zero⇒ + ; !-unique = λ {X} g → + let open SR B.setoid + in f-mono zero⇒ (ker.kernel⇒ ∘ g) λ x → begin + ⟦ f ⟧ A.ε ≈⟨ ε-homo f ⟩ + B.ε ≈˘⟨ proj₂ (⟦ g ⟧ x) ⟩ + ⟦ f ⟧ (proj₁ (⟦ g ⟧ x)) ∎ + } + } + + trivial-kernel-injective : ∀ {x y} → IsZero (AbelianGroups (c ⊔ ℓ) (c ⊔ ℓ)) ker.kernel → ⟦ f ⟧ x B.≈ ⟦ f ⟧ y → x A.≈ y + trivial-kernel-injective {x = x} {y = y} kernel-zero eq = + let + -- First, let us show that x⁻¹y ∈ ker f + in-kernel = begin + ⟦ f ⟧ (x A.⁻¹ A.∙ y) ≈⟨ homo f (x A.⁻¹) y ⟩ + ⟦ f ⟧ (x A.⁻¹) B.∙ ⟦ f ⟧ y ≈⟨ B.∙-cong (⁻¹-homo f x) (B.sym eq) ⟩ + (⟦ f ⟧ x B.⁻¹ B.∙ ⟦ f ⟧ x) ≈⟨ B.inverseˡ (⟦ f ⟧ x) ⟩ + B.ε ∎ + -- However, the kernel is trivial, so x⁻¹y ≈ ε + is-inverse = zero-trivial kernel-zero ((x A.⁻¹ A.∙ y) , in-kernel) (A.ε , ε-homo f) + -- Furthermore, inverses are unique, so this means that x ≈ y + in ⁻¹-injective A $ inverseˡ-unique A (x A.⁻¹) y is-inverse + where + open SR B.setoid + module kernel-zero = IsZero kernel-zero + + mono-injective : ∀ {x y} → Mono f → ⟦ f ⟧ x B.≈ ⟦ f ⟧ y → x A.≈ y + mono-injective f-mono = trivial-kernel-injective (mono-trivial-kernel f-mono) + +-- module _ {c ℓ} {H G : AbelianGroup (c ⊔ ℓ) (c ⊔ ℓ)} (sub : AbelianGroups (c ⊔ ℓ) (c ⊔ ℓ) [ H ↣ G ]) where +-- private +-- module G = AbelianGroup G +-- module H = AbelianGroup H +-- open Mor._↣_ sub renaming (mor to inj) +-- open SR G.setoid + +-- record Quot (x y : G.Carrier) : Set (c ⊔ ℓ) where +-- constructor quot +-- field +-- witness : H.Carrier +-- element : ⟦ inj ⟧ witness G.≈ (x G.∙ (y G.⁻¹)) +-- -- Need to show that if x ≈ y, that the two witnesses produced are the same! + +-- open Quot + +-- -- I guess this is right... huh +-- quot-cong : ∀ {x y} → (p q : Quot x y) → (witness p) H.≈ (witness q) +-- quot-cong {x = x} {y = y} eq p q = mono-injective {c = c} {ℓ = ℓ} inj mono $ begin +-- ⟦ inj ⟧ (witness p) ≈⟨ element p ⟩ +-- (x G.∙ y G.⁻¹) ≈˘⟨ element q ⟩ +-- ⟦ inj ⟧ (witness q) ∎ + + + epi-trivial-cokernel : Epi f → IsZero (AbelianGroups (c ⊔ ℓ) (c ⊔ ℓ)) coker.cokernel + epi-trivial-cokernel f-epi = record + { isInitial = record + { ! = zero⇒ + ; !-unique = λ {X} g → + let module X = AbelianGroup X + open SR X.setoid + in f-epi zero⇒ (g ∘ coker.cokernel⇒) λ x → begin + X.ε ≈˘⟨ ε-homo g ⟩ + ⟦ g ⟧ B.ε ≈˘⟨ cong g (coker.commute x) ⟩ + ⟦ g ⟧ (⟦ f ⟧ x) ∎ + } + ; isTerminal = record + { ! = zero⇒ + ; !-unique = λ {X} g x → + let module X = AbelianGroup X + open SR B.setoid + open MR (Delooping B) + (a , a-eq) = f-epi coker.cokernel⇒ zero⇒ (λ a → a A.⁻¹ , (B.trans (B.∙-congˡ (⁻¹-homo f a)) (B.inverseʳ (⟦ f ⟧ a)))) (⟦ g ⟧ x) + eq = begin + B.ε B.∙ ⟦ f ⟧ (a A.⁻¹) ≈⟨ B.∙-cong (B.sym a-eq) (⁻¹-homo f a) ⟩ + ⟦ g ⟧ x B.∙ ⟦ f ⟧ a B.∙ (⟦ f ⟧ a B.⁻¹) ≈⟨ cancelʳ (B.inverseʳ (⟦ f ⟧ a)) ⟩ + ⟦ g ⟧ x ∎ + in a A.⁻¹ , eq + } + } + + record Surjection : Set (c ⊔ ℓ) where + field + from : AbelianGroupHomomorphism B A + right-inverse : ∀ (b : B.Carrier) → ⟦ f ⟧ (⟦ from ⟧ b) B.≈ b + + + trivial-cokernel-surjective : IsZero (AbelianGroups (c ⊔ ℓ) (c ⊔ ℓ)) coker.cokernel → Surjection + trivial-cokernel-surjective cokernel-zero = record + { from = record + { ⟦_⟧ = λ x → preimage x + ; cong = λ {x} {y} x≈y → + let open SR A.setoid + ϕ = λ x → proj₁ (cokernel-zero.¡-unique {coker.cokernel} (zero⇒ {coker.cokernel} {coker.cokernel}) (x B.⁻¹)) + in begin + -- ((proj₁ (cokernel-zero.¡-unique zero⇒ (x B.⁻¹)) A.⁻¹ A.∙ (proj₁ (cokernel-zero.¡-unique (coker.universal {!!}) (x B.⁻¹)) A.∙ A.ε)) A.⁻¹ A.∙ (proj₁ (cokernel-zero.¡-unique zero⇒ B.ε) A.⁻¹ A.∙ (proj₁ (cokernel-zero.¡-unique (coker.universal {!!}) B.ε) A.∙ A.ε) A.∙ A.ε)) ≈⟨ {!!} ⟩ + ((ϕ x A.⁻¹ A.∙ ({!!} A.∙ A.ε)) A.⁻¹ A.∙ ({!ϕ x!} A.⁻¹ A.∙ ({!ϕ x!} A.∙ A.ε) A.∙ A.ε)) ≈⟨ {!!} ⟩ + ((ϕ y A.⁻¹ A.∙ ({!foo!} A.∙ A.ε)) A.⁻¹ A.∙ ({!!} A.⁻¹ A.∙ ({!!} A.∙ A.ε) A.∙ A.ε)) ∎ + ; homo = {!!} + } + ; right-inverse = {!!} + } + where + module cokernel-zero = IsZero cokernel-zero + + preimage : B.Carrier → A.Carrier + preimage x = proj₁ (zero-trivial cokernel-zero (⟦ coker.cokernel⇒ ⟧ (x B.⁻¹)) (coker.cokernel .ε)) + + preimage-eq : (x : B.Carrier) → x B.⁻¹ B.∙ ⟦ f ⟧ (preimage x) B.≈ B.ε + preimage-eq x = proj₂ (zero-trivial cokernel-zero (⟦ coker.cokernel⇒ ⟧ (x B.⁻¹)) (coker.cokernel .ε)) + + quot-cong : ∀ {x y} → x B.≈ y → preimage x A.≈ preimage y + quot-cong eq = mono-injective {!!} {!!} + -- -- proj₂ (zero-trivial cokernel-zero (⟦ coker.cokernel⇒ ⟧ (x B.⁻¹)) (coker.cokernel .ε)) + -- This is wrong :( + -- trivial-cokernel-surjective : IsZero (AbelianGroups (c ⊔ ℓ) (c ⊔ ℓ)) coker.cokernel → (x : B.Carrier) → Σ[ a ∈ A.Carrier ] (⟦ f ⟧ a B.≈ x) + -- trivial-cokernel-surjective cokernel-zero x = + -- let open SR B.setoid + -- -- As the cokernel is trivial, all elements of it are equal. + -- -- However, due to how equality in the cokernel is defined + -- -- (IE: b₁ ≈ b₁ := Σ[ a ∈ A ], b₁ ∙ ⟦ f ⟧ a ≈ b₂) + -- -- we get an explicit element a ∈ A such that 'x⁻¹ ∙ f a ≈ ε' + -- (a , coker-eq) = zero-trivial cokernel-zero (⟦ coker.cokernel⇒ ⟧ (x B.⁻¹)) (coker.cokernel .ε) + -- -- However, inverses are unique, so 'f a ≈ x' + -- is-inverse = begin + -- (x B.∙ (⟦ f ⟧ a) B.⁻¹) B.⁻¹ ≈˘⟨ ⁻¹-∙-comm B x ((⟦ f ⟧ a) B.⁻¹) ⟩ + -- x B.⁻¹ B.∙ (⟦ f ⟧ a B.⁻¹) B.⁻¹ ≈⟨ B.∙-congˡ (⁻¹-involutive B (⟦ f ⟧ a)) ⟩ + -- x B.⁻¹ B.∙ ⟦ f ⟧ a ≈⟨ coker-eq ⟩ + -- B.ε ≈˘⟨ ε⁻¹≈ε B ⟩ + -- B.ε B.⁻¹ ∎ + -- in a , ⁻¹-injective B (inverseʳ-unique B x ((⟦ f ⟧ a) B.⁻¹) (⁻¹-injective B is-inverse)) + -- where + -- module cokernel-zero = IsZero cokernel-zero + + -- -- We don't really care how this computes, so let's mark it as abstract + -- abstract + -- epi-surjective : Epi f → (x : B.Carrier) → Σ[ a ∈ A.Carrier ] (⟦ f ⟧ a B.≈ x) + -- epi-surjective f-epi = trivial-cokernel-surjective (epi-trivial-cokernel f-epi) + + -- preimage : Epi f → B.Carrier → A.Carrier + -- preimage f-epi b = proj₁ (epi-surjective f-epi b) + +AbelianGroupsPreAbelian : PreAbelian (AbelianGroups (c ⊔ ℓ) (c ⊔ ℓ)) +AbelianGroupsPreAbelian {c = c} {ℓ = ℓ} = record + { additive = AbelianGroupsAdditive + ; kernel = kernels {c = (c ⊔ ℓ)} {ℓ = (c ⊔ ℓ)} + ; cokernel = cokernels {c = (c ⊔ ℓ)} {ℓ = (c ⊔ ℓ)} + } diff --git a/src/Experiments/Category/Instance/AbelianGroups/Preadditive.agda b/src/Experiments/Category/Instance/AbelianGroups/Preadditive.agda new file mode 100644 index 000000000..28fccabdb --- /dev/null +++ b/src/Experiments/Category/Instance/AbelianGroups/Preadditive.agda @@ -0,0 +1,72 @@ +{-# OPTIONS --without-K --safe #-} +module Experiments.Category.Instance.AbelianGroups.Preadditive where + +open import Level +open import Data.Unit.Polymorphic +open import Data.Product using (Σ-syntax; _,_; _×_; proj₁; proj₂) + +import Algebra.Construct.DirectProduct as DirectProduct +open import Algebra.Properties.AbelianGroup + +import Relation.Binary.Reasoning.Setoid as SR + +open import Categories.Object.Zero +open import Categories.Object.Biproduct + +import Categories.Morphism.Reasoning as MR + +open import Experiments.Category.Instance.AbelianGroups +open import Categories.Category.Preadditive + +private + variable + c ℓ : Level + +open AbelianGroup +open AbelianGroupHomomorphism + +AbelianGroupsPreadditive : Preadditive (AbelianGroups c ℓ) +AbelianGroupsPreadditive = record + { _+_ = λ {G} {H} f g → + let open SR (setoid H) + open MR (Delooping H) + in record + { ⟦_⟧ = λ x → H [ ⟦ f ⟧ x ∙ ⟦ g ⟧ x ] + ; cong = λ eq → ∙-cong H (cong f eq) (cong g eq) + ; homo = λ x y → begin + H [ ⟦ f ⟧ (G [ x ∙ y ]) ∙ ⟦ g ⟧ (G [ x ∙ y ]) ] ≈⟨ ∙-cong H (homo f x y) (homo g x y) ⟩ + H [ H [ ⟦ f ⟧ x ∙ ⟦ f ⟧ y ] ∙ H [ ⟦ g ⟧ x ∙ ⟦ g ⟧ y ] ] ≈⟨ center (comm H (⟦ f ⟧ y) (⟦ g ⟧ x)) ⟩ + H [ ⟦ f ⟧ x ∙ H [ H [ ⟦ g ⟧ x ∙ ⟦ f ⟧ y ] ∙ ⟦ g ⟧ y ] ] ≈⟨ pull-first (refl H) ⟩ + H [ H [ ⟦ f ⟧ x ∙ ⟦ g ⟧ x ] ∙ H [ ⟦ f ⟧ y ∙ ⟦ g ⟧ y ] ] ∎ + } + ; 0H = λ {G} {H} → record + { ⟦_⟧ = λ _ → ε H + ; cong = λ _ → refl H + ; homo = λ _ _ → sym H (identityʳ H _) + } + ; -_ = λ {G} {H} f → + let open SR (setoid H) + in record + { ⟦_⟧ = λ x → H [ ⟦ f ⟧ x ⁻¹] + ; cong = λ eq → ⁻¹-cong H (cong f eq) + ; homo = λ x y → begin + H [ ⟦ f ⟧ (G [ x ∙ y ]) ⁻¹] ≈⟨ ⁻¹-cong H (homo f x y) ⟩ + H [ H [ ⟦ f ⟧ x ∙ ⟦ f ⟧ y ] ⁻¹] ≈⟨ ⁻¹-distrib-∙ H (⟦ f ⟧ x) (⟦ f ⟧ y) ⟩ + H [ H [ ⟦ f ⟧ x ⁻¹] ∙ H [ ⟦ f ⟧ y ⁻¹] ] ∎ + } + ; HomIsAbGroup = λ A B → isAbGroupHelper record + { isEquivalence = record + { refl = λ x → refl B + ; sym = λ eq x → sym B (eq x) + ; trans = λ eq₁ eq₂ x → trans B (eq₁ x) (eq₂ x) + } + ; ∙-cong = λ eq₁ eq₂ x → ∙-cong B (eq₁ x) (eq₂ x) + ; ⁻¹-cong = λ eq x → ⁻¹-cong B (eq x) + ; assoc = λ f g h x → assoc B (⟦ f ⟧ x) (⟦ g ⟧ x) (⟦ h ⟧ x) + ; identityˡ = λ f x → identityˡ B (⟦ f ⟧ x) + ; inverseˡ = λ f x → inverseˡ B (⟦ f ⟧ x) + ; comm = λ f g x → comm B (⟦ f ⟧ x) (⟦ g ⟧ x) + } + ; +-resp-∘ = λ {A} {B} {C} {D} {f} {g} {h} {i} x → homo i (⟦ f ⟧ (⟦ h ⟧ x)) (⟦ g ⟧ (⟦ h ⟧ x)) + } + diff --git a/src/Experiments/Category/Instance/AbelianGroups/Properties.agda b/src/Experiments/Category/Instance/AbelianGroups/Properties.agda new file mode 100644 index 000000000..7c606d30d --- /dev/null +++ b/src/Experiments/Category/Instance/AbelianGroups/Properties.agda @@ -0,0 +1,32 @@ +{-# OPTIONS --without-K --safe #-} +module Experiments.Category.Instance.AbelianGroups.Properties where + +open import Level +open import Data.Unit.Polymorphic +open import Data.Product using (Σ-syntax; _,_; _×_; proj₁; proj₂) + +import Algebra.Construct.DirectProduct as DirectProduct +open import Algebra.Properties.AbelianGroup + +import Relation.Binary.Reasoning.Setoid as SR + +open import Categories.Object.Zero +open import Categories.Object.Biproduct +open import Categories.Object.Kernel +open import Categories.Object.Cokernel + +open import Experiments.Category.Instance.AbelianGroups + +open import Categories.Category.Preadditive +open import Categories.Category.Additive +open import Experiments.Category.PreAbelian + +import Categories.Morphism.Reasoning as MR + +private + variable + c ℓ : Level + +open AbelianGroup +open AbelianGroupHomomorphism + diff --git a/src/Experiments/Category/Instance/NonNegativeChainComplexes.agda b/src/Experiments/Category/Instance/NonNegativeChainComplexes.agda new file mode 100644 index 000000000..2cdb2afb5 --- /dev/null +++ b/src/Experiments/Category/Instance/NonNegativeChainComplexes.agda @@ -0,0 +1,71 @@ +{-# OPTIONS --without-K --safe #-} + + +open import Categories.Category.Core +open import Experiments.Category.Abelian + +module Experiments.Category.Instance.NonNegativeChainComplexes {o ℓ e} {𝒜 : Category o ℓ e} (abelian : Abelian 𝒜) where + +open import Level + +open import Data.Nat using (ℕ) + +open import Categories.Morphism.Reasoning 𝒜 + +open Category 𝒜 +open Abelian abelian + +open HomReasoning +open Equiv + +record ChainComplex : Set (o ⊔ ℓ ⊔ e) where + field + Chain : ℕ → Obj + boundary : ∀ (n : ℕ) → Chain (ℕ.suc n) ⇒ Chain n + bounary-zero : ∀ {n} → boundary n ∘ boundary (ℕ.suc n) ≈ zero⇒ + +record ChainMap (V W : ChainComplex) : Set (ℓ ⊔ e) where + private + module V = ChainComplex V + module W = ChainComplex W + field + hom : ∀ (n : ℕ) → V.Chain n ⇒ W.Chain n + commute : ∀ {n : ℕ} → (hom n ∘ V.boundary n) ≈ (W.boundary n ∘ hom (ℕ.suc n)) + +ChainComplexes : Category (o ⊔ ℓ ⊔ e) (ℓ ⊔ e) e +ChainComplexes = record + { Obj = ChainComplex + ; _⇒_ = ChainMap + ; _≈_ = λ f g → + let module f = ChainMap f + module g = ChainMap g + in ∀ {n : ℕ} → f.hom n ≈ g.hom n + ; id = record + { hom = λ _ → id + ; commute = id-comm-sym + } + ; _∘_ = λ {U} {V} {W} f g → + let module U = ChainComplex U + module V = ChainComplex V + module W = ChainComplex W + module f = ChainMap f + module g = ChainMap g + in record + { hom = λ n → f.hom n ∘ g.hom n + ; commute = λ {n} → begin + (f.hom n ∘ g.hom n) ∘ U.boundary n ≈⟨ pullʳ g.commute ⟩ + f.hom n ∘ V.boundary n ∘ g.hom (ℕ.suc n) ≈⟨ extendʳ f.commute ⟩ + W.boundary n ∘ f.hom (ℕ.suc n) ∘ g.hom (ℕ.suc n) ∎ + } + ; assoc = assoc + ; sym-assoc = sym-assoc + ; identityˡ = identityˡ + ; identityʳ = identityʳ + ; identity² = identity² + ; equiv = record + { refl = refl + ; sym = λ eq → sym eq + ; trans = λ eq₁ eq₂ → trans eq₁ eq₂ + } + ; ∘-resp-≈ = λ eq₁ eq₂ → ∘-resp-≈ eq₁ eq₂ + } diff --git a/src/Experiments/Category/Object/ChainComplex.agda b/src/Experiments/Category/Object/ChainComplex.agda new file mode 100644 index 000000000..2b1e2fda4 --- /dev/null +++ b/src/Experiments/Category/Object/ChainComplex.agda @@ -0,0 +1,14 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category.Core +open import Categories.Object.Zero + +module Experiments.Category.Object.ChainComplex {o ℓ e} {𝒞 : Category o ℓ e} (has-zero : Zero 𝒞) where + +open import Level + +open import Data.Nat using (ℕ) + +open Category 𝒞 +open Zero has-zero + diff --git a/src/Experiments/Category/PreAbelian.agda b/src/Experiments/Category/PreAbelian.agda new file mode 100644 index 000000000..7e1f7bd1d --- /dev/null +++ b/src/Experiments/Category/PreAbelian.agda @@ -0,0 +1,31 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category + +module Experiments.Category.PreAbelian {o ℓ e} (𝒞 : Category o ℓ e) where + +open import Level + +open import Categories.Category.Additive + +open import Categories.Object.Kernel +open import Categories.Object.Cokernel + +open Category 𝒞 +open HomReasoning + +private + variable + A B C : Obj + f g : A ⇒ B + +record PreAbelian : Set (o ⊔ ℓ ⊔ e) where + field + additive : Additive 𝒞 + + open Additive additive public + + field + kernel : (f : A ⇒ B) → Kernel 𝟎 f + cokernel : (f : A ⇒ B) → Cokernel 𝟎 f + diff --git a/src/Experiments/Functor/Exact.agda b/src/Experiments/Functor/Exact.agda new file mode 100644 index 000000000..662ddf6d6 --- /dev/null +++ b/src/Experiments/Functor/Exact.agda @@ -0,0 +1,29 @@ +{-# OPTIONS --without-K --safe #-} +module Experiments.Functor.Exact where + +open import Level + +open import Categories.Category +open import Categories.Functor +open import Categories.Functor.Limits + +open import Categories.Diagram.Limit +open import Categories.Diagram.Colimit + +open import Categories.Category.Finite.Fin + +private + variable + o ℓ e : Level + 𝒞 𝒟 ℐ : Category o ℓ e + +LeftExact : (F : Functor 𝒞 𝒟) → Set _ +LeftExact {𝒞 = 𝒞} F = ∀ {shape : FinCatShape} {J : Functor (FinCategory shape) 𝒞} → (L : Limit J) → PreservesLimit F L + +RightExact : (F : Functor 𝒞 𝒟) → Set _ +RightExact {𝒞 = 𝒞} F = ∀ {shape : FinCatShape} {J : Functor (FinCategory shape) 𝒞} → (L : Colimit J) → PreservesColimit F L + +record Exact (F : Functor 𝒞 𝒟) : Set (levelOfTerm 𝒞 ⊔ levelOfTerm 𝒟) where + field + left-exact : LeftExact F + right-exact : RightExact F