wip homotopy group LES

src/ThesisWork/Exactness.agda

@@ -35,4 +35,6 @@ module _ {A B C : Group ℓ} where
   isExactAt f g = (b : ⟨ B ⟩) → (isInKer g b → isInIm f b) × (isInIm f b → isInKer g b)
 
   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))
+  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

src/ThesisWork/HomotopyGroupLES.agda

@@ -0,0 +1,105 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.HomotopyGroupLES where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
+open import Cubical.HITs.TypeQuotients
+open import Cubical.Foundations.Structure
+open import Cubical.Data.Sigma
+open import Cubical.Data.Fin
+open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order
+open import Cubical.Data.Empty renaming (rec to ⊥-rec)
+open import Cubical.Relation.Nullary
+open import Cubical.Structures.Successor
+open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Homotopy.Group.Base
+open import Cubical.Homotopy.Loopspace
+
+-- 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
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+module _ where
+  open SuccStr
+
+  NFin3 : Type ℓ-zero
+  NFin3 = ℕ × Fin 3
+
+  sucNFin3 : NFin3 → NFin3
+  sucNFin3 (n , 0 , _) = n , fsuc fzero
+  sucNFin3 (n , 1 , _) = n , fsuc (fsuc fzero)
+  sucNFin3 (n , 2 , _) = (suc n) , fzero
+  sucNFin3 (n , suc (suc (suc _)) , p) = ⊥-rec (¬m+n<m p)
+
+  NFin3+ : SuccStr ℓ-zero
+  NFin3+ .Index = NFin3
+  NFin3+ .succ = sucNFin3
+
+Fiber : {A B : Pointed ℓ} (f : A →∙ B) → Pointed ℓ
+Fiber {A = A , a} {B = B , b} (f , feq) = (fiber f b) , a , feq
+
+-- Lemma 4.1.5 in FVD thesis
+-- Suppose given a pointed map f : A →∗ B
+module _ {A B : Pointed ℓ} (f : A →∙ B) where
+  private
+    -- Let p1 : fib_f →∗ A be the first projection. 
+    p₁ : Fiber f →∙ A
+    p₁ = fst , refl
+
+  -- Then there is a pointed natural equivalence e_f
+  lemmaEqv : Fiber p₁ ≃∙ Ω B
+  lemmaEqv .fst = {!   !}
+  lemmaEqv .snd = {!   !}
+
+module πLES {X Y : Pointed ℓ} (f : X →∙ Y) where
+  private
+    F : Pointed ℓ
+    F = Fiber f
+
+  πSeq : NFin3 → Group ℓ
+  πSeq (n , 0 , p) = πGr n Y
+  πSeq (n , 1 , p) = πGr n X
+  πSeq (n , 2 , p) = πGr n F
+  πSeq (n , suc (suc (suc k)) , p) = ⊥-rec (¬m+n<m p)  
+
+  -- First projection pointed function
+  p₁ : F →∙ X
+  p₁ = fst , refl
+
+  -- Step 1
+  module Step1 where
+    arrow* = Σ (Pointed ℓ) λ X → Σ (Pointed ℓ) λ Y → X →∙ Y
+
+    private
+      F' : arrow* → arrow*
+      F' (X , Y , f) = Fiber f , X , fst , refl
+
+      F'^ : (n : ℕ) → arrow* → arrow*
+      F'^ zero a = a
+      F'^ (suc n) a = F' (F'^ n a)
+
+      -- Given a pointed map f : X →∗ Y, we define its fiber sequence
+      ASeq : ℕ → Pointed ℓ
+      ASeq n = (F'^ n (X , Y , f)) .snd .fst
+
+      fSeq : (n : ℕ) → (ASeq (suc n) →∙ ASeq n)
+      fSeq n = (F'^ n (X , Y , f)) .snd .snd
+
+    -- δ : ΩY → F
+    δ : Ω Y →∙ F
+    δ = {! p₁  !} ∘∙ {!   !}
+
+  π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)  

src/ThesisWork/Spectrum.agda

@@ -40,8 +40,8 @@ record IsSpectrum {ℓ ℓ' : Level} {N : SuccStr ℓ'} (P : Prespectrum {ℓ =
   field
     eIsEquiv : ∀ (n : Index) → isPointedEquiv (e n)
 
-Spectrum : SuccStr ℓ → Type (ℓ-suc ℓ)
-Spectrum {ℓ = ℓ} N = Σ (Prespectrum N) IsSpectrum
+Spectrum : ∀ {ℓ ℓ'} → SuccStr ℓ' → Type (ℓ-max (ℓ-suc ℓ) ℓ')
+Spectrum {ℓ} {ℓ'} N = Σ (Prespectrum {ℓ} {ℓ'} N) IsSpectrum
 
 ℤ-Spectrum : Type (ℓ-suc ℓ-zero)
 ℤ-Spectrum = Spectrum ℤ+
@@ -59,3 +59,15 @@ record PrespectrumMap {ℓN ℓ₁ ℓ₂ : Level} {N : SuccStr ℓN}
 
     -- TODO: Visualize this
     p : (n : Index) → (e₂ n ∘∙ f n) ∙∼ (Ω→ (f (succ n)) ∘∙ e₁ n)
+
+-- Also from definition 5.3.1 of FVD thesis
+-- TODO: Are we sure we can just discard the spectrum data?
+SpectrumMap : {ℓN ℓ₁ ℓ₂ : Level} {N : SuccStr ℓN} (S₁ : Spectrum {ℓ = ℓ₁} N) (S₂ : Spectrum {ℓ = ℓ₂} N) → Type (ℓ-max ℓN (ℓ-max ℓ₁ ℓ₂)) 
+SpectrumMap S₁ S₂ = PrespectrumMap (S₁ .fst) (S₂ .fst)
+
+  -- open Prespectrum (S₁ .fst) renaming (Y to Y₁; e to e₁)
+  -- open Prespectrum (S₂ .fst) renaming (Y to Y₂; e to e₂)
+  -- open SuccStr N
+  -- field
+  --   f : (n : Index) → Y₁ n →∙ Y₂ n
+  --   p : (n : Index) → (e₂ n ∘∙ f n) ∙∼ (Ω→ (f (succ n)) ∘∙ e₁ n)

src/ThesisWork/SpectrumLES.agda

@@ -0,0 +1,22 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.SpectrumLES where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Function
+open import Cubical.HITs.TypeQuotients
+open import Cubical.Foundations.Structure
+open import Cubical.Structures.Successor
+
+-- The main theorem of this file is the long exact sequence of spectra
+-- from Theorem 5.3.5 of FVD thesis
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+-- First, lemma 5.3.6 of FVD thesis
+private
+  module _ {N M : SuccStr ℓ} where
+    lemma : {!   !}