wip on five lemma and exact sequences
This commit is contained in:
parent
a959efa0b6
commit
fd9f01f914
4 changed files with 195 additions and 20 deletions
118
src/Misc/Exact.agda
Normal file
118
src/Misc/Exact.agda
Normal file
|
|
@ -0,0 +1,118 @@
|
|||
{-# OPTIONS --cubical #-}
|
||||
|
||||
module Misc.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.Foundations.Equiv
|
||||
open import Cubical.Foundations.Pointed
|
||||
open import Cubical.Foundations.Prelude
|
||||
open import Cubical.Foundations.Structure
|
||||
open import Cubical.Functions.Embedding
|
||||
open import Cubical.Functions.Surjection
|
||||
|
||||
private
|
||||
variable
|
||||
ℓ ℓ' : Level
|
||||
|
||||
module _ (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 = hasKernels (coker f) .Kernel.k , (ker (coker f))
|
||||
|
||||
isExact : {x y z : ob} (f : Hom[ x , y ]) (g : Hom[ y , z ]) → Type ℓ'
|
||||
isExact {y = y} f g = Σ (Hom[ (Kernel.k g-ker) , (fst f-im) ]) λ m → isIso cat m where
|
||||
f-im = image f
|
||||
g-ker = hasKernels g
|
||||
|
||||
module _ where
|
||||
open import Data.Fin
|
||||
open import Data.Nat
|
||||
open import Data.Vec
|
||||
|
||||
finExactSequence : {n : ℕ}
|
||||
→ (obSeq : Fin (suc (suc n)) → ob)
|
||||
→ (homSeq : (m : Fin (suc n)) → Hom[ (obSeq (inject₁ m)) , (obSeq (suc m)) ])
|
||||
→ Type ℓ'
|
||||
finExactSequence {n = n} obSeq homSeq =
|
||||
(m : Fin n) → isExact (homSeq (inject₁ m)) (homSeq (suc m))
|
||||
|
||||
pattern 3+ n = suc (suc (suc n))
|
||||
|
||||
-- Ob sequences must have at least 2 elements
|
||||
obSeq : (n : ℕ) → Type ℓ
|
||||
obSeq n = Vec ob (2+ n)
|
||||
|
||||
private
|
||||
z = ℕ.zero
|
||||
|
||||
zFin2 : Fin 2
|
||||
zFin2 = inject₁ Fin.zero
|
||||
|
||||
-- I am using Vec in the reverse way!!!
|
||||
|
||||
-- Fin 5 4 3 2 1 0
|
||||
-- obSeq = E :: D :: C :: B :: A :: []
|
||||
|
||||
-- Fin 4 3 2 1 0
|
||||
-- homSeq = de :: cd :: bc :: [ab]
|
||||
|
||||
-- sequence of Homs
|
||||
data HomSeq : {n : ℕ} → (os : obSeq n) → Type (ℓ-max ℓ ℓ') where
|
||||
h[_] : {os : obSeq z} → Hom[ lookup os (inject₁ Fin.zero) , lookup os (suc Fin.zero) ] → HomSeq os
|
||||
_h∷_ : {n : ℕ} {os : obSeq n} {o : ob}
|
||||
→ Hom[ (head os) , o ] → HomSeq os → HomSeq (o ∷ os)
|
||||
|
||||
homSeqN : {n : ℕ} → (os : obSeq n) → (m : Fin (suc n)) → Type ℓ'
|
||||
homSeqN {n = n} os m = Hom[ (lookup os (inject₁ m)) , (lookup os (suc m)) ]
|
||||
|
||||
op-inv : {n : ℕ} → (m : Fin n) → opposite (opposite m) ≡ m
|
||||
op-inv {n = n} m = sym (fuckyou2 n (opposite (opposite m))) ∙ {! !} ∙ fuckyou2 n m where
|
||||
fuckyou1 : (n : ℕ) → (m : Fin n) → Data.Nat._<_ (toℕ m) n
|
||||
fuckyou1 (suc n) Fin.zero = z<s
|
||||
fuckyou1 (suc n) (suc m) = s<s (fuckyou1 n m)
|
||||
|
||||
fuckyou2 : (n : ℕ) → (m : Fin n) → fromℕ< {m = toℕ m} (fuckyou1 n m) ≡ m
|
||||
fuckyou2 (suc n) Fin.zero = refl
|
||||
fuckyou2 (suc n) (suc m) = let IH = fuckyou2 n m in cong suc IH
|
||||
|
||||
fuckyou3 : (n : ℕ) → (m : Fin n) → Data.Nat._<_ (toℕ (opposite m)) n
|
||||
fuckyou3 (suc ℕ.zero) Fin.zero = z<s
|
||||
fuckyou3 (2+ n) Fin.zero = let IH = fuckyou3 (suc n) Fin.zero in s<s IH
|
||||
fuckyou3 (suc n) (suc m) = let IH = fuckyou3 n m in {! !}
|
||||
|
||||
homSeqLookup : {n : ℕ} {os : obSeq n} → HomSeq os → (m : Fin (suc n)) → homSeqN os m
|
||||
homSeqLookup {n = ℕ.zero} h[ x ] Fin.zero = x
|
||||
homSeqLookup {n = suc n} (_h∷_ {os = os} {o = o} h1 hs) m = helper {! opposite m !} where
|
||||
op = opposite m
|
||||
helper : (k : Fin (2+ n)) → homSeqN (o ∷ os) (opposite k)
|
||||
helper k = {! !}
|
||||
|
||||
-- Retrieve the LAST hom in the sequence
|
||||
hhead : ∀ {n : ℕ} {os : obSeq n} → HomSeq os → Hom[ {! !} , {! !} ]
|
||||
-- hhead h[ x ] = x
|
||||
-- hhead (x h∷ hs) = x
|
||||
|
||||
-- htail : ∀ {n : ℕ} {os : obSeq (suc n)} → HomSeq os → HomSeq (tail os)
|
||||
-- htail {n} {x ∷ os} (x₁ h∷ hs) = hs
|
||||
|
||||
-- hlookup : ∀ {n : ℕ} {os : obSeq (suc n)}
|
||||
-- → HomSeq os → (m : Fin n) → Hom[ lookup os (inject₁ (inject₁ (inject₁ m))) , lookup os (inject₁ (inject₁ (suc m))) ]
|
||||
-- hlookup {n = suc ℕ.zero} (x h∷ hs) m = {! x !}
|
||||
-- hlookup {n = 2+ n} hs m = {! !}
|
||||
|
||||
-- -- exactHomSeq must have at least 3 obs
|
||||
-- exactHomSeq : {n : ℕ} → {os : obSeq (suc n)} → HomSeq os → (m : Fin (suc n)) → Type ℓ'
|
||||
-- exactHomSeq {n = ℕ.zero} (y h∷ h[ x ]) Fin.zero = isExact x y
|
||||
-- exactHomSeq {n = suc n} (y h∷ (x h∷ x₂)) Fin.zero = {! !}
|
||||
-- exactHomSeq {n = suc n} (y h∷ (x h∷ x₂)) (suc m) = {! !}
|
||||
|
||||
-- -- exactHomVec : Type (ℓ-max ℓ ℓ')
|
||||
-- -- exactHomVec = {n : ℕ} {o : ob} →
|
||||
-- -- Σ (HomVec o n) λ h → finExactSequence {! !} {! !}
|
||||
|
|
@ -7,6 +7,7 @@ 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.Foundations.Equiv
|
||||
open import Cubical.Foundations.Pointed
|
||||
open import Cubical.Foundations.Prelude
|
||||
|
|
@ -23,19 +24,12 @@ module fiveLemma (AC : AbelianCategory ℓ ℓ') where
|
|||
|
||||
-- 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
|
||||
image f = hasKernels (coker f) .Kernel.k , (ker (coker f))
|
||||
|
||||
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
|
||||
isExact {y = y} f g = Σ (Hom[ (Kernel.k g-ker) , (fst f-im) ]) λ m → isIso cat m where
|
||||
f-im = image f
|
||||
g-ker = hasKernels g
|
||||
|
||||
module _
|
||||
(A B C D E A' B' C' D' E' : ob)
|
||||
|
|
@ -52,10 +46,25 @@ module fiveLemma (AC : AbelianCategory ℓ ℓ') where
|
|||
(s : Hom[ B' , C' ])
|
||||
(t : Hom[ C' , D' ])
|
||||
(u : Hom[ D' , E' ])
|
||||
(fgExact : {! ker g !} ≃ {! !})
|
||||
(fgExact : isExact f g)
|
||||
(ghExact : isExact g h)
|
||||
(hjExact : isExact h j)
|
||||
(rsExact : isExact r s)
|
||||
(stExact : isExact s t)
|
||||
(tuExact : isExact t u)
|
||||
(lEpi : isEpic cat l)
|
||||
(mIso : isIso cat m)
|
||||
(pIso : isIso cat p)
|
||||
(qMono : isMonic cat q)
|
||||
(sq1 : (_⋆_ l r) ≡ (_⋆_ f m))
|
||||
(sq2 : (_⋆_ m s) ≡ (_⋆_ g n))
|
||||
(sq3 : (_⋆_ n t) ≡ (_⋆_ h p))
|
||||
(sq4 : (_⋆_ p u) ≡ (_⋆_ j q))
|
||||
where
|
||||
z = let z1 = ker f in {! !}
|
||||
x = isEmbedding×isSurjection→isEquiv
|
||||
nEpi : isEpic cat n
|
||||
nEpi b∘n≡b'∘n = {! !} where
|
||||
|
||||
|
||||
-- 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)
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
```
|
||||
{-# OPTIONS --cubical #-}
|
||||
|
||||
module Misc.FiveLemmaGroup where
|
||||
|
|
@ -11,12 +12,13 @@ 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)
|
||||
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
|
||||
|
||||
|
|
@ -60,21 +62,36 @@ module _
|
|||
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)).
|
||||
u[t[c']] : ⟨ E' ⟩
|
||||
u[t[c']] = u .fst (t .fst c')
|
||||
|
||||
-- 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 : u[t[c']] ≡ E' .snd .1g
|
||||
u[t[c']]≡0 = {! d'-ker-u .snd !}
|
||||
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
|
||||
|
|
@ -92,4 +109,5 @@ module _
|
|||
lemma = gg , {! !} , {! !} where
|
||||
gg : C' .fst → C .fst
|
||||
gg c' = {! !}
|
||||
|
||||
|
||||
```
|
||||
|
|
@ -2,3 +2,33 @@
|
|||
|
||||
module Misc.SnakeLemma 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.Foundations.Equiv
|
||||
open import Cubical.Foundations.Pointed
|
||||
open import Cubical.Foundations.Prelude
|
||||
open import Cubical.Foundations.Structure
|
||||
open import Cubical.Functions.Embedding
|
||||
open import Cubical.Functions.Surjection
|
||||
|
||||
open import Misc.Exact
|
||||
|
||||
private
|
||||
variable
|
||||
ℓ ℓ' : Level
|
||||
|
||||
module snakeLemma (AC : AbelianCategory ℓ ℓ') where
|
||||
open AbelianCategory AC
|
||||
|
||||
module _
|
||||
(A B C A' B' C' : ob)
|
||||
(asdf : exactHomSeq ?)
|
||||
(f : Hom[ A , B ]) (g : Hom[ B , C ])
|
||||
(f' : Hom[ A' , B' ]) (g' : Hom[ B' , C' ])
|
||||
(a : Hom[ A , A' ]) (b : Hom[ B , B' ]) (c : Hom[ C , C' ])
|
||||
where
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue