-
Notifications
You must be signed in to change notification settings - Fork 132
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
CW complexes, cellular homology + a lot more (#1111)
* t * duplicate * wups * rme * ganea stuff * w * w * w * fix * stuff * stuff * more * .. * done? * wups * wups * wups * fixes * ugh... * wups * stuff * stuff * stuff * stuf * More * stuff * stuff * stuff * done? * stuff * cleanup * readme * wups * ugh * wups * broken code * ojdå * comments * minor
- Loading branch information
1 parent
cb0328e
commit 36a14f8
Showing
67 changed files
with
6,983 additions
and
98 deletions.
There are no files selected for viewing
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,6 @@ | ||
| {-# OPTIONS --safe #-} | ||
| module Cubical.Algebra.ChainComplex where | ||
|
|
||
| open import Cubical.Algebra.ChainComplex.Base public | ||
| open import Cubical.Algebra.ChainComplex.Homology public | ||
| open import Cubical.Algebra.ChainComplex.Finite public |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,114 @@ | ||
| {-# OPTIONS --safe --lossy-unification #-} | ||
| module Cubical.Algebra.ChainComplex.Base where | ||
|
|
||
| open import Cubical.Foundations.Prelude | ||
| open import Cubical.Foundations.Function | ||
| open import Cubical.Foundations.Equiv | ||
|
|
||
| open import Cubical.Data.Sigma | ||
| open import Cubical.Data.Nat | ||
|
|
||
| open import Cubical.Algebra.Group | ||
| open import Cubical.Algebra.Group.MorphismProperties | ||
| open import Cubical.Algebra.AbGroup | ||
|
|
||
| private | ||
| variable | ||
| ℓ ℓ' ℓ'' : Level | ||
|
|
||
| record ChainComplex (ℓ : Level) : Type (ℓ-suc ℓ) where | ||
| field | ||
| chain : (i : ℕ) → AbGroup ℓ | ||
| bdry : (i : ℕ) → AbGroupHom (chain (suc i)) (chain i) | ||
| bdry²=0 : (i : ℕ) → compGroupHom (bdry (suc i)) (bdry i) ≡ trivGroupHom | ||
|
|
||
| record ChainComplexMap {ℓ ℓ' : Level} | ||
| (A : ChainComplex ℓ) (B : ChainComplex ℓ') : Type (ℓ-max ℓ ℓ') where | ||
| open ChainComplex | ||
| field | ||
| chainmap : (i : ℕ) → AbGroupHom (chain A i) (chain B i) | ||
| bdrycomm : (i : ℕ) | ||
| → compGroupHom (chainmap (suc i)) (bdry B i) ≡ compGroupHom (bdry A i) (chainmap i) | ||
|
|
||
| record ChainHomotopy {ℓ : Level} {A : ChainComplex ℓ} {B : ChainComplex ℓ'} | ||
| (f g : ChainComplexMap A B) : Type (ℓ-max ℓ' ℓ) where | ||
| open ChainComplex | ||
| open ChainComplexMap | ||
| field | ||
| htpy : (i : ℕ) → AbGroupHom (chain A i) (chain B (suc i)) | ||
| bdryhtpy : (i : ℕ) | ||
| → subtrGroupHom (chain A (suc i)) (chain B (suc i)) | ||
| (chainmap f (suc i)) (chainmap g (suc i)) | ||
| ≡ addGroupHom (chain A (suc i)) (chain B (suc i)) | ||
| (compGroupHom (htpy (suc i)) (bdry B (suc i))) | ||
| (compGroupHom (bdry A i) (htpy i)) | ||
|
|
||
| record CoChainComplex (ℓ : Level) : Type (ℓ-suc ℓ) where | ||
| field | ||
| cochain : (i : ℕ) → AbGroup ℓ | ||
| cobdry : (i : ℕ) → AbGroupHom (cochain i) (cochain (suc i)) | ||
| cobdry²=0 : (i : ℕ) → compGroupHom (cobdry i) (cobdry (suc i)) | ||
| ≡ trivGroupHom | ||
|
|
||
| open ChainComplexMap | ||
| ChainComplexMap≡ : {A : ChainComplex ℓ} {B : ChainComplex ℓ'} | ||
| {f g : ChainComplexMap A B} | ||
| → ((i : ℕ) → chainmap f i ≡ chainmap g i) | ||
| → f ≡ g | ||
| chainmap (ChainComplexMap≡ p i) n = p n i | ||
| bdrycomm (ChainComplexMap≡ {A = A} {B = B} {f = f} {g = g} p i) n = | ||
| isProp→PathP {B = λ i → compGroupHom (p (suc n) i) (ChainComplex.bdry B n) | ||
| ≡ compGroupHom (ChainComplex.bdry A n) (p n i)} | ||
| (λ i → isSetGroupHom _ _) | ||
| (bdrycomm f n) (bdrycomm g n) i | ||
|
|
||
| compChainMap : {A : ChainComplex ℓ} {B : ChainComplex ℓ'} {C : ChainComplex ℓ''} | ||
| → (f : ChainComplexMap A B) (g : ChainComplexMap B C) | ||
| → ChainComplexMap A C | ||
| compChainMap {A = A} {B} {C} ϕ' ψ' = main | ||
| where | ||
| ϕ = chainmap ϕ' | ||
| commϕ = bdrycomm ϕ' | ||
| ψ = chainmap ψ' | ||
| commψ = bdrycomm ψ' | ||
|
|
||
| main : ChainComplexMap A C | ||
| chainmap main n = compGroupHom (ϕ n) (ψ n) | ||
| bdrycomm main n = | ||
| Σ≡Prop (λ _ → isPropIsGroupHom _ _) | ||
| (funExt λ x | ||
| → (funExt⁻ (cong fst (commψ n)) (ϕ (suc n) .fst x)) | ||
| ∙ cong (fst (ψ n)) (funExt⁻ (cong fst (commϕ n)) x)) | ||
|
|
||
| isChainEquiv : {A : ChainComplex ℓ} {B : ChainComplex ℓ'} | ||
| → ChainComplexMap A B → Type (ℓ-max ℓ ℓ') | ||
| isChainEquiv f = ((n : ℕ) → isEquiv (chainmap f n .fst)) | ||
|
|
||
| _≃Chain_ : (A : ChainComplex ℓ) (B : ChainComplex ℓ') → Type (ℓ-max ℓ ℓ') | ||
| A ≃Chain B = Σ[ f ∈ ChainComplexMap A B ] (isChainEquiv f) | ||
|
|
||
| idChainMap : (A : ChainComplex ℓ) → ChainComplexMap A A | ||
| chainmap (idChainMap A) _ = idGroupHom | ||
| bdrycomm (idChainMap A) _ = | ||
| Σ≡Prop (λ _ → isPropIsGroupHom _ _) refl | ||
|
|
||
| invChainMap : {A : ChainComplex ℓ} {B : ChainComplex ℓ'} | ||
| → (A ≃Chain B) → ChainComplexMap B A | ||
| chainmap (invChainMap (ϕ , eq)) n = | ||
| GroupEquiv→GroupHom (invGroupEquiv ((chainmap ϕ n .fst , eq n) , snd (chainmap ϕ n))) | ||
| bdrycomm (invChainMap {B = B} (ϕ' , eq)) n = | ||
| Σ≡Prop (λ _ → isPropIsGroupHom _ _) | ||
| (funExt λ x | ||
| → sym (retEq (_ , eq n ) _) | ||
| ∙∙ cong (invEq (_ , eq n )) | ||
| (sym (funExt⁻ (cong fst (ϕcomm n)) (invEq (_ , eq (suc n)) x))) | ||
| ∙∙ cong (invEq (ϕ n .fst , eq n ) ∘ fst (ChainComplex.bdry B n)) | ||
| (secEq (_ , eq (suc n)) x)) | ||
| where | ||
| ϕ = chainmap ϕ' | ||
| ϕcomm = bdrycomm ϕ' | ||
|
|
||
| invChainEquiv : {A : ChainComplex ℓ} {B : ChainComplex ℓ'} | ||
| → A ≃Chain B → B ≃Chain A | ||
| fst (invChainEquiv e) = invChainMap e | ||
| snd (invChainEquiv e) n = snd (invEquiv (chainmap (fst e) n .fst , snd e n)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,123 @@ | ||
| {-# OPTIONS --safe --lossy-unification #-} | ||
| module Cubical.Algebra.ChainComplex.Finite where | ||
|
|
||
| {- When dealing with chain maps and chain homotopies constructively, | ||
| it is often the case the case that one only is able to obtain a finite | ||
| approximation rather than the full thing. This file contains | ||
| definitions of | ||
| (1) finite chain maps, | ||
| (2) finite chain homotopies | ||
| (3) finite chain equivalences | ||
| and proof their induced behaviour on homology | ||
| -} | ||
|
|
||
| open import Cubical.Foundations.Prelude | ||
| open import Cubical.Foundations.Function | ||
| open import Cubical.Foundations.Equiv | ||
|
|
||
| open import Cubical.Data.Sigma | ||
| open import Cubical.Data.Nat | ||
| open import Cubical.Data.Fin.Inductive.Base | ||
|
|
||
| open import Cubical.Algebra.ChainComplex.Base | ||
| open import Cubical.Algebra.Group.MorphismProperties | ||
| open import Cubical.Algebra.AbGroup | ||
|
|
||
| private | ||
| variable | ||
| ℓ ℓ' ℓ'' : Level | ||
|
|
||
| module _ where | ||
| record finChainComplexMap {ℓ ℓ' : Level} (m : ℕ) | ||
| (A : ChainComplex ℓ) (B : ChainComplex ℓ') : Type (ℓ-max ℓ ℓ') where | ||
| open ChainComplex | ||
| field | ||
| fchainmap : (i : Fin (suc m)) | ||
| → AbGroupHom (chain A (fst i)) (chain B (fst i)) | ||
| fbdrycomm : (i : Fin m) | ||
| → compGroupHom (fchainmap (fsuc i)) (bdry B (fst i)) | ||
| ≡ compGroupHom (bdry A (fst i)) (fchainmap (injectSuc i)) | ||
|
|
||
| record finChainHomotopy {ℓ : Level} (m : ℕ) | ||
| {A : ChainComplex ℓ} {B : ChainComplex ℓ'} | ||
| (f g : finChainComplexMap m A B) : Type (ℓ-max ℓ' ℓ) where | ||
| open ChainComplex | ||
| open finChainComplexMap | ||
| field | ||
| fhtpy : (i : Fin (suc m)) | ||
| → AbGroupHom (chain A (fst i)) (chain B (suc (fst i))) | ||
| fbdryhtpy : (i : Fin m) | ||
| → subtrGroupHom (chain A (suc (fst i))) (chain B (suc (fst i))) | ||
| (fchainmap f (fsuc i)) (fchainmap g (fsuc i)) | ||
| ≡ addGroupHom (chain A (suc (fst i))) (chain B (suc (fst i))) | ||
| (compGroupHom (fhtpy (fsuc i)) (bdry B (suc (fst i)))) | ||
| (compGroupHom (bdry A (fst i)) (fhtpy (injectSuc i))) | ||
|
|
||
| open finChainComplexMap | ||
| finChainComplexMap≡ : | ||
| {A : ChainComplex ℓ} {B : ChainComplex ℓ'} {m : ℕ} | ||
| {f g : finChainComplexMap m A B} | ||
| → ((i : Fin (suc m)) → fchainmap f i ≡ fchainmap g i) | ||
| → f ≡ g | ||
| fchainmap (finChainComplexMap≡ p i) n = p n i | ||
| fbdrycomm (finChainComplexMap≡ {A = A} {B = B} {f = f} {g = g} p i) n = | ||
| isProp→PathP {B = λ i | ||
| → compGroupHom (p (fsuc n) i) (ChainComplex.bdry B (fst n)) | ||
| ≡ compGroupHom (ChainComplex.bdry A (fst n)) (p (injectSuc n) i)} | ||
| (λ i → isSetGroupHom _ _) | ||
| (fbdrycomm f n) (fbdrycomm g n) i | ||
|
|
||
| compFinChainMap : | ||
| {A : ChainComplex ℓ} {B : ChainComplex ℓ'} {C : ChainComplex ℓ''} {m : ℕ} | ||
| → (f : finChainComplexMap m A B) (g : finChainComplexMap m B C) | ||
| → finChainComplexMap m A C | ||
| compFinChainMap {A = A} {B} {C} {m = m} ϕ' ψ' = main | ||
| where | ||
| ϕ = fchainmap ϕ' | ||
| commϕ = fbdrycomm ϕ' | ||
| ψ = fchainmap ψ' | ||
| commψ = fbdrycomm ψ' | ||
|
|
||
| main : finChainComplexMap m A C | ||
| fchainmap main n = compGroupHom (ϕ n) (ψ n) | ||
| fbdrycomm main n = | ||
| Σ≡Prop (λ _ → isPropIsGroupHom _ _) | ||
| (funExt λ x | ||
| → (funExt⁻ (cong fst (commψ n)) (ϕ (fsuc n) .fst x)) | ||
| ∙ cong (fst (ψ (injectSuc n))) (funExt⁻ (cong fst (commϕ n)) x)) | ||
|
|
||
| isFinChainEquiv : {A : ChainComplex ℓ} {B : ChainComplex ℓ'} {m : ℕ} | ||
| → finChainComplexMap m A B → Type (ℓ-max ℓ ℓ') | ||
| isFinChainEquiv {m = m} f = ((n : Fin (suc m)) → isEquiv (fchainmap f n .fst)) | ||
|
|
||
| _≃⟨_⟩Chain_ : (A : ChainComplex ℓ) (m : ℕ) (B : ChainComplex ℓ') | ||
| → Type (ℓ-max ℓ ℓ') | ||
| A ≃⟨ m ⟩Chain B = Σ[ f ∈ finChainComplexMap m A B ] (isFinChainEquiv f) | ||
|
|
||
| idFinChainMap : (m : ℕ) (A : ChainComplex ℓ) → finChainComplexMap m A A | ||
| fchainmap (idFinChainMap m A) _ = idGroupHom | ||
| fbdrycomm (idFinChainMap m A) _ = | ||
| Σ≡Prop (λ _ → isPropIsGroupHom _ _) refl | ||
|
|
||
| invFinChainMap : {A : ChainComplex ℓ} {B : ChainComplex ℓ'} {m : ℕ} | ||
| → (A ≃⟨ m ⟩Chain B) → finChainComplexMap m B A | ||
| fchainmap (invFinChainMap {m = m} (ϕ , eq)) n = | ||
| GroupEquiv→GroupHom | ||
| (invGroupEquiv ((fchainmap ϕ n .fst , eq n) , snd (fchainmap ϕ n))) | ||
| fbdrycomm (invFinChainMap {B = B} {m = m} (ϕ' , eq)) n = | ||
| Σ≡Prop (λ _ → isPropIsGroupHom _ _) | ||
| (funExt λ x | ||
| → sym (retEq (_ , eq (injectSuc n) ) _) | ||
| ∙∙ cong (invEq (_ , eq (injectSuc n) )) | ||
| (sym (funExt⁻ (cong fst (ϕcomm n)) (invEq (_ , eq (fsuc n)) x))) | ||
| ∙∙ cong (invEq (ϕ (injectSuc n) .fst , eq (injectSuc n) ) | ||
| ∘ fst (ChainComplex.bdry B (fst n))) | ||
| (secEq (_ , eq (fsuc n)) x)) | ||
| where | ||
| ϕ = fchainmap ϕ' | ||
| ϕcomm = fbdrycomm ϕ' | ||
|
|
||
| invFinChainEquiv : {A : ChainComplex ℓ} {B : ChainComplex ℓ'} {m : ℕ} | ||
| → A ≃⟨ m ⟩Chain B → B ≃⟨ m ⟩Chain A | ||
| fst (invFinChainEquiv e) = invFinChainMap e | ||
| snd (invFinChainEquiv e) n = snd (invEquiv (fchainmap (fst e) n .fst , snd e n)) |
Oops, something went wrong.