From b7cba30de213ca16f650bb648b27950a0bb2fc51 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Sat, 4 Jan 2025 02:33:22 -0500
Subject: [PATCH] showed that this is an exact sequence

---
 src/ThesisWork/Exactness.agda        | 10 +++++-
 src/ThesisWork/HomotopyGroupLES.agda | 49 ++++++++++++++++++++++++++--
 2 files changed, 55 insertions(+), 4 deletions(-)

diff --git a/src/ThesisWork/Exactness.agda b/src/ThesisWork/Exactness.agda
index c62be5d..1fd00f1 100644
--- a/src/ThesisWork/Exactness.agda
+++ b/src/ThesisWork/Exactness.agda
@@ -9,6 +9,7 @@ open import Cubical.Foundations.Equiv
 open import Cubical.Algebra.Group
 open import Cubical.Algebra.Group.Morphisms
 open import Cubical.Data.Sigma
+open import Cubical.Structures.Successor
 
 private
   variable
@@ -37,4 +38,11 @@ module _ {A B C : Group ℓ} where
   isWeakExactAtRefl : (f : GroupHom A B) (g : GroupHom B C) → isWeakExactAt f g refl ≡ isExactAt f g
   isWeakExactAtRefl f g i = (b : ⟨ B ⟩) → (isInKer g (transportRefl b i) → isInIm f b) × (isInIm f b → isInKer g (transportRefl b i))
 
-record ExactSequence : Type where
\ No newline at end of file
+-- Type-valued exact sequence
+-- No truncations
+record ExactSequence∙ {ℓ ℓN : Level} (N : SuccStr ℓN) : Type (ℓ-max ℓN (ℓ-suc ℓ)) where
+  open SuccStr N
+  field
+    seq : (n : Index) → Pointed ℓ
+    fun : (n : Index) → seq (succ n) →∙ seq n
+    exactness : (n : Index) → isExactAt∙ (fun (succ n)) (fun n)
\ No newline at end of file
diff --git a/src/ThesisWork/HomotopyGroupLES.agda b/src/ThesisWork/HomotopyGroupLES.agda
index 801c743..952c35c 100644
--- a/src/ThesisWork/HomotopyGroupLES.agda
+++ b/src/ThesisWork/HomotopyGroupLES.agda
@@ -20,6 +20,8 @@ open import Cubical.Algebra.Group.Morphisms
 open import Cubical.Homotopy.Group.Base
 open import Cubical.Homotopy.Loopspace
 
+open import ThesisWork.Exactness
+
 -- The long exact sequence of homotopy groups
 -- Except indexed by a successor structure (Cubical.Structures.Successor)
 -- Also based off of Axel Ljungstrom's work in Cubical.Homotopy.Group.LES
@@ -94,12 +96,53 @@ module πLES {X Y : Pointed ℓ} (f : X →∙ Y) where
       fSeq : (n : ℕ) → (ASeq (suc n) →∙ ASeq n)
       fSeq n = (F'^ n (X , Y , f)) .snd .snd
 
+    module _ where
+      open ExactSequence∙
+      -- It is easy to show that (Aₙ,fₙ)ₙ is a type-valued exact sequence, since
+      -- Aₙ₊₂ is (definitionally) the fiber of fₙ
+      Aₙ,fₙ-ExactSequence∙ : ExactSequence∙ ℕ+
+      Aₙ,fₙ-ExactSequence∙ .seq = ASeq
+      Aₙ,fₙ-ExactSequence∙ .fun = fSeq
+      Aₙ,fₙ-ExactSequence∙ .exactness n b = ker→im , im→ker where
+        ker→im : isInKer∙ (fSeq n) b → isInIm∙ (fSeq (suc n)) b
+        ker→im k =
+          -- k : fₙ(b) ≡ 0_Aₙ
+          -- now trying to find an element b' : Aₙ₊₂ s.t fₙ₊₁(b') ≡ b
+          -- but we know Aₙ₊₂ is definitionally equal to the fiber of fₙ at Aₙ's basepoint
+          -- so essentially we are looking to find a pair:
+          -- - b'₁, an element of Aₙ₊₁
+          -- - b'₂, a proof that fₙ(b'₁) ≡ 0_Aₙ
+          -- Fortunately, we already have b and k to satisfy this.
+          --
+          -- The last part requires that fₙ₊₁((b, k)) ≡ b
+          -- But fₙ₊₁ is defined to be the fst projection
+          -- So this is refl
+          (b , k) , refl
+
+        im→ker : isInIm∙ (fSeq (suc n)) b → isInKer∙ (fSeq n) b
+        im→ker p =
+          -- p : b is in the image of fₙ₊₁
+          -- the proof of p is
+          -- - p₁, an element of the domain of fₙ₊₁, which is Aₙ₊₂
+          -- - p₂, a proof that fₙ₊₁(p₁) ≡ b
+          --
+          -- But since Aₙ₊₂ is defined to be the fiber of fₙ at Aₙ's basepoint
+          -- which means it consists of pairs...
+          -- - p₁₁, an element of Aₙ₊₁
+          -- - p₁₂, a proof that fₙ(p₁₁) ≡ 0_Aₙ
+          --
+          -- we now look for a proof that fₙ(b) ≡ 0_Aₙ
+          -- this is (_ : fₙ(b) ≡ fₙ(fₙ₊₁(p₁))) ∙ (_ : fₙ(p₁₁) ≡ 0_Aₙ)
+          cong (fSeq n .fst) (sym (p .snd)) ∙ p .fst .snd
+
     -- δ : ΩY → F
     δ : Ω Y →∙ F
-    δ = {! p₁  !} ∘∙ {!   !}
+    δ = {!   !} ∘∙ {! e⁻¹ .fst  !} where
+      e = lemmaEqv f
+      e⁻¹ = invEquiv∙ e
 
   πSeqHom : (n : NFin3) → GroupHom (πSeq (sucNFin3 n)) (πSeq n)
   πSeqHom (n , 0 , p) = πHom n f
   πSeqHom (n , 1 , p) = πHom n p₁
-  πSeqHom (n , 2 , p) = {! πHom  !} 
-  πSeqHom (n , suc (suc (suc k)) , p) = ⊥-rec (¬m+n<m p)  
\ No newline at end of file
+  πSeqHom (n , 2 , p) = {! πHom  !}  
+  πSeqHom (n , suc (suc (suc k)) , p) = ⊥-rec (¬m+n<m p)   
\ No newline at end of file