Skip to content

Commit 385066b

Browse files
loic-ploic-p
authored
Reduced homology of CW complexes (#1175)
* Reduced homology of CW complexes * explicit description of the augmentation map
1 parent e8ff0c1 commit 385066b

File tree

8 files changed

+536
-289
lines changed

8 files changed

+536
-289
lines changed

‎Cubical/Algebra/AbGroup/Instances/FreeAbGroup.agda‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ open import Cubical.HITs.FreeAbGroup
1919
open import Cubical.Algebra.AbGroup
2020
open import Cubical.Algebra.AbGroup.Instances.Pi
2121
open import Cubical.Algebra.AbGroup.Instances.Int
22+
open import Cubical.Algebra.AbGroup.Instances.DirectProduct
2223
open import Cubical.Algebra.Group
2324
open import Cubical.Algebra.Group.Morphisms
2425
open import Cubical.Algebra.Group.MorphismProperties
@@ -413,3 +414,49 @@ agreeOnℤFinGenerator→≡ {n} {m} {ϕ} {ψ} idr =
413414
λ f p → IsGroupHom.presinv (snd ϕ) f
414415
∙∙ (λ i x → -ℤ (p i x))
415416
∙∙ sym (IsGroupHom.presinv (snd ψ) f)))
417+
418+
--
419+
sumCoefficients : (n : ℕ) → AbGroupHom (ℤ[Fin n ]) (ℤ[Fin 1 ])
420+
fst (sumCoefficients n) v = λ _ → sumFinℤ v
421+
snd (sumCoefficients n) = makeIsGroupHom (λ x y → funExt λ _ → sumFinℤHom x y)
422+
423+
ℤFinProductIso : (n m : ℕ) → Iso (ℤ[Fin (n +ℕ m) ] .fst) ((AbDirProd ℤ[Fin n ] ℤ[Fin m ]) .fst)
424+
ℤFinProductIso n m = iso sum→product product→sum product→sum→product sum→product→sum
425+
where
426+
sum→product : (ℤ[Fin (n +ℕ m) ] .fst) → ((AbDirProd ℤ[Fin n ] ℤ[Fin m ]) .fst)
427+
sum→product x = ((λ (a , Ha) → x (a , <→<ᵗ (≤-trans (<ᵗ→< Ha) (≤SumLeft {n}{m}))))
428+
, λ (a , Ha) → x (n +ℕ a , <→<ᵗ (<-k+ {a}{m}{n} (<ᵗ→< Ha))))
429+
430+
product→sum : ((AbDirProd ℤ[Fin n ] ℤ[Fin m ]) .fst) → (ℤ[Fin (n +ℕ m) ] .fst)
431+
product→sum (x , y) (a , Ha) with (a ≟ᵗ n)
432+
... | lt H = x (a , H)
433+
... | eq H = y (a ∸ n , <→<ᵗ (subst (a ∸ n <_) (∸+ m n) (<-∸-< a (n +ℕ m) n (<ᵗ→< Ha) (subst (λ a → a < n +ℕ m) H (<ᵗ→< Ha)))))
434+
... | gt H = y (a ∸ n , <→<ᵗ (subst (a ∸ n <_) (∸+ m n) (<-∸-< a (n +ℕ m) n (<ᵗ→< Ha) (<ᵗ→< (<ᵗ-trans {n}{a}{n +ℕ m} H Ha)))))
435+
436+
product→sum→product : ∀ x → sum→product (product→sum x) ≡ x
437+
product→sum→product (x , y) = ≡-× (funExt (λ (a , Ha) → lemx a Ha)) (funExt (λ (a , Ha) → lemy a Ha))
438+
where
439+
lemx : (a : ℕ) (Ha : a <ᵗ n) → fst (sum→product (product→sum (x , y))) (a , Ha) ≡ x (a , Ha)
440+
lemx a Ha with (a ≟ᵗ n)
441+
... | lt H = cong x (Fin≡ (a , H) (a , Ha) refl)
442+
... | eq H = rec (¬m<ᵗm (subst (λ a → a <ᵗ n) H Ha))
443+
... | gt H = rec (¬m<ᵗm (<ᵗ-trans Ha H))
444+
445+
lemy : (a : ℕ) (Ha : a <ᵗ m) → snd (sum→product (product→sum (x , y))) (a , Ha) ≡ y (a , Ha)
446+
lemy a Ha with ((n +ℕ a) ≟ᵗ n)
447+
... | lt H = rec (¬m<m (≤<-trans (≤SumLeft {n}{a}) (<ᵗ→< H)))
448+
... | eq H = cong y (Fin≡ _ _ (∸+ a n))
449+
... | gt H = cong y (Fin≡ _ _ (∸+ a n))
450+
451+
sum→product→sum : ∀ x → product→sum (sum→product x) ≡ x
452+
sum→product→sum x = funExt (λ (a , Ha) → lem a Ha)
453+
where
454+
lem : (a : ℕ) (Ha : a <ᵗ (n +ℕ m)) → product→sum (sum→product x) (a , Ha) ≡ x (a , Ha)
455+
lem a Ha with (a ≟ᵗ n)
456+
... | lt H = cong x (Fin≡ _ _ refl)
457+
... | eq H = cong x (Fin≡ _ _ ((+-comm n (a ∸ n)) ∙ ≤-∸-+-cancel (subst (n ≤_) (sym H) ≤-refl)))
458+
... | gt H = cong x (Fin≡ _ _ ((+-comm n (a ∸ n)) ∙ ≤-∸-+-cancel (<-weaken (<ᵗ→< H))))
459+
460+
ℤFinProduct : (n m : ℕ) → AbGroupIso ℤ[Fin (n +ℕ m) ] (AbDirProd ℤ[Fin n ] ℤ[Fin m ])
461+
fst (ℤFinProduct n m) = ℤFinProductIso n m
462+
snd (ℤFinProduct n m) = makeIsGroupHom (λ x y → refl)

