redefine homology to use smash with prespectra

algebra/seq_colim.hlean

@@ -6,7 +6,7 @@ namespace group
 
   section
 
-    parameters (A : ℕ → AbGroup) (f : Πi , A i → A (i + 1))
+    parameters (A : ℕ → AbGroup) (f : Πi , A i →g A (i + 1))
     variables {A' : AbGroup}
 
     definition seq_colim_carrier : AbGroup := dirsum A
@@ -72,8 +72,21 @@ namespace group
 
   definition seq_colim_functor [constructor] {A A' : ℕ → AbGroup}
     {f : Πi , A i →g A (i + 1)} {f' : Πi , A' i →g A' (i + 1)}
-    (h : Πi, A i →g A' i) : seq_colim A f →g seq_colim A' f' :=
+    (h : Πi, A i →g A' i) (p : Πi, hsquare (f i) (f' i) (h i) (h (i+1))) :
-  sorry --_ ∘g _
+    seq_colim A f →g seq_colim A' f' :=
+  seq_colim_elim (λi, seq_colim_incl i ∘g h i)
+    begin
+      intro i a,
+      refine !homomorphism_comp_compute ⬝ _ ⬝ !homomorphism_comp_compute⁻¹,
+      refine _ ⬝ ap (seq_colim_incl (succ i)) (p i a)⁻¹,
+      apply seq_colim_glue
+    end
 
+  -- definition seq_colim_functor_compose [constructor] {A A' A'' : ℕ → AbGroup}
+  --   {f : Πi , A i →g A (i + 1)} {f' : Πi , A' i →g A' (i + 1)} {f'' : Πi , A'' i →g A'' (i + 1)}
+  --   (h : Πi, A i →g A' i) (p : Πi (a : A i), h (i+1) (f i a) = f' i (h i a))
+  --   (h : Πi, A i →g A' i) (p : Πi (a : A i), h (i+1) (f i a) = f' i (h i a)) :
+  --   seq_colim A f →g seq_colim A' f' :=
+  -- sorry
 
 end group

colim.hlean

@@ -377,6 +377,12 @@ namespace seq_colim
     exact !pcompose_pid
   end
 
+  definition seq_colim_equiv_zigzag (g : Π⦃n⦄, A n → A' n) (h : Π⦃n⦄, A' n → A (succ n))
+    (p : Π⦃n⦄ (a : A n), h (g a) = f a) (q : Π⦃n⦄ (a : A' n), g (h a) = f' a) :
+    seq_colim f ≃ seq_colim f' :=
+  sorry
+
+
   definition is_equiv_seq_colim_rec (P : seq_colim f → Type) :
     is_equiv (seq_colim_rec_unc :
       (Σ(Pincl : Π ⦃n : ℕ⦄ (a : A n), P (ι f a)),

homology/homology.hlean

@@ -112,8 +112,8 @@ notation `pH_` n `[`:0 binders `, ` r:(scoped E, parametrized_homology E n) `]`:
 definition unpointed_homology (X : Type) (E : spectrum) (n : ℤ) : AbGroup :=
 H_ n[X₊, E]
 
-definition homology_functor [constructor] {X Y : Type*} {E F : spectrum} (f : X →* Y) (g : E →ₛ F) (n : ℤ)
+definition homology_functor [constructor] {X Y : Type*} {E F : prespectrum} (f : X →* Y)
-  : homology X E n →g homology Y F n :=
+  (g : E →ₛ F) (n : ℤ) : homology X E n →g homology Y F n :=
 pshomotopy_group_fun n (smash_prespectrum_fun f g)
 
 definition homology_theory_spectrum.{u} [constructor] (E : spectrum.{u}) : homology_theory.{u} :=

homotopy/smash.hlean

@@ -664,7 +664,7 @@ namespace smash
   (!smash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans) ⬝pv**
   smash_functor_pconst_pcompose (pid A) (pid A) g
 
-  /- these lemmas are use to show that smash_functor_right is natural in all arguments -/
+  /- Using these lemmas we show that smash_functor_right is natural in all arguments -/
   definition smash_functor_right_natural_right (f : C →* C') :
     psquare (smash_functor_right A B C) (smash_functor_right A B C')
             (ppcompose_left f) (ppcompose_left (pid A ∧→ f)) :=
@@ -926,8 +926,8 @@ namespace smash
       refine _ ⬝hp (!ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluer)⁻¹, exact hrfl },
   end
 
-  definition smash_flip_smash_functor (f : A →* C) (g : B →* D) : psquare
+  definition smash_flip_smash_functor (f : A →* C) (g : B →* D) :
-    (smash_flip A B) (smash_flip C D) (f ∧→ g) (g ∧→ f) :=
+    psquare (smash_flip A B) (smash_flip C D) (f ∧→ g) (g ∧→ f) :=
   begin
     apply phomotopy.mk (smash_flip_smash_functor' f g), refine !idp_con ⬝ _ ⬝ !idp_con⁻¹,
     refine !ap_ap011 ⬝ _, apply ap011_flip,

homotopy/spectrum.hlean

@@ -98,7 +98,7 @@ namespace spectrum
   | succ_str.of_nat zero   := z
   | succ_str.of_nat (succ k) := S (succ_str.of_nat k)
 
-  definition psp_of_gen_indexed [constructor] {N : succ_str} (z : N) (E : gen_prespectrum N) : gen_prespectrum +ℤ :=
+  definition psp_of_gen_indexed [constructor] {N : succ_str} (z : N) (E : gen_prespectrum N) : prespectrum :=
     psp_of_nat_indexed (gen_prespectrum.mk (λn, E (succ_str.of_nat z n)) (λn, gen_prespectrum.glue E (succ_str.of_nat z n)))
 
   definition is_spectrum_of_gen_indexed [instance] {N : succ_str} (z : N) (E : gen_prespectrum N) [H : is_spectrum E]
@@ -257,20 +257,26 @@ namespace spectrum
 
   /- homotopy group of a prespectrum -/
 
-  definition pshomotopy_group (n : ℤ) (E : prespectrum) : AbGroup :=
+  definition pshomotopy_group_hom (n : ℤ) (E : prespectrum) (k : ℕ)
-  group.seq_colim (λ(k : ℕ), πag[k+2] (E (-n - 2 + k)))
+    : πag[k + 2] (E (-n - 2 + k)) →g πag[k + 3] (E (-n - 2 + (k + 1))) :=
   begin
-    intro k,
+    refine _ ∘g π→g[k+2] (glue E _),
-    refine _ ∘ π→g[k+2] (glue E _),
+    refine (ghomotopy_group_succ_in _ (k+1))⁻¹ᵍ ∘g _,
-    refine (homotopy_group_succ_in _ (k+2))⁻¹ᵉ* ∘ _,
+    refine homotopy_group_isomorphism_of_pequiv (k+1)
-    refine homotopy_group_pequiv (k+2) (loop_pequiv_loop (pequiv_of_eq (ap E !add.assoc)))
+      (loop_pequiv_loop (pequiv_of_eq (ap E !add.assoc)))
   end
 
+  definition pshomotopy_group (n : ℤ) (E : prespectrum) : AbGroup :=
+  group.seq_colim (λ(k : ℕ), πag[k+2] (E (-n - 2 + k))) (pshomotopy_group_hom n E)
+
   notation `πₚₛ[`:95 n:0 `]`:0 := pshomotopy_group n
 
   definition pshomotopy_group_fun (n : ℤ) {E F : prespectrum} (f : E →ₛ F) :
     πₚₛ[n] E →g πₚₛ[n] F :=
-  sorry --group.seq_colim_functor _ _
+  group.seq_colim_functor (λk, π→g[k+2] (f (-n - 2 +[ℤ] k)))
+    begin
+      exact sorry
+    end
 
   notation `πₚₛ→[`:95 n:0 `]`:0 := pshomotopy_group_fun n