Reduced homology of CW complexes

Cubical/Algebra/AbGroup/Instances/FreeAbGroup.agda

@@ -19,6 +19,7 @@ open import Cubical.HITs.FreeAbGroup
 open import Cubical.Algebra.AbGroup
 open import Cubical.Algebra.AbGroup.Instances.Pi
 open import Cubical.Algebra.AbGroup.Instances.Int
+open import Cubical.Algebra.AbGroup.Instances.DirectProduct
 open import Cubical.Algebra.Group
 open import Cubical.Algebra.Group.Morphisms
 open import Cubical.Algebra.Group.MorphismProperties
@@ -413,3 +414,49 @@ agreeOnℤFinGenerator→≡ {n} {m} {ϕ} {ψ} idr =
       λ f p → IsGroupHom.presinv (snd ϕ) f
            ∙∙ (λ i x → -ℤ (p i x))
            ∙∙ sym (IsGroupHom.presinv (snd ψ) f)))
+
+--
+sumCoefficients : (n : ℕ) → AbGroupHom (ℤ[Fin n ]) (ℤ[Fin 1 ])
+fst (sumCoefficients n) v = λ _ → sumFinℤ v
+snd (sumCoefficients n) = makeIsGroupHom (λ x y → funExt λ _ → sumFinℤHom x y)
+
+ℤFinProductIso : (n m : ℕ) → Iso (ℤ[Fin (n +ℕ m) ] .fst) ((AbDirProd ℤ[Fin n ] ℤ[Fin m ]) .fst)
+ℤFinProductIso n m = iso sum→product product→sum product→sum→product sum→product→sum
+  where
+    sum→product : (ℤ[Fin (n +ℕ m) ] .fst) → ((AbDirProd ℤ[Fin n ] ℤ[Fin m ]) .fst)
+    sum→product x = ((λ (a , Ha) → x (a , <→<ᵗ (≤-trans (<ᵗ→< Ha) (≤SumLeft {n}{m}))))
+                    , λ (a , Ha) → x (n +ℕ a , <→<ᵗ (<-k+ {a}{m}{n} (<ᵗ→< Ha))))
+
+    product→sum : ((AbDirProd ℤ[Fin n ] ℤ[Fin m ]) .fst) → (ℤ[Fin (n +ℕ m) ] .fst)
+    product→sum (x , y) (a , Ha) with (a ≟ᵗ n)
+    ... | lt H = x (a , H)
+    ... | eq H = y (a ∸ n , <→<ᵗ (subst (a ∸ n <_) (∸+ m n) (<-∸-< a (n +ℕ m) n (<ᵗ→< Ha) (subst (λ a → a < n +ℕ m) H (<ᵗ→< Ha)))))
+    ... | gt H = y (a ∸ n , <→<ᵗ (subst (a ∸ n <_) (∸+ m n) (<-∸-< a (n +ℕ m) n (<ᵗ→< Ha) (<ᵗ→< (<ᵗ-trans {n}{a}{n +ℕ m} H Ha)))))
+
+    product→sum→product : ∀ x → sum→product (product→sum x) ≡ x
+    product→sum→product (x , y) = ≡-× (funExt (λ (a , Ha) → lemx a Ha)) (funExt (λ (a , Ha) → lemy a Ha))
+      where
+        lemx : (a : ℕ) (Ha : a <ᵗ n) → fst (sum→product (product→sum (x , y))) (a , Ha) ≡ x (a , Ha)
+        lemx a Ha with (a ≟ᵗ n)
+        ... | lt H = cong x (Fin≡ (a , H) (a , Ha) refl)
+        ... | eq H = rec (¬m<ᵗm (subst (λ a → a <ᵗ n) H Ha))
+        ... | gt H = rec (¬m<ᵗm (<ᵗ-trans Ha H))
+
+        lemy : (a : ℕ) (Ha : a <ᵗ m) → snd (sum→product (product→sum (x , y))) (a , Ha) ≡ y (a , Ha)
+        lemy a Ha with ((n +ℕ a) ≟ᵗ n)
+        ... | lt H = rec (¬m<m (≤<-trans (≤SumLeft {n}{a}) (<ᵗ→< H)))
+        ... | eq H = cong y (Fin≡ _ _ (∸+ a n))
+        ... | gt H = cong y (Fin≡ _ _ (∸+ a n))
+
+    sum→product→sum : ∀ x → product→sum (sum→product x) ≡ x
+    sum→product→sum x = funExt (λ (a , Ha) → lem a Ha)
+      where
+        lem : (a : ℕ) (Ha : a <ᵗ (n +ℕ m)) → product→sum (sum→product x) (a , Ha) ≡ x (a , Ha)
+        lem a Ha with (a ≟ᵗ n)
+        ... | lt H = cong x (Fin≡ _ _ refl)
+        ... | eq H = cong x (Fin≡ _ _ ((+-comm n (a ∸ n)) ∙ ≤-∸-+-cancel (subst (n ≤_) (sym H) ≤-refl)))
+        ... | gt H = cong x (Fin≡ _ _ ((+-comm n (a ∸ n)) ∙ ≤-∸-+-cancel (<-weaken (<ᵗ→< H))))
+
+ℤFinProduct : (n m : ℕ) → AbGroupIso ℤ[Fin (n +ℕ m) ] (AbDirProd ℤ[Fin n ] ℤ[Fin m ])
+fst (ℤFinProduct n m) = ℤFinProductIso n m
+snd (ℤFinProduct n m) = makeIsGroupHom (λ x y → refl)

