|
| 1 | +{-# OPTIONS --safe #-} |
| 2 | +module Cubical.Homotopy.Spectrum.Fiber where |
| 3 | + |
| 4 | +open import Cubical.Data.Int |
| 5 | +open import Cubical.Data.Sigma |
| 6 | +open import Cubical.Foundations.Equiv |
| 7 | +open import Cubical.Foundations.Function |
| 8 | +open import Cubical.Foundations.GroupoidLaws |
| 9 | +open import Cubical.Foundations.Isomorphism |
| 10 | +open import Cubical.Foundations.Pointed |
| 11 | +open import Cubical.Foundations.Pointed.Fiber |
| 12 | +open import Cubical.Foundations.Prelude |
| 13 | +open import Cubical.Foundations.Structure |
| 14 | +open import Cubical.Foundations.Univalence |
| 15 | +open import Cubical.Homotopy.Group.LES |
| 16 | +open import Cubical.Homotopy.Loopspace |
| 17 | +open import Cubical.Homotopy.Prespectrum |
| 18 | +open import Cubical.Homotopy.Spectrum |
| 19 | + |
| 20 | +private variable ℓ ℓ' : Level |
| 21 | + |
| 22 | +open Spectrum |
| 23 | +open GenericPrespectrum |
| 24 | + |
| 25 | +module _ {X Y : Spectrum ℓ} (f : X →Sp Y) where |
| 26 | + FiberSpSpace : ℤ → Pointed ℓ |
| 27 | + FiberSpSpace n = fiber∙ (f .fst n) |
| 28 | + |
| 29 | + -- This is just EquivJ but the other way around |
| 30 | + EquivJ' : {ℓ ℓ' : Level} {A B : Type ℓ} (P : (B : Type ℓ) → (e : A ≃ B) → Type ℓ') |
| 31 | + → (r : P A (idEquiv A)) → (e : A ≃ B) → P B e |
| 32 | + EquivJ' {A = A} {B} P r e = |
| 33 | + let r' = subst (λ z → P A z) (sym pathToEquivRefl) r in |
| 34 | + let zz = J (λ B' p' → P B' (pathToEquiv p')) r' (ua e) in |
| 35 | + subst (λ z → P B z) (pathToEquiv-ua e) zz |
| 36 | + |
| 37 | + Equiv∙J' : {ℓ ℓ' : Level} {A : Pointed ℓ} (C : (B : Pointed ℓ) → A ≃∙ B → Type ℓ') |
| 38 | + → C A (idEquiv (fst A) , refl) |
| 39 | + → {B : _} (e : A ≃∙ B) → C B e |
| 40 | + Equiv∙J' {ℓ = ℓ} {ℓ'} {A} C ind {B} (e , e₀) = let |
| 41 | + ind2 = |
| 42 | + EquivJ' |
| 43 | + (λ B' e' → (a' : ⟨ A ⟩) → (b' : B') |
| 44 | + → (p' : e' .fst a' ≡ b') |
| 45 | + → (C' : (B'' : Pointed ℓ) → A .fst , a' ≃∙ B'' → Type ℓ') |
| 46 | + → C' (A .fst , a') ((idEquiv (A .fst)) , refl) |
| 47 | + → C' (B' , b') (e' , p')) |
| 48 | + (λ a' b' p' C' ind' → J (λ b'' p'' → C' (A .fst , b'') ((idEquiv (A .fst)) , p'')) ind' p') |
| 49 | + in ind2 e (A .snd) (B .snd) e₀ C ind |
| 50 | + |
| 51 | + FiberSpMap : (n : ℤ) → FiberSpSpace n ≃∙ Ω (FiberSpSpace (sucℤ n)) |
| 52 | + FiberSpMap n = compEquiv∙ fib[fn]≡fib[Ωfn+1] Ωfib[fn+1]≡fib[Ωfn+1] where |
| 53 | + preEquivFiber : {ℓ : Level} {A B C : Pointed ℓ} (e : A ≃∙ B) (f : B →∙ C) → fiber∙ f ≃∙ fiber∙ (f ∘∙ ≃∙map e) |
| 54 | + preEquivFiber {A = A} {B} {C} e∙ @ (e , e₀) f∙ @ (f , f₀) = |
| 55 | + Equiv∙J' (λ B' e' → (f' : B' →∙ C) → fiber∙ f' ≃∙ fiber∙ (f' ∘∙ ≃∙map e')) reflCase e∙ f∙ where |
| 56 | + reflCase : (f' : (fst A , A .snd) →∙ C) → fiber∙ f' ≃∙ fiber∙ (f' ∘∙ ≃∙map (idEquiv (fst A) , refl)) |
| 57 | + reflCase f' .fst = isoToEquiv (iso (idfun _) (idfun _) (λ _ → refl) (λ _ → refl)) |
| 58 | + reflCase f' .snd = ΣPathP (refl , (lUnit _)) |
| 59 | + |
| 60 | + postEquivFiber : {ℓ : Level} {A B C : Pointed ℓ} (f : A →∙ B) (e : B ≃∙ C) → fiber∙ f ≃∙ fiber∙ (≃∙map e ∘∙ f) |
| 61 | + postEquivFiber {A = A} {B} {C} f∙ @ (f , f₀) e∙ @ (e , e₀) = |
| 62 | + Equiv∙J (λ B' e' → (f' : A →∙ B') → fiber∙ f' ≃∙ fiber∙ (≃∙map e' ∘∙ f')) reflCase e∙ f∙ where |
| 63 | + reflCase : (f' : A →∙ C) → fiber∙ f' ≃∙ fiber∙ (≃∙map (idEquiv (fst C) , refl) ∘∙ f') |
| 64 | + reflCase f' .fst = isoToEquiv (iso (idfun _) (idfun _) (λ _ → refl) (λ _ → refl)) |
| 65 | + reflCase f' .snd = ΣPathP (refl , rUnit (f' .snd)) |
| 66 | + |
| 67 | + fib[fn]≡fib[Ωfn+1] : fiber∙ (f .fst n) ≃∙ fiber∙ (Ω→ (f .fst (sucℤ n))) |
| 68 | + fib[fn]≡fib[Ωfn+1] = compEquiv∙ seg1 (compEquiv∙ seg2 (invEquiv∙ seg3)) where |
| 69 | + seg1 : fiber∙ (f .fst n) ≃∙ fiber∙ (≃∙map (spectrumEquiv Y n) ∘∙ f .fst n) |
| 70 | + seg1 = postEquivFiber (f .fst n) (spectrumEquiv Y n) |
| 71 | + |
| 72 | + seg3 : fiber∙ (Ω→ (f .fst (sucℤ n))) ≃∙ fiber∙ (Ω→ (f .fst (sucℤ n)) ∘∙ ≃∙map (spectrumEquiv X n)) |
| 73 | + seg3 = preEquivFiber (spectrumEquiv X n) (Ω→ (f .fst (sucℤ n))) |
| 74 | + |
| 75 | + pathToEquiv∙ : {A B : Pointed ℓ} → (A ≡ B) → A ≃∙ B |
| 76 | + pathToEquiv∙ p .fst = pathToEquiv (cong fst p) |
| 77 | + pathToEquiv∙ p .snd = fromPathP (cong snd p) |
| 78 | + |
| 79 | + seg2 : fiber∙ (≃∙map (spectrumEquiv Y n) ∘∙ f .fst n) ≃∙ fiber∙ (Ω→ (f .fst (sucℤ n)) ∘∙ ≃∙map (spectrumEquiv X n)) |
| 80 | + seg2 = fiber∙-respects-∙∼ (f .snd n) |
| 81 | + |
| 82 | + Ωfib[fn+1]≡fib[Ωfn+1] : fiber∙ (Ω→ (f .fst (sucℤ n))) ≃∙ Ω (FiberSpSpace (sucℤ n)) |
| 83 | + Ωfib[fn+1]≡fib[Ωfn+1] = invEquiv∙ ((isoToEquiv (ΩFibreIso (f .fst (sucℤ n)))) , ΩFibreIso∙ (f .fst (sucℤ n))) |
| 84 | + |
| 85 | + FiberSp : Spectrum ℓ |
| 86 | + FiberSp .prespectrum .space = FiberSpSpace |
| 87 | + FiberSp .prespectrum .map n = ≃∙map (FiberSpMap n) |
| 88 | + FiberSp .equiv n = FiberSpMap n .fst .snd |
0 commit comments