-
Notifications
You must be signed in to change notification settings - Fork 138
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
201 changed files
with
13,394 additions
and
1,850 deletions.
There are no files selected for viewing
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
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.