solve the second part too, closes #48
This commit is contained in:
parent
57ce453194
commit
90f76baca0
6 changed files with 223 additions and 26 deletions
|
|
@ -1,13 +1,13 @@
|
|||
{-# OPTIONS --cubical #-}
|
||||
|
||||
module Misc.Exact where
|
||||
module Misc.FiveLemma.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.Data.Sigma
|
||||
open import Cubical.Foundations.Equiv
|
||||
open import Cubical.Foundations.Pointed
|
||||
open import Cubical.Foundations.Prelude
|
||||
|
|
@ -15,6 +15,8 @@ open import Cubical.Foundations.Structure
|
|||
open import Cubical.Functions.Embedding
|
||||
open import Cubical.Functions.Surjection
|
||||
|
||||
open import Misc.FiveLemma.GroupMorphisms
|
||||
|
||||
private
|
||||
variable
|
||||
ℓ ℓ' : Level
|
||||
|
|
|
|||
18
src/Misc/FiveLemma/Group/Exact.agda
Normal file
18
src/Misc/FiveLemma/Group/Exact.agda
Normal file
|
|
@ -0,0 +1,18 @@
|
|||
{-# OPTIONS --cubical #-}
|
||||
|
||||
module Misc.FiveLemma.Group.Exact where
|
||||
|
||||
open import Agda.Primitive
|
||||
open import Cubical.Algebra.Group.Base
|
||||
open import Cubical.Algebra.Group.Morphisms
|
||||
open import Cubical.Foundations.Equiv
|
||||
open import Cubical.Foundations.Prelude
|
||||
open import Cubical.Foundations.Structure
|
||||
open import Misc.FiveLemma.Group.Morphisms
|
||||
|
||||
private
|
||||
variable
|
||||
ℓ ℓ' : Level
|
||||
|
||||
isExact : {A B C : Group ℓ} → (f : GroupHom A B) → (g : GroupHom B C) → Type ℓ
|
||||
isExact {B = B} f g = (b : ⟨ B ⟩) → (isInKer g b) ≃ (isInIm' f b)
|
||||
134
src/Misc/FiveLemma/Group/Injective.agda
Normal file
134
src/Misc/FiveLemma/Group/Injective.agda
Normal file
|
|
@ -0,0 +1,134 @@
|
|||
{-# OPTIONS --cubical #-}
|
||||
|
||||
module Misc.FiveLemma.Group.Injective where
|
||||
|
||||
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.Algebra.Monoid
|
||||
open import Cubical.Algebra.Semigroup
|
||||
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 ; elim to propTruncElim)
|
||||
open import Cubical.HITs.Pushout.Base
|
||||
open import Cubical.HITs.Pushout
|
||||
|
||||
open import Misc.FiveLemma.Group.Morphisms
|
||||
open import Misc.FiveLemma.Group.Exact
|
||||
|
||||
open BijectionIso'
|
||||
open IsGroupHom
|
||||
open GroupStr using (1g)
|
||||
|
||||
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 : isExact f g) (gh : isExact g h) (hj : isExact h j)
|
||||
(rs : isExact r s) (st : isExact s t) (tu : isExact 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
|
||||
nInjective : isInjective n
|
||||
nInjective c c-in-ker[n] =
|
||||
let
|
||||
t[n[c]]≡0 : t .fst (n .fst c) ≡ D' .snd .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 .1g
|
||||
p[h[c]]≡0 = sym t[n[c]]≡p[h[c]] ∙ t[n[c]]≡0
|
||||
|
||||
h[c]≡0 : h .fst c ≡ D .snd .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]
|
||||
|
||||
b : ⟨ B ⟩
|
||||
b = fst c-in-im[g]
|
||||
|
||||
g[b]≡c : g .fst b ≡ c
|
||||
g[b]≡c = snd c-in-im[g]
|
||||
|
||||
n[g[b]]≡0 : n .fst (g .fst b) ≡ C' .snd .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 .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]
|
||||
|
||||
a' : ⟨ A' ⟩
|
||||
a' = fst m[b]-in-im[r]
|
||||
|
||||
r[a']≡m[b] : r .fst a' ≡ m[b]
|
||||
r[a']≡m[b] = snd m[b]-in-im[r]
|
||||
|
||||
a : ⟨ A ⟩
|
||||
a = lSurj a' .fst
|
||||
|
||||
l[a]≡a' : l .fst a ≡ a'
|
||||
l[a]≡a' = lSurj a' .snd
|
||||
|
||||
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] = invIsEq (fg (f .fst a) .snd) f[a]-in-im[f]
|
||||
|
||||
g[f[a]]≡0 : g .fst (f .fst a) ≡ C .snd .1g
|
||||
g[f[a]]≡0 = f[a]-in-ker[g]
|
||||
|
||||
c≡0 : c ≡ C .snd .1g
|
||||
c≡0 = sym g[f[a]]≡c ∙ g[f[a]]≡0
|
||||
in c≡0
|
||||
57
src/Misc/FiveLemma/Group/Lemma.agda
Normal file
57
src/Misc/FiveLemma/Group/Lemma.agda
Normal file
|
|
@ -0,0 +1,57 @@
|
|||
{-# OPTIONS --cubical #-}
|
||||
|
||||
module Misc.FiveLemma.Group.Lemma where
|
||||
|
||||
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.Algebra.Monoid
|
||||
open import Cubical.Algebra.Semigroup
|
||||
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 ; elim to propTruncElim)
|
||||
open import Cubical.HITs.Pushout.Base
|
||||
open import Cubical.HITs.Pushout
|
||||
|
||||
open import Misc.FiveLemma.Group.Morphisms
|
||||
open import Misc.FiveLemma.Group.Exact
|
||||
open import Misc.FiveLemma.Group.Injective
|
||||
open import Misc.FiveLemma.Group.Surjective
|
||||
|
||||
open BijectionIso'
|
||||
open IsGroupHom
|
||||
open GroupStr using (1g)
|
||||
|
||||
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 : isExact f g) (gh : isExact g h) (hj : isExact h j)
|
||||
(rs : isExact r s) (st : isExact s t) (tu : isExact 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
|
||||
nInj = nInjective A B C D E A' B' C' D' E' f g h j l m n p q r s t u fg gh hj rs st tu lSurj qInj sq1 sq2 sq3 sq4
|
||||
nSur = nSurjective A B C D E A' B' C' D' E' f g h j l m n p q r s t u fg gh hj rs st tu lSurj qInj sq1 sq2 sq3 sq4
|
||||
|
||||
lemma : BijectionIso' C C'
|
||||
lemma = bijIso' n nInj nSur
|
||||
|
|
@ -4,7 +4,7 @@
|
|||
-- Not sure why it's defined this way yet
|
||||
-- TODO: Find out
|
||||
|
||||
module Misc.FiveLemma.GroupMorphisms where
|
||||
module Misc.FiveLemma.Group.Morphisms where
|
||||
|
||||
open import Agda.Primitive
|
||||
open import Cubical.Algebra.Group
|
||||
|
|
@ -1,7 +1,6 @@
|
|||
```
|
||||
{-# OPTIONS --cubical #-}
|
||||
|
||||
module Misc.FiveLemma.FiveLemmaGroup where
|
||||
module Misc.FiveLemma.Group.Surjective where
|
||||
|
||||
open import Cubical.Algebra.Group.Base
|
||||
open import Cubical.Algebra.Group.GroupPath
|
||||
|
|
@ -24,7 +23,8 @@ open import Cubical.HITs.PropositionalTruncation.Properties
|
|||
open import Cubical.HITs.Pushout.Base
|
||||
open import Cubical.HITs.Pushout
|
||||
|
||||
open import Misc.FiveLemma.GroupMorphisms
|
||||
open import Misc.FiveLemma.Group.Morphisms
|
||||
open import Misc.FiveLemma.Group.Exact
|
||||
|
||||
open BijectionIso'
|
||||
open IsGroupHom
|
||||
|
|
@ -34,9 +34,6 @@ private
|
|||
variable
|
||||
ℓ ℓ' : Level
|
||||
|
||||
isExact : {A B C : Group ℓ} → (f : GroupHom A B) → (g : GroupHom B C) → Type ℓ
|
||||
isExact {B = B} f g = (b : ⟨ B ⟩) → (isInKer g b) ≃ (isInIm' f b)
|
||||
|
||||
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)
|
||||
|
|
@ -44,16 +41,15 @@ module _
|
|||
(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)
|
||||
(qMono : isMono q)
|
||||
(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
|
||||
|
||||
sur : isSurjective' n
|
||||
sur c' =
|
||||
nSurjective : isSurjective' n
|
||||
nSurjective c' =
|
||||
let
|
||||
d' : ⟨ D' ⟩
|
||||
d' = t .fst c'
|
||||
|
|
@ -92,7 +88,7 @@ module _
|
|||
q[j[d]]≡0 = sym u[p[d]]≡q[j[d]] ∙ u[p[d]]≡0
|
||||
|
||||
j[d]≡0 : j[d] ≡ E .snd .1g
|
||||
j[d]≡0 = qMono (q[j[d]]≡0 ∙ sym (q .snd .IsGroupHom.pres1))
|
||||
j[d]≡0 = qInj j[d] q[j[d]]≡0
|
||||
|
||||
d-in-ker[j] : isInKer j d
|
||||
d-in-ker[j] = j[d]≡0
|
||||
|
|
@ -189,14 +185,4 @@ module _
|
|||
|
||||
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'
|
||||
in g[b]+c , n[g[b]+c]≡c'
|
||||
|
||||
mono : isMono n
|
||||
mono x = {! !}
|
||||
|
||||
lemma : isIso (n .fst)
|
||||
lemma = gg , {! !} , {! !} where
|
||||
gg : C' .fst → C .fst
|
||||
gg c' = {! !}
|
||||
|
||||
```
|
||||
in g[b]+c , n[g[b]+c]≡c'
|
||||
Loading…
Reference in a new issue