From e21f6f701e5131d71bd03e554c7ac0dd973a0d4c Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Wed, 8 Jan 2025 16:32:17 -0500 Subject: [PATCH] eilenberg maclane spaces forms a spectrum --- src/ThesisWork/Cohomology.agda | 52 +++++++- src/ThesisWork/EMSpace.agda | 175 +++------------------------ src/ThesisWork/EMSpaceOld0.agda | 168 +++++++++++++++++++++++++ src/ThesisWork/Ext.agda | 1 + src/ThesisWork/HomotopyGroupLES.agda | 11 +- src/ThesisWork/README.md | 8 +- src/ThesisWork/Sequence.agda | 12 +- src/ThesisWork/SpectralSequence.agda | 2 +- src/ThesisWork/Spectrum.agda | 23 +++- 9 files changed, 276 insertions(+), 176 deletions(-) create mode 100644 src/ThesisWork/EMSpaceOld0.agda diff --git a/src/ThesisWork/Cohomology.agda b/src/ThesisWork/Cohomology.agda index 0e0fac8..d448c05 100644 --- a/src/ThesisWork/Cohomology.agda +++ b/src/ThesisWork/Cohomology.agda @@ -4,7 +4,55 @@ module ThesisWork.Cohomology where open import Cubical.Foundations.Prelude open import Cubical.Foundations.Pointed +open import Cubical.Foundations.Isomorphism +open import Cubical.Homotopy.Loopspace open import Cubical.Algebra.AbGroup +open import Cubical.Algebra.Group +open import Cubical.HITs.SetTruncation as ST +open import Cubical.HITs.Sn +open import Cubical.HITs.Susp +open import Cubical.Homotopy.EilenbergMacLane.Base +open import Cubical.Data.Nat +open import Cubical.Foundations.Equiv -Cohomology : ∀ {l} → (X : Pointed l) → AbGroup l -Cohomology = {! !} \ No newline at end of file +private + variable + ℓ ℓ' ℓ'' : Level + +-- nth Unreduced cohomology +UnreducedCohomology : (n : ℕ) → (X : Type ℓ) → (G : AbGroup ℓ') → Type (ℓ-max ℓ ℓ') +UnreducedCohomology n X G = ∥ (X → EM G n) ∥₂ + +-- nth Reduced cohomology +ReducedCohomology : (n : ℕ) → (X : Pointed ℓ) → (G : AbGroup ℓ') → Type (ℓ-max ℓ ℓ') +ReducedCohomology n X G = ∥ X →∙ EM∙ G n ∥₂ + +-- Examples +module Examples where + -- Theorem 4.1.7 in JHY thesis + module UnitCohomology (k : ℕ) where + open import Cubical.Data.Unit + open import Cubical.Data.Int + open import Cubical.Algebra.AbGroup.Instances.Int + + Unit∙ : Pointed₀ + Unit∙ = Unit , tt + + Lift∙ : ∀ {ℓ} → Pointed₀ → Pointed ℓ + Lift∙ (T , t) = (Lift T) , lift t + + module _ {B : Pointed₀} {n : ℕ} where + lemma1 : ∀ {n : ℕ} → + (S₊∙ (suc n) →∙ (Ω^ n) B ∙) + ≃∙ (S₊∙ n →∙ (Ω^ (suc n)) B ∙) + lemma1 {n} = + (S₊∙ (suc n) →∙ (Ω^ n) B ∙) ≃∙⟨ {! !} ⟩ + (Susp∙ (S₊ n) →∙ (Ω^ n) B ∙) ≃∙⟨ invEquiv (isoToEquiv ΩSuspAdjointIso) , {! !} ⟩ + (S₊∙ n →∙ Ω ((Ω^ n) B) ∙) ≃∙⟨ {! idEquiv∙ !} ⟩ + (S₊∙ n →∙ (Ω^ (suc n)) B ∙) ∎≃∙ + + lemma : (Lift∙ {ℓ} (S₊∙ n) →∙ B ∙) ≃∙ (Ω^ n) B + lemma = {! !} + + UnitCohomology : ReducedCohomology k Unit∙ ℤAbGroup ≡ Unit + UnitCohomology = isContr→≡Unit ({! !} , {! !}) \ No newline at end of file diff --git a/src/ThesisWork/EMSpace.agda b/src/ThesisWork/EMSpace.agda index 7ec0cc0..2108b61 100644 --- a/src/ThesisWork/EMSpace.agda +++ b/src/ThesisWork/EMSpace.agda @@ -2,167 +2,24 @@ module ThesisWork.EMSpace where -open import Cubical.Algebra.Group -open import Cubical.Algebra.Group.Base -open import Cubical.Algebra.Monoid -open import Cubical.Algebra.Semigroup -open import Cubical.Algebra.Group.Morphisms -open import Cubical.Data.Nat using (ℕ) -open import Cubical.Foundations.Function -open import Cubical.Foundations.HLevels -open import Cubical.Foundations.GroupoidLaws -open import Cubical.Foundations.Equiv -open import Cubical.Foundations.Isomorphism -open import Cubical.Foundations.Univalence -open import Cubical.Foundations.Pointed open import Cubical.Foundations.Prelude open import Cubical.Foundations.Structure -open import Cubical.Homotopy.Loopspace -open import Cubical.Homotopy.Group.Base -open import Cubical.HITs.SetTruncation as ST hiding (rec) -open import Cubical.HITs.GroupoidTruncation as GT hiding (rec) +open import Cubical.Algebra.Group -variable - ℓ ℓ' : Level - -data K[_,1] {ℓ : Level} (G : Group ℓ) : Type ℓ where - base : K[ G ,1] - loop : ⟨ G ⟩ → base ≡ base - loop-1g : loop (str G .GroupStr.1g) ≡ refl - loop-∙ : (x y : ⟨ G ⟩) → loop (G .snd .GroupStr._·_ x y) ≡ loop y ∙ loop x - squash : (x y : K[ G ,1]) (p q : x ≡ y) (r s : p ≡ q) → r ≡ s +private + variable + ℓ ℓ' ℓ'' : Level + +module _ {ℓ : Level} (GG : Group ℓ) where + G = GG .fst + open GroupStr (GG .snd) + data EM0 : Type ℓ where + base : EM0 + loop : G → base ≡ base + loop-1g : loop 1g ≡ refl + loop-∙ : (x y : G) → loop (x · y) ≡ loop y ∙ loop x + squash : (x y : EM0) (p q : x ≡ y) (r s : p ≡ q) → r ≡ s module _ where - open import Cubical.HITs.S1 renaming (base to S¹-base; loop to S¹-loop) - open import Cubical.Data.Int - open import Cubical.Algebra.Group.Instances.Int - - test : S¹ ≃ K[ ℤGroup ,1] - test = isoToEquiv (iso {! !} {! !} {! !} {! !}) where - loop^_ : ℤ → S¹-base ≡ S¹-base - -- loop^ pos (suc n) = (loop^ (pos n)) ∙ S¹-loop - -- loop^ pos zero = refl - -- loop^ negsuc zero = sym S¹-loop - -- loop^ negsuc (suc n) = (loop^ (negsuc n)) ∙ sym S¹-loop - - Code1 : S¹ → Type - Code1 S¹-base = ℤ - Code1 (S¹-loop i) = sucPathℤ i - - -- f : S¹ → K[ ℤGroup ,1] - -- f S¹-base = base - -- f (S¹-loop i) = loop (subst Code1 {! !} {! !}) i - - -- f : S¹ → K[ ℤGroup ,1] - -- f S¹-base = base - -- f (S¹-loop i) = loop (subst Code1 {! !} {! !}) i - - -- g : K[ ℤGroup ,1] → S¹ - -- g base = S¹-base - -- g (loop x i) = {! !} - -- g (loop-1g i i₁) = {! !} - -- g (loop-∙ x y i i₁) = {! !} - -- g (squash x y p q r s i j k) = {! !} - - - -------------------------------------------------------------------------------- --- Properties - --- ΩK(G,1) ≃ G - -module _ (G : Group ℓ) where - open GroupStr (G .snd) - - _⊙_ = _·_ - - K[G,1] = K[ G ,1] - - K[G,1]∙ : Pointed ℓ - K[G,1]∙ = K[G,1] , base - - ΩK[G,1] = Ω K[G,1]∙ - π1K[G,1] = π 1 K[G,1]∙ - - lemma1 : isOfHLevel 3 K[G,1] - lemma1 = squash - - lemma2 : isOfHLevel 2 ⟨ ΩK[G,1] ⟩ - lemma2 = squash base base - - ΩSetG : Pointed (ℓ-suc ℓ) - ΩSetG = (hSet ℓ) , (fst G) , is-set - - module Codes-aux where - f : (g : ⟨ G ⟩) → ⟨ G ⟩ ≃ ⟨ G ⟩ - f x = isoToEquiv (iso (λ y → y ⊙ x) (λ y → y ⊙ inv x) fg gf) where - fg : section (λ y → y ⊙ x) (λ y → y ⊙ inv x) - fg b = sym (·Assoc b (inv x) x) ∙ cong (b ⊙_) (·InvL x) ∙ ·IdR b - gf : retract (λ y → y ⊙ x) (λ y → y ⊙ inv x) - gf a = sym (·Assoc a x (inv x)) ∙ cong (a ⊙_) (·InvR x) ∙ ·IdR a - - feq : (g : ⟨ G ⟩) → ⟨ G ⟩ ≡ ⟨ G ⟩ - feq g = ua (f g) - - f1≡id : f 1g ≡ idEquiv ⟨ G ⟩ - f1≡id = equivEq (funExt (λ x → ·IdR x)) - - feq1≡refl : feq 1g ≡ refl - feq1≡refl = cong ua f1≡id ∙ uaIdEquiv - - flemma2 : (x y : ⟨ G ⟩) → f (x · y) ≡ compEquiv (f x) (f y) - flemma2 x y = equivEq (funExt (λ z → ·Assoc z x y)) - - S = Square - transpose : {A : Type ℓ} {a00 a01 a10 a11 : A} - {a0- : a00 ≡ a01} {a1- : a10 ≡ a11} {a-0 : a00 ≡ a10} {a-1 : a01 ≡ a11} - → Square a0- a1- a-0 a-1 → Square a-0 a-1 a0- a1- - transpose s i j = s j i - - Codes : K[G,1] → hSet ℓ - Codes base = ⟨ G ⟩ , is-set - Codes (loop x i) = (Codes-aux.feq x i) , z i where - z : PathP (λ i → isSet (Codes-aux.feq x i)) is-set is-set - z = toPathP (isPropIsSet (transport (λ i₁ → isSet (Codes-aux.feq x i₁)) is-set) is-set) - Codes (loop-1g i j) = {! !} - Codes (loop-∙ x y i j) = {! !} , {! !} - Codes (squash x y p q r s i j k) = CodesGpd (Codes x) (Codes y) (cong Codes p) (cong Codes q) (cong (cong Codes) r) (cong (cong Codes) s) i j k where - CodesGpd = isOfHLevelTypeOfHLevel 2 - - -- For point-free transports - Codes2 : K[G,1] → Type ℓ - Codes2 x = Codes x .fst - - fact : (x y : ⟨ G ⟩) → subst Codes2 (loop x) y ≡ y ⊙ x - fact x y = let z = sym (subst-filler {! !} {! !} {! !}) in {! !} - - encode : (z : K[G,1]) → base ≡ z → ⟨ Codes z ⟩ - encode z p = subst Codes2 p 1g - - decode : ⟨ G ⟩ → base ≡ base - decode x = loop x - - encode-decode : (x : ⟨ G ⟩) → encode base (decode x) ≡ x - encode-decode x = - encode base (decode x) ≡⟨ refl ⟩ - encode base (loop x) ≡⟨ refl ⟩ - subst Codes2 (loop x) 1g ≡⟨ fact x 1g ⟩ - 1g ⊙ x ≡⟨ ·IdL x ⟩ - x ∎ - - ΩKG1≃G' : GroupIso {! ΩK[G,1] !} G - - ΩKG1≃G : ⟨ ΩK[G,1] ⟩ ≃ ⟨ G ⟩ - ΩKG1≃G = isoToEquiv (iso f {! !} {! !} {! !}) where - f : ⟨ ΩK[G,1] ⟩ → ⟨ G ⟩ - f p = {! !} - - ΩKG1-idem-trunc : π 1 (K[G,1]∙) ≃ ⟨ ΩK[G,1] ⟩ - ΩKG1-idem-trunc = isoToEquiv (setTruncIdempotentIso lemma2) - - π₁KG1≃G : ⟨ πGr 0 (K[G,1]∙) ⟩ ≃ ⟨ G ⟩ - π₁KG1≃G = compEquiv ΩKG1-idem-trunc ΩKG1≃G - --- Uniqueness - -module _ (n : ℕ) (X Y : Pointed ℓ) where \ No newline at end of file + open import Cubical.HITs.EilenbergMacLane1 + open import Cubical.Homotopy.EilenbergMacLane.Base diff --git a/src/ThesisWork/EMSpaceOld0.agda b/src/ThesisWork/EMSpaceOld0.agda new file mode 100644 index 0000000..fe135b2 --- /dev/null +++ b/src/ThesisWork/EMSpaceOld0.agda @@ -0,0 +1,168 @@ +{-# OPTIONS --cubical #-} + +module ThesisWork.EMSpaceOld0 where + +open import Cubical.Algebra.Group +open import Cubical.Algebra.Group.Base +open import Cubical.Algebra.Monoid +open import Cubical.Algebra.Semigroup +open import Cubical.Algebra.Group.Morphisms +open import Cubical.Data.Nat using (ℕ) +open import Cubical.Foundations.Function +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.GroupoidLaws +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Pointed +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Structure +open import Cubical.Homotopy.Loopspace +open import Cubical.Homotopy.Group.Base +open import Cubical.HITs.SetTruncation as ST hiding (rec) +open import Cubical.HITs.GroupoidTruncation as GT hiding (rec) + +variable + ℓ ℓ' : Level + +data K[_,1] {ℓ : Level} (G : Group ℓ) : Type ℓ where + base : K[ G ,1] + loop : ⟨ G ⟩ → base ≡ base + loop-1g : loop (str G .GroupStr.1g) ≡ refl + loop-∙ : (x y : ⟨ G ⟩) → loop (G .snd .GroupStr._·_ x y) ≡ loop y ∙ loop x + squash : (x y : K[ G ,1]) (p q : x ≡ y) (r s : p ≡ q) → r ≡ s + +module _ where + open import Cubical.HITs.S1 renaming (base to S¹-base; loop to S¹-loop) + open import Cubical.Data.Int + open import Cubical.Algebra.Group.Instances.Int + + test : S¹ ≃ K[ ℤGroup ,1] + test = isoToEquiv (iso {! !} {! !} {! !} {! !}) where + loop^_ : ℤ → S¹-base ≡ S¹-base + -- loop^ pos (suc n) = (loop^ (pos n)) ∙ S¹-loop + -- loop^ pos zero = refl + -- loop^ negsuc zero = sym S¹-loop + -- loop^ negsuc (suc n) = (loop^ (negsuc n)) ∙ sym S¹-loop + + Code1 : S¹ → Type + Code1 S¹-base = ℤ + Code1 (S¹-loop i) = sucPathℤ i + + -- f : S¹ → K[ ℤGroup ,1] + -- f S¹-base = base + -- f (S¹-loop i) = loop (subst Code1 {! !} {! !}) i + + -- f : S¹ → K[ ℤGroup ,1] + -- f S¹-base = base + -- f (S¹-loop i) = loop (subst Code1 {! !} {! !}) i + + -- g : K[ ℤGroup ,1] → S¹ + -- g base = S¹-base + -- g (loop x i) = {! !} + -- g (loop-1g i i₁) = {! !} + -- g (loop-∙ x y i i₁) = {! !} + -- g (squash x y p q r s i j k) = {! !} + + + +------------------------------------------------------------------------------- +-- Properties + +-- ΩK(G,1) ≃ G + +module _ (G : Group ℓ) where + open GroupStr (G .snd) + + _⊙_ = _·_ + + K[G,1] = K[ G ,1] + + K[G,1]∙ : Pointed ℓ + K[G,1]∙ = K[G,1] , base + + ΩK[G,1] = Ω K[G,1]∙ + π1K[G,1] = π 1 K[G,1]∙ + + lemma1 : isOfHLevel 3 K[G,1] + lemma1 = squash + + lemma2 : isOfHLevel 2 ⟨ ΩK[G,1] ⟩ + lemma2 = squash base base + + ΩSetG : Pointed (ℓ-suc ℓ) + ΩSetG = (hSet ℓ) , (fst G) , is-set + + module Codes-aux where + f : (g : ⟨ G ⟩) → ⟨ G ⟩ ≃ ⟨ G ⟩ + f x = isoToEquiv (iso (λ y → y ⊙ x) (λ y → y ⊙ inv x) fg gf) where + fg : section (λ y → y ⊙ x) (λ y → y ⊙ inv x) + fg b = sym (·Assoc b (inv x) x) ∙ cong (b ⊙_) (·InvL x) ∙ ·IdR b + gf : retract (λ y → y ⊙ x) (λ y → y ⊙ inv x) + gf a = sym (·Assoc a x (inv x)) ∙ cong (a ⊙_) (·InvR x) ∙ ·IdR a + + feq : (g : ⟨ G ⟩) → ⟨ G ⟩ ≡ ⟨ G ⟩ + feq g = ua (f g) + + f1≡id : f 1g ≡ idEquiv ⟨ G ⟩ + f1≡id = equivEq (funExt (λ x → ·IdR x)) + + feq1≡refl : feq 1g ≡ refl + feq1≡refl = cong ua f1≡id ∙ uaIdEquiv + + flemma2 : (x y : ⟨ G ⟩) → f (x · y) ≡ compEquiv (f x) (f y) + flemma2 x y = equivEq (funExt (λ z → ·Assoc z x y)) + + S = Square + transpose : {A : Type ℓ} {a00 a01 a10 a11 : A} + {a0- : a00 ≡ a01} {a1- : a10 ≡ a11} {a-0 : a00 ≡ a10} {a-1 : a01 ≡ a11} + → Square a0- a1- a-0 a-1 → Square a-0 a-1 a0- a1- + transpose s i j = s j i + + Codes : K[G,1] → hSet ℓ + Codes base = ⟨ G ⟩ , is-set + Codes (loop x i) = (Codes-aux.feq x i) , z i where + z : PathP (λ i → isSet (Codes-aux.feq x i)) is-set is-set + z = toPathP (isPropIsSet (transport (λ i₁ → isSet (Codes-aux.feq x i₁)) is-set) is-set) + Codes (loop-1g i j) = {! !} + Codes (loop-∙ x y i j) = {! !} , {! !} + Codes (squash x y p q r s i j k) = CodesGpd (Codes x) (Codes y) (cong Codes p) (cong Codes q) (cong (cong Codes) r) (cong (cong Codes) s) i j k where + CodesGpd = isOfHLevelTypeOfHLevel 2 + + -- For point-free transports + Codes2 : K[G,1] → Type ℓ + Codes2 x = Codes x .fst + + fact : (x y : ⟨ G ⟩) → subst Codes2 (loop x) y ≡ y ⊙ x + fact x y = let z = sym (subst-filler {! !} {! !} {! !}) in {! !} + + encode : (z : K[G,1]) → base ≡ z → ⟨ Codes z ⟩ + encode z p = subst Codes2 p 1g + + decode : ⟨ G ⟩ → base ≡ base + decode x = loop x + + encode-decode : (x : ⟨ G ⟩) → encode base (decode x) ≡ x + encode-decode x = + encode base (decode x) ≡⟨ refl ⟩ + encode base (loop x) ≡⟨ refl ⟩ + subst Codes2 (loop x) 1g ≡⟨ fact x 1g ⟩ + 1g ⊙ x ≡⟨ ·IdL x ⟩ + x ∎ + + ΩKG1≃G' : GroupIso {! ΩK[G,1] !} G + + ΩKG1≃G : ⟨ ΩK[G,1] ⟩ ≃ ⟨ G ⟩ + ΩKG1≃G = isoToEquiv (iso f {! !} {! !} {! !}) where + f : ⟨ ΩK[G,1] ⟩ → ⟨ G ⟩ + f p = {! !} + + ΩKG1-idem-trunc : π 1 (K[G,1]∙) ≃ ⟨ ΩK[G,1] ⟩ + ΩKG1-idem-trunc = isoToEquiv (setTruncIdempotentIso lemma2) + + π₁KG1≃G : ⟨ πGr 0 (K[G,1]∙) ⟩ ≃ ⟨ G ⟩ + π₁KG1≃G = compEquiv ΩKG1-idem-trunc ΩKG1≃G + +-- Uniqueness + +module _ (n : ℕ) (X Y : Pointed ℓ) where \ No newline at end of file diff --git a/src/ThesisWork/Ext.agda b/src/ThesisWork/Ext.agda index 12b33cf..d551081 100644 --- a/src/ThesisWork/Ext.agda +++ b/src/ThesisWork/Ext.agda @@ -5,6 +5,7 @@ module ThesisWork.Ext where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Pointed open import Cubical.Foundations.Structure open import Cubical.Foundations.Function open import Cubical.Algebra.Module diff --git a/src/ThesisWork/HomotopyGroupLES.agda b/src/ThesisWork/HomotopyGroupLES.agda index 6f7042d..70b099f 100644 --- a/src/ThesisWork/HomotopyGroupLES.agda +++ b/src/ThesisWork/HomotopyGroupLES.agda @@ -50,14 +50,15 @@ module _ where 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 +p₁ : ∀ {ℓ} {A∙ B∙ : Pointed ℓ} {f∙ : A∙ →∙ B∙} → Fiber f∙ →∙ A∙ +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 private -- Let p1 : fib_f →∗ A be the first projection. - p₁ : Fiber f∙ →∙ A∙ - p₁ = fst , refl - lol : (f∙ .fst a ≡ b) , f-eq ≃∙ (b ≡ b) , (λ i → b) lol .fst = pathToEquiv (cong (λ z → z ≡ b) f-eq) lol .snd i j = {! !} @@ -81,10 +82,6 @@ module πLES {X Y : Pointed ℓ} (f : X →∙ Y) where πSeq (n , 2 , p) = πGr n F πSeq (n , suc (suc (suc k)) , p) = ⊥-rec (¬m+n ExactSequence ChainComplex --> Homology ChainComplex --> CochainComplex + ChainComplex --> Homology CochainComplex --> Cohomology ChainComplex --> ExactSequence CochainComplex --> ExactSequence Cohomology --> Theorem5410 + ExactCouple --> DerivedCouple ExactSequence --> ExactCouple - + ExactSequence --> HomotopyGroupLES HomotopyGroupLES --> SpectrumLES Spectrum --> SpectrumMap SpectrumMap --> SpectrumMapTruncation SpectrumMapTruncation --> PostnikovTowerForSpectra - + ExactCouple --> BoundedExactCouple BoundedExactCouple --> ExactCoupleConvergence ExactCoupleConvergence --> Theorem537 - + Lemma549 --> Theorem5410 Theorem537 --> Theorem5410 PostnikovTowerForSpectra --> Theorem5410 diff --git a/src/ThesisWork/Sequence.agda b/src/ThesisWork/Sequence.agda index 1a43604..3ef5292 100644 --- a/src/ThesisWork/Sequence.agda +++ b/src/ThesisWork/Sequence.agda @@ -18,12 +18,18 @@ module _ {ℓN : Level} (N : SuccStr ℓN) where Sequence : ∀ {ℓ : Level} → (A : Index → Type ℓ) → Type (ℓ-max ℓ ℓN) Sequence A = (n : Index) → A n - record IsChainComplex {ℓS N : Level} + record IsChainComplex {ℓS : Level} (S : Sequence (λ _ → Pointed ℓS)) (F : Sequence (λ n → S (succ n) →∙ S n)) : Type (ℓ-max ℓN ℓS) where field - property : (n : Index) → + CC : (n : Index) → let Tₙ₊₂ = S (succ (succ n)) in let Tₙ₊₁ = S (succ n) in let Tₙ = S n in let dₙ₊₁ = F (succ n) in let dₙ = F n in - (dₙ ∘∙ dₙ₊₁) ≡ const∙ Tₙ₊₂ Tₙ \ No newline at end of file + (dₙ ∘∙ dₙ₊₁) ≡ const∙ Tₙ₊₂ Tₙ + + record IsExactSequence {ℓS : Level} + (S : Sequence (λ _ → Pointed ℓS)) + (F : Sequence (λ n → S (succ n) →∙ S n)) + : Type (ℓ-max ℓN ℓS) where + field \ No newline at end of file diff --git a/src/ThesisWork/SpectralSequence.agda b/src/ThesisWork/SpectralSequence.agda index 03822cf..d46f91e 100644 --- a/src/ThesisWork/SpectralSequence.agda +++ b/src/ThesisWork/SpectralSequence.agda @@ -41,4 +41,4 @@ module _ (R : Ring ℓ) where dᵣ∘dᵣ≡0 : (s : ℕ) → compGradedModuleHom (d s) (d s) ≡ idGradedModuleHom (E s) -- Isomorphisms - -- the cohomology of the cochain complex determined by dᵣ. \ No newline at end of file + -- the cohomology of the cochain complex determined by dᵣ. diff --git a/src/ThesisWork/Spectrum.agda b/src/ThesisWork/Spectrum.agda index bff9ef6..df68565 100644 --- a/src/ThesisWork/Spectrum.agda +++ b/src/ThesisWork/Spectrum.agda @@ -3,6 +3,7 @@ module ThesisWork.Spectrum where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Pointed open import Cubical.Foundations.Structure open import Cubical.Foundations.Equiv @@ -35,6 +36,7 @@ isPtEquivTo≃∙ f (fEqv , fPt) = (f .fst , fEqv) , fPt -- An Ω-spectrum or spectrum is a prespectrum (Y, e) where eₙ is a -- pointed equivalence for all n. record IsSpectrum {ℓ ℓ' : Level} {N : SuccStr ℓ'} (P : Prespectrum {ℓ = ℓ} N) : Type (ℓ-max ℓ ℓ') where + constructor mkIsSpectrum open Prespectrum P open SuccStr N field @@ -70,4 +72,23 @@ SpectrumMap S₁ S₂ = PrespectrumMap (S₁ .fst) (S₂ .fst) -- open SuccStr N -- field -- f : (n : Index) → Y₁ n →∙ Y₂ n - -- p : (n : Index) → (e₂ n ∘∙ f n) ∙∼ (Ω→ (f (succ n)) ∘∙ e₁ n) \ No newline at end of file + -- p : (n : Index) → (e₂ n ∘∙ f n) ∙∼ (Ω→ (f (succ n)) ∘∙ e₁ n) + +module _ where + open import Cubical.HITs.EilenbergMacLane1 + open import Cubical.Homotopy.EilenbergMacLane.Base + open import Cubical.Homotopy.EilenbergMacLane.Properties + open import Cubical.Structures.Successor + open import Cubical.Data.Nat + open import Cubical.Algebra.AbGroup + + -- EilenbergMacLane spaces form a spectrum + + open Prespectrum + + EMPrespectrum : (G : AbGroup ℓ) → Prespectrum {ℓ = ℓ} ℕ+ + EMPrespectrum G .Y n = EM∙ G n + EMPrespectrum G .e n = EM→ΩEM+1∙ n + + EMSpectrum : (G : AbGroup ℓ) → Spectrum {ℓ = ℓ} ℕ+ + EMSpectrum G = EMPrespectrum G , mkIsSpectrum (λ n → isoToIsEquiv (Iso-EM-ΩEM+1 n) , EM→ΩEM+1-0ₖ n) \ No newline at end of file