Merge branch 'master' of github.com:fpvandoorn/Spectral

algebra/direct_sum.hlean

@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Copyright (c) 2015 Floris van Doorn, Egbert Rijke, Favonia. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn, Egbert Rijke
+Authors: Floris van Doorn, Egbert Rijke, Favonia
 
 Constructions with groups
 -/
@@ -124,7 +124,7 @@ namespace group
   dirsum_elim (λi, dirsum_incl Y' i ∘g f i)
 
   theorem dirsum_functor_compose (f' : Πi, Y' i →g Y'' i) (f : Πi, Y i →g Y' i) :
-    dirsum_functor f' ∘a dirsum_functor f ~ dirsum_functor (λi, f' i ∘a f i) :=
+    dirsum_functor f' ∘g dirsum_functor f ~ dirsum_functor (λi, f' i ∘g f i) :=
   begin
     apply dirsum_homotopy,
     intro i y, reflexivity,
@@ -156,4 +156,30 @@ namespace group
   definition dirsum_functor_left [constructor] (f : J → I) : dirsum (Y ∘ f) →g dirsum Y :=
   dirsum_elim (λj, dirsum_incl Y (f j))
 
+  definition dirsum_isomorphism [constructor] (f : Πi, Y i ≃g Y' i) : dirsum Y ≃g dirsum Y' :=
+  let to_hom := dirsum_functor (λ i, f i) in
+  let from_hom := dirsum_functor (λ i, (f i)⁻¹ᵍ) in
+  begin
+    fapply isomorphism.mk,
+    exact dirsum_functor (λ i, f i),
+    fapply is_equiv.adjointify,
+    exact dirsum_functor (λ i, (f i)⁻¹ᵍ),
+    { intro ds,
+      refine (homomorphism_comp_compute (dirsum_functor (λ i, f i)) (dirsum_functor (λ i, (f i)⁻¹ᵍ)) _)⁻¹ ⬝ _,
+      refine dirsum_functor_compose (λ i, f i) (λ i, (f i)⁻¹ᵍ) ds ⬝ _,
+      refine @dirsum_functor_homotopy I Y' Y' _ (λ i, !gid) (λ i, to_right_inv (equiv_of_isomorphism (f i))) ds ⬝ _,
+      exact !dirsum_functor_gid
+    },
+    { intro ds,
+      refine (homomorphism_comp_compute (dirsum_functor (λ i, (f i)⁻¹ᵍ)) (dirsum_functor (λ i, f i)) _)⁻¹ ⬝ _,
+      refine dirsum_functor_compose (λ i, (f i)⁻¹ᵍ) (λ i, f i) ds ⬝ _,
+      refine @dirsum_functor_homotopy I Y Y _ (λ i, !gid) (λ i x,
+        proof
+          to_left_inv (equiv_of_isomorphism (f i)) x
+        qed
+      ) ds ⬝ _,
+      exact !dirsum_functor_gid
+    }
+  end
+
 end group

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 !homomorphism_comp_compute ⬝ _,
-     refine gqg_eq_of_rel _ _ ⬝ (!grp_comp_comp)⁻¹,
+     refine gqg_eq_of_rel _ _ ⬝ (!homomorphism_comp_compute)⁻¹,
-     exact tr (seq_colim_rel.rmk _ _) 
+     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) := 
+      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⁻¹
+        λ 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

colim.hlean

@@ -399,8 +399,8 @@ namespace seq_colim
   equiv.mk _ !is_equiv_seq_colim_rec
   end functor
 
