wip
This commit is contained in:
parent
fd9f01f914
commit
e02f49c46d
6 changed files with 256 additions and 113 deletions
195
src/Misc/FiveLemma/FiveLemmaGroup.lagda.md
Normal file
195
src/Misc/FiveLemma/FiveLemmaGroup.lagda.md
Normal file
|
|
@ -0,0 +1,195 @@
|
|||
```
|
||||
{-# OPTIONS --cubical #-}
|
||||
|
||||
module Misc.FiveLemma.FiveLemmaGroup 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.GroupMorphisms
|
||||
|
||||
open BijectionIso'
|
||||
open IsGroupHom
|
||||
open GroupStr using (1g)
|
||||
|
||||
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)
|
||||
(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)
|
||||
(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
|
||||
|
||||
sur : isSurjective' n
|
||||
-- Let c′ be an element of C′.
|
||||
sur c' =
|
||||
let
|
||||
d' : ⟨ D' ⟩
|
||||
d' = t .fst c'
|
||||
|
||||
-- Since p is surjective, there exists an element d in D with p(d) = t(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] = invIsEq (tu d' .snd) in
|
||||
im[t]→ker[u] (c' , refl)
|
||||
|
||||
u[p[d]]≡0 : u[p[d]] ≡ E' .snd .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 .1g
|
||||
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))
|
||||
|
||||
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]
|
||||
|
||||
c : ⟨ C ⟩
|
||||
c = d-in-im[h] .fst
|
||||
|
||||
h[c]≡d : h .fst c ≡ d
|
||||
h[c]≡d = d-in-im[h] .snd
|
||||
|
||||
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 .1g
|
||||
t[c'-n[c]]≡0 =
|
||||
let open GroupStr (C' .snd) renaming (_·_ to _·ᶜ_; inv to invᶜ) in
|
||||
let open GroupStr (D' .snd) renaming (_·_ to _·ᵈ_; inv to invᵈ) 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 (C' .snd .1g) ≡⟨ t .snd .pres1 ⟩
|
||||
D' .snd .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]
|
||||
|
||||
b' : ⟨ B' ⟩
|
||||
b' = [c'-n[c]]-in-im[s] .fst
|
||||
|
||||
s[b']≡c'-n[c] : s .fst b' ≡ c'-n[c]
|
||||
s[b']≡c'-n[c] = [c'-n[c]]-in-im[s] .snd
|
||||
|
||||
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]
|
||||
|
||||
n[g[b]] : ⟨ C' ⟩
|
||||
n[g[b]] = n .fst (g .fst 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'
|
||||
in c , {! !}
|
||||
|
||||
mono : isMono n
|
||||
mono x = {! !}
|
||||
|
||||
lemma : isIso (n .fst)
|
||||
lemma = gg , {! !} , {! !} where
|
||||
gg : C' .fst → C .fst
|
||||
gg c' = {! !}
|
||||
|
||||
```
|
||||
61
src/Misc/FiveLemma/GroupMorphisms.agda
Normal file
61
src/Misc/FiveLemma/GroupMorphisms.agda
Normal file
|
|
@ -0,0 +1,61 @@
|
|||
{-# OPTIONS --cubical #-}
|
||||
|
||||
-- I'm doing this just because isInIm is defined to be a mere prop
|
||||
-- Not sure why it's defined this way yet
|
||||
-- TODO: Find out
|
||||
|
||||
module Misc.FiveLemma.GroupMorphisms where
|
||||
|
||||
open import Agda.Primitive
|
||||
open import Cubical.Algebra.Group
|
||||
open import Cubical.Algebra.Group.MorphismProperties
|
||||
open import Cubical.Algebra.Group.Morphisms
|
||||
open import Cubical.Algebra.Semigroup
|
||||
open import Cubical.Data.Sigma
|
||||
open import Cubical.Foundations.Isomorphism
|
||||
open import Cubical.Foundations.Prelude
|
||||
open import Cubical.Foundations.Structure
|
||||
open import Cubical.HITs.PropositionalTruncation
|
||||
|
||||
private
|
||||
variable
|
||||
ℓ ℓ' : Level
|
||||
G H : Group ℓ
|
||||
|
||||
isInIm' : GroupHom G H → ⟨ H ⟩ → Type _
|
||||
isInIm' {G = G} ϕ h = Σ[ g ∈ ⟨ G ⟩ ] ϕ .fst g ≡ h
|
||||
|
||||
Im' : GroupHom G H → Type _
|
||||
Im' {H = H} ϕ = Σ[ x ∈ ⟨ H ⟩ ] isInIm' ϕ x
|
||||
|
||||
isSurjective' : GroupHom G H → Type _
|
||||
isSurjective' {H = H} ϕ = (x : ⟨ H ⟩) → isInIm' ϕ x
|
||||
|
||||
-- Group bijections
|
||||
record BijectionIso' (G : Group ℓ) (H : Group ℓ') : Type (ℓ-max ℓ ℓ') where
|
||||
constructor bijIso'
|
||||
|
||||
field
|
||||
fun : GroupHom G H
|
||||
inj : isInjective fun
|
||||
surj : isSurjective' fun
|
||||
|
||||
module _ where
|
||||
open GroupStr
|
||||
open BijectionIso'
|
||||
|
||||
BijectionIso'→GroupIso : BijectionIso' G H → GroupIso G H
|
||||
BijectionIso'→GroupIso {G = G} {H = H} i = grIso
|
||||
where
|
||||
f = fst (fun i)
|
||||
|
||||
helper : (b : _) → isProp (Σ[ a ∈ ⟨ G ⟩ ] f a ≡ b)
|
||||
helper _ (a , ha) (b , hb) =
|
||||
Σ≡Prop (λ _ → is-set (snd H) _ _)
|
||||
(isInjective→isMono (fun i) (inj i) (ha ∙ sym hb) )
|
||||
|
||||
grIso : GroupIso G H
|
||||
grIso = iso f g fg gf , snd (fun i) where
|
||||
g = λ b → rec (helper b) (λ a → a) ∣ (surj i b) ∣₁ .fst
|
||||
fg = λ b → rec (helper b) (λ a → a) ∣ (surj i b) ∣₁ .snd
|
||||
gf = λ b j → rec (helper (f b)) (λ a → a) (squash₁ ∣ (surj i (f b)) ∣₁ ∣ (b , refl) ∣₁ j) .fst
|
||||
|
|
@ -1,113 +0,0 @@
|
|||
```
|
||||
{-# OPTIONS --cubical #-}
|
||||
|
||||
module Misc.FiveLemmaGroup 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.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 BijectionIso
|
||||
open GroupStr
|
||||
|
||||
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 : 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)
|
||||
(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
|
||||
|
||||
sur : isSurjective n
|
||||
-- Let c′ be an element of C′.
|
||||
sur c' =
|
||||
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
|
||||
|
||||
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)).
|
||||
|
||||
-- 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 : 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
|
||||
-- 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
|
||||
mono x = {! !}
|
||||
|
||||
lemma : isIso (n .fst)
|
||||
lemma = gg , {! !} , {! !} where
|
||||
gg : C' .fst → C .fst
|
||||
gg c' = {! !}
|
||||
|
||||
```
|
||||
Loading…
Reference in a new issue