[WIP] A bunch of junk with abelian categories

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                                             ∎

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

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 = {!!}
+  }

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