more work on homotopy group LES

This commit is contained in:
Michael Zhang 2025-01-23 23:10:11 -06:00
parent 858dfb532e
commit fea38f46f5
8 changed files with 441 additions and 12 deletions

View file

@ -6,6 +6,7 @@ open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.HITs.TypeQuotients
open import Cubical.Foundations.Structure
@ -21,6 +22,8 @@ open import Cubical.Algebra.Group.Morphisms
open import Cubical.Homotopy.Group.Base
open import Cubical.Homotopy.Loopspace
import Cubical.Homotopy.Group.LES
open import ThesisWork.Exactness
-- The long exact sequence of homotopy groups
@ -47,7 +50,7 @@ module _ where
NFin3+ .Index = NFin3
NFin3+ .succ = sucNFin3
Fiber : {A B : Pointed } (f : A B) Pointed
Fiber : {A B : Pointed } (f : A B) Pointed
Fiber {A = A , a} {B = B , b} (f , feq) = (fiber f b) , a , feq
-- General definition of p₁ as the first projection
@ -57,18 +60,77 @@ p₁ = fst , refl
-- Lemma 4.1.5 in FVD thesis
-- Suppose given a pointed map f : A →∗ B
module _ {A @ (A , a) B∙ @ (B , b) : Pointed } (f∙ @ (f , f-eq) : A∙ B∙) where
-- Fix this instance of p1
p1 = p₁ {A∙ = A∙} {B∙ = B∙} {f∙ = f∙}
private
-- Let p1 : fib_f →∗ A be the first projection.
lol : (f∙ .fst a b) , f-eq ≃∙ (b b) , (λ i b)
lol .fst = pathToEquiv (cong (λ z z b) f-eq)
lol .snd i j = {! !}
leg1 : (Σ (fiber f b) λ (a' , p) a' a) , ((a , f-eq) , refl) ≃∙ (Σ A λ a' (a' a) × (f a' b)) , (a , refl , f-eq)
leg1 = isoToEquiv (iso f1 g1 {! !} {! !}) , {! !} where
f1 : (Σ (fiber f b) λ (a' , p) a' a) (Σ A λ a' (a' a) × (f a' b))
f1 (fib , fib-eq) = (fib .fst) , fib-eq , subst (λ p f∙ .fst p b) (sym fib-eq) f-eq
g1 : (Σ A λ a' (a' a) × (f a' b)) (Σ (fiber f b) λ (a' , p) a' a)
g1 (a , a-pf , f-a) = (a , subst (λ p f∙ .fst p b) (sym a-pf) f-eq) , a-pf
fg : section f1 g1
fg x = {! !}
leg2 : (Σ A λ a' (a' a) × (f a' b)) , (a , refl , f-eq) ≃∙ (f a b) , f-eq
leg2 = isoToEquiv (iso f1 g1 {! !} {! !}) , {! !} where
f1 : (Σ A λ a' (a' a) × (f a' b)) (f a b)
f1 (a' , a-prf , f-prf) = subst (λ p f p b) a-prf f-prf
g1 : (f a b) (Σ A λ a' (a' a) × (f a' b))
g1 p = a , refl , p
fg : section f1 g1
fg p = substRefl {B = λ p f p b} p
gf : retract f1 g1
gf (a' , a-prf , f-prf) =
{! !}
-- f(a',a-prf,f-prf) = subst (λ p → f p ≡ b) a-prf f-prf
-- g(f(...)) = a , refl , subst (λ p → f p ≡ b) a-prf f-prf
-- ≡ a' , a-prf , f-prf
-- this becomes: a , refl , subst (λ p → f p ≡ b) refl f-prf ≡ a , refl , f-prf
leg3 : (f a b) , f-eq ≃∙ (b b) , refl
leg3 = (isoToEquiv (iso f1 g1 fg {! λ _ → refl !})) , {! !} where
f1 : f a b b b
f1 p = subst (λ x x b) p p
g1 : b b f a b
g1 p = f-eq p
fg : section f1 g1
fg p =
-- g1(p) = f-eq ∙ p
-- f1(g1(p)) = subst (λ x → x ≡ b) (f-eq ∙ p) (f-eq ∙ p)
{! !}
-- Then there is a pointed natural equivalence e_f
lemmaEqv∙ : Fiber p₁ ≃∙ Ω B∙
lemmaEqv∙ : Fiber p1 ≃∙ Ω B∙
lemmaEqv∙ =
Fiber p₁ ≃∙⟨ {! !}
(f a b) , f-eq ≃∙⟨ {! !}
Fiber p1 ≃∙⟨ idEquiv∙ (Fiber p1)
(Σ (fiber f b) λ (a' , p) a' a) , ((a , f-eq) , refl) ≃∙⟨ leg1
(Σ A λ a' (a' a) × (f a' b)) , (a , refl , f-eq) ≃∙⟨ {! leg2 !}
(f a b) , f-eq ≃∙⟨ leg3
(b b) , refl ≃∙⟨ idEquiv∙ (Ω B∙)
Ω B∙ ∎≃∙
-- wtf : (f a ≡ b) → (b ≡ b)
-- wtf p = subst (λ x → x ≡ b) p p
-- wtf2 : (f a ≡ b) ≃ (b ≡ b)
-- wtf2 = isoToEquiv (iso {! wtf !} {! !} {! !} {! !})
-- Fiber p1 ≃∙⟨ idEquiv∙ (Fiber p1) ⟩
-- fiber fst a , (a , f-eq) , refl ≃∙⟨ {! !} ⟩
-- (f a ≡ b) , f-eq ≃∙⟨ {! !} ⟩
-- (b ≡ b) , refl ≃∙⟨ idEquiv∙ (Ω B∙) ⟩
-- Ω B∙ ∎≃∙
-- lemmaEqv∙ .snd = {! !}
module πLES {X Y : Pointed } (f : X Y) where
@ -106,7 +168,7 @@ module πLES {X Y : Pointed } (f : X →∙ Y) where
_ : ASeq 2 F
_ = refl
_ : ASeq 3 Fiber (fst , {! refl !})
_ : ASeq 3 Fiber (fst , refl)
_ = refl
fSeq : (n : ) (ASeq (suc n) ASeq n)
@ -180,10 +242,10 @@ module πLES {X Y : Pointed } (f : X →∙ Y) where
gSeq (suc (suc (suc n))) = {! !}
diagHom : (n : ) GroupHom (πGr (suc n) Y) (πGr n F)
diagHom n = {! δ .fst !} , {! !}
diagHom n = {! δ .fst !} , record { pres· = {! !} ; pres1 = {! !} ; presinv = {! !} }
π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) = diagHom n
πSeqHom (n , suc (suc (suc k)) , p) = ⊥-rec (¬m+n<m p)
πSeqHom (n , suc (suc (suc k)) , p) = ⊥-rec (¬m+n<m p)

View file

@ -0,0 +1,68 @@
{-# OPTIONS --cubical #-}
module ThesisWork.HomotopyGroupLES2 where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Isomorphism
open import Cubical.Structures.Successor
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order hiding (eq)
open import Cubical.Data.Fin
open import Cubical.Data.Sigma
open import Cubical.Data.Empty renaming (rec to ⊥-rec)
open import Cubical.Homotopy.Loopspace
open import ThesisWork.Exactness
open import ThesisWork.HomotopyGroupLES2.Lemma415
open import ThesisWork.HomotopyGroupLES2.Util
open import ThesisWork.HomotopyGroupLES2.Step1 renaming (A to A')
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
module _ {} {X @ (X , x₀) : Pointed } {Y∙ @ (Y , y₀) : Pointed } where
module ΩLES (f∙ @ (f , f-eq) : X∙ Y∙) where
-- Fiber of f
F∙ : Pointed
F∙ = fiber f y₀ , x₀ , f-eq
-- Fix this instance of p1
p1 = p₁ {f∙ = f∙}
Lift∙ : ( ' : Level) Pointed Pointed (-max ')
Lift∙ ' P = (Lift {j = '} (P .fst)) , lift (P .snd)
seq : (n* : NFin3) Pointed
seq (n , 0 , _) = (Ω^ n) Y∙
seq (n , 1 , _) = (Ω^ n) X∙
seq (n , 2 , _) = ((Ω^ n) F∙)
seq (n , suc (suc (suc _)) , p) = ⊥-rec (¬m+n<m p)
fibfst : (n : ) (Ω^ n) F∙ (Ω^ n) X∙
fibfst n = Ω^→ n p1
A : (n : ) Pointed
A = A' f∙

View file

@ -0,0 +1,110 @@
{-# OPTIONS --cubical #-}
module ThesisWork.HomotopyGroupLES2.Lemma415 where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Isomorphism
open import Cubical.Homotopy.Loopspace
open import Cubical.Data.Sigma
open import ThesisWork.HomotopyGroupLES2.Util
private
variable
' '' : Level
module _ {A @ (A , a₀) : Pointed } {B∙ @ (B , b₀) : Pointed } (f∙ @ (f , f₀) : A∙ B∙) where
private
p1 : Fiber f∙ A∙
p1 = fst , refl
leg2 : (Σ (fiber f b₀) λ (a , p) a a₀) , ((a₀ , f₀) , refl) ≃∙ (Σ A λ a (a a₀) × (f a b₀)) , (a₀ , refl , f₀)
leg2 = isoToEquiv (iso fw gw (λ _ refl) (λ _ refl)) , refl where
fw : (Σ (fiber f b₀) λ (a , p) a a₀) (Σ A λ a (a a₀) × (f a b₀))
fw ((a , p) , q) = a , q , p
gw : (Σ A λ a (a a₀) × (f a b₀)) (Σ (fiber f b₀) λ (a , p) a a₀)
gw (a , q , p) = (a , p) , q
-- p : f(a) ≡ b₀
-- q : a ≡ a₀
--
-- ap_f(q) : f(a) ≡ f(a₀)
-- sym(ap_f(q)) ∙ p : f(a₀) ≡ b₀
-- f₀ : f(a₀) ≡ b₀
-- sym(f₀) ∙ sym(ap_f(q)) ∙ p : b₀ ≡ b₀
leg3 : (Σ A λ a (a a₀) × (f a b₀)) , (a₀ , refl , f₀) ≃∙ (f a₀ b₀) , f₀
leg3 = (isoToEquiv (iso fw gw fg gf)) , eq where
P : A Type
P a = f a b₀
fw : Σ A (λ a (a a₀) × (f a b₀)) f a₀ b₀
fw (a , p , feq) = subst P p feq
gw : f a₀ b₀ Σ A (λ a (a a₀) × (f a b₀))
gw p = a₀ , refl , p
fg : section fw gw
fg p = substRefl {B = λ a f a b₀} p
gf : retract fw gw
-- p : f a₀ ≡ b₀
-- fw (gw p) ≡ p
-- fw (a₀ , refl , p) ≡ p
-- subst (λ a' → f a' ≡ b₀) refl p ≡ p
test : (feq : f a₀ b₀) subst P refl feq feq
test feq = substRefl {B = P} feq
module _ (a : A) (p : a a₀) (feq : f a b₀) where
-- bottomFace : Square (subst P p feq) (subst P refl feq) (λ i → f (p (~ i))) refl
-- bottomFace i j = subst {! !} {! !} {! !} {! !}
postulate
-- TODO: FINISH THIS
topFace : Square (λ i f (p (~ i))) (λ i b₀) (subst P p feq) feq
-- topFace = {! !}
gf (a , p , feq) i = p (~ i) , (λ j p (~ i j)) , λ j topFace a p feq j i
-- gw (fw (a , p , feq)) ≡ (a , p , feq)
-- gw (subst (λ a' → f a' ≡ b₀) p feq) ≡ (a , p , feq)
-- (a₀ , refl , p) ≡ (a , p , feq)
eq : subst P refl f₀ f₀
eq = substRefl {B = P} f₀
leg4 : (f a₀ b₀) , f₀ ≃∙ Ω B∙
leg4 = isoToEquiv (iso fw gw fg gf) , eq where
fw : f a₀ b₀ b₀ b₀
fw p = sym f₀ p
gw : b₀ b₀ f a₀ b₀
gw p = f₀ p
fg : section fw gw
fg p = assoc (sym f₀) f₀ p cong (_∙ p) (lCancel f₀) sym (lUnit p)
gf : retract fw gw
gf p = assoc f₀ (sym f₀) p cong (_∙ p) (rCancel f₀) sym (lUnit p)
eq : sym f₀ f₀ refl
eq = lCancel f₀
eqv∙ : Fiber p1 ≃∙ Ω B∙
eqv∙ =
Fiber p1 ≃∙⟨ idEquiv∙ (Fiber p1)
(Σ (fiber f b₀) λ (a , p) a a₀) , ((a₀ , f₀) , refl) ≃∙⟨ leg2
(Σ A λ a (a a₀) × (f a b₀)) , (a₀ , refl , f₀) ≃∙⟨ leg3
(f a₀ b₀) , f₀ ≃∙⟨ leg4
Ω B∙ ∎≃∙
: Ω A∙ Ω B∙
= Ω→ f∙ ∘∙ sym∙
module _ {A @ (A , a₀) : Pointed } {B∙ @ (B , b₀) : Pointed } (f∙ @ (f , f₀) : A∙ B∙) where
private
p1 : Fiber f∙ A∙
p1 = fst , refl
q1 : Fiber p1 Fiber f∙
q1 = fst , refl
r1 : Fiber q1 Fiber p1
r1 = fst , refl
postulate
-- TODO: Finish
comm : ≃∙map (eqv∙ f∙) ∘∙ r1 f∙ ∘∙ ≃∙map (eqv∙ p1)

View file

@ -0,0 +1,93 @@
{-# OPTIONS --cubical #-}
module ThesisWork.HomotopyGroupLES2.Step1 where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Equiv
open import Cubical.Data.Sigma
open import Cubical.Homotopy.Loopspace
open import Cubical.Structures.Successor
open import Cubical.Data.Nat
open import ThesisWork.Exactness
open import ThesisWork.HomotopyGroupLES2.Util
open import ThesisWork.HomotopyGroupLES2.Lemma415
private
variable
' '' : Level
arrow : ( : Level) Type (-suc )
arrow = Σ (Pointed ) (λ X Σ (Pointed ) (λ Y X Y))
F : arrow arrow
F (X , Y , f) = ((fiber (f .fst) (Y .snd)) , (X .snd , f .snd)) , X , (fst , refl)
F^ : (n : ) arrow arrow
F^ zero x = x
F^ (suc n) x = F (F^ n x)
module _ {X @ (X , x) : Pointed } {Y∙ @ (Y , y) : Pointed } (f∙ @ (f , f₀) : X∙ Y∙) where
private
p1 : arrow Pointed
p1 (X , Y , f) = X
p2 : arrow Pointed
p2 (X , Y , f) = Y
p3 : (a : arrow ) (p1 a p2 a)
p3 (X , Y , f) = f
A : (n : ) Pointed
A n = p2 (F^ n (X∙ , Y∙ , f∙))
f^ : (n : ) A (suc n) A n
f^ n = p3 (F^ n (X∙ , Y∙ , f∙))
Aⁿ⁺²≡fibfⁿ : (n : ) A (suc (suc n)) Fiber (f^ n)
Aⁿ⁺²≡fibfⁿ n = refl
ker→im : (n : ) (b : fst (A (suc n))) isInKer∙ (f^ n) b isInIm∙ (f^ (suc n)) b
ker→im n b isInKer = (b , isInKer) , refl
-- b is in the kernel of fⁿ means that fⁿ(b) ≡ 0_(Aⁿ)
-- we need to prove that there is some (a : Aⁿ⁺²) s.t fⁿ⁺¹(a) ≡ b
-- but since Aⁿ⁺² ≡ fiber(fⁿ), then fst(a) : Aⁿ⁺¹ and snd(a) : fⁿ(fst(a)) ≡ 0_(Aⁿ)
im→ker : (n : ) (b : fst (A (suc n))) isInIm∙ (f^ (suc n)) b isInKer∙ (f^ n) b
im→ker n b (a , aIsInIm) = goal where
a' : fiber (f^ n .fst) (A n .snd)
a' = a
a'1 : A (suc n) .fst
a'1 = fst a'
a'2 : (f^ n .fst) a'1 A n .snd
a'2 = snd a'
a'IsInIm : (f^ (suc n) .fst) a' b
a'IsInIm = aIsInIm
goal : (f^ n .fst) b A n .snd
goal = subst (λ p (f^ n .fst) p A n .snd) a'IsInIm a'2
-- b isInIm means that there exists some (a : Aⁿ⁺²) s.t fⁿ⁺¹(a) ≡ b
-- we need to prove that fⁿ(b) ≡ 0_(Aⁿ)
-- but since Aⁿ⁺² ≡ fiber(fⁿ), fst(a) : Aⁿ⁺¹ and snd(a) : fⁿ(fst(a)) ≡ 0_(Aⁿ)
-- so we just need to substitute some fst(a) ≡ b into snd(a)
AⁿisExact : (n : ) isExactAt∙ (f^ (suc n)) (f^ n)
AⁿisExact n b = (ker→im n b) , (im→ker n b)
open ExactSequence∙
ASeq : ExactSequence∙ +
ASeq .seq = A
ASeq .fun = f^
ASeq .exactness = AⁿisExact
eqvf : (A 3) ≃∙ (Ω Y∙)
eqvf = eqv∙ f∙
-- Diagonal map
δ : Ω Y∙ Fiber f∙
δ = p₁ ∘∙ ≃∙map (invEquiv∙ eqvf)

View file

@ -0,0 +1,64 @@
{-# OPTIONS --cubical #-}
module ThesisWork.HomotopyGroupLES2.Step2 where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Data.Sigma
open import Cubical.Homotopy.Loopspace
open import Cubical.Data.Nat
open import Cubical.Structures.Successor
open import ThesisWork.Exactness
open import ThesisWork.HomotopyGroupLES2.Util
open import ThesisWork.HomotopyGroupLES2.Step1
open import ThesisWork.HomotopyGroupLES2.Lemma415
private
variable
' '' : Level
pattern 3+ n = suc (suc (suc n))
module _ {X @ (X , x) : Pointed } {Y∙ @ (Y , y) : Pointed } (f∙ @ (f , f₀) : X∙ Y∙) where
F∙ = Fiber f∙
B : (n : ) Pointed
B 0 = Y∙
B 1 = X∙
B 2 = F∙
B (3+ n) = Ω (B n)
g^ : (n : ) B (suc n) B n
g^ 0 = f∙
g^ 1 = p₁
g^ 2 = δ f∙
g^ (3+ n) = (g^ n)
_ : A f∙ 3 B 3
_ = ua∙ (eqv∙ f∙ .fst) (eqv∙ f∙ .snd)
module Lemma416 where
η : (n : ) A f∙ n ≃∙ B n
η 0 = idEquiv∙ Y∙
η 1 = idEquiv∙ X∙
η 2 = idEquiv∙ F∙
η (3+ n) =
A f∙ (3+ n) ≃∙⟨ eqv∙ (f^ f∙ n)
Ω (A f∙ n) ≃∙⟨ cong-≃∙ Ω (η n)
Ω (B n) ∎≃∙
eqvfg : (n : ) (≃∙map (η n) ∘∙ f^ f∙ n) ∙∼ (g^ n ∘∙ ≃∙map (η (suc n)))
eqvfg 0 = {! !}
eqvfg 1 = {! !}
eqvfg 2 = {! !}
eqvfg (3+ n) = {! !}
open ExactSequence∙
BSeq : ExactSequence∙ +
BSeq .seq = B
BSeq .fun = g^
BSeq .exactness = {! !}

View file

@ -0,0 +1,3 @@
{-# OPTIONS --cubical #-}
module ThesisWork.HomotopyGroupLES2.Step3 where

View file

@ -0,0 +1,29 @@
{-# OPTIONS --cubical #-}
module ThesisWork.HomotopyGroupLES2.Util where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Equiv
open import Cubical.Homotopy.Loopspace
private
variable
' '' : Level
-- Pointed fiber
Fiber : {X∙ Y∙ : Pointed } (f∙ @ (f , f-eq) : X∙ Y∙) Pointed
Fiber {X∙ = X∙} {Y∙ = Y∙} f∙ @ (f , f-eq) = (fiber f (Y∙ .snd)) , X∙ .snd , f-eq
-- General definition of p₁ as the first projection
p₁ : {A∙ B∙ : Pointed } {f∙ : A∙ B∙} Fiber f∙ A∙
p₁ = fst , refl
sym∙ : {A∙ @ (A , a) : Pointed } (Ω A∙) (Ω A∙)
sym∙ = sym , refl
Lift∙ : {i j : Level} Pointed i Pointed (-max i j)
Lift∙ {i = i} {j = j} P = (Lift {j = j} (P .fst)) , lift (P .snd)
cong-≃∙ : { '} {A∙ B∙ : Pointed } (f : Pointed Pointed ') (p : A∙ ≃∙ B∙) f A∙ ≃∙ f B∙
cong-≃∙ { = } {' = '} {B∙ = B∙} f p = Equiv∙J (λ T∙ T≃∙B f T∙ ≃∙ f B∙) (idEquiv∙ (f B∙)) p

View file

@ -1,2 +1,2 @@
include: src src/ThesisWork src/AOP talks
include: src src/AOP talks
depend: standard-library cubical