Five lemma

Cubical/Algebra/Group/Exact.agda

@@ -1,11 +1,22 @@
 {-# OPTIONS --safe #-}
+
 module Cubical.Algebra.Group.Exact where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Function
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.HLevels
 
+open import Cubical.Data.Empty
+open import Cubical.Data.Fin
+open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum
 open import Cubical.Data.Unit
+open import Cubical.Data.Vec
 
 open import Cubical.Algebra.Group.Base
 open import Cubical.Algebra.Group.Morphisms
@@ -15,11 +26,23 @@ open import Cubical.Algebra.Group.Instances.Unit
 
 open import Cubical.HITs.PropositionalTruncation as PT
 
+private
+  variable
+    ℓ ℓ' : Level
+
+-- Exactness except the intersecting Group is only propositionally equal
+isWeakExactAt : {A B B' C : Group ℓ} (f : GroupHom A B) (g : GroupHom B' C) (p : B ≡ B') → Type ℓ
+isWeakExactAt {ℓ = ℓ} {B = B} {B' = B'} f g p = (b : ⟨ B ⟩) → (isInKer g (tr b) → isInIm f b) × (isInIm f b → isInKer g (tr b)) where
+  tr = λ (b : ⟨ B ⟩) → subst (λ (a : Σ (Type ℓ) GroupStr) → fst a) p b
 
--- TODO : Define exact sequences
--- (perhaps short, finite, ℕ-indexed and ℤ-indexed)
+isExactAt : {A B C : Group ℓ} (f : GroupHom A B) (g : GroupHom B C) → Type ℓ
+isExactAt {B = B} f g = (b : ⟨ B ⟩) → (isInKer g b → isInIm f b) × (isInIm f b → isInKer g b)
 
-SES→isEquiv : ∀ {ℓ ℓ'} {L R : Group ℓ-zero}
+isWeakExactAtRefl : {A B C : Group ℓ} (f : GroupHom A B) (g : GroupHom B C)
+  → isWeakExactAt f g refl ≡ isExactAt f g
+isWeakExactAtRefl {ℓ = ℓ} {B = B} f g i = (b : ⟨ B ⟩) → (isInKer g (transportRefl b i) → isInIm f b) × (isInIm f b → isInKer g (transportRefl b i))
+
+SES→isEquiv : {L R : Group ℓ-zero}
   → {G : Group ℓ} {H : Group ℓ'}
   → UnitGroup₀ ≡ L
   → UnitGroup₀ ≡ R
@@ -138,3 +161,4 @@ transportExact4 {G = G} {G₂ = G₂} {H = H} {H₂ = H₂} {L = L} {L₂ = L₂
       (J (λ z q → (r : x₃ ≡ w) (s : x₄ ≡ u) → B x z w u refl q r s)
         (J (λ w r → (s : x₄ ≡ u) → B x x₂ w u refl refl r s)
           (J (λ u s → B x x₂ x₃ u refl refl refl s) b)))
+

Cubical/Algebra/Group/Five.agda

@@ -0,0 +1,270 @@
+{-# OPTIONS --safe #-}
+
+-- This module proves the Five lemma[1] over group homomorphisms.
+--
+-- [1]: https://en.wikipedia.org/wiki/Five_lemma
+
+module Cubical.Algebra.Group.Five where
+
+open import Agda.Primitive
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Isomorphism
+
+open import Cubical.HITs.PropositionalTruncation.Base
+open import Cubical.HITs.PropositionalTruncation as PT
+
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Group.Exact
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.Morphisms
+
+open BijectionIso
+open IsGroupHom
+
+private
+  variable
+    ℓ ℓ' : Level
+
+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 : isExactAt f g) (gh : isExactAt g h) (hj : isExactAt h j)
+  (rs : isExactAt r s) (st : isExactAt s t) (tu : isExactAt t u)
+  (lSurj : isSurjective l)
+  (qInj : isInjective 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
+    module _ where
+      nInjective : isInjective n
+      nInjective c c-in-ker[n] = goal where
+        goalTy = c ≡ C .snd .GroupStr.1g
+        goalTyIsProp = let open GroupStr (C .snd) in is-set c 1g
+        untrunc = λ (p : ∥ goalTy ∥₁) → PT.rec goalTyIsProp (λ x → x) p
+
+        t[n[c]]≡0 : t .fst (n .fst c) ≡ D' .snd .GroupStr.1g
+        t[n[c]]≡0 = cong (t .fst) c-in-ker[n] ∙ t .snd .pres1
+
+        t[n[c]]≡p[h[c]] : t .fst (n .fst c) ≡ p .fun .fst (h .fst c)
+        t[n[c]]≡p[h[c]] = sq3 c
+
+        p[h[c]]≡0 : p .fun .fst (h .fst c) ≡ D' .snd .GroupStr.1g
+        p[h[c]]≡0 = sym t[n[c]]≡p[h[c]] ∙ t[n[c]]≡0
+
+        h[c]≡0 : h .fst c ≡ D .snd .GroupStr.1g
+        h[c]≡0 = p .inj (h .fst c) p[h[c]]≡0
+
+        c-in-ker[h] : isInKer h c
+        c-in-ker[h] = h[c]≡0
+
+        c-in-im[g] : isInIm g c
+        c-in-im[g] = gh c .fst c-in-ker[h]
+
+        rest : (b : ⟨ B ⟩) → (g .fst b ≡ c) → goalTy
+
+        goal = untrunc (PT.map (λ x → rest (fst x) (snd x)) c-in-im[g])
+
+        rest b g[b]≡c = goal2 where
+
+          n[g[b]]≡0 : n .fst (g .fst b) ≡ C' .snd .GroupStr.1g
+          n[g[b]]≡0 = cong (n .fst) g[b]≡c ∙ c-in-ker[n]
+
+          m[b] : ⟨ B' ⟩
+          m[b] = m .fun .fst b
+
+          s[m[b]]≡n[g[b]] : s .fst m[b] ≡ n .fst (g .fst b)
+          s[m[b]]≡n[g[b]] = sq2 b
+
+          s[m[b]]≡0 : s .fst m[b] ≡ C' .snd .GroupStr.1g
+          s[m[b]]≡0 = s[m[b]]≡n[g[b]] ∙ n[g[b]]≡0
+
+          m[b]-in-ker[s] : isInKer s m[b]
+          m[b]-in-ker[s] = s[m[b]]≡0
+
+          m[b]-in-im[r] : isInIm r m[b]
+          m[b]-in-im[r] = rs m[b] .fst m[b]-in-ker[s]
+
+          rest2 : (a' : ⟨ A' ⟩) → (r .fst a' ≡ m[b]) → (a : ⟨ A ⟩) → l .fst a ≡ a' → goalTy
+
+          goal2 =
+            let inner = λ x → untrunc (PT.map (λ y → rest2 (x .fst) (x .snd) (y .fst) (y .snd)) (lSurj (x .fst))) in
+            untrunc (PT.map inner m[b]-in-im[r])
+
+          rest2 a' r[a']≡m[b] a l[a]≡a' = c≡0 where
+
+            m[f[a]] : ⟨ B' ⟩
+            m[f[a]] = m .fun .fst (f .fst a)
+
+            r[l[a]]≡m[f[a]] : r .fst (l .fst a) ≡ m[f[a]]
+            r[l[a]]≡m[f[a]] = sq1 a
+
+            m[f[a]]≡m[b] : m[f[a]] ≡ m[b]
+            m[f[a]]≡m[b] = sym r[l[a]]≡m[f[a]] ∙ cong (r .fst) l[a]≡a' ∙ r[a']≡m[b]
+
+            f[a]≡b : f .fst a ≡ b
+            f[a]≡b = isInjective→isMono (m .fun) (m .inj) m[f[a]]≡m[b]
+
+            g[f[a]]≡c : g .fst (f .fst a) ≡ c
+            g[f[a]]≡c = cong (g .fst) f[a]≡b ∙ g[b]≡c
+
+            f[a]-in-im[f] : isInIm f (f .fst a)
+            f[a]-in-im[f] = ∣ a , refl ∣₁
+
+            f[a]-in-ker[g] : isInKer g (f .fst a)
+            f[a]-in-ker[g] = fg (f .fst a) .snd f[a]-in-im[f]
+
+            g[f[a]]≡0 : g .fst (f .fst a) ≡ C .snd .GroupStr.1g
+            g[f[a]]≡0 = f[a]-in-ker[g]
+
+            c≡0 : c ≡ C .snd .GroupStr.1g
+            c≡0 = sym g[f[a]]≡c ∙ g[f[a]]≡0
+
+    module _ where
+      nSurjective : isSurjective n
+      nSurjective c' = goal where
+        goalTy = isInIm n c'
+        untrunc = λ (p : ∥ goalTy ∥₁) → PT.rec (isPropIsInIm n c') (λ x → x) p
+
+        d' : ⟨ D' ⟩
+        d' = t .fst c'
+
+        pGroupIso = BijectionIso→GroupIso p
+        pIso = pGroupIso .fst
+        pInv = Iso.inv pIso
+
+        d : ⟨ D ⟩
+        d = pInv d'
+
+        p[d]≡t[c'] : p .fun .fst d ≡ t .fst c'
+        p[d]≡t[c'] = Iso.rightInv pIso d'
+
+        u[p[d]] : ⟨ E' ⟩
+        u[p[d]] = u .fst (p .fun .fst d)
+
+        j[d] : ⟨ E ⟩
+        j[d] = j .fst d
+
+        q[j[d]] : ⟨ E' ⟩
+        q[j[d]] = q .fst j[d]
+
+        u[p[d]]≡q[j[d]] : u[p[d]] ≡ q[j[d]]
+        u[p[d]]≡q[j[d]] = sq4 d
+
+        d'-in-ker[u] : isInKer u d'
+        d'-in-ker[u] = let im[t]→ker[u] = tu d' .snd in
+          im[t]→ker[u] ∣ (c' , refl) ∣₁
+
+        u[p[d]]≡0 : u[p[d]] ≡ E' .snd .GroupStr.1g
+        u[p[d]]≡0 = cong (u .fst) p[d]≡t[c'] ∙ d'-in-ker[u]
+
+        q[j[d]]≡0 : q[j[d]] ≡ E' .snd .GroupStr.1g
+        q[j[d]]≡0 = sym u[p[d]]≡q[j[d]] ∙ u[p[d]]≡0
+
+        j[d]≡0 : j[d] ≡ E .snd .GroupStr.1g
+        j[d]≡0 = qInj j[d] q[j[d]]≡0
+
+        d-in-ker[j] : isInKer j d
+        d-in-ker[j] = j[d]≡0
+
+        d-in-im[h] : isInIm h d
+        d-in-im[h] =
+          let ker[j]→im[h] = hj d .fst in
+          ker[j]→im[h] d-in-ker[j]
+
+        rest : (c : ⟨ C ⟩) → h .fst c ≡ d → goalTy
+
+        goal = untrunc (PT.map (λ x → rest (x .fst) (x .snd)) d-in-im[h])
+
+        rest c h[c]≡d = goal2 where
+          n[c] : ⟨ C' ⟩
+          n[c] = n .fst c
+
+          t[n[c]]≡p[h[c]] : t .fst n[c] ≡ p .fun .fst (h .fst c)
+          t[n[c]]≡p[h[c]] = sq3 c
+
+          t[n[c]]≡t[c'] : t .fst n[c] ≡ t .fst c'
+          t[n[c]]≡t[c'] =
+            t .fst n[c]             ≡⟨ t[n[c]]≡p[h[c]] ⟩
+            p .fun .fst (h .fst c)  ≡⟨ cong (p .fun .fst) h[c]≡d ⟩
+            p .fun .fst d           ≡⟨ p[d]≡t[c'] ⟩
+            t .fst c' ∎
+
+          c'-n[c] : ⟨ C' ⟩
+          c'-n[c] = let open GroupStr (C' .snd) in c' · (inv n[c])
+
+          t[c'-n[c]]≡0 : t .fst c'-n[c] ≡ D' .snd .GroupStr.1g
+          t[c'-n[c]]≡0 =
+            let open GroupStr (C' .snd) renaming (_·_ to _·ᶜ_; inv to invᶜ; 1g to 1gᶜ) in
+            let open GroupStr (D' .snd) renaming (_·_ to _·ᵈ_; inv to invᵈ; 1g to 1gᵈ) hiding (isGroup) in
+            t .fst (c' ·ᶜ (invᶜ n[c]))          ≡⟨ t .snd .pres· c' (invᶜ n[c]) ⟩
+            (t .fst c') ·ᵈ (t .fst (invᶜ n[c])) ≡⟨ cong ((t .fst c') ·ᵈ_) (t .snd .presinv n[c]) ⟩
+            (t .fst c') ·ᵈ (invᵈ (t .fst n[c])) ≡⟨ cong (λ z → (t .fst c') ·ᵈ (invᵈ z)) t[n[c]]≡t[c'] ⟩
+            (t .fst c') ·ᵈ (invᵈ (t .fst c'))   ≡⟨ cong ((t .fst c') ·ᵈ_) (sym (t .snd .presinv c')) ⟩
+            (t .fst c') ·ᵈ (t .fst (invᶜ c'))   ≡⟨ sym (t .snd .pres· c' (invᶜ c')) ⟩
+            t .fst (c' ·ᶜ (invᶜ c'))            ≡⟨ cong (t .fst) (IsGroup.·InvR isGroup c') ⟩
+            t .fst 1gᶜ                          ≡⟨ t .snd .pres1 ⟩
+            1gᵈ ∎
+
+          [c'-n[c]]-in-ker[t] : isInKer t c'-n[c]
+          [c'-n[c]]-in-ker[t] = t[c'-n[c]]≡0
+
+          [c'-n[c]]-in-im[s] : isInIm s c'-n[c]
+          [c'-n[c]]-in-im[s] =
+            let ker[t]→im[s] = st c'-n[c] .fst in
+            ker[t]→im[s] [c'-n[c]]-in-ker[t]
+
+          rest2 : (b' : ⟨ B' ⟩) → s .fst b' ≡ c'-n[c] → goalTy
+
+          goal2 = untrunc (PT.map (λ x → rest2 (x .fst) (x .snd)) [c'-n[c]]-in-im[s])
+
+          rest2 b' s[b']≡c'-n[c] = goal3 where
+            mGroupIso = BijectionIso→GroupIso m
+            mIso = mGroupIso .fst
+            mInv = Iso.inv mIso
+
+            b : ⟨ B ⟩
+            b = mInv b'
+
+            m[b]≡b' : m .fun .fst b ≡ b'
+            m[b]≡b' = Iso.rightInv mIso b'
+
+            s[m[b]]≡s[b'] : s .fst (m .fun .fst b) ≡ s .fst b'
+            s[m[b]]≡s[b'] = cong (s .fst) m[b]≡b'
+
+            s[m[b]]≡c'-n[c] : s .fst (m .fun .fst b) ≡ c'-n[c]
+            s[m[b]]≡c'-n[c] = s[m[b]]≡s[b'] ∙ s[b']≡c'-n[c]
+
+            g[b] : ⟨ C ⟩
+            g[b] = g .fst b
+
+            g[b]+c : ⟨ C ⟩
+            g[b]+c = C .snd .GroupStr._·_ g[b] c
+
+            n[g[b]] : ⟨ C' ⟩
+            n[g[b]] = n .fst g[b]
+
+            n[g[b]]≡s[m[b]] : n[g[b]] ≡ s .fst (m .fun .fst b)
+            n[g[b]]≡s[m[b]] = sym (sq2 b)
+
+            n[g[b]]≡c'-n[c] : n[g[b]] ≡ c'-n[c]
+            n[g[b]]≡c'-n[c] = n[g[b]]≡s[m[b]] ∙ s[m[b]]≡c'-n[c]
+
+            n[g[b]]+n[c]≡c' : C' .snd .GroupStr._·_ n[g[b]] n[c] ≡ c'
+            n[g[b]]+n[c]≡c' =
+              let open GroupStr (C' .snd) in
+              cong (_· n[c]) n[g[b]]≡c'-n[c] ∙ sym (·Assoc c' (inv n[c]) n[c]) ∙ cong (c' ·_) (·InvL n[c]) ∙ ·IdR c'
+
+            n[g[b]+c]≡c' : n .fst g[b]+c ≡ c'
+            n[g[b]+c]≡c' = n .snd .pres· g[b] c ∙ n[g[b]]+n[c]≡c'
+
+            goal3 = ∣ (g[b]+c , n[g[b]+c]≡c') ∣₁
+
+    lemma : BijectionIso C C'
+    lemma = bijIso n nInjective nSurjective