wip

src/Misc/FiveLemma.agda

@@ -7,7 +7,6 @@ open import Cubical.Data.Sigma
 open import Cubical.Categories.Abelian
 open import Cubical.Categories.Additive
 open import Cubical.Categories.Category
-open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Pointed
 open import Cubical.Foundations.Prelude
@@ -57,6 +56,22 @@ private
 module fiveLemma (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 =
+    let z1 = coker f in
+    let z2 = ker z1 in
+    hasKernels (coker f) .Kernel.k , z2
+
+  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
+
   module _
     (A B C D E A' B' C' D' E' : ob)
     (f : Hom[ A , B ])
@@ -72,9 +87,10 @@ module fiveLemma (AC : AbelianCategory ℓ ℓ') where
     (s : Hom[ B' , C' ])
     (t : Hom[ C' , D' ])
     (u : Hom[ D' , E' ])
-    (fgExact : ker g ≃ ?)
+    (fgExact : {! ker g  !} ≃ {!   !})
     where
       z = let z1 = ker f in {!   !}
+      x = isEmbedding×isSurjection→isEquiv 
         -- 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)
@@ -85,4 +101,4 @@ module fiveLemma (AC : AbelianCategory ℓ ℓ') where
         --     nIsEmbedding c1 c2 = {!   !}
 
         --     nIsSurjection : isSurjection (fst n)
-        --     nIsSurjection b = {!   !} 
+        --     nIsSurjection b = {!   !}  

src/Misc/FiveLemmaGroup.agda

@@ -0,0 +1,60 @@
+{-# OPTIONS --cubical #-}
+
+module Misc.FiveLemmaGroup where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Isomorphism
+
+open import Cubical.Data.Unit
+
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.GroupPath
+open import Cubical.Algebra.Group.Instances.Unit
+
+private
+  variable
+    ℓ ℓ' : Level
+
+isExact : {A B C : Group ℓ} → (f : GroupHom A B) → (g : GroupHom B C) → Type ℓ
+isExact f g = Ker g ≃ Im f
+
+module _
+  (A B C D E A' B' C' D' E' : Group ℓ)
+  (f : GroupHom A B)
+  (g : GroupHom B C)
+  (h : GroupHom C D)
+  (j : GroupHom D E)
+  (l : GroupHom A A')
+  (m : GroupHom B B')
+  (n : GroupHom C C')
+  (p : GroupHom D D')
+  (q : GroupHom E E')
+  (r : GroupHom A' B')
+  (s : GroupHom B' C')
+  (t : GroupHom C' D')
+  (u : GroupHom D' E')
+  (fg : isExact f g)
+  (gh : isExact g h)
+  (hj : isExact h j)
+  (rs : isExact r s)
+  (st : isExact s t)
+  (tu : isExact t u)
+  (lEpi : isSurjective l)
+  (mIso : isIso (m .fst))
+  (pIso : isIso (p .fst))
+  (q : isMono p)
+  where
+
+    sur : isSurjective n
+
+    mono : isMono n
+
+    lemma : isIso (n .fst)
+    lemma = gg , {!   !} , {!   !} where
+      gg : C' .fst → C .fst
+      gg = {!   !}
+    

src/Sorry.agda

@@ -0,0 +1,8 @@
+{-# OPTIONS --cubical-compatible #-}
+
+module Sorry where
+
+open import Agda.Primitive
+
+postulate
+  sorry : {l : Level} → {A : Set l} → A