wip

src/Misc/FiveLemmaGroup.agda

@@ -2,19 +2,26 @@
 
 module Misc.FiveLemmaGroup where
 
-open import Cubical.Foundations.Prelude
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Group.GroupPath
+open import Cubical.Algebra.Group.Instances.Unit
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.Morphisms
+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.Isomorphism
+open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Structure
-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.Properties
-open import Cubical.Algebra.Group.Instances.Unit
-open import Cubical.HITs.PropositionalTruncation.Properties renaming (rec to propTruncRec)
+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)
+open import Cubical.HITs.Pushout.Base        
+open import Cubical.HITs.Pushout
+
+open BijectionIso
+open GroupStr
 
 private
   variable
@@ -25,38 +32,57 @@ 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 : BijectionIso B B')
-  (n : GroupHom C C')
-  (p : BijectionIso 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)
+  (f : GroupHom A B) (g : GroupHom B C) (h : GroupHom C D) (j : GroupHom D E)
+  (l : GroupHom A A') (m : BijectionIso B B') (n : GroupHom C C') (p : BijectionIso 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)
-  (q : isMono q)
+  (qMono : isMono q)
+  (sq1 : (a : fst A) → r .fst (l .fst a) ≡ m .fun .fst (f .fst a))
+  (sq2 : (b : fst B) → s .fst (m .fun .fst b) ≡ n .fst (g .fst b))
+  (sq3 : (c : fst C) → t .fst (n .fst c) ≡ p .fun .fst (h .fst c))
+  (sq4 : (d : fst D) → u .fst (p .fun .fst d) ≡ q .fst (j .fst d))
   where
-    open BijectionIso
 
     sur : isSurjective n
+    -- Let c′ be an element of C′.
     sur c' =
-      let pSurj = p .surj in
-      let t[c'] = t .fst c' in
-      let step1 = pSurj t[c'] in
-      let d-thing = snd D in
-      let d-is-group = isPropIsGroup {!   !} {!   !} {!   !} in
-      let step2 = propTruncRec {!   !} (λ x → fst x) step1 in
+      let
+        d' : fst D'
+        d' = t .fst c'
+
+        -- Since p is surjective, there exists an element d in D with p(d) = t(c′).
+        d : ∥ ⟨ D ⟩ ∥₁
+        d = propTruncMap fst (p .surj d')
+
+        -- By commutativity of the diagram, u(p(d)) = q(j(d)).
+        u[p[d]] : ∥ ⟨ E' ⟩ ∥₁
+        u[p[d]] = propTruncMap (λ d → u .fst (p .fun .fst d)) d
+
+        q[j[d]] : ∥ ⟨ E' ⟩ ∥₁
+        q[j[d]] = propTruncMap2 (λ e' d → subst (λ _ → ⟨ E' ⟩) (sq4 d) e') u[p[d]] 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'-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 !}
+      in
+
+      -- let pSurj = p .surj in
+      -- let t[c'] = t .fst c' in
+      -- let step1 = pSurj t[c'] in
+      -- let d-thing = snd D in
+      -- let d-is-group = isPropIsGroup {!   !} {!   !} {!   !} in
+      -- let step2 = propTruncRec {!   !} (λ x → fst x) step1 in
       {!   !}
 
     mono : isMono n
@@ -66,4 +92,4 @@ module _
     lemma = gg , {!   !} , {!   !} where
       gg : C' .fst → C .fst
       gg c' = {!  !}
-     
+