wip
This commit is contained in:
parent
c7f6942d7c
commit
4e65fc2a32
2 changed files with 39 additions and 11 deletions
src/ThesisWork/HomotopyGroupLES2
|
@ -13,7 +13,7 @@ open import Cubical.Structures.Successor
|
|||
|
||||
open import ThesisWork.Exactness
|
||||
open import ThesisWork.HomotopyGroupLES2.Util
|
||||
open import ThesisWork.HomotopyGroupLES2.Step1
|
||||
open import ThesisWork.HomotopyGroupLES2.Step1 renaming (A to A' ; f^ to f^')
|
||||
open import ThesisWork.HomotopyGroupLES2.Lemma415
|
||||
|
||||
private
|
||||
|
@ -23,6 +23,8 @@ private
|
|||
pattern 3+ n = suc (suc (suc n))
|
||||
|
||||
module _ {X∙ @ (X , x) : Pointed ℓ} {Y∙ @ (Y , y) : Pointed ℓ} (f∙ @ (f , f₀) : X∙ →∙ Y∙) where
|
||||
A = A' f∙
|
||||
f^ = f^' f∙
|
||||
F∙ = Fiber f∙
|
||||
|
||||
B : (n : ℕ) → Pointed ℓ
|
||||
|
@ -37,28 +39,50 @@ module _ {X∙ @ (X , x) : Pointed ℓ} {Y∙ @ (Y , y) : Pointed ℓ} (f∙ @ (
|
|||
g^ 2 = δ f∙
|
||||
g^ (3+ n) = -Ω (g^ n)
|
||||
|
||||
_ : A f∙ 3 ≡ B 3
|
||||
_ : A 3 ≡ B 3
|
||||
_ = ua∙ (eqv∙ f∙ .fst) (eqv∙ f∙ .snd)
|
||||
|
||||
module Lemma416 where
|
||||
η : (n : ℕ) → A f∙ n ≃∙ B n
|
||||
η : (n : ℕ) → A 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) ⟩
|
||||
A (3+ n) ≃∙⟨ eqv∙ (f^ n) ⟩
|
||||
Ω (A 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) = {! !}
|
||||
A≡B : A ≡ B
|
||||
A≡B = funExt (λ n → ua∙ (η n .fst) (η n .snd))
|
||||
|
||||
postulate
|
||||
-- TODO: Finish
|
||||
f∙∼g : (n : ℕ) → (≃∙map (η n) ∘∙ f^ n) ∙∼P (g^ n ∘∙ ≃∙map (η (suc n)))
|
||||
-- eqvfg 0 = {! !}
|
||||
-- eqvfg 1 = {! !}
|
||||
-- eqvfg 2 = {! !}
|
||||
-- eqvfg (3+ n) = {! !}
|
||||
|
||||
-- TODO: Is this actually easier?
|
||||
-- Potential point of deviation from FVD thesis
|
||||
f≡g' : (n : ℕ) → PathP (λ i → A≡B i (suc n) →∙ A≡B i n) (f^ n) (g^ n)
|
||||
f≡g' 0 i = {! !}
|
||||
-- at i = i0, A^ 1 →∙ A^ 0
|
||||
-- at i = i1, B^ 1 →∙ B^ 0
|
||||
f≡g' 1 i = {! !}
|
||||
f≡g' 2 i = {! !}
|
||||
f≡g' (3+ n) = {! !}
|
||||
|
||||
f≡g : PathP (λ i → (n : ℕ) → A≡B i (suc n) →∙ A≡B i n) f^ g^
|
||||
f≡g = funExt f≡g'
|
||||
|
||||
open Lemma416 using (f≡g)
|
||||
|
||||
BⁿisExact : (n : ℕ) → isExactAt∙ (g^ (suc n)) (g^ n)
|
||||
BⁿisExact n = transp (λ i → isExactAt∙ ((f≡g i) (suc n)) ((f≡g i) n)) i0 (AⁿisExact f∙ n)
|
||||
|
||||
open ExactSequence∙
|
||||
BSeq : ExactSequence∙ ℕ+
|
||||
BSeq .seq = B
|
||||
BSeq .fun = g^
|
||||
BSeq .exactness = {! !}
|
||||
BSeq .exactness = BⁿisExact
|
|
@ -1,3 +1,7 @@
|
|||
{-# OPTIONS --cubical #-}
|
||||
|
||||
module ThesisWork.HomotopyGroupLES2.Step3 where
|
||||
|
||||
open import ThesisWork.HomotopyGroupLES2.Step2 renaming (B to B' ; g^ to g^')
|
||||
|
||||
module _ {X∙ @ (X , x) : Pointed ℓ} {Y∙ @ (Y , y) : Pointed ℓ} (f∙ @ (f , f₀) : X∙ →∙ Y∙) where
|
||||
|
|
Loading…
Add table
Reference in a new issue