‎Cubical/Algebra/ChainComplex/Homology.agda‎

Lines changed: 15 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -35,42 +35,30 @@ open ChainComplex
3535
open finChainComplexMap
3636
open IsGroupHom
3737

38-
-- Definition of homology
39-
homology : (n : ℕ) → ChainComplex ℓ → Group ℓ
40-
homology n C = ker∂n / img∂+1⊂ker∂n
41-
where
42-
Cn+2 = AbGroup→Group (chain C (suc (suc n)))
43-
∂n = bdry C n
44-
∂n+1 = bdry C (suc n)
45-
ker∂n = kerGroup ∂n
46-
47-
-- Restrict ∂n+1 to ker∂n
48-
∂'-fun : Cn+2 .fst → ker∂n .fst
49-
fst (∂'-fun x) = ∂n+1 .fst x
50-
snd (∂'-fun x) = t
51-
where
52-
opaque
53-
t : ⟨ fst (kerSubgroup ∂n) (∂n+1 .fst x) ⟩
54-
t = funExt⁻ (cong fst (bdry²=0 C n)) x
38+
module _ (n : ℕ) (C : ChainComplex ℓ) where
39+
ker∂n = kerGroup (bdry C n)
5540

56-
∂' : GroupHom Cn+2 ker∂n
57-
fst ∂' = ∂'-fun
58-
snd ∂' = isHom
41+
∂ker : GroupHom (AbGroup→Group (chain C (suc (suc n)))) ker∂n
42+
∂ker .fst x = (bdry C (suc n) .fst x) , t
5943
where
6044
opaque
61-
isHom : IsGroupHom (Cn+2 .snd) ∂'-fun (ker∂n .snd)
62-
isHom = makeIsGroupHom λ x y
63-
→ kerGroup≡ ∂n (∂n+1 .snd .pres· x y)
45+
t : ⟨ fst (kerSubgroup (bdry C n)) (bdry C (suc n) .fst x) ⟩
46+
t = funExt⁻ (cong fst (bdry²=0 C n)) x
47+
∂ker .snd = makeIsGroupHom (λ x y → kerGroup≡ (bdry C n) ((bdry C (suc n) .snd .pres· x y)))
6448

6549
img∂+1⊂ker∂n : NormalSubgroup ker∂n
66-
fst img∂+1⊂ker∂n = imSubgroup ∂'
50+
fst img∂+1⊂ker∂n = imSubgroup ∂ker
6751
snd img∂+1⊂ker∂n = isNormalImSubGroup
6852
where
6953
opaque
7054
module C1 = AbGroupStr (chain C (suc n) .snd)
71-
isNormalImSubGroup : isNormal (imSubgroup ∂')
72-
isNormalImSubGroup = isNormalIm ∂'
73-
(λ x y → kerGroup≡ ∂n (C1.+Comm (fst x) (fst y)))
55+
isNormalImSubGroup : isNormal (imSubgroup ∂ker)
56+
isNormalImSubGroup = isNormalIm ∂ker
57+
(λ x y → kerGroup≡ (bdry C n) (C1.+Comm (fst x) (fst y)))
58+
59+
-- Definition of homology
60+
homology : (n : ℕ) → ChainComplex ℓ → Group ℓ
61+
homology n C = (ker∂n n C) / (img∂+1⊂ker∂n n C)
7462

7563
-- Induced maps on cohomology by finite chain complex maps/homotopies
7664
module _ where

‎Cubical/CW/ChainComplex.agda‎

Lines changed: 94 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -10,11 +10,17 @@ open import Cubical.Foundations.Isomorphism
1010
open import Cubical.Foundations.Function
1111

1212
open import Cubical.Data.Nat
13+
open import Cubical.Data.Nat.Order.Inductive
14+
open import Cubical.Data.Int renaming (_+_ to _+ℤ_ ; _·_ to _·ℤ_)
15+
open import Cubical.Data.Bool
16+
open import Cubical.Data.Empty renaming (rec to emptyrec)
1317
open import Cubical.Data.Fin.Inductive.Base
1418
open import Cubical.Data.Fin.Inductive.Properties
1519
open import Cubical.Data.Sigma
1620

21+
open import Cubical.HITs.S1
1722
open import Cubical.HITs.Sn
23+
open import Cubical.HITs.Sn.Degree renaming (degreeConst to degree-const)
1824
open import Cubical.HITs.Pushout
1925
open import Cubical.HITs.Susp
2026
open import Cubical.HITs.SphereBouquet
@@ -23,6 +29,7 @@ open import Cubical.HITs.SphereBouquet.Degree
2329
open import Cubical.Algebra.Group.Base
2430
open import Cubical.Algebra.Group.MorphismProperties
2531
open import Cubical.Algebra.AbGroup
32+
open import Cubical.Algebra.AbGroup.Instances.FreeAbGroup
2633
open import Cubical.Algebra.ChainComplex
2734

2835

@@ -63,6 +70,9 @@ module _ {ℓ} (C : CWskel ℓ) where
6370
isoCofBouquet : cofibCW n C → SphereBouquet n (Fin An)
6471
isoCofBouquet = Iso.fun (BouquetIso-gen n An αn (snd C .snd .snd .snd n))
6572

73+
isoCofBouquetInv : SphereBouquet n (Fin An) → cofibCW n C
74+
isoCofBouquetInv = Iso.inv (BouquetIso-gen n An αn (snd C .snd .snd .snd n))
75+
6676
isoCofBouquetInv↑ : SphereBouquet (suc n) (Fin An+1) → cofibCW (suc n) C
6777
isoCofBouquetInv↑ = Iso.inv (BouquetIso-gen (suc n) An+1 αn+1 (snd C .snd .snd .snd (suc n)))
6878

@@ -179,14 +189,90 @@ module _ {ℓ} (C : CWskel ℓ) where
179189
∂≡∂↑ : ∂ n ≡ ∂↑
180190
∂≡∂↑ = bouquetDegreeSusp (pre∂ n)
181191

192+
-- alternative description of the boundary for 1-dimensional cells
193+
module ∂₀ where
194+
src₀ : Fin (C .snd .fst 1) → Fin (C .snd .fst 0)
195+
src₀ x = CW₁-discrete C .fst (C .snd .snd .fst 1 (x , true))
182196

183-
open ChainComplex
197+
dest₀ : Fin (C .snd .fst 1) → Fin (C .snd .fst 0)
198+
dest₀ x = CW₁-discrete C .fst (C .snd .snd .fst 1 (x , false))
199+
200+
src : AbGroupHom (ℤ[A 1 ]) (ℤ[A 0 ])
201+
src = ℤFinFunct src₀
202+
203+
dest : AbGroupHom (ℤ[A 1 ]) (ℤ[A 0 ])
204+
dest = ℤFinFunct dest₀
205+
206+
∂₀ : AbGroupHom (ℤ[A 1 ]) (ℤ[A 0 ])
207+
∂₀ = subtrGroupHom (ℤ[A 1 ]) (ℤ[A 0 ]) dest src
208+
209+
-- ∂₀-alt : ∂ 0 ≡ ∂₀
210+
-- ∂₀-alt = agreeOnℤFinGenerator→≡ λ x → funExt λ a → {!!}
211+
212+
-- augmentation map, in order to define reduced homology
213+
module augmentation where
214+
ε : Susp (cofibCW 0 C) → SphereBouquet 1 (Fin 1)
215+
ε north = inl tt
216+
ε south = inl tt
217+
ε (merid (inl tt) i) = inl tt
218+
ε (merid (inr x) i) = (push fzero ∙∙ (λ i → inr (fzero , loop i)) ∙∙ (λ i → push fzero (~ i))) i
219+
ε (merid (push x i₁) i) with (C .snd .snd .snd .fst x)
220+
ε (merid (push x i₁) i) | ()
221+
222+
εδ : ∀ (x : cofibCW 1 C) → (ε ∘ (suspFun (to_cofibCW 0 C)) ∘ (δ 1 C)) x ≡ inl tt
223+
εδ (inl tt) = refl
224+
εδ (inr x) i = (push fzero ∙∙ (λ i → inr (fzero , loop i)) ∙∙ (λ i → push fzero (~ i))) (~ i)
225+
εδ (push a i) j = (push fzero ∙∙ (λ i → inr (fzero , loop i)) ∙∙ (λ i → push fzero (~ i))) (i ∧ (~ j))
184226

185-
CW-ChainComplex : ChainComplex ℓ-zero
186-
chain CW-ChainComplex n = ℤ[A n ]
187-
bdry CW-ChainComplex n = ∂ n
188-
bdry²=0 CW-ChainComplex n = ∂∂≡0 n
227+
preϵ : SphereBouquet 1 (Fin (preboundary.An 0)) → SphereBouquet 1 (Fin 1)
228+
preϵ = ε ∘ (suspFun isoCofBouquetInv) ∘ isoSuspBouquetInv
229+
where
230+
open preboundary 0
231+
232+
opaque
233+
preϵpre∂≡0 : ∀ (x : SphereBouquet 1 (Fin (preboundary.An+1 0))) → (preϵ ∘ preboundary.pre∂ 0) x ≡ inl tt
234+
preϵpre∂≡0 x = cong (ε ∘ (suspFun isoCofBouquetInv))
235+
(Iso.leftInv sphereBouquetSuspIso
236+
(((suspFun isoCofBouquet) ∘ (suspFun (to_cofibCW 0 C)) ∘ (δ 1 C) ∘ isoCofBouquetInv↑) x))
237+
∙ cong ε (aux (((suspFun (to_cofibCW 0 C)) ∘ (δ 1 C) ∘ isoCofBouquetInv↑) x))
238+
∙ εδ (isoCofBouquetInv↑ x)
239+
where
240+
open preboundary 0
241+
aux : ∀ (x : Susp (cofibCW 0 C)) → (suspFun (isoCofBouquetInv) ∘ (suspFun isoCofBouquet)) x ≡ x
242+
aux north = refl
243+
aux south = refl
244+
aux (merid a i) j = merid (Iso.leftInv (BouquetIso-gen 0 An αn (snd C .snd .snd .snd 0)) a j) i
245+
246+
ϵ : AbGroupHom (ℤ[A 0 ]) (ℤ[Fin 1 ])
247+
ϵ = bouquetDegree preϵ
248+
249+
ϵ-alt : ϵ ≡ sumCoefficients _
250+
ϵ-alt = GroupHom≡ (funExt λ (x : ℤ[A 0 ] .fst) → funExt λ y → cong sumFinℤ (funExt (lem1 x y)))
251+
where
252+
An = snd C .fst 0
253+
254+
lem0 : (y : Fin 1) (a : Fin An) → (degree _ (pickPetal {k = 1} y ∘ preϵ ∘ inr ∘ (a ,_))) ≡ pos 1
255+
lem0 (zero , y₁) a = refl
256+
257+
lem1 : (x : ℤ[A 0 ] .fst) (y : Fin 1) (a : Fin An) → x a ·ℤ (degree _ (pickPetal {k = 1} y ∘ preϵ ∘ inr ∘ (a ,_))) ≡ x a
258+
lem1 x y a = cong (x a ·ℤ_) (lem0 y a) ∙ ·IdR (x a)
259+
260+
opaque
261+
ϵ∂≡0 : compGroupHom (∂ 0) ϵ ≡ trivGroupHom
262+
ϵ∂≡0 = sym (bouquetDegreeComp (preϵ) (preboundary.pre∂ 0))
263+
∙ cong bouquetDegree (funExt preϵpre∂≡0)
264+
∙ bouquetDegreeConst _ _ _
265+
266+
open ChainComplex
189267

190-
-- Cellular homology
191-
Hˢᵏᵉˡ : (n : ℕ) → Group₀
192-
Hˢᵏᵉˡ n = homology n CW-ChainComplex
268+
CW-AugChainComplex : ChainComplex ℓ-zero
269+
chain CW-AugChainComplex (zero) = ℤ[Fin 1 ]
270+
chain CW-AugChainComplex (suc n) = ℤ[A n ]
271+
bdry CW-AugChainComplex (zero) = augmentation.ϵ
272+
bdry CW-AugChainComplex (suc n) = ∂ n
273+
bdry²=0 CW-AugChainComplex (zero) = augmentation.ϵ∂≡0
274+
bdry²=0 CW-AugChainComplex (suc n) = ∂∂≡0 n
275+
276+
-- Reduced cellular homology
277+
H̃ˢᵏᵉˡ : (n : ℕ) → Group₀
278+
H̃ˢᵏᵉˡ n = homology n CW-AugChainComplex

0 commit comments

Comments
 (0)