michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add HH_base_indep.

Browse source
This commit is contained in:
favonia 2017-06-06 14:29:41 -06:00
parent e2a12f7db7
commit 61c9f175d3
1 changed files with 26 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
homology/homology.hlean
View file

@ -5,9 +5,9 @@ open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops equ
namespace homology namespace homology
/- homology theory -/ /- homology theory -/
structure homology_theory.{u} : Type.{u+1} := structure homology_theory.{u} : Type.{u+1} :=
(HH : ℤ → pType.{u} → AbGroup.{u}) (HH : ℤ → pType.{u} → AbGroup.{u})
(Hh : Π(n : ℤ) {X Y : Type*} (f : X →* Y), HH n X →g HH n Y) (Hh : Π(n : ℤ) {X Y : Type*} (f : X →* Y), HH n X →g HH n Y)
(Hid : Π(n : ℤ) {X : Type*} (x : HH n X), Hh n (pid X) x = x) (Hid : Π(n : ℤ) {X : Type*} (x : HH n X), Hh n (pid X) x = x)
@ -19,5 +19,17 @@ structure homology_theory.{u} : Type.{u+1} :=
(Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n f) (Hh n (pcod f))) (Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n f) (Hh n (pcod f)))
(Hadditive : Π(n : ℤ) {I : Set.{u}} (X : I → Type*), is_equiv ( (Hadditive : Π(n : ℤ) {I : Set.{u}} (X : I → Type*), is_equiv (
dirsum_elim (λi, Hh n (pinl i)) : dirsum (λi, HH n (X i)) → HH n (⋁ X)) dirsum_elim (λi, Hh n (pinl i)) : dirsum (λi, HH n (X i)) → HH n (⋁ X))
) )
section
parameter (theory : homology_theory)
open homology_theory
definition HH_base_indep (n : ℤ) {A : Type} (a b : A)
: HH theory n (pType.mk A a) ≃g HH theory n (pType.mk A b) :=
calc HH theory n (pType.mk A a) ≃g HH theory (int.succ n) (psusp A) : by exact (Hsusp theory n (pType.mk A a)) ⁻¹ᵍ
... ≃g HH theory n (pType.mk A b) : by exact Hsusp theory n (pType.mk A b)
end
end homology end homology