work on homotopy group of prespectrum

algebra/seq_colim.hlean

@@ -6,7 +6,7 @@ namespace group
 
   section
 
-    parameters (A : @trunctype.mk 0 ℕ _ → AbGroup) (f : Πi , A i → A (i + 1))
+    parameters (A : ℕ → AbGroup) (f : Πi , A i → A (i + 1))
     variables {A' : AbGroup}
 
     definition seq_colim_carrier : AbGroup := dirsum A
@@ -15,17 +15,18 @@ namespace group
 
     definition seq_colim : AbGroup := quotient_ab_group_gen seq_colim_carrier (λa, ∥seq_colim_rel a∥)
 
+    parameters {A f}
     definition seq_colim_incl [constructor] (i : ℕ) : A i →g seq_colim :=
       gqg_map _ _ ∘g dirsum_incl A i
 
     definition seq_colim_quotient (h : Πi, A i →g A') (k : Πi a, h i a = h (succ i) (f i a))
                                   (v : seq_colim_carrier) (r : ∥seq_colim_rel v∥) : dirsum_elim h v = 1 :=
       begin
-        induction r with r, induction r, 
+        induction r with r, induction r,
         refine !to_respect_mul ⬝ _,
-        refine ap (λγ, group_fun (dirsum_elim h) (group_fun (dirsum_incl A i) a) * group_fun (dirsum_elim h) γ) 
+        refine ap (λγ, group_fun (dirsum_elim h) (group_fun (dirsum_incl A i) a) * group_fun (dirsum_elim h) γ)
                   (!to_respect_inv)⁻¹ ⬝ _,
-        refine ap (λγ, γ * group_fun (dirsum_elim h) (group_fun (dirsum_incl A (succ i)) (f i a)⁻¹)) 
+        refine ap (λγ, γ * group_fun (dirsum_elim h) (group_fun (dirsum_incl A (succ i)) (f i a)⁻¹))
                   !dirsum_elim_compute ⬝ _,
         refine ap (λγ, (h i a) * γ) !dirsum_elim_compute ⬝ _,
         refine ap (λγ, γ * group_fun (h (succ i)) (f i a)⁻¹) !k ⬝ _,
@@ -38,7 +39,7 @@ namespace group
       gqg_elim _ (dirsum_elim h) (seq_colim_quotient h k)
 
     definition seq_colim_compute (h : Πi, A i →g A')
-                                 (k : Πi a, h i a = h (succ i) (f i a)) (i : ℕ) (a : A i) : 
+                                 (k : Πi a, h i a = h (succ i) (f i a)) (i : ℕ) (a : A i) :
                (seq_colim_elim h k) (seq_colim_incl i a) = h i a :=
       begin
         refine gqg_elim_compute (λa, ∥seq_colim_rel a∥) (dirsum_elim h) (seq_colim_quotient h k) (dirsum_incl A i a) ⬝ _,
@@ -47,17 +48,17 @@ namespace group
 
     definition seq_colim_glue {i : @trunctype.mk 0 ℕ _} {a : A i} : seq_colim_incl i a = seq_colim_incl (succ i) (f i a) :=
    begin
-     refine !grp_comp_comp ⬝ _,
-     refine gqg_eq_of_rel _ _ ⬝ (!grp_comp_comp)⁻¹,
-     exact tr (seq_colim_rel.rmk _ _) 
+     refine !homomorphism_comp_compute ⬝ _,
+     refine gqg_eq_of_rel _ _ ⬝ (!homomorphism_comp_compute)⁻¹,
+     exact tr (seq_colim_rel.rmk _ _)
    end
 
     section
       local abbreviation h (m : seq_colim →g A') : Πi, A i →g A' := λi, m ∘g (seq_colim_incl i)
-      local abbreviation k (m : seq_colim →g A') : Πi a, h m i a = h m (succ i) (f i a) := 
-        λ i a, !grp_comp_comp ⬝ ap m (@seq_colim_glue i a) ⬝ !grp_comp_comp⁻¹
+      local abbreviation k (m : seq_colim →g A') : Πi a, h m i a = h m (succ i) (f i a) :=
+        λ i a, !homomorphism_comp_compute ⬝ ap m (@seq_colim_glue i a) ⬝ !homomorphism_comp_compute⁻¹
 
-      definition seq_colim_unique (m : seq_colim →g A') : 
+      definition seq_colim_unique (m : seq_colim →g A') :
         Πv, seq_colim_elim (h m) (k m) v = m v :=
       begin
         intro v, refine (gqg_elim_unique _ (dirsum_elim (h m)) _ m _ _)⁻¹ ⬝ _,
@@ -69,4 +70,10 @@ namespace group
 
   end
 
+  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' :=
+  sorry --_ ∘g _
+
+
 end group

homology/homology.hlean

@@ -14,7 +14,6 @@ open eq spectrum int pointed group algebra sphere nat equiv susp is_trunc
 namespace homology
 
   /- homology theory -/
-
   structure homology_theory.{u} : Type.{u+1} :=
     (HH : ℤ → pType.{u} → AbGroup.{u})
     (Hh : Π(n : ℤ) {X Y : Type*} (f : X →* Y), HH n X →g HH n Y)
@@ -89,8 +88,12 @@ namespace homology
 
   end
 
-/- homology theory associated to a spectrum -/
-definition homology (X : Type*) (E : spectrum) (n : ℤ) : AbGroup :=
+/- homology theory associated to a prespectrum -/
+definition homology (X : Type*) (E : prespectrum) (n : ℤ) : AbGroup :=
+pshomotopy_group n (smash_prespectrum X E)
+
+/- an alternative definition, which might be a bit harder to work with -/
+definition homology_spectrum (X : Type*) (E : spectrum) (n : ℤ) : AbGroup :=
 shomotopy_group n (smash_spectrum X E)
 
 definition parametrized_homology {X : Type*} (E : X → spectrum) (n : ℤ) : AbGroup :=
@@ -109,12 +112,13 @@ 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 : ℤ) : homology X E n →g homology Y F n :=
-shomotopy_group_fun n (smash_spectrum_fun f g)
+definition homology_functor [constructor] {X Y : Type*} {E F : spectrum} (f : X →* Y) (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} :=
 begin
-  refine homology_theory.mk _ _ _ _ _ _ _ _,
+  fapply homology_theory.mk,
   exact (λn X, H_ n[X, E]),
   exact (λn X Y f, homology_functor f (sid E) n),
   exact sorry, -- Hid is uninteresting but potentially very hard to prove

homotopy/spectrum.hlean

@@ -5,9 +5,9 @@ Authors: Michael Shulman, Floris van Doorn
 
 -/
 
-import homotopy.LES_of_homotopy_groups .splice ..colim types.pointed2 .EM ..pointed_pi .smash_adjoint
+import homotopy.LES_of_homotopy_groups .splice ..colim types.pointed2 .EM ..pointed_pi .smash_adjoint ..algebra.seq_colim
 open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
-     seq_colim succ_str EM EM.ops
+     seq_colim succ_str EM EM.ops function
 
 /---------------------
   Basic definitions
@@ -227,6 +227,25 @@ namespace spectrum
 
   notation `πₛ→[`:95 n:0 `]`:0 := shomotopy_group_fun n
 
+  /- homotopy group of a prespectrum -/
+
+  definition pshomotopy_group (n : ℤ) (E : prespectrum) : AbGroup :=
+  group.seq_colim (λ(k : ℕ), πag[k+2] (E (-n - 2 + k)))
+  begin
+    intro k,
+    refine _ ∘ π→g[k+2] (glue E _),
+    refine (homotopy_group_succ_in _ (k+2))⁻¹ᵉ* ∘ _,
+    refine homotopy_group_pequiv (k+2) (loop_pequiv_loop (pequiv_of_eq (ap E !add.assoc)))
+  end
+
+  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 _ _
+
+  notation `πₚₛ→[`:95 n:0 `]`:0 := pshomotopy_group_fun n
+
   /-------------------------------
     Cotensor of spectra by types
   -------------------------------/
@@ -401,7 +420,7 @@ namespace spectrum
     spectrify_type_fun' X n (succ k) ~* Ω→ (spectrify_type_fun' X n k) :=
   begin
     refine _ ⬝* !ap1_pcompose⁻¹*,
-    apply !pwhisker_right, 
+    apply !pwhisker_right,
     refine !to_pinv_pequiv_MK2
   end
 
@@ -452,7 +471,7 @@ namespace spectrum
       refine _ ◾* (spectrify_type_fun_zero X n ⬝* !pid_pcompose⁻¹*),
       refine !passoc ⬝* pwhisker_left _ !pseq_colim_pequiv_pinclusion ⬝* _,
       refine pwhisker_left _ (pwhisker_left _ (ap1_pid) ⬝* !pcompose_pid) ⬝* _,
-      refine !passoc ⬝* pwhisker_left _ !seq_colim_equiv_constant_pinclusion ⬝* _, 
+      refine !passoc ⬝* pwhisker_left _ !seq_colim_equiv_constant_pinclusion ⬝* _,
       apply pinv_left_phomotopy_of_phomotopy,
       exact !pseq_colim_loop_pinclusion⁻¹*
     }