From fd9f01f9142b2e9123bd58265823e0fcfb6f5f1c Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 4 Nov 2024 21:26:26 -0600
Subject: [PATCH] wip on five lemma and exact sequences

---
 src/Misc/Exact.agda                           | 118 ++++++++++++++++++
 src/Misc/FiveLemma.agda                       |  37 +++---
 ...emmaGroup.agda => FiveLemmaGroup.lagda.md} |  30 ++++-
 src/Misc/SnakeLemma.agda                      |  30 +++++
 4 files changed, 195 insertions(+), 20 deletions(-)
 create mode 100644 src/Misc/Exact.agda
 rename src/Misc/{FiveLemmaGroup.agda => FiveLemmaGroup.lagda.md} (78%)

diff --git a/src/Misc/Exact.agda b/src/Misc/Exact.agda
new file mode 100644
index 0000000..f9e6502
--- /dev/null
+++ b/src/Misc/Exact.agda
@@ -0,0 +1,118 @@
+{-# OPTIONS --cubical #-}
+
+module Misc.Exact where
+
+open import Agda.Primitive
+open import Cubical.Data.Sigma
+open import Cubical.Categories.Abelian
+open import Cubical.Categories.Additive
+open import Cubical.Categories.Category
+open import Cubical.Categories.Morphism
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Functions.Embedding
+open import Cubical.Functions.Surjection
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module _ (AC : AbelianCategory ℓ ℓ') where
+  open AbelianCategory AC
+
+  -- image is defined as kernel (cokernel f)
+  image : {x y : ob} (f : Hom[ x , y ]) → Σ ob (λ i → Hom[ i , y ])
+  image f = hasKernels (coker f) .Kernel.k , (ker (coker f))
+
+  isExact : {x y z : ob} (f : Hom[ x , y ]) (g : Hom[ y , z ]) → Type ℓ'
+  isExact {y = y} f g = Σ (Hom[ (Kernel.k g-ker) , (fst f-im) ]) λ m → isIso cat m where
+    f-im = image f
+    g-ker = hasKernels g
+
+  module _ where
+    open import Data.Fin
+    open import Data.Nat
+    open import Data.Vec
+
+    finExactSequence : {n : ℕ}
+      → (obSeq : Fin (suc (suc n)) → ob)
+      → (homSeq : (m : Fin (suc n)) → Hom[ (obSeq (inject₁ m)) , (obSeq (suc m)) ])
+      → Type ℓ'
+    finExactSequence {n = n} obSeq homSeq =
+      (m : Fin n) → isExact (homSeq (inject₁ m)) (homSeq (suc m))
+
+    pattern 3+ n = suc (suc (suc n))
+
+    -- Ob sequences must have at least 2 elements
+    obSeq : (n : ℕ) → Type ℓ
+    obSeq n = Vec ob (2+ n)
+
+    private
+      z = ℕ.zero
+
+      zFin2 : Fin 2
+      zFin2 = inject₁ Fin.zero
+
+    -- I am using Vec in the reverse way!!!
+
+    -- Fin 5   4    3    2    1    0
+    -- obSeq = E :: D :: C :: B :: A :: []
+
+    -- Fin 4    3     2     1      0
+    -- homSeq = de :: cd :: bc :: [ab]
+
+    -- sequence of Homs
+    data HomSeq : {n : ℕ} → (os : obSeq n) → Type (ℓ-max ℓ ℓ') where
+      h[_] : {os : obSeq z} → Hom[ lookup os (inject₁ Fin.zero) , lookup os (suc Fin.zero) ] → HomSeq os
+      _h∷_ : {n : ℕ} {os : obSeq n} {o : ob}
+        → Hom[ (head os) , o ] → HomSeq os → HomSeq (o ∷ os)
+
+    homSeqN : {n : ℕ} → (os : obSeq n) → (m : Fin (suc n)) → Type ℓ'
+    homSeqN {n = n} os m = Hom[ (lookup os (inject₁ m)) , (lookup os (suc m)) ]
+
+    op-inv : {n : ℕ} → (m : Fin n) → opposite (opposite m) ≡ m
+    op-inv {n = n} m = sym (fuckyou2 n (opposite (opposite m))) ∙ {!    !} ∙ fuckyou2 n m where
+      fuckyou1 : (n : ℕ) → (m : Fin n) → Data.Nat._<_ (toℕ m) n
+      fuckyou1 (suc n) Fin.zero = z<s
+      fuckyou1 (suc n) (suc m) = s<s (fuckyou1 n m)
+
+      fuckyou2 : (n : ℕ) → (m : Fin n) → fromℕ< {m = toℕ m} (fuckyou1 n m) ≡ m
+      fuckyou2 (suc n) Fin.zero = refl
+      fuckyou2 (suc n) (suc m) = let IH = fuckyou2 n m in cong suc IH
+
+      fuckyou3 : (n : ℕ) → (m : Fin n) → Data.Nat._<_ (toℕ (opposite m)) n
+      fuckyou3 (suc ℕ.zero) Fin.zero = z<s
+      fuckyou3 (2+ n) Fin.zero = let IH = fuckyou3 (suc n) Fin.zero in s<s IH
+      fuckyou3 (suc n) (suc m) = let IH = fuckyou3 n m in {!   !}
+
+    homSeqLookup : {n : ℕ} {os : obSeq n} → HomSeq os → (m : Fin (suc n)) → homSeqN os m
+    homSeqLookup {n = ℕ.zero} h[ x ] Fin.zero = x
+    homSeqLookup {n = suc n} (_h∷_ {os = os} {o = o} h1 hs) m = helper {! opposite m   !} where
+      op = opposite m
+      helper : (k : Fin (2+ n)) → homSeqN (o ∷ os) (opposite k)
+      helper k = {!   !}
+    
+    -- Retrieve the LAST hom in the sequence
+    hhead : ∀ {n : ℕ} {os : obSeq n} → HomSeq os → Hom[ {!   !} , {!   !} ]
+    -- hhead h[ x ] = x
+    -- hhead (x h∷ hs) = x
+
+    -- htail : ∀ {n : ℕ} {os : obSeq (suc n)} → HomSeq os → HomSeq (tail os)
+    -- htail {n} {x ∷ os} (x₁ h∷ hs) = hs
+
+    -- hlookup : ∀ {n : ℕ} {os : obSeq (suc n)}
+    --   → HomSeq os → (m : Fin n) → Hom[ lookup os (inject₁ (inject₁ (inject₁ m))) , lookup os (inject₁ (inject₁ (suc m))) ]
+    -- hlookup {n = suc ℕ.zero} (x h∷ hs) m = {! x  !}
+    -- hlookup {n = 2+ n} hs m = {!   !}
+
+    -- -- exactHomSeq must have at least 3 obs
+    -- exactHomSeq : {n : ℕ} → {os : obSeq (suc n)} → HomSeq os → (m : Fin (suc n)) → Type ℓ'
+    -- exactHomSeq {n = ℕ.zero} (y h∷ h[ x ]) Fin.zero = isExact x y
+    -- exactHomSeq {n = suc n} (y h∷ (x h∷ x₂)) Fin.zero = {!   !}
+    -- exactHomSeq {n = suc n} (y h∷ (x h∷ x₂)) (suc m) = {!   !}
+
+    -- -- exactHomVec : Type (ℓ-max ℓ ℓ')
+    -- -- exactHomVec = {n : ℕ} {o : ob} →               
+    -- --   Σ (HomVec o n) λ h → finExactSequence {!   !} {!   !} 
\ No newline at end of file
diff --git a/src/Misc/FiveLemma.agda b/src/Misc/FiveLemma.agda
index 3413c4f..7e859f1 100644
--- a/src/Misc/FiveLemma.agda
+++ b/src/Misc/FiveLemma.agda
@@ -7,6 +7,7 @@ open import Cubical.Data.Sigma
 open import Cubical.Categories.Abelian
 open import Cubical.Categories.Additive
 open import Cubical.Categories.Category
+open import Cubical.Categories.Morphism
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Pointed
 open import Cubical.Foundations.Prelude
@@ -23,19 +24,12 @@ module fiveLemma (AC : AbelianCategory ℓ ℓ') where
 
   -- image is defined as kernel (cokernel f)
   image : {x y : ob} (f : Hom[ x , y ]) → Σ ob (λ i → Hom[ i , y ])
-  image f =
-    let z1 = coker f in
-    let z2 = ker z1 in
-    hasKernels (coker f) .Kernel.k , z2
+  image f = hasKernels (coker f) .Kernel.k , (ker (coker f))
 
   isExact : {x y z : ob} (f : Hom[ x , y ]) (g : Hom[ y , z ]) → Type ℓ'
-  isExact {y = y} f g =
-    let g-ker = hasKernels g in
-    let f-im = image f in
-    let k = g-ker .Kernel.k in
-    let ker = g-ker .Kernel.ker in
-    let i = fst f-im in
-    Σ (Hom[ k , i ]) λ m → isIso cat m
+  isExact {y = y} f g = Σ (Hom[ (Kernel.k g-ker) , (fst f-im) ]) λ m → isIso cat m where
+    f-im = image f
+    g-ker = hasKernels g
 
   module _
     (A B C D E A' B' C' D' E' : ob)
@@ -52,10 +46,25 @@ module fiveLemma (AC : AbelianCategory ℓ ℓ') where
     (s : Hom[ B' , C' ])
     (t : Hom[ C' , D' ])
     (u : Hom[ D' , E' ])
-    (fgExact : {! ker g  !} ≃ {!   !})
+    (fgExact : isExact f g)
+    (ghExact : isExact g h)
+    (hjExact : isExact h j)
+    (rsExact : isExact r s)
+    (stExact : isExact s t)
+    (tuExact : isExact t u)
+    (lEpi : isEpic cat l)
+    (mIso : isIso cat m)
+    (pIso : isIso cat p)
+    (qMono : isMonic cat q)
+    (sq1 : (_⋆_ l r) ≡ (_⋆_ f m))
+    (sq2 : (_⋆_ m s) ≡ (_⋆_ g n))
+    (sq3 : (_⋆_ n t) ≡ (_⋆_ h p))
+    (sq4 : (_⋆_ p u) ≡ (_⋆_ j q))
     where
-      z = let z1 = ker f in {!   !}
-      x = isEmbedding×isSurjection→isEquiv 
+      nEpi : isEpic cat n
+      nEpi b∘n≡b'∘n = {!   !} where
+        
+
         -- lemma : isExact f g → isExact g h → isExact h j
         --   → isExact r s → isExact s t → isExact t u
         --   → isSurjection (fst l) → isEquiv (fst m) → isEquiv (fst p) → isEmbedding (fst q)
diff --git a/src/Misc/FiveLemmaGroup.agda b/src/Misc/FiveLemmaGroup.lagda.md
similarity index 78%
rename from src/Misc/FiveLemmaGroup.agda
rename to src/Misc/FiveLemmaGroup.lagda.md
index e74b3b7..8324ea3 100644
--- a/src/Misc/FiveLemmaGroup.agda
+++ b/src/Misc/FiveLemmaGroup.lagda.md
@@ -1,3 +1,4 @@
+```
 {-# OPTIONS --cubical #-}
 
 module Misc.FiveLemmaGroup where
@@ -11,12 +12,13 @@ open import Cubical.Algebra.Group.Properties
 open import Cubical.Data.Unit
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Structure
 open import Cubical.HITs.PropositionalTruncation.Base
 open import Cubical.HITs.PropositionalTruncation.Properties
-  renaming (rec to propTruncRec ; map to propTruncMap ; rec2 to propTruncRec2 ; map2 to propTruncMap2)
+  renaming (rec to propTruncRec ; map to propTruncMap ; rec2 to propTruncRec2 ; map2 to propTruncMap2 ; elim to propTruncElim)
 open import Cubical.HITs.Pushout.Base        
 open import Cubical.HITs.Pushout
 
@@ -60,21 +62,36 @@ module _
         u[p[d]] : ∥ ⟨ E' ⟩ ∥₁
         u[p[d]] = propTruncMap (λ d → u .fst (p .fun .fst d)) d
 
+        u[t[c']] : ∥ ⟨ E' ⟩ ∥₁
+        u[t[c']] = ∣ (u .fst (t .fst c')) ∣₁
+
+        u[p[d]]≡u[t[c']] : u[p[d]] ≡ u[t[c']]
+        u[p[d]]≡u[t[c']] = squash₁ u[p[d]] u[t[c']]
+
         q[j[d]] : ∥ ⟨ E' ⟩ ∥₁
         q[j[d]] = propTruncMap2 (λ e' d → subst (λ _ → ⟨ E' ⟩) (sq4 d) e') u[p[d]] d
 
+        u[p[d]]≡q[j[d]] : u[p[d]] ≡ q[j[d]]
+        u[p[d]]≡q[j[d]] = squash₁ u[p[d]] q[j[d]]
+
         j[d] = ∥ ⟨ E ⟩ ∥₁
         j[d] = propTruncMap (λ d → j .fst d) d
 
         -- Since im t = ker u by exactness, 0 = u(t(c′)) = u(p(d)) = q(j(d)).
-        u[t[c']] : ⟨ E' ⟩
-        u[t[c']] = u .fst (t .fst c')
 
+        -- d' is in the kernel of u
         d'-ker-u : Ker u
         d'-ker-u = invIsEq (tu .snd) (d' , ∣ (c' , refl) ∣₁)
 
-        u[t[c']]≡0 : u[t[c']] ≡ E' .snd .1g
-        u[t[c']]≡0 = {!  d'-ker-u .snd !}
+        u[t[c']]≡0 : isInKer u (fst d'-ker-u)
+        u[t[c']]≡0 = snd d'-ker-u
+
+        q[j[d]]≡0 : q[j[d]] ≡ ∣ (E' .snd .1g) ∣₁
+        q[j[d]]≡0 = squash₁ q[j[d]] ∣ (E' .snd .1g) ∣₁
+        -- q[j[d]]≡0 = sym u[p[d]]≡q[j[d]] ∙ {!   !} ∙ cong ∣_∣₁ u[t[c']]≡0
+
+        j[d]≡0 : j[d] ≡ ∣ (E .snd .1g) ∣₁
+        j[d]≡0 = {!   !}
       in
 
       -- let pSurj = p .surj in
@@ -92,4 +109,5 @@ module _
     lemma = gg , {!   !} , {!   !} where
       gg : C' .fst → C .fst
       gg c' = {!  !}
-      
\ No newline at end of file
+      
+```
\ No newline at end of file
diff --git a/src/Misc/SnakeLemma.agda b/src/Misc/SnakeLemma.agda
index 6cc9a42..4d54730 100644
--- a/src/Misc/SnakeLemma.agda
+++ b/src/Misc/SnakeLemma.agda
@@ -2,3 +2,33 @@
 
 module Misc.SnakeLemma where
 
+open import Agda.Primitive
+open import Cubical.Data.Sigma
+open import Cubical.Categories.Abelian
+open import Cubical.Categories.Additive
+open import Cubical.Categories.Category
+open import Cubical.Categories.Morphism
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Functions.Embedding
+open import Cubical.Functions.Surjection
+
+open import Misc.Exact
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module snakeLemma (AC : AbelianCategory ℓ ℓ') where
+  open AbelianCategory AC
+
+  module _
+    (A B C A' B' C' : ob)
+    (asdf : exactHomSeq ?)
+    (f : Hom[ A , B ]) (g : Hom[ B , C ])
+    (f' : Hom[ A' , B' ]) (g' : Hom[ B' , C' ])
+    (a : Hom[ A , A' ]) (b : Hom[ B , B' ]) (c : Hom[ C , C' ])
+    where
+