dev

src/ThesisWork/Cohomology.agda

@@ -25,34 +25,4 @@ 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 ({!   !} , {!   !}) 
+ReducedCohomology n X G = ∥ X →∙ EM∙ G n ∥₂

src/ThesisWork/Cohomology/Unit.agda

@@ -0,0 +1,56 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.Cohomology.Unit where
+
+import Cubical.HITs.SetTruncation as ST
+open import Cubical.Algebra.AbGroup
+open import Cubical.Algebra.AbGroup.Instances.Int
+open import Cubical.Algebra.Group
+open import Cubical.Data.Int
+open import Cubical.Data.Nat
+open import Cubical.Data.Unit
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Prelude
+open import Cubical.HITs.Sn
+open import Cubical.HITs.Susp
+open import Cubical.Homotopy.EilenbergMacLane.Base
+open import Cubical.Homotopy.Loopspace
+
+open import ThesisWork.Cohomology
+open ST using (∣_∣₂)
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+module UnitCohomology (k : ℕ) where
+  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 = {!   !}
+
+  fun : (n : ℕ) → Unit∙ →∙ EM∙ ℤAbGroup n
+  fun zero = (λ x → 0) , refl
+  fun (suc n) = (λ x → {!   !}) , {!   !}
+
+  reducedCohomologyIsContractible : isContr (ReducedCohomology k Unit∙ ℤAbGroup)
+  reducedCohomologyIsContractible = ∣ (fun k) ∣₂ , {!   !}
+
+  UnitCohomology : ReducedCohomology k Unit∙ ℤAbGroup ≡ Unit 
+  UnitCohomology = isContr→≡Unit reducedCohomologyIsContractible