From 173e6d4bbf108bdeb80105d1c4117405b6e97e19 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Sat, 2 Nov 2024 14:48:30 -0500 Subject: [PATCH] wip --- src/Misc/FiveLemma.agda | 22 +++++++++++-- src/Misc/FiveLemmaGroup.agda | 60 ++++++++++++++++++++++++++++++++++++ src/Sorry.agda | 8 +++++ 3 files changed, 87 insertions(+), 3 deletions(-) create mode 100644 src/Misc/FiveLemmaGroup.agda create mode 100644 src/Sorry.agda diff --git a/src/Misc/FiveLemma.agda b/src/Misc/FiveLemma.agda index a287655..b6c1015 100644 --- a/src/Misc/FiveLemma.agda +++ b/src/Misc/FiveLemma.agda @@ -7,7 +7,6 @@ open import Cubical.Data.Sigma open import Cubical.Categories.Abelian open import Cubical.Categories.Additive open import Cubical.Categories.Category -open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Equiv open import Cubical.Foundations.Pointed open import Cubical.Foundations.Prelude @@ -57,6 +56,22 @@ private module fiveLemma (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 = + let z1 = coker f in + let z2 = ker z1 in + hasKernels (coker f) .Kernel.k , z2 + + 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 + module _ (A B C D E A' B' C' D' E' : ob) (f : Hom[ A , B ]) @@ -72,9 +87,10 @@ module fiveLemma (AC : AbelianCategory ℓ ℓ') where (s : Hom[ B' , C' ]) (t : Hom[ C' , D' ]) (u : Hom[ D' , E' ]) - (fgExact : ker g ≃ ?) + (fgExact : {! ker g !} ≃ {! !}) where z = let z1 = ker f in {! !} + x = isEmbedding×isSurjection→isEquiv -- 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) @@ -85,4 +101,4 @@ module fiveLemma (AC : AbelianCategory ℓ ℓ') where -- nIsEmbedding c1 c2 = {! !} -- nIsSurjection : isSurjection (fst n) - -- nIsSurjection b = {! !} \ No newline at end of file + -- nIsSurjection b = {! !} \ No newline at end of file diff --git a/src/Misc/FiveLemmaGroup.agda b/src/Misc/FiveLemmaGroup.agda new file mode 100644 index 0000000..e206960 --- /dev/null +++ b/src/Misc/FiveLemmaGroup.agda @@ -0,0 +1,60 @@ +{-# OPTIONS --cubical #-} + +module Misc.FiveLemmaGroup where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Function +open import Cubical.Foundations.Isomorphism + +open import Cubical.Data.Unit + +open import Cubical.Algebra.Group.Base +open import Cubical.Algebra.Group.Morphisms +open import Cubical.Algebra.Group.MorphismProperties +open import Cubical.Algebra.Group.GroupPath +open import Cubical.Algebra.Group.Instances.Unit + +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 : GroupHom B B') + (n : GroupHom C C') + (p : GroupHom 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) + (mIso : isIso (m .fst)) + (pIso : isIso (p .fst)) + (q : isMono p) + where + + sur : isSurjective n + + mono : isMono n + + lemma : isIso (n .fst) + lemma = gg , {! !} , {! !} where + gg : C' .fst → C .fst + gg = {! !} + \ No newline at end of file diff --git a/src/Sorry.agda b/src/Sorry.agda new file mode 100644 index 0000000..55a57dd --- /dev/null +++ b/src/Sorry.agda @@ -0,0 +1,8 @@ +{-# OPTIONS --cubical-compatible #-} + +module Sorry where + +open import Agda.Primitive + +postulate + sorry : {l : Level} → {A : Set l} → A