Cubical/Algebra/ChainComplex/Homology.agda

@@ -35,42 +35,30 @@ open ChainComplex
 open finChainComplexMap
 open IsGroupHom
 
--- Definition of homology
-homology : (n : ℕ) → ChainComplex ℓ → Group ℓ
-homology n C = ker∂n / img∂+1⊂ker∂n
-  where
-  Cn+2 = AbGroup→Group (chain C (suc (suc n)))
-  ∂n = bdry C n
-  ∂n+1 = bdry C (suc n)
-  ker∂n = kerGroup ∂n
-
-  -- Restrict ∂n+1 to ker∂n
-  ∂'-fun : Cn+2 .fst → ker∂n .fst
-  fst (∂'-fun x) = ∂n+1 .fst x
-  snd (∂'-fun x) = t
-    where
-    opaque
-     t : ⟨ fst (kerSubgroup ∂n) (∂n+1 .fst x) ⟩
-     t = funExt⁻ (cong fst (bdry²=0 C n)) x
+module _ (n : ℕ) (C : ChainComplex ℓ) where
+  ker∂n = kerGroup (bdry C n)
 
-  ∂' : GroupHom Cn+2 ker∂n
-  fst ∂' = ∂'-fun
-  snd ∂' = isHom
+  ∂ker : GroupHom (AbGroup→Group (chain C (suc (suc n)))) ker∂n
+  ∂ker .fst x = (bdry C (suc n) .fst x) , t
     where
     opaque
-      isHom : IsGroupHom (Cn+2 .snd) ∂'-fun (ker∂n .snd)
-      isHom = makeIsGroupHom λ x y
-        → kerGroup≡ ∂n (∂n+1 .snd .pres· x y)
+     t : ⟨ fst (kerSubgroup (bdry C n)) (bdry C (suc n) .fst x) ⟩
+     t = funExt⁻ (cong fst (bdry²=0 C n)) x
+  ∂ker .snd = makeIsGroupHom (λ x y → kerGroup≡ (bdry C n) ((bdry C (suc n) .snd .pres· x y)))
 
   img∂+1⊂ker∂n : NormalSubgroup ker∂n
-  fst img∂+1⊂ker∂n = imSubgroup ∂'
+  fst img∂+1⊂ker∂n = imSubgroup ∂ker
   snd img∂+1⊂ker∂n = isNormalImSubGroup
     where
     opaque
       module C1 = AbGroupStr (chain C (suc n)  .snd)
-      isNormalImSubGroup : isNormal (imSubgroup ∂')
-      isNormalImSubGroup = isNormalIm ∂'
-        (λ x y → kerGroup≡ ∂n (C1.+Comm (fst x) (fst y)))
+      isNormalImSubGroup : isNormal (imSubgroup ∂ker)
+      isNormalImSubGroup = isNormalIm ∂ker
+        (λ x y → kerGroup≡ (bdry C n) (C1.+Comm (fst x) (fst y)))
+
+-- Definition of homology
+homology : (n : ℕ) → ChainComplex ℓ → Group ℓ
+homology n C = (ker∂n n C) / (img∂+1⊂ker∂n n C)
 
 -- Induced maps on cohomology by finite chain complex maps/homotopies
 module _ where

Cubical/CW/ChainComplex.agda

@@ -10,11 +10,17 @@ open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Function
 
 open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order.Inductive
+open import Cubical.Data.Int renaming (_+_ to _+ℤ_ ; _·_ to _·ℤ_)
+open import Cubical.Data.Bool
+open import Cubical.Data.Empty renaming (rec to emptyrec)
 open import Cubical.Data.Fin.Inductive.Base
 open import Cubical.Data.Fin.Inductive.Properties
 open import Cubical.Data.Sigma
 
+open import Cubical.HITs.S1
 open import Cubical.HITs.Sn
+open import Cubical.HITs.Sn.Degree renaming (degreeConst to degree-const)
 open import Cubical.HITs.Pushout
 open import Cubical.HITs.Susp
 open import Cubical.HITs.SphereBouquet
@@ -23,6 +29,7 @@ open import Cubical.HITs.SphereBouquet.Degree
 open import Cubical.Algebra.Group.Base
 open import Cubical.Algebra.Group.MorphismProperties
 open import Cubical.Algebra.AbGroup
+open import Cubical.Algebra.AbGroup.Instances.FreeAbGroup
 open import Cubical.Algebra.ChainComplex
 
 
@@ -63,6 +70,9 @@ module _ {ℓ} (C : CWskel ℓ) where
     isoCofBouquet : cofibCW n C → SphereBouquet n (Fin An)
     isoCofBouquet = Iso.fun (BouquetIso-gen n An αn (snd C .snd .snd .snd n))
 
+    isoCofBouquetInv : SphereBouquet n (Fin An) → cofibCW n C
+    isoCofBouquetInv = Iso.inv (BouquetIso-gen n An αn (snd C .snd .snd .snd n))
+
     isoCofBouquetInv↑ : SphereBouquet (suc n) (Fin An+1) → cofibCW (suc n) C
     isoCofBouquetInv↑ = Iso.inv (BouquetIso-gen (suc n) An+1 αn+1 (snd C .snd .snd .snd (suc n)))
 
@@ -179,14 +189,90 @@ module _ {ℓ} (C : CWskel ℓ) where
         ∂≡∂↑ : ∂ n ≡ ∂↑
         ∂≡∂↑ = bouquetDegreeSusp (pre∂ n)
 
+  -- alternative description of the boundary for 1-dimensional cells
+  module ∂₀ where
+    src₀ : Fin (C .snd .fst 1) → Fin (C .snd .fst 0)
+    src₀ x = CW₁-discrete C .fst (C .snd .snd .fst 1 (x , true))
 
-  open ChainComplex
+    dest₀ : Fin (C .snd .fst 1) → Fin (C .snd .fst 0)
+    dest₀ x = CW₁-discrete C .fst (C .snd .snd .fst 1 (x , false))
+
+    src : AbGroupHom (ℤ[A 1 ]) (ℤ[A 0 ])
+    src = ℤFinFunct src₀
+
+    dest : AbGroupHom (ℤ[A 1 ]) (ℤ[A 0 ])
+    dest = ℤFinFunct dest₀
+
+    ∂₀ : AbGroupHom (ℤ[A 1 ]) (ℤ[A 0 ])
+    ∂₀ = subtrGroupHom (ℤ[A 1 ]) (ℤ[A 0 ]) dest src
+
+    -- ∂₀-alt : ∂ 0 ≡ ∂₀
+    -- ∂₀-alt = agreeOnℤFinGenerator→≡ λ x → funExt λ a → {!!}
+
+  -- augmentation map, in order to define reduced homology
+  module augmentation where
+    ε : Susp (cofibCW 0 C) → SphereBouquet 1 (Fin 1)
+    ε north = inl tt
+    ε south = inl tt
+    ε (merid (inl tt) i) = inl tt
+    ε (merid (inr x) i) = (push fzero ∙∙ (λ i → inr (fzero , loop i)) ∙∙ (λ i → push fzero (~ i))) i
+    ε (merid (push x i₁) i) with (C .snd .snd .snd .fst x)
+    ε (merid (push x i₁) i) | ()
+
+    εδ : ∀ (x : cofibCW 1 C) → (ε ∘ (suspFun (to_cofibCW 0 C)) ∘ (δ 1 C)) x ≡ inl tt
+    εδ (inl tt) = refl
+    εδ (inr x) i = (push fzero ∙∙ (λ i → inr (fzero , loop i)) ∙∙ (λ i → push fzero (~ i))) (~ i)
+    εδ (push a i) j = (push fzero ∙∙ (λ i → inr (fzero , loop i)) ∙∙ (λ i → push fzero (~ i))) (i ∧ (~ j))
 
-  CW-ChainComplex : ChainComplex ℓ-zero
-  chain CW-ChainComplex n = ℤ[A n ]
-  bdry CW-ChainComplex n = ∂ n
-  bdry²=0 CW-ChainComplex n = ∂∂≡0 n
+    preϵ : SphereBouquet 1 (Fin (preboundary.An 0)) → SphereBouquet 1 (Fin 1)
+    preϵ = ε ∘ (suspFun isoCofBouquetInv) ∘ isoSuspBouquetInv
+      where
+        open preboundary 0
+
+    opaque
+      preϵpre∂≡0 : ∀ (x : SphereBouquet 1 (Fin (preboundary.An+1 0))) → (preϵ ∘ preboundary.pre∂ 0) x ≡ inl tt
+      preϵpre∂≡0 x = cong (ε ∘ (suspFun isoCofBouquetInv))
+                          (Iso.leftInv sphereBouquetSuspIso
+                                       (((suspFun isoCofBouquet) ∘ (suspFun (to_cofibCW 0 C)) ∘ (δ 1 C) ∘ isoCofBouquetInv↑) x))
+                   ∙ cong ε (aux (((suspFun (to_cofibCW 0 C)) ∘ (δ 1 C) ∘ isoCofBouquetInv↑) x))
+                   ∙ εδ (isoCofBouquetInv↑ x)
+        where
+          open preboundary 0
+          aux : ∀ (x : Susp (cofibCW 0 C)) → (suspFun (isoCofBouquetInv) ∘ (suspFun isoCofBouquet)) x ≡ x
+          aux north = refl
+          aux south = refl
+          aux (merid a i) j = merid (Iso.leftInv (BouquetIso-gen 0 An αn (snd C .snd .snd .snd 0)) a j) i
+
+    ϵ : AbGroupHom (ℤ[A 0 ]) (ℤ[Fin 1 ])
+    ϵ = bouquetDegree preϵ
+
+    ϵ-alt : ϵ ≡ sumCoefficients _
+    ϵ-alt = GroupHom≡ (funExt λ (x : ℤ[A 0 ] .fst) → funExt λ y → cong sumFinℤ (funExt (lem1 x y)))
+      where
+        An = snd C .fst 0
+
+        lem0 : (y : Fin 1) (a : Fin An) → (degree _ (pickPetal {k = 1} y ∘ preϵ ∘ inr ∘ (a ,_))) ≡ pos 1
+        lem0 (zero , y₁) a = refl
+
+        lem1 : (x : ℤ[A 0 ] .fst) (y : Fin 1) (a : Fin An) → x a ·ℤ (degree _ (pickPetal {k = 1} y ∘ preϵ ∘ inr ∘ (a ,_))) ≡ x a
+        lem1 x y a = cong (x a ·ℤ_) (lem0 y a) ∙ ·IdR (x a)
+
+    opaque
+      ϵ∂≡0 : compGroupHom (∂ 0) ϵ ≡ trivGroupHom
+      ϵ∂≡0 = sym (bouquetDegreeComp (preϵ) (preboundary.pre∂ 0))
+           ∙ cong bouquetDegree (funExt preϵpre∂≡0)
+           ∙ bouquetDegreeConst _ _ _
+
+  open ChainComplex
 
-  -- Cellular homology
-  Hˢᵏᵉˡ : (n : ℕ) → Group₀
-  Hˢᵏᵉˡ n = homology n CW-ChainComplex
+  CW-AugChainComplex : ChainComplex ℓ-zero
+  chain CW-AugChainComplex (zero) = ℤ[Fin 1 ]
+  chain CW-AugChainComplex (suc n) = ℤ[A n ]
+  bdry CW-AugChainComplex (zero) = augmentation.ϵ
+  bdry CW-AugChainComplex (suc n) = ∂ n
+  bdry²=0 CW-AugChainComplex (zero) = augmentation.ϵ∂≡0
+  bdry²=0 CW-AugChainComplex (suc n) = ∂∂≡0 n
+
+  -- Reduced cellular homology
+  H̃ˢᵏᵉˡ : (n : ℕ) → Group₀
+  H̃ˢᵏᵉˡ n = homology n CW-AugChainComplex