exact sequences
This commit is contained in:
parent
90f76baca0
commit
ea7085c26d
5 changed files with 54 additions and 67 deletions
|
|
@ -1,6 +1,6 @@
|
|||
{-# OPTIONS --cubical #-}
|
||||
|
||||
module Misc.FiveLemma.Exact where
|
||||
module Misc.FiveLemma.Category.Exact where
|
||||
|
||||
open import Agda.Primitive
|
||||
open import Cubical.Categories.Abelian
|
||||
|
|
@ -15,8 +15,6 @@ open import Cubical.Foundations.Structure
|
|||
open import Cubical.Functions.Embedding
|
||||
open import Cubical.Functions.Surjection
|
||||
|
||||
open import Misc.FiveLemma.GroupMorphisms
|
||||
|
||||
private
|
||||
variable
|
||||
ℓ ℓ' : Level
|
||||
|
|
@ -59,7 +57,7 @@ module _ (AC : AbelianCategory ℓ ℓ') where
|
|||
|
||||
-- I am using Vec in the reverse way!!!
|
||||
|
||||
-- Fin 5 4 3 2 1 0
|
||||
-- Fin 5 0 1 2 3 4
|
||||
-- obSeq = E :: D :: C :: B :: A :: []
|
||||
|
||||
-- Fin 4 3 2 1 0
|
||||
|
|
@ -67,37 +65,24 @@ module _ (AC : AbelianCategory ℓ ℓ') where
|
|||
|
||||
-- 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)
|
||||
h[_] : {os : obSeq z} → Hom[ lookup os (suc Fin.zero) , lookup os (inject₁ 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)) ]
|
||||
homSeqN {n = n} os m = Hom[ (lookup os (opposite (inject₁ m))) , (lookup os (opposite (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 = {! !}
|
||||
-- homSeqLookupOpp : {n : ℕ} {os : obSeq n} → HomSeq os → (m : Fin (suc n)) → homSeqN os m
|
||||
-- homSeqLookupOpp {n = ℕ.zero} {os = y ∷ x ∷ []} h[ h ] Fin.zero = h
|
||||
-- homSeqLookupOpp {n = suc n} {os = y ∷ x ∷ os} (h1 h∷ hs) (suc m) =
|
||||
-- homSeqLookupOpp {n = n} {os = x ∷ os} hs {! !}
|
||||
-- homSeqLookup {n = ℕ.zero} h[ x ] Fin.zero = {! x !}
|
||||
-- homSeqLookup {n = suc n} (_h∷_ {os = os} {o = o} h1 hs) m = helper {! !} 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 : ∀ {n : ℕ} {os : obSeq n} → HomSeq os → Hom[ {! !} , {! !} ]
|
||||
-- hhead h[ x ] = x
|
||||
-- hhead (x h∷ hs) = x
|
||||
|
||||
|
|
@ -116,5 +101,5 @@ module _ (AC : AbelianCategory ℓ ℓ') where
|
|||
-- exactHomSeq {n = suc n} (y h∷ (x h∷ x₂)) (suc m) = {! !}
|
||||
|
||||
-- -- exactHomVec : Type (ℓ-max ℓ ℓ')
|
||||
-- -- exactHomVec = {n : ℕ} {o : ob} →
|
||||
-- -- exactHomVec = {n : ℕ} {o : ob} →
|
||||
-- -- Σ (HomVec o n) λ h → finExactSequence {! !} {! !}
|
||||
|
|
@ -1,6 +1,6 @@
|
|||
{-# OPTIONS --cubical #-}
|
||||
|
||||
module Misc.FiveLemma where
|
||||
module Misc.FiveLemma.Category.Lemma where
|
||||
|
||||
open import Agda.Primitive
|
||||
open import Cubical.Data.Sigma
|
||||
|
|
@ -15,4 +15,4 @@ private
|
|||
ℓ ℓ' : 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)
|
||||
isExact {B = B} f g = (b : ⟨ B ⟩) → (isInKer g b) ≃ (isInIm' f b)
|
||||
36
src/Misc/FiveLemma/Group/ExactSequence.agda
Normal file
36
src/Misc/FiveLemma/Group/ExactSequence.agda
Normal file
|
|
@ -0,0 +1,36 @@
|
|||
{-# OPTIONS --cubical #-}
|
||||
|
||||
module Misc.FiveLemma.Group.ExactSequence where
|
||||
|
||||
open import Agda.Primitive
|
||||
open import Cubical.Algebra.Group.Base
|
||||
open import Cubical.Algebra.Group.Morphisms
|
||||
open import Cubical.Data.Nat
|
||||
open import Data.Fin
|
||||
open import Cubical.Foundations.Equiv
|
||||
open import Cubical.Foundations.Prelude
|
||||
open import Cubical.Foundations.Structure
|
||||
open import Misc.FiveLemma.Group.Exact
|
||||
open import Misc.FiveLemma.Group.Morphisms
|
||||
|
||||
private
|
||||
variable
|
||||
ℓ ℓ' : Level
|
||||
|
||||
pattern 1+ n = suc n
|
||||
pattern 2+ n = suc (suc n)
|
||||
|
||||
inj1 = λ {m : ℕ} (n : Fin m) → inject₁ n
|
||||
inj2 = λ {m : ℕ} (n : Fin m) → inject₁ (inject₁ n)
|
||||
|
||||
FiniteLES : {len : ℕ}
|
||||
→ (groupSeq : (n : Fin (2+ len)) → Group ℓ)
|
||||
→ (homSeq : (m : Fin (1+ len)) → GroupHom (groupSeq (inj1 m)) (groupSeq (suc m)))
|
||||
→ Type ℓ
|
||||
FiniteLES {len = len} groupSeq homSeq = (m : Fin len) → isExact (homSeq (inj1 m)) (homSeq (suc m))
|
||||
|
||||
InfiniteLES :
|
||||
(groupSeq : (n : ℕ) → Group ℓ)
|
||||
→ (homSeq : (n : ℕ) → GroupHom (groupSeq n) (groupSeq (suc n)))
|
||||
→ Type ℓ
|
||||
InfiniteLES groupSeq homSeq = (m : ℕ) → isExact (homSeq m) (homSeq (suc m))
|
||||
|
|
@ -1,34 +0,0 @@
|
|||
{-# OPTIONS --cubical #-}
|
||||
|
||||
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