From c990ea3b5f38d1ef0daebac13868efe145254326 Mon Sep 17 00:00:00 2001 From: loic-p Date: Sun, 22 Dec 2024 21:21:41 +0100 Subject: [PATCH 1/2] Reduced homology of CW complexes --- Cubical/CW/ChainComplex.agda | 68 +++++++-- Cubical/CW/Homology.agda | 228 +++++++++++++++--------------- Cubical/CW/Homotopy.agda | 267 ++++++++++++++++++++++------------- Cubical/CW/Map.agda | 82 +++++++++-- Cubical/CW/Subcomplex.agda | 51 +++---- 5 files changed, 434 insertions(+), 262 deletions(-) diff --git a/Cubical/CW/ChainComplex.agda b/Cubical/CW/ChainComplex.agda index 54d32db729..afa2d60bbb 100644 --- a/Cubical/CW/ChainComplex.agda +++ b/Cubical/CW/ChainComplex.agda @@ -10,10 +10,13 @@ open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Function open import Cubical.Data.Nat +open import Cubical.Data.Int +open import Cubical.Data.Bool 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.Pushout open import Cubical.HITs.Susp @@ -23,6 +26,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 +67,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 +186,59 @@ module _ {ℓ} (C : CWskel ℓ) where ∂≡∂↑ : ∂ n ≡ ∂↑ ∂≡∂↑ = bouquetDegreeSusp (pre∂ n) + -- 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)) + + 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ϵ + + opaque + ϵ∂≡0 : compGroupHom (∂ 0) ϵ ≡ trivGroupHom + ϵ∂≡0 = sym (bouquetDegreeComp (preϵ) (preboundary.pre∂ 0)) + ∙ cong bouquetDegree (funExt preϵpre∂≡0) + ∙ bouquetDegreeConst _ _ _ open ChainComplex - CW-ChainComplex : ChainComplex ℓ-zero - chain CW-ChainComplex n = ℤ[A n ] - bdry CW-ChainComplex n = ∂ n - bdry²=0 CW-ChainComplex n = ∂∂≡0 n - - -- 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 diff --git a/Cubical/CW/Homology.agda b/Cubical/CW/Homology.agda index c216a36d01..98cedb90a9 100644 --- a/Cubical/CW/Homology.agda +++ b/Cubical/CW/Homology.agda @@ -36,56 +36,56 @@ private variable ℓ ℓ' ℓ'' : Level ------- Part 1. Functoriality of Hˢᵏᵉˡ ------ -Hˢᵏᵉˡ→-pre : (C : CWskel ℓ) (D : CWskel ℓ') (m : ℕ) +------ Part 1. Functoriality of H̃ˢᵏᵉˡ ------ +H̃ˢᵏᵉˡ→-pre : (C : CWskel ℓ) (D : CWskel ℓ') (m : ℕ) (f : finCellMap (suc (suc (suc m))) C D) - → GroupHom (Hˢᵏᵉˡ C m) (Hˢᵏᵉˡ D m) -Hˢᵏᵉˡ→-pre C D m f = finCellMap→HomologyMap m f + → GroupHom (H̃ˢᵏᵉˡ C m) (H̃ˢᵏᵉˡ D m) +H̃ˢᵏᵉˡ→-pre C D m f = finCellMap→HomologyMap m f private - Hˢᵏᵉˡ→-pre' : (C : CWskel ℓ) (D : CWskel ℓ') (m : ℕ) + H̃ˢᵏᵉˡ→-pre' : (C : CWskel ℓ) (D : CWskel ℓ') (m : ℕ) → (f : realise C → realise D) → ∥ finCellApprox C D f (suc (suc (suc m))) ∥₁ - → GroupHom (Hˢᵏᵉˡ C m) (Hˢᵏᵉˡ D m) - Hˢᵏᵉˡ→-pre' C D m f = + → GroupHom (H̃ˢᵏᵉˡ C m) (H̃ˢᵏᵉˡ D m) + H̃ˢᵏᵉˡ→-pre' C D m f = rec→Set isSetGroupHom - (λ f → Hˢᵏᵉˡ→-pre C D m (f .fst)) + (λ f → H̃ˢᵏᵉˡ→-pre C D m (f .fst)) main where - main : 2-Constant (λ f₁ → Hˢᵏᵉˡ→-pre C D m (f₁ .fst)) + main : 2-Constant (λ f₁ → H̃ˢᵏᵉˡ→-pre C D m (f₁ .fst)) main f g = PT.rec (isSetGroupHom _ _) (λ q → finChainHomotopy→HomologyPath _ _ (cellHom-to-ChainHomotopy _ q) flast) (pathToCellularHomotopy _ (fst f) (fst g) λ x → funExt⁻ (snd f ∙ sym (snd g)) (fincl flast x)) -Hˢᵏᵉˡ→ : {C : CWskel ℓ} {D : CWskel ℓ'} (m : ℕ) +H̃ˢᵏᵉˡ→ : {C : CWskel ℓ} {D : CWskel ℓ'} (m : ℕ) (f : realise C → realise D) - → GroupHom (Hˢᵏᵉˡ C m) (Hˢᵏᵉˡ D m) -Hˢᵏᵉˡ→ {C = C} {D} m f = - Hˢᵏᵉˡ→-pre' C D m f + → GroupHom (H̃ˢᵏᵉˡ C m) (H̃ˢᵏᵉˡ D m) +H̃ˢᵏᵉˡ→ {C = C} {D} m f = + H̃ˢᵏᵉˡ→-pre' C D m f (CWmap→finCellMap C D f (suc (suc (suc m)))) -Hˢᵏᵉˡ→β : (C : CWskel ℓ) (D : CWskel ℓ') (m : ℕ) +H̃ˢᵏᵉˡ→β : (C : CWskel ℓ) (D : CWskel ℓ') (m : ℕ) {f : realise C → realise D} (ϕ : finCellApprox C D f (suc (suc (suc m)))) - → Hˢᵏᵉˡ→ {C = C} {D} m f ≡ Hˢᵏᵉˡ→-pre C D m (ϕ .fst) -Hˢᵏᵉˡ→β C D m {f = f} ϕ = - cong (Hˢᵏᵉˡ→-pre' C D m f) (squash₁ _ ∣ ϕ ∣₁) - -Hˢᵏᵉˡ→id : (m : ℕ) {C : CWskel ℓ} - → Hˢᵏᵉˡ→ {C = C} m (idfun _) ≡ idGroupHom -Hˢᵏᵉˡ→id m {C = C} = - Hˢᵏᵉˡ→β C C m {idfun _} (idFinCellApprox (suc (suc (suc m)))) + → H̃ˢᵏᵉˡ→ {C = C} {D} m f ≡ H̃ˢᵏᵉˡ→-pre C D m (ϕ .fst) +H̃ˢᵏᵉˡ→β C D m {f = f} ϕ = + cong (H̃ˢᵏᵉˡ→-pre' C D m f) (squash₁ _ ∣ ϕ ∣₁) + +H̃ˢᵏᵉˡ→id : (m : ℕ) {C : CWskel ℓ} + → H̃ˢᵏᵉˡ→ {C = C} m (idfun _) ≡ idGroupHom +H̃ˢᵏᵉˡ→id m {C = C} = + H̃ˢᵏᵉˡ→β C C m {idfun _} (idFinCellApprox (suc (suc (suc m)))) ∙ finCellMap→HomologyMapId _ -Hˢᵏᵉˡ→comp : (m : ℕ) +H̃ˢᵏᵉˡ→comp : (m : ℕ) {C : CWskel ℓ} {D : CWskel ℓ'} {E : CWskel ℓ''} (g : realise D → realise E) (f : realise C → realise D) - → Hˢᵏᵉˡ→ m (g ∘ f) - ≡ compGroupHom (Hˢᵏᵉˡ→ m f) (Hˢᵏᵉˡ→ m g) -Hˢᵏᵉˡ→comp m {C = C} {D = D} {E = E} g f = + → H̃ˢᵏᵉˡ→ m (g ∘ f) + ≡ compGroupHom (H̃ˢᵏᵉˡ→ m f) (H̃ˢᵏᵉˡ→ m g) +H̃ˢᵏᵉˡ→comp m {C = C} {D = D} {E = E} g f = PT.rec2 (isSetGroupHom _ _) main (CWmap→finCellMap C D f (suc (suc (suc m)))) @@ -97,148 +97,148 @@ Hˢᵏᵉˡ→comp m {C = C} {D = D} {E = E} g f = comps : finCellApprox C E (g ∘ f) (suc (suc (suc m))) comps = compFinCellApprox _ {g = g} {f} G F - eq1 : Hˢᵏᵉˡ→ m (g ∘ f) - ≡ Hˢᵏᵉˡ→-pre C E m (composeFinCellMap _ (fst G) (fst F)) - eq1 = Hˢᵏᵉˡ→β C E m {g ∘ f} comps + eq1 : H̃ˢᵏᵉˡ→ m (g ∘ f) + ≡ H̃ˢᵏᵉˡ→-pre C E m (composeFinCellMap _ (fst G) (fst F)) + eq1 = H̃ˢᵏᵉˡ→β C E m {g ∘ f} comps - eq2 : compGroupHom (Hˢᵏᵉˡ→ m f) (Hˢᵏᵉˡ→ m g) - ≡ compGroupHom (Hˢᵏᵉˡ→-pre C D m (fst F)) (Hˢᵏᵉˡ→-pre D E m (fst G)) - eq2 = cong₂ compGroupHom (Hˢᵏᵉˡ→β C D m {f = f} F) (Hˢᵏᵉˡ→β D E m {f = g} G) + eq2 : compGroupHom (H̃ˢᵏᵉˡ→ m f) (H̃ˢᵏᵉˡ→ m g) + ≡ compGroupHom (H̃ˢᵏᵉˡ→-pre C D m (fst F)) (H̃ˢᵏᵉˡ→-pre D E m (fst G)) + eq2 = cong₂ compGroupHom (H̃ˢᵏᵉˡ→β C D m {f = f} F) (H̃ˢᵏᵉˡ→β D E m {f = g} G) - main : Hˢᵏᵉˡ→ m (g ∘ f) ≡ compGroupHom (Hˢᵏᵉˡ→ m f) (Hˢᵏᵉˡ→ m g) + main : H̃ˢᵏᵉˡ→ m (g ∘ f) ≡ compGroupHom (H̃ˢᵏᵉˡ→ m f) (H̃ˢᵏᵉˡ→ m g) main = eq1 ∙∙ finCellMap→HomologyMapComp _ _ _ ∙∙ sym eq2 -- preservation of equivalence -Hˢᵏᵉˡ→Iso : {C : CWskel ℓ} {D : CWskel ℓ'} (m : ℕ) - (e : realise C ≃ realise D) → GroupIso (Hˢᵏᵉˡ C m) (Hˢᵏᵉˡ D m) -Iso.fun (fst (Hˢᵏᵉˡ→Iso m e)) = fst (Hˢᵏᵉˡ→ m (fst e)) -Iso.inv (fst (Hˢᵏᵉˡ→Iso m e)) = fst (Hˢᵏᵉˡ→ m (invEq e)) -Iso.rightInv (fst (Hˢᵏᵉˡ→Iso m e)) = - funExt⁻ (cong fst (sym (Hˢᵏᵉˡ→comp m (fst e) (invEq e)) - ∙∙ cong (Hˢᵏᵉˡ→ m) (funExt (secEq e)) - ∙∙ Hˢᵏᵉˡ→id m)) -Iso.leftInv (fst (Hˢᵏᵉˡ→Iso m e)) = - funExt⁻ (cong fst (sym (Hˢᵏᵉˡ→comp m (invEq e) (fst e)) - ∙∙ cong (Hˢᵏᵉˡ→ m) (funExt (retEq e)) - ∙∙ Hˢᵏᵉˡ→id m)) -snd (Hˢᵏᵉˡ→Iso m e) = snd (Hˢᵏᵉˡ→ m (fst e)) - -Hˢᵏᵉˡ→Equiv : {C : CWskel ℓ} {D : CWskel ℓ'} (m : ℕ) - (e : realise C ≃ realise D) → GroupEquiv (Hˢᵏᵉˡ C m) (Hˢᵏᵉˡ D m) -Hˢᵏᵉˡ→Equiv m e = GroupIso→GroupEquiv (Hˢᵏᵉˡ→Iso m e) +H̃ˢᵏᵉˡ→Iso : {C : CWskel ℓ} {D : CWskel ℓ'} (m : ℕ) + (e : realise C ≃ realise D) → GroupIso (H̃ˢᵏᵉˡ C m) (H̃ˢᵏᵉˡ D m) +Iso.fun (fst (H̃ˢᵏᵉˡ→Iso m e)) = fst (H̃ˢᵏᵉˡ→ m (fst e)) +Iso.inv (fst (H̃ˢᵏᵉˡ→Iso m e)) = fst (H̃ˢᵏᵉˡ→ m (invEq e)) +Iso.rightInv (fst (H̃ˢᵏᵉˡ→Iso m e)) = + funExt⁻ (cong fst (sym (H̃ˢᵏᵉˡ→comp m (fst e) (invEq e)) + ∙∙ cong (H̃ˢᵏᵉˡ→ m) (funExt (secEq e)) + ∙∙ H̃ˢᵏᵉˡ→id m)) +Iso.leftInv (fst (H̃ˢᵏᵉˡ→Iso m e)) = + funExt⁻ (cong fst (sym (H̃ˢᵏᵉˡ→comp m (invEq e) (fst e)) + ∙∙ cong (H̃ˢᵏᵉˡ→ m) (funExt (retEq e)) + ∙∙ H̃ˢᵏᵉˡ→id m)) +snd (H̃ˢᵏᵉˡ→Iso m e) = snd (H̃ˢᵏᵉˡ→ m (fst e)) + +H̃ˢᵏᵉˡ→Equiv : {C : CWskel ℓ} {D : CWskel ℓ'} (m : ℕ) + (e : realise C ≃ realise D) → GroupEquiv (H̃ˢᵏᵉˡ C m) (H̃ˢᵏᵉˡ D m) +H̃ˢᵏᵉˡ→Equiv m e = GroupIso→GroupEquiv (H̃ˢᵏᵉˡ→Iso m e) ------ Part 2. Definition of cellular homology ------ -Hᶜʷ : ∀ (C : CW ℓ) (n : ℕ) → Group₀ -Hᶜʷ (C , CWstr) n = +H̃ᶜʷ : ∀ (C : CW ℓ) (n : ℕ) → Group₀ +H̃ᶜʷ (C , CWstr) n = PropTrunc→Group - (λ Cskel → Hˢᵏᵉˡ (Cskel .fst) n) + (λ Cskel → H̃ˢᵏᵉˡ (Cskel .fst) n) (λ Cskel Dskel - → Hˢᵏᵉˡ→Equiv n (compEquiv (invEquiv (snd Cskel)) (snd Dskel))) + → H̃ˢᵏᵉˡ→Equiv n (compEquiv (invEquiv (snd Cskel)) (snd Dskel))) coh CWstr where - coh : (Cskel Dskel Eskel : isCW C) (t : fst (Hˢᵏᵉˡ (Cskel .fst) n)) - → fst (fst (Hˢᵏᵉˡ→Equiv n (compEquiv (invEquiv (snd Dskel)) (snd Eskel)))) - (fst (fst (Hˢᵏᵉˡ→Equiv n (compEquiv (invEquiv (snd Cskel)) (snd Dskel)))) t) - ≡ fst (fst (Hˢᵏᵉˡ→Equiv n (compEquiv (invEquiv (snd Cskel)) (snd Eskel)))) t + coh : (Cskel Dskel Eskel : isCW C) (t : fst (H̃ˢᵏᵉˡ (Cskel .fst) n)) + → fst (fst (H̃ˢᵏᵉˡ→Equiv n (compEquiv (invEquiv (snd Dskel)) (snd Eskel)))) + (fst (fst (H̃ˢᵏᵉˡ→Equiv n (compEquiv (invEquiv (snd Cskel)) (snd Dskel)))) t) + ≡ fst (fst (H̃ˢᵏᵉˡ→Equiv n (compEquiv (invEquiv (snd Cskel)) (snd Eskel)))) t coh (C' , e) (D , f) (E , h) = funExt⁻ (cong fst - (sym (Hˢᵏᵉˡ→comp n (fst (compEquiv (invEquiv f) h)) + (sym (H̃ˢᵏᵉˡ→comp n (fst (compEquiv (invEquiv f) h)) (fst (compEquiv (invEquiv e) f))) - ∙ cong (Hˢᵏᵉˡ→ n) (funExt λ x → cong (fst h) (retEq f _)))) + ∙ cong (H̃ˢᵏᵉˡ→ n) (funExt λ x → cong (fst h) (retEq f _)))) -- lemmas for functoriality private module _ {C : Type ℓ} {D : Type ℓ'} (f : C → D) (n : ℕ) where right : (cwC : isCW C) (cwD1 : isCW D) (cwD2 : isCW D) - → PathP (λ i → GroupHom (Hᶜʷ (C , ∣ cwC ∣₁) n) - (Hᶜʷ (D , squash₁ ∣ cwD1 ∣₁ ∣ cwD2 ∣₁ i) n)) - (Hˢᵏᵉˡ→ n (λ x → fst (snd cwD1) (f (invEq (snd cwC) x)))) - (Hˢᵏᵉˡ→ n (λ x → fst (snd cwD2) (f (invEq (snd cwC) x)))) + → PathP (λ i → GroupHom (H̃ᶜʷ (C , ∣ cwC ∣₁) n) + (H̃ᶜʷ (D , squash₁ ∣ cwD1 ∣₁ ∣ cwD2 ∣₁ i) n)) + (H̃ˢᵏᵉˡ→ n (λ x → fst (snd cwD1) (f (invEq (snd cwC) x)))) + (H̃ˢᵏᵉˡ→ n (λ x → fst (snd cwD2) (f (invEq (snd cwC) x)))) right cwC cwD1 cwD2 = PathPGroupHomₗ _ - (cong (Hˢᵏᵉˡ→ n) (funExt (λ s + (cong (H̃ˢᵏᵉˡ→ n) (funExt (λ s → cong (fst (snd cwD2)) (sym (retEq (snd cwD1) _)))) - ∙ Hˢᵏᵉˡ→comp n _ _) + ∙ H̃ˢᵏᵉˡ→comp n _ _) left : (cwC1 : isCW C) (cwC2 : isCW C) (cwD : isCW D) - → PathP (λ i → GroupHom (Hᶜʷ (C , squash₁ ∣ cwC1 ∣₁ ∣ cwC2 ∣₁ i) n) - (Hᶜʷ (D , ∣ cwD ∣₁) n)) - (Hˢᵏᵉˡ→ n (λ x → fst (snd cwD) (f (invEq (snd cwC1) x)))) - (Hˢᵏᵉˡ→ n (λ x → fst (snd cwD) (f (invEq (snd cwC2) x)))) + → PathP (λ i → GroupHom (H̃ᶜʷ (C , squash₁ ∣ cwC1 ∣₁ ∣ cwC2 ∣₁ i) n) + (H̃ᶜʷ (D , ∣ cwD ∣₁) n)) + (H̃ˢᵏᵉˡ→ n (λ x → fst (snd cwD) (f (invEq (snd cwC1) x)))) + (H̃ˢᵏᵉˡ→ n (λ x → fst (snd cwD) (f (invEq (snd cwC2) x)))) left cwC1 cwC2 cwD = - PathPGroupHomᵣ (Hˢᵏᵉˡ→Equiv n (compEquiv (invEquiv (snd cwC1)) (snd cwC2))) - (sym (Hˢᵏᵉˡ→comp n (λ x → fst (snd cwD) (f (invEq (snd cwC2) x))) + PathPGroupHomᵣ (H̃ˢᵏᵉˡ→Equiv n (compEquiv (invEquiv (snd cwC1)) (snd cwC2))) + (sym (H̃ˢᵏᵉˡ→comp n (λ x → fst (snd cwD) (f (invEq (snd cwC2) x))) (compEquiv (invEquiv (snd cwC1)) (snd cwC2) .fst)) - ∙ cong (Hˢᵏᵉˡ→ n) (funExt (λ x + ∙ cong (H̃ˢᵏᵉˡ→ n) (funExt (λ x → cong (fst (snd cwD) ∘ f) (retEq (snd cwC2) _)))) left-right : (x y : isCW C) (v w : isCW D) → SquareP (λ i j → - GroupHom (Hᶜʷ (C , squash₁ ∣ x ∣₁ ∣ y ∣₁ i) n) - (Hᶜʷ (D , squash₁ ∣ v ∣₁ ∣ w ∣₁ j) n)) + GroupHom (H̃ᶜʷ (C , squash₁ ∣ x ∣₁ ∣ y ∣₁ i) n) + (H̃ᶜʷ (D , squash₁ ∣ v ∣₁ ∣ w ∣₁ j) n)) (right x v w) (right y v w) (left x y v) (left x y w) left-right _ _ _ _ = isSet→SquareP (λ _ _ → isSetGroupHom) _ _ _ _ - Hᶜʷ→pre : (cwC : ∥ isCW C ∥₁) (cwD : ∥ isCW D ∥₁) - → GroupHom (Hᶜʷ (C , cwC) n) (Hᶜʷ (D , cwD) n) - Hᶜʷ→pre = + H̃ᶜʷ→pre : (cwC : ∥ isCW C ∥₁) (cwD : ∥ isCW D ∥₁) + → GroupHom (H̃ᶜʷ (C , cwC) n) (H̃ᶜʷ (D , cwD) n) + H̃ᶜʷ→pre = elim2→Set (λ _ _ → isSetGroupHom) - (λ cwC cwD → Hˢᵏᵉˡ→ n (fst (snd cwD) ∘ f ∘ invEq (snd cwC))) + (λ cwC cwD → H̃ˢᵏᵉˡ→ n (fst (snd cwD) ∘ f ∘ invEq (snd cwC))) left right (λ _ _ _ _ → isSet→SquareP (λ _ _ → isSetGroupHom) _ _ _ _) -- functoriality -Hᶜʷ→ : {C : CW ℓ} {D : CW ℓ'} (n : ℕ) (f : C →ᶜʷ D) - → GroupHom (Hᶜʷ C n) (Hᶜʷ D n) -Hᶜʷ→ {C = C , cwC} {D = D , cwD} n f = Hᶜʷ→pre f n cwC cwD +H̃ᶜʷ→ : {C : CW ℓ} {D : CW ℓ'} (n : ℕ) (f : C →ᶜʷ D) + → GroupHom (H̃ᶜʷ C n) (H̃ᶜʷ D n) +H̃ᶜʷ→ {C = C , cwC} {D = D , cwD} n f = H̃ᶜʷ→pre f n cwC cwD -Hᶜʷ→id : {C : CW ℓ} (n : ℕ) - → Hᶜʷ→ {C = C} {C} n (idfun (fst C)) +H̃ᶜʷ→id : {C : CW ℓ} (n : ℕ) + → H̃ᶜʷ→ {C = C} {C} n (idfun (fst C)) ≡ idGroupHom -Hᶜʷ→id {C = C , cwC} n = +H̃ᶜʷ→id {C = C , cwC} n = PT.elim {P = λ cwC - → Hᶜʷ→ {C = C , cwC} {C , cwC} n (idfun C) ≡ idGroupHom} + → H̃ᶜʷ→ {C = C , cwC} {C , cwC} n (idfun C) ≡ idGroupHom} (λ _ → isSetGroupHom _ _) - (λ cwC* → cong (Hˢᵏᵉˡ→ n) (funExt (secEq (snd cwC*))) - ∙ Hˢᵏᵉˡ→id n) cwC + (λ cwC* → cong (H̃ˢᵏᵉˡ→ n) (funExt (secEq (snd cwC*))) + ∙ H̃ˢᵏᵉˡ→id n) cwC -Hᶜʷ→comp : {C : CW ℓ} {D : CW ℓ'} {E : CW ℓ''} (n : ℕ) +H̃ᶜʷ→comp : {C : CW ℓ} {D : CW ℓ'} {E : CW ℓ''} (n : ℕ) (g : D →ᶜʷ E) (f : C →ᶜʷ D) - → Hᶜʷ→ {C = C} {E} n (g ∘ f) - ≡ compGroupHom (Hᶜʷ→ {C = C} {D} n f) (Hᶜʷ→ {C = D} {E} n g) -Hᶜʷ→comp {C = C , cwC} {D = D , cwD} {E = E , cwE} n g f = + → H̃ᶜʷ→ {C = C} {E} n (g ∘ f) + ≡ compGroupHom (H̃ᶜʷ→ {C = C} {D} n f) (H̃ᶜʷ→ {C = D} {E} n g) +H̃ᶜʷ→comp {C = C , cwC} {D = D , cwD} {E = E , cwE} n g f = PT.elim3 {P = λ cwC cwD cwE - → Hᶜʷ→ {C = C , cwC} {E , cwE} n (g ∘ f) - ≡ compGroupHom (Hᶜʷ→ {C = C , cwC} {D , cwD} n f) - (Hᶜʷ→ {C = D , cwD} {E , cwE} n g)} + → H̃ᶜʷ→ {C = C , cwC} {E , cwE} n (g ∘ f) + ≡ compGroupHom (H̃ᶜʷ→ {C = C , cwC} {D , cwD} n f) + (H̃ᶜʷ→ {C = D , cwD} {E , cwE} n g)} (λ _ _ _ → isSetGroupHom _ _) (λ cwC cwD cwE - → cong (Hˢᵏᵉˡ→ n) (funExt (λ x → cong (fst (snd cwE) ∘ g) + → cong (H̃ˢᵏᵉˡ→ n) (funExt (λ x → cong (fst (snd cwE) ∘ g) (sym (retEq (snd cwD) _)))) - ∙ Hˢᵏᵉˡ→comp n _ _) + ∙ H̃ˢᵏᵉˡ→comp n _ _) cwC cwD cwE -- preservation of equivalence -Hᶜʷ→Iso : {C : CW ℓ} {D : CW ℓ'} (m : ℕ) - (e : fst C ≃ fst D) → GroupIso (Hᶜʷ C m) (Hᶜʷ D m) -Iso.fun (fst (Hᶜʷ→Iso m e)) = fst (Hᶜʷ→ m (fst e)) -Iso.inv (fst (Hᶜʷ→Iso m e)) = fst (Hᶜʷ→ m (invEq e)) -Iso.rightInv (fst (Hᶜʷ→Iso m e)) = - funExt⁻ (cong fst (sym (Hᶜʷ→comp m (fst e) (invEq e)) - ∙∙ cong (Hᶜʷ→ m) (funExt (secEq e)) - ∙∙ Hᶜʷ→id m)) -Iso.leftInv (fst (Hᶜʷ→Iso m e)) = - funExt⁻ (cong fst (sym (Hᶜʷ→comp m (invEq e) (fst e)) - ∙∙ cong (Hᶜʷ→ m) (funExt (retEq e)) - ∙∙ Hᶜʷ→id m)) -snd (Hᶜʷ→Iso m e) = snd (Hᶜʷ→ m (fst e)) - -Hᶜʷ→Equiv : {C : CW ℓ} {D : CW ℓ'} (m : ℕ) - (e : fst C ≃ fst D) → GroupEquiv (Hᶜʷ C m) (Hᶜʷ D m) -Hᶜʷ→Equiv m e = GroupIso→GroupEquiv (Hᶜʷ→Iso m e) +H̃ᶜʷ→Iso : {C : CW ℓ} {D : CW ℓ'} (m : ℕ) + (e : fst C ≃ fst D) → GroupIso (H̃ᶜʷ C m) (H̃ᶜʷ D m) +Iso.fun (fst (H̃ᶜʷ→Iso m e)) = fst (H̃ᶜʷ→ m (fst e)) +Iso.inv (fst (H̃ᶜʷ→Iso m e)) = fst (H̃ᶜʷ→ m (invEq e)) +Iso.rightInv (fst (H̃ᶜʷ→Iso m e)) = + funExt⁻ (cong fst (sym (H̃ᶜʷ→comp m (fst e) (invEq e)) + ∙∙ cong (H̃ᶜʷ→ m) (funExt (secEq e)) + ∙∙ H̃ᶜʷ→id m)) +Iso.leftInv (fst (H̃ᶜʷ→Iso m e)) = + funExt⁻ (cong fst (sym (H̃ᶜʷ→comp m (invEq e) (fst e)) + ∙∙ cong (H̃ᶜʷ→ m) (funExt (retEq e)) + ∙∙ H̃ᶜʷ→id m)) +snd (H̃ᶜʷ→Iso m e) = snd (H̃ᶜʷ→ m (fst e)) + +H̃ᶜʷ→Equiv : {C : CW ℓ} {D : CW ℓ'} (m : ℕ) + (e : fst C ≃ fst D) → GroupEquiv (H̃ᶜʷ C m) (H̃ᶜʷ D m) +H̃ᶜʷ→Equiv m e = GroupIso→GroupEquiv (H̃ᶜʷ→Iso m e) diff --git a/Cubical/CW/Homotopy.agda b/Cubical/CW/Homotopy.agda index 430437223a..2ab2efae3b 100644 --- a/Cubical/CW/Homotopy.agda +++ b/Cubical/CW/Homotopy.agda @@ -20,6 +20,7 @@ open import Cubical.Foundations.Function open import Cubical.Foundations.GroupoidLaws open import Cubical.Data.Nat renaming (_+_ to _+ℕ_) +open import Cubical.Data.Nat.Order.Inductive open import Cubical.Data.Int renaming (_·_ to _·ℤ_ ; -_ to -ℤ_) open import Cubical.Data.Fin.Inductive.Base open import Cubical.Data.Fin.Inductive.Properties @@ -85,7 +86,6 @@ finCellHom↓ : {m : ℕ} {C : CWskel ℓ} {D : CWskel ℓ'} fhom (finCellHom↓ ϕ) n x = fhom ϕ (injectSuc n) x fcoh (finCellHom↓ {m = suc m} ϕ) n x = fcoh ϕ (injectSuc n) x --- Extracting a map between sphere bouquets from a MMmap cofibIso : (n : ℕ) (C : CWskel ℓ) → Iso (Susp (cofibCW n C)) (SphereBouquet (suc n) (CWskel-fields.A C n)) cofibIso n C = @@ -197,7 +197,6 @@ module MMchainHomotopy* (m : ℕ) (C : CWskel ℓ) (D : CWskel ℓ') ∙∙ (cong inr (fhom H (injectSuc n) x)) ∙∙ (cong inr (g .fcomm n x)) - ww = MMΣcellMap -- the suspension of f as a MMmap MMΣf : MMmap m n merid-f merid-tt MMΣf = MMΣcellMap m n f @@ -390,8 +389,7 @@ module realiseMMmap (C : CWskel ℓ) (D : CWskel ℓ') (m : ℕ) (cong inr (g .fcomm n x)) (~ l) i) (~ k) }) south - -- realisation of MMΣH∂ is equal to Susp H∂ - -- TODO: it is the same code as before. factorise! +-- realisation of MMΣH∂ (suc n) is equal to Susp H∂ realiseMMΣH∂ : (C : CWskel ℓ) (D : CWskel ℓ') (m : ℕ) (f g : finCellMap (suc m) C D) (H : finCellHom (suc m) f g) (n : Fin m) (x : Susp (cofibCW (suc (fst n)) C)) → @@ -438,6 +436,40 @@ realiseMMΣH∂ C D (suc m) f g H n x = (i ∨ (~ k))}) south +-- realisation of MMΣH∂ zero is constant +realiseMMΣH∂₀ : (C : CWskel ℓ) (D : CWskel ℓ') (m : ℕ) + (f g : finCellMap (suc m) C D) (H : finCellHom (suc m) f g) + (x : Susp (cofibCW zero C)) → + MMmaps.realiseMMmap C D (suc m) fzero (λ x → inl tt) (λ x → inl tt) + (MMchainHomotopy*.MMΣH∂ (suc m) C D f g H fzero) x + ≡ north +realiseMMΣH∂₀ C D m f g H x = + realiseMMmap1≡2 fzero fzero (λ x → inl tt) + (λ x → inl tt) (MMΣH∂ fzero) x ∙ aux x + where + open FinSequenceMap + open MMmaps C D + open MMchainHomotopy* (suc m) C D f g H + open preChainHomotopy (suc m) C D f g H + open realiseMMmap C D (suc m) f g H + + aux : (x : Susp (cofibCW zero C)) → + realiseMMmap.realiseMMmap2 C D (suc m) f g H fzero fzero + (λ x₁ → inl tt) (λ x₁ → inl tt) + (MMchainHomotopy*.MMΣH∂ (suc m) C D f g H fzero) x + ≡ north + aux north = refl + aux south = refl + aux (merid (inl x) i) = refl + aux (merid (inr x) i) j = + hcomp (λ k → λ { (j = i0) → doubleCompPath-filler (merid (inl tt)) (λ _ → south) (λ i → merid (inl tt) (~ i)) k i + ; (j = i1) → north + ; (i = i0) → merid (inl tt) ((~ j) ∧ (~ k)) + ; (i = i1) → merid (inl tt) ((~ j) ∧ (~ k)) }) + (merid (inl tt) (~ j)) + aux (merid (push a i₁) i) with (C .snd .snd .snd .fst a) + aux (merid (push a i₁) i) | () + -- Then, we connect the addition of MMmaps to the addition of abelian maps module bouquetAdd where open MMmaps @@ -591,24 +623,24 @@ module bouquetAdd where -- Now we have all the ingredients, we can get the chain homotopy equation module chainHomEquation (m : ℕ) (C : CWskel ℓ) (D : CWskel ℓ') - (f g : finCellMap (suc m) C D) (H : finCellHom (suc m) f g) (n : Fin m) where + (f g : finCellMap m C D) (H : finCellHom m f g) (n : Fin m) where open SequenceMap - open MMmaps C D (suc m) (fsuc n) - open MMchainHomotopy* (suc m) C D f g H (fsuc n) - open preChainHomotopy (suc m) C D f g H - -- open realiseMMmap m C D f g H + open MMmaps C D m n + open MMchainHomotopy* m C D f g H n + open preChainHomotopy m C D f g H private ℤ[AC_] = CWskel-fields.ℤ[A_] C ℤ[AD_] = CWskel-fields.ℤ[A_] D -- The four abelian group maps that are involved in the equation - ∂H H∂ fn+1 gn+1 : AbGroupHom (ℤ[AC (suc (fst n))]) (ℤ[AD (suc (fst n)) ]) + ∂H H∂ fn gn : AbGroupHom (ℤ[AC (fst n) ]) (ℤ[AD (fst n) ]) - ∂H = compGroupHom (chainHomotopy (fsuc n)) (∂ D (suc (fst n))) - H∂ = compGroupHom (∂ C (fst n)) (chainHomotopy (injectSuc n)) - fn+1 = prefunctoriality.chainFunct (suc m) f (fsuc n) - gn+1 = prefunctoriality.chainFunct (suc m) g (fsuc n) + ∂H = compGroupHom (chainHomotopy n) (∂ D (fst n)) + -- H∂ = compGroupHom (∂ C (fst n)) (chainHomotopy (injectSuc n)) + H∂ = bouquetDegree (bouquetMMmap merid-tt merid-tt MMΣH∂) + fn = prefunctoriality.chainFunct m f n + gn = prefunctoriality.chainFunct m g n -- Technical lemma regarding suspensions of Iso's suspIso-suspFun : ∀ {ℓ ℓ' ℓ'' ℓ'''} {A : Type ℓ} {B : Type ℓ'} @@ -639,79 +671,52 @@ module chainHomEquation (m : ℕ) (C : CWskel ℓ) (D : CWskel ℓ') -- connecting MM∂H to ∂H bouquet∂H : bouquetDegree (bouquetMMmap merid-f merid-g MM∂H) ≡ ∂H bouquet∂H = - cong (λ X → bouquetDegree ((Iso.fun (cofibIso (suc (fst n)) D)) - ∘ X ∘ (Iso.inv (cofibIso (suc (fst n)) C)))) - (funExt (realiseMMmap.realiseMM∂H C D (suc m) f g H (fsuc n))) + cong (λ X → bouquetDegree ((Iso.fun (cofibIso (fst n) D)) + ∘ X ∘ (Iso.inv (cofibIso (fst n) C)))) + (funExt (realiseMMmap.realiseMM∂H C D m f g H n)) ∙ cong bouquetDegree ιδH≡pre∂∘H - ∙ bouquetDegreeComp (preboundary.pre∂ D (suc (fst n))) - (bouquetHomotopy (fsuc n)) + ∙ bouquetDegreeComp (preboundary.pre∂ D (fst n)) + (bouquetHomotopy n) where - ιδH : SphereBouquet (suc (suc (fst n))) - (Fin (CWskel-fields.card C (suc (fst n)))) - → SphereBouquet (suc (suc (fst n))) - (Fin (CWskel-fields.card D (suc (fst n)))) - ιδH = Iso.fun (cofibIso (suc (fst n)) D) - ∘ suspFun (to_cofibCW (suc (fst n)) D) - ∘ δ (suc (suc (fst n))) D - ∘ Hn+1/Hn (fsuc n) - ∘ Iso.inv (cofibIso (suc (fst n)) C) - - ιδH≡pre∂∘H : ιδH ≡ (preboundary.pre∂ D (suc (fst n))) - ∘ bouquetHomotopy (fsuc n) + ιδH : SphereBouquet (suc (fst n)) + (Fin (CWskel-fields.card C (fst n))) + → SphereBouquet (suc (fst n)) + (Fin (CWskel-fields.card D (fst n))) + ιδH = Iso.fun (cofibIso (fst n) D) + ∘ suspFun (to_cofibCW (fst n) D) + ∘ δ (suc (fst n)) D + ∘ Hn+1/Hn n + ∘ Iso.inv (cofibIso (fst n) C) + + ιδH≡pre∂∘H : ιδH ≡ (preboundary.pre∂ D (fst n)) + ∘ bouquetHomotopy n ιδH≡pre∂∘H = - cong (λ X → Iso.fun (cofibIso (suc (fst n)) D) - ∘ suspFun (to_cofibCW (suc (fst n)) D) - ∘ δ (suc (suc (fst n))) D ∘ X ∘ Hn+1/Hn (fsuc n) - ∘ Iso.inv (cofibIso (suc (fst n)) C)) - (sym (funExt (Iso.leftInv (BouquetIso D (suc (suc (fst n))))))) - - -- connecting MMΣH∂ to H∂ - bouquetΣH∂ : bouquetDegree (bouquetMMmap merid-tt merid-tt MMΣH∂) ≡ H∂ - bouquetΣH∂ = - cong (λ X → bouquetDegree ((Iso.fun (cofibIso (suc (fst n)) D)) - ∘ X ∘ (Iso.inv (cofibIso (suc (fst n)) C)))) - (funExt (realiseMMΣH∂ C D m f g H n)) - ∙ cong bouquetDegree (cofibIso-suspFun _ C D (Hn+1/Hn (injectSuc n) - ∘ suspFun (to_cofibCW (fst n) C) ∘ δ (suc (fst n)) C)) - ∙ sym (bouquetDegreeSusp Hιδ) - ∙ cong bouquetDegree Hιδ≡H∘pre∂ - ∙ bouquetDegreeComp (bouquetHomotopy (injectSuc n)) - (preboundary.pre∂ C (fst n)) - where - Hιδ : SphereBouquet (suc (fst n)) (Fin (CWskel-fields.card C (suc (fst n)))) - → SphereBouquet (suc (fst n)) (Fin (CWskel-fields.card D (suc (fst n)))) - Hιδ = Iso.fun (BouquetIso D (suc (fst n))) - ∘ (Hn+1/Hn (injectSuc n)) - ∘ suspFun (to_cofibCW (fst n) C) - ∘ δ (suc (fst n)) C ∘ Iso.inv (BouquetIso C (suc (fst n))) - - Hιδ≡H∘pre∂ : Hιδ ≡ bouquetHomotopy (injectSuc n) ∘ (preboundary.pre∂ C (fst n)) - Hιδ≡H∘pre∂ = cong (λ X → Iso.fun (BouquetIso D (suc (fst n))) - ∘ (Hn+1/Hn (injectSuc n)) ∘ X - ∘ suspFun (to_cofibCW (fst n) C) ∘ δ (suc (fst n)) C - ∘ Iso.inv (BouquetIso C (suc (fst n)))) - (sym (funExt (Iso.leftInv (cofibIso (fst n) C)))) + cong (λ X → Iso.fun (cofibIso (fst n) D) + ∘ suspFun (to_cofibCW (fst n) D) + ∘ δ (suc (fst n)) D ∘ X ∘ Hn+1/Hn n + ∘ Iso.inv (cofibIso (fst n) C)) + (sym (funExt (Iso.leftInv (BouquetIso D (suc (fst n)))))) -- connecting MMΣf to fn+1 - bouquetΣf : bouquetDegree (bouquetMMmap merid-f merid-tt MMΣf) ≡ fn+1 - bouquetΣf = cong (λ X → bouquetDegree ((Iso.fun (cofibIso (suc (fst n)) D)) - ∘ X ∘ (Iso.inv (cofibIso (suc (fst n)) C)))) - (funExt (realiseMMmap.realiseMMΣf C D (suc m) f g H (fsuc n))) - ∙ (cong bouquetDegree (cofibIso-suspFun (suc (fst n)) C D - (prefunctoriality.fn+1/fn (suc m) f (fsuc n)))) - ∙ sym (bouquetDegreeSusp (prefunctoriality.bouquetFunct (suc m) f (fsuc n))) + bouquetΣf : bouquetDegree (bouquetMMmap merid-f merid-tt MMΣf) ≡ fn + bouquetΣf = cong (λ X → bouquetDegree ((Iso.fun (cofibIso (fst n) D)) + ∘ X ∘ (Iso.inv (cofibIso (fst n) C)))) + (funExt (realiseMMmap.realiseMMΣf C D m f g H n)) + ∙ (cong bouquetDegree (cofibIso-suspFun (fst n) C D + (prefunctoriality.fn+1/fn m f n))) + ∙ sym (bouquetDegreeSusp (prefunctoriality.bouquetFunct m f n)) -- connecting MMΣg to gn+1 - bouquetΣg : bouquetDegree (bouquetMMmap merid-g merid-tt MMΣg) ≡ gn+1 - bouquetΣg = cong (λ X → bouquetDegree ((Iso.fun (cofibIso (suc (fst n)) D)) - ∘ X ∘ (Iso.inv (cofibIso (suc (fst n)) C)))) - (funExt (realiseMMmap.realiseMMΣg C D (suc m) f g H (fsuc n))) - ∙ (cong bouquetDegree (cofibIso-suspFun (suc (fst n)) C D - (prefunctoriality.fn+1/fn (suc m) g (fsuc n)))) - ∙ sym (bouquetDegreeSusp (prefunctoriality.bouquetFunct (suc m) g (fsuc n))) + bouquetΣg : bouquetDegree (bouquetMMmap merid-g merid-tt MMΣg) ≡ gn + bouquetΣg = cong (λ X → bouquetDegree ((Iso.fun (cofibIso (fst n) D)) + ∘ X ∘ (Iso.inv (cofibIso (fst n) C)))) + (funExt (realiseMMmap.realiseMMΣg C D m f g H n)) + ∙ (cong bouquetDegree (cofibIso-suspFun (fst n) C D + (prefunctoriality.fn+1/fn m g n))) + ∙ sym (bouquetDegreeSusp (prefunctoriality.bouquetFunct m g n)) -- Alternative formulation of the chain homotopy equation - chainHomotopy1 : addGroupHom _ _ (addGroupHom _ _ ∂H gn+1) H∂ ≡ fn+1 + chainHomotopy1 : addGroupHom _ _ (addGroupHom _ _ ∂H gn) H∂ ≡ fn chainHomotopy1 = cong (λ X → addGroupHom _ _ X H∂) aux ∙ aux2 @@ -719,32 +724,29 @@ module chainHomEquation (m : ℕ) (C : CWskel ℓ) (D : CWskel ℓ') (funExt MMchainHomotopy) ∙ bouquetΣf where - module T = MMchainHomotopy* (suc m) C D f g H (fsuc n) + module T = MMchainHomotopy* m C D f g H n MM∂H+MMΣg = MMmap-add T.merid-f T.merid-g T.merid-tt T.MM∂H T.MMΣg MM∂H+MMΣg+MMΣH∂ = MMmap-add merid-f merid-tt merid-tt MM∂H+MMΣg MMΣH∂ - aux : addGroupHom _ _ ∂H gn+1 + aux : addGroupHom _ _ ∂H gn ≡ bouquetDegree (bouquetMMmap merid-f merid-tt MM∂H+MMΣg) aux = cong₂ (λ X Y → addGroupHom _ _ X Y) (sym bouquet∂H) (sym bouquetΣg) - ∙ sym (bouquetAdd.realiseMMmap-hom C D (suc m) (fsuc n) + ∙ sym (bouquetAdd.realiseMMmap-hom C D m n T.merid-f T.merid-g T.merid-tt T.MM∂H T.MMΣg) aux2 : addGroupHom _ _ (bouquetDegree (bouquetMMmap merid-f merid-tt MM∂H+MMΣg)) H∂ ≡ bouquetDegree (bouquetMMmap merid-f merid-tt MM∂H+MMΣg+MMΣH∂) - aux2 = cong (addGroupHom _ _ (bouquetDegree - (bouquetMMmap merid-f merid-tt MM∂H+MMΣg))) - (sym bouquetΣH∂) - ∙ sym (bouquetAdd.realiseMMmap-hom C D (suc m) (fsuc n) + aux2 = sym (bouquetAdd.realiseMMmap-hom C D m n T.merid-f T.merid-tt T.merid-tt MM∂H+MMΣg T.MMΣH∂) -- Standard formulation of the chain homotopy equation - chainHomotopy2 : subtrGroupHom _ _ fn+1 gn+1 ≡ addGroupHom _ _ ∂H H∂ + chainHomotopy2 : subtrGroupHom _ _ fn gn ≡ addGroupHom _ _ ∂H H∂ chainHomotopy2 = - GroupHom≡ (funExt λ x → aux (fn+1 .fst x) (∂H .fst x) (gn+1 .fst x) + GroupHom≡ (funExt λ x → aux (fn .fst x) (∂H .fst x) (gn .fst x) (H∂ .fst x) (cong (λ X → X .fst x) chainHomotopy1)) where - open AbGroupStr (snd (ℤ[AD (suc (fst n)) ])) + open AbGroupStr (snd (ℤ[AD (fst n) ])) renaming (_+_ to _+G_ ; -_ to -G_ ; +Assoc to +AssocG ; +Comm to +CommG) aux : ∀ w x y z → (x +G y) +G z ≡ w → w +G (-G y) ≡ x +G z aux w x y z H = cong (λ X → X +G (-G y)) (sym H) @@ -755,12 +757,87 @@ module chainHomEquation (m : ℕ) (C : CWskel ℓ) (D : CWskel ℓ') ∙ cong (λ X → x +G X) (+InvR y) ∙ +IdR x) +module chainHomEquationSuc (m : ℕ) (C : CWskel ℓ) (D : CWskel ℓ') + (f g : finCellMap (suc m) C D) (H : finCellHom (suc m) f g) (n : Fin m) where + open SequenceMap + open MMmaps C D (suc m) (fsuc n) + open MMchainHomotopy* (suc m) C D f g H (fsuc n) + open preChainHomotopy (suc m) C D f g H + open chainHomEquation (suc m) C D f g H (fsuc n) + + private + ℤ[AC_] = CWskel-fields.ℤ[A_] C + ℤ[AD_] = CWskel-fields.ℤ[A_] D + + H∂' : AbGroupHom (ℤ[AC (suc (fst n)) ]) (ℤ[AD (suc (fst n)) ]) + H∂' = compGroupHom (∂ C (fst n)) (chainHomotopy (injectSuc n)) + + -- connecting MMΣH∂ to H∂' + bouquetΣH∂ : H∂ ≡ H∂' + bouquetΣH∂ = + cong (λ X → bouquetDegree ((Iso.fun (cofibIso (suc (fst n)) D)) + ∘ X ∘ (Iso.inv (cofibIso (suc (fst n)) C)))) + (funExt (realiseMMΣH∂ C D m f g H n)) + ∙ cong bouquetDegree (cofibIso-suspFun _ C D (Hn+1/Hn (injectSuc n) + ∘ suspFun (to_cofibCW (fst n) C) ∘ δ (suc (fst n)) C)) + ∙ sym (bouquetDegreeSusp Hιδ) + ∙ cong bouquetDegree Hιδ≡H∘pre∂ + ∙ bouquetDegreeComp (bouquetHomotopy (injectSuc n)) + (preboundary.pre∂ C (fst n)) + where + Hιδ : SphereBouquet (suc (fst n)) (Fin (CWskel-fields.card C (suc (fst n)))) + → SphereBouquet (suc (fst n)) (Fin (CWskel-fields.card D (suc (fst n)))) + Hιδ = Iso.fun (BouquetIso D (suc (fst n))) + ∘ (Hn+1/Hn (injectSuc n)) + ∘ suspFun (to_cofibCW (fst n) C) + ∘ δ (suc (fst n)) C ∘ Iso.inv (BouquetIso C (suc (fst n))) + + Hιδ≡H∘pre∂ : Hιδ ≡ bouquetHomotopy (injectSuc n) ∘ (preboundary.pre∂ C (fst n)) + Hιδ≡H∘pre∂ = cong (λ X → Iso.fun (BouquetIso D (suc (fst n))) + ∘ (Hn+1/Hn (injectSuc n)) ∘ X + ∘ suspFun (to_cofibCW (fst n) C) ∘ δ (suc (fst n)) C + ∘ Iso.inv (BouquetIso C (suc (fst n)))) + (sym (funExt (Iso.leftInv (cofibIso (fst n) C)))) + + chainHomotopySuc : subtrGroupHom _ _ fn gn ≡ addGroupHom _ _ ∂H H∂' + chainHomotopySuc = chainHomotopy2 ∙ cong (addGroupHom _ _ ∂H) bouquetΣH∂ + +module chainHomEquationZero (m : ℕ) (C : CWskel ℓ) (D : CWskel ℓ') + (f g : finCellMap (suc m) C D) (H : finCellHom (suc m) f g) where + open SequenceMap + open MMmaps C D (suc m) fzero + open MMchainHomotopy* (suc m) C D f g H fzero + open preChainHomotopy (suc m) C D f g H + open chainHomEquation (suc m) C D f g H fzero + + private + ℤ[AC_] = CWskel-fields.ℤ[A_] C + ℤ[AD_] = CWskel-fields.ℤ[A_] D + + H∂' : AbGroupHom (ℤ[AC 0 ]) (ℤ[AD 0 ]) + H∂' = compGroupHom (augmentation.ϵ C) trivGroupHom + + MMΣH∂-const : ∀ x → bouquetMMmap merid-tt merid-tt MMΣH∂ x ≡ inl tt + MMΣH∂-const x = cong (Iso.fun (cofibIso 0 D)) (realiseMMΣH∂₀ C D m f g H (Iso.inv (cofibIso 0 C) x)) + + bouquetΣH∂ : H∂ ≡ H∂' + bouquetΣH∂ = cong bouquetDegree (funExt MMΣH∂-const) + ∙ bouquetDegreeConst _ _ _ + ∙ GroupHom≡ refl + + chainHomotopyZero : subtrGroupHom _ _ fn gn ≡ addGroupHom _ _ ∂H H∂' + chainHomotopyZero = chainHomotopy2 ∙ cong (addGroupHom _ _ ∂H) bouquetΣH∂ + -- Going from a cell homotopy to a chain homotopy cellHom-to-ChainHomotopy : {C : CWskel ℓ} {D : CWskel ℓ'} (m : ℕ) - {f g : finCellMap (suc m) C D} (H : finCellHom (suc m) f g) - → finChainHomotopy m (finCellMap→finChainComplexMap m f) - (finCellMap→finChainComplexMap m g) -cellHom-to-ChainHomotopy {C = C} {D} m {f} {g} H .finChainHomotopy.fhtpy n = - preChainHomotopy.chainHomotopy (suc m) C D f g H n -cellHom-to-ChainHomotopy {C = C} {D} m {f} {g} H .finChainHomotopy.fbdryhtpy n = - chainHomEquation.chainHomotopy2 m C D f g H n + {f g : finCellMap (suc (suc m)) C D} (H : finCellHom (suc (suc m)) f g) + → finChainHomotopy (suc m) (finCellMap→finChainComplexMap m f) + (finCellMap→finChainComplexMap m g) +cellHom-to-ChainHomotopy {C = C} {D} m {f} {g} H .finChainHomotopy.fhtpy (zero , _) = + trivGroupHom +cellHom-to-ChainHomotopy {C = C} {D} m {f} {g} H .finChainHomotopy.fhtpy (suc n , n Date: Tue, 21 Jan 2025 16:16:02 +0100 Subject: [PATCH 2/2] explicit description of the augmentation map --- .../AbGroup/Instances/FreeAbGroup.agda | 47 +++++++++++++++++++ Cubical/Algebra/ChainComplex/Homology.agda | 42 ++++++----------- Cubical/CW/ChainComplex.agda | 36 +++++++++++++- Cubical/Data/Fin/Inductive/Properties.agda | 6 +++ 4 files changed, 103 insertions(+), 28 deletions(-) diff --git a/Cubical/Algebra/AbGroup/Instances/FreeAbGroup.agda b/Cubical/Algebra/AbGroup/Instances/FreeAbGroup.agda index 53f6b48a79..f16052a98e 100644 --- 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