-  definition pseq_colim.elim' [constructor] {A : ℕ → Type*} {B : Type*} {f : Π{n}, A n →* A (n+1)}
+  definition pseq_colim.elim' [constructor] {A : ℕ → Type*} {B : Type*} {f : Πn, A n →* A (n+1)}
-    (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f ~ g n) : pseq_colim @f →* B :=
+    (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f n ~ g n) : pseq_colim f →* B :=
   begin
     fapply pmap.mk,
     { intro x, induction x with n a n a,
@@ -409,10 +409,38 @@ namespace seq_colim
     { esimp, apply respect_pt }
   end
 
-  definition pseq_colim.elim [constructor] {A : ℕ → Type*} {B : Type*} {f : Π{n}, A n →* A (n+1)}
+  definition pseq_colim.elim [constructor] {A : ℕ → Type*} {B : Type*} {f : Πn, A n →* A (n+1)}
-    (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f ~* g n) : pseq_colim @f →* B :=
+    (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f n ~* g n) : pseq_colim @f →* B :=
   pseq_colim.elim' g p
 
+  definition pseq_colim.elim_pinclusion {A : ℕ → Type*} {B : Type*} {f : Πn, A n →* A (n+1)}
+    (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f n ~* g n) (n : ℕ) :
+  pseq_colim.elim g p ∘* pinclusion f n ~* g n :=
+  begin
+    refine phomotopy.mk phomotopy.rfl _,
+    refine !idp_con ⬝ _,
+    esimp,
+    induction n with n IH,
+    { esimp, esimp[inclusion_pt], exact !idp_con⁻¹ },
+    { esimp, esimp[inclusion_pt],
+      rewrite ap_con, rewrite ap_con,
+      rewrite elim_glue,
+      rewrite [-ap_inv],
+      rewrite [-ap_compose'], esimp,
+      rewrite [(eq_con_inv_of_con_eq (!to_homotopy_pt))],
+      rewrite [IH],
+      rewrite [con_inv],
+      rewrite [-+con.assoc],
+      refine _ ⬝ whisker_right _ !con.assoc⁻¹,
+      rewrite [con.left_inv], esimp,
+      refine _ ⬝ !con.assoc⁻¹,
+      rewrite [con.left_inv], esimp,
+      rewrite [ap_inv],
+      rewrite [-con.assoc],
+      refine !idp_con⁻¹ ⬝ whisker_right _ !con.left_inv⁻¹,
+    }
+  end
+
   definition prep0 [constructor] {A : ℕ → Type*} (f : pseq_diagram A) (k : ℕ) : A 0 →* A k :=
   pmap.mk (rep0 (λn x, f x) k)
           begin induction k with k p, reflexivity, exact ap (@f k) p ⬝ !respect_pt end

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 -/
+/- homology theory associated to a prespectrum -/
-definition homology (X : Type*) (E : spectrum) (n : ℤ) : AbGroup :=
+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 :=
+definition homology_functor [constructor] {X Y : Type*} {E F : spectrum} (f : X →* Y) (g : E →ₛ F) (n : ℤ)
-shomotopy_group_fun n (smash_spectrum_fun f g)
+  : 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
@@ -235,6 +235,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
   -------------------------------/
@@ -409,7 +428,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
 
@@ -460,34 +479,47 @@ 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⁻¹*
     }
   end
 
+  definition spectrify.elim_n {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N}
+    (f : X →ₛ Y) (n : N) : (spectrify X) n →* Y n :=
+  begin
+    fapply pseq_colim.elim,
+    { intro k, refine !equiv_gluen⁻¹ᵉ* ∘* apn k (f (n +' k)) },
+    { intro k, refine !passoc ⬝* pwhisker_right _ !equiv_gluen_inv_succ ⬝* _,
+      refine !passoc ⬝* _, apply pwhisker_left,
+      refine !passoc ⬝* _,
+      refine pwhisker_left _ ((passoc _ _ (_ ∘* _))⁻¹*) ⬝* _,
+      refine pwhisker_left _ !passoc⁻¹* ⬝* _,
+      refine pwhisker_left _ (pwhisker_right _ (phomotopy_pinv_right_of_phomotopy (!loopn_succ_in_natural)⁻¹*)⁻¹*) ⬝* _,
+      refine pwhisker_right _ !apn_pinv ⬝* _,
+      refine (phomotopy_pinv_left_of_phomotopy _)⁻¹*,
+      refine pwhisker_right _ !pmap_eta⁻¹* ⬝* _,
+      refine apn_psquare k _,
+      refine pwhisker_right _ _  ⬝* psquare_of_phomotopy !smap.glue_square,
+      exact !pmap_eta⁻¹*
+    }
+  end
+
   definition spectrify.elim {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N}
     (f : X →ₛ Y) : spectrify X →ₛ Y :=
   begin
     fapply smap.mk,
-    { intro n, fapply pseq_colim.elim,
+    { intro n, exact spectrify.elim_n f n },
-      { intro k, refine !equiv_gluen⁻¹ᵉ* ∘* apn k (f (n +' k)) },
-      { intro k, refine !passoc ⬝* pwhisker_right _ !equiv_gluen_inv_succ ⬝* _,
-        refine !passoc ⬝* _, apply pwhisker_left,
-        refine !passoc ⬝* _,
-        refine pwhisker_left _ ((passoc _ _ (_ ∘* _))⁻¹*) ⬝* _,
-        refine pwhisker_left _ !passoc⁻¹* ⬝* _,
-        refine pwhisker_left _ (pwhisker_right _ (phomotopy_pinv_right_of_phomotopy (!loopn_succ_in_natural)⁻¹*)⁻¹*) ⬝* _,
-        refine pwhisker_right _ !apn_pinv ⬝* _,
-        refine (phomotopy_pinv_left_of_phomotopy _)⁻¹*,
-        refine pwhisker_right _ !pmap_eta⁻¹* ⬝* _,
-        refine apn_psquare k _,
-        refine pwhisker_right _ _  ⬝* psquare_of_phomotopy !smap.glue_square,
-        exact !pmap_eta⁻¹*
-      }},
     { intro n, exact sorry }
   end
 
+  definition phomotopy_spectrify.elim {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N}
+    (f : X →ₛ Y) (n : N) : spectrify.elim_n f n ∘* spectrify_map n ~* f n :=
+  begin
+    refine pseq_colim.elim_pinclusion _ _ 0 ⬝* _,
+    exact !pid_pcompose
+  end
+
   definition spectrify_fun {N : succ_str} {X Y : gen_prespectrum N} (f : X →ₛ Y) : spectrify X →ₛ spectrify Y :=
   spectrify.elim ((@spectrify_map _ Y) ∘ₛ f)