explicit description of the augmentation map

agda · Jan 21, 2025 · ebbd453 · ebbd453
1 parent c990ea3
commit ebbd453
Show file tree

Hide file tree

Showing 4 changed files with 103 additions and 28 deletions.
diff --git a/Cubical/Algebra/AbGroup/Instances/FreeAbGroup.agda b/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)
diff --git a/Cubical/Algebra/ChainComplex/Homology.agda b/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

diff --git a/Cubical/CW/ChainComplex.agda b/Cubical/CW/ChainComplex.agda
@@ -10,14 +10,17 @@ open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Function
 
 open import Cubical.Data.Nat
-open import Cubical.Data.Int
+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
@@ -186,6 +189,26 @@ 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))
+
+    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)
@@ -223,6 +246,17 @@ module _ {ℓ} (C : CWskel ℓ) where
     ϵ : 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))

diff --git a/Cubical/Data/Fin/Inductive/Properties.agda b/Cubical/Data/Fin/Inductive/Properties.agda
@@ -25,6 +25,12 @@ open import Cubical.Relation.Nullary
 
 open import Cubical.Algebra.AbGroup.Base using (move4)
 
+Fin≡ : {m : ℕ} (a b : Fin m) → fst a ≡ fst b → a ≡ b
+Fin≡ {m} (a , Ha) (b , Hb) H i =
+  (H i , hcomp (λ j → λ { (i = i0) → Ha
+                        ; (i = i1) → isProp<ᵗ {b}{m} (transp (λ j → H j <ᵗ m) i0 Ha) Hb j })
+               (transp (λ j → H (i ∧ j) <ᵗ m) (~ i) Ha))
+
 fsuc-injectSuc : {m : ℕ} (n : Fin m)
   → injectSuc {n = suc m} (fsuc {n = m} n) ≡ fsuc (injectSuc n)
 fsuc-injectSuc {m = suc m} (x , p) = refl