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

algebra/direct_sum.hlean

@@ -8,7 +8,7 @@ Constructions with groups
 
 import .quotient_group .free_commutative_group .product_group
 
-open eq is_equiv algebra is_trunc set_quotient relation sigma prod sum list trunc function equiv sigma.ops
+open eq is_equiv algebra is_trunc set_quotient relation sigma prod sum list trunc function equiv sigma.ops lift
 
 namespace group
 
@@ -118,7 +118,7 @@ namespace group
     }
   end
 
-  variables {I J : Set} {Y Y' Y'' : I → AbGroup}
+  variables {I J : Type} [is_set I] [is_set J] {Y Y' Y'' : I → AbGroup}
 
   definition dirsum_functor [constructor] (f : Πi, Y i →g Y' i) : dirsum Y →g dirsum Y' :=
   dirsum_elim (λi, dirsum_incl Y' i ∘g f i)
@@ -146,7 +146,7 @@ namespace group
     intro i y, exact sorry
   end
 
-  definition dirsum_functor_homotopy {f f' : Πi, Y i →g Y' i} (p : f ~2 f') :
+  definition dirsum_functor_homotopy (f f' : Πi, Y i →g Y' i) (p : f ~2 f') :
     dirsum_functor f ~ dirsum_functor f' :=
   begin
     apply dirsum_homotopy,
@@ -167,13 +167,13 @@ namespace group
     { 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 ⬝ _,
+      refine dirsum_functor_homotopy _ (λ 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,
+      refine dirsum_functor_homotopy _ (λ i, !gid) (λ i x,
         proof
           to_left_inv (equiv_of_isomorphism (f i)) x
         qed
@@ -183,3 +183,36 @@ namespace group
   end
 
 end group
+
+namespace group
+
+  definition dirsum_down_left.{u v} {I : Type.{u}} [is_set I] {Y : I → AbGroup}
+    : dirsum (Y ∘ down.{u v}) ≃g dirsum Y :=
+  let to_hom := @dirsum_functor_left _ _ _ _ Y down.{u v} in
+  let from_hom := dirsum_elim (λi, dirsum_incl (Y ∘ down) (up i)) in
+  begin
+    fapply isomorphism.mk,
+    { exact to_hom },
+    fapply adjointify,
+    { exact from_hom },
+    { intro ds,
+      refine (homomorphism_comp_compute to_hom from_hom ds)⁻¹ ⬝ _,
+      refine @dirsum_homotopy I _ Y (dirsum Y) (to_hom ∘g from_hom) !gid _ ds,
+      intro i y,
+      refine homomorphism_comp_compute to_hom from_hom _ ⬝ _,
+      refine ap to_hom (dirsum_elim_compute (λi, dirsum_incl (Y ∘ down) (up i)) i y) ⬝ _,
+      refine dirsum_elim_compute _ (up i) y ⬝ _,
+      reflexivity
+    },
+    { intro ds,
+      refine (homomorphism_comp_compute from_hom to_hom ds)⁻¹ ⬝ _,
+      refine @dirsum_homotopy _ _ (Y ∘ down) (dirsum (Y ∘ down)) (from_hom ∘g to_hom) !gid _ ds,
+      intro i y, induction i with i,
+      refine homomorphism_comp_compute from_hom to_hom _ ⬝ _,
+      refine ap from_hom (dirsum_elim_compute (λi, dirsum_incl Y (down i)) (up i) y) ⬝ _,
+      refine dirsum_elim_compute _ i y ⬝ _,
+      reflexivity
+    }
+  end
+
+end group

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,10 +112,21 @@ 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_is_exact.{u} (E : spectrum.{u}) (n : ℤ) {X Y : Type*} (f : X →* Y) :
+  is_exact_g (homology_functor f (sid (gen_spectrum.to_prespectrum E)) n)
+      (homology_functor (pcod f) (sid (gen_spectrum.to_prespectrum E)) n) :=
+begin
+  esimp[is_exact_g],
+  -- fconstructor,
+  -- { intro a, exact sorry },
+  -- { intro a, exact sorry }
+  exact sorry
+end
+
 definition homology_theory_spectrum.{u} [constructor] (E : spectrum.{u}) : homology_theory.{u} :=
 begin
   fapply homology_theory.mk,
@@ -125,7 +136,7 @@ begin
   exact sorry,
   exact sorry,
   exact sorry,
-  exact sorry,
+  apply homology_theory_spectrum_is_exact,
   exact sorry
   -- sorry
   -- sorry

homotopy/fwedge.hlean

@@ -7,7 +7,7 @@ The Wedge Sum of a family of Pointed Types
 -/
 import homotopy.wedge ..move_to_lib ..choice
 
-open eq pushout pointed unit trunc_index sigma bool equiv trunc choice unit is_trunc sigma.ops lift
+open eq is_equiv pushout pointed unit trunc_index sigma bool equiv trunc choice unit is_trunc sigma.ops lift function
 
 definition fwedge' {I : Type} (F : I → Type*) : Type := pushout (λi, ⟨i, Point (F i)⟩) (λi, ⋆)
 definition pt' [constructor] {I : Type} {F : I → Type*} : fwedge' F := inr ⋆
@@ -123,6 +123,15 @@ namespace fwedge
     { exact con.left_inv (respect_pt g) }
   end
 
+  definition fwedge_pmap_pinl [constructor] {I : Type} {F : I → Type*} : fwedge_pmap (λi, pinl i) ~* pid (⋁ F) :=
+  begin
+    fconstructor,
+    { intro x, induction x,
+        reflexivity, reflexivity,
+        apply eq_pathover, apply hdeg_square, refine !elim_glue ⬝ !ap_id⁻¹ },
+    { reflexivity }
+  end
+
   definition fwedge_pmap_equiv [constructor] {I : Type} (F : I → Type*) (X : Type*) :
     ⋁F →* X ≃ Πi, F i →* X :=
   begin
@@ -167,7 +176,7 @@ namespace fwedge
                                      ... ~* fwedge_pmap (λ i, !pid ∘* pinl i) : by exact fwedge_pmap_phomotopy (λ i, phomotopy.symm (pid_pcompose (pinl i)))
                                      ... ~* !pid : by exact fwedge_pmap_eta !pid
 
-  definition fwedge_functor_compose {I : Type} {F F' F'' : I → Type*} (g : Π i, F' i →* F'' i)
+  definition fwedge_functor_pcompose {I : Type} {F F' F'' : I → Type*} (g : Π i, F' i →* F'' i)
     (f : Π i, F i →* F' i) : fwedge_functor (λ i, g i ∘* f i) ~* fwedge_functor g ∘* fwedge_functor f :=
   calc        fwedge_functor (λ i, g i ∘* f i)
            ~* fwedge_pmap (λ i, (pinl i ∘* g i) ∘* f i)
@@ -183,7 +192,7 @@ namespace fwedge
        ... ~* fwedge_functor g ∘* fwedge_functor f
               : by exact fwedge_pmap_eta (fwedge_functor g ∘* fwedge_functor f)
 
-  definition fwedge_functor_homotopy {I : Type} {F F' : I → Type*} {f g : Π i, F i →* F' i}
+  definition fwedge_functor_phomotopy {I : Type} {F F' : I → Type*} {f g : Π i, F i →* F' i}
     (h : Π i, f i ~* g i) : fwedge_functor f ~* fwedge_functor g :=
     fwedge_pmap_phomotopy (λ i, pwhisker_left (pinl i) (h i))
 
@@ -192,19 +201,45 @@ namespace fwedge
   let pfrom := fwedge_functor (λ i, (f i)⁻¹ᵉ*) in
   begin
     fapply pequiv_of_pmap, exact pto,
-    fapply is_equiv.adjointify, exact pfrom,
+    fapply adjointify, exact pfrom,
-    { intro y, refine (fwedge_functor_compose (λ i, f i) (λ i, (f i)⁻¹ᵉ*) y)⁻¹ ⬝ _,
+    { intro y, refine (fwedge_functor_pcompose (λ i, f i) (λ i, (f i)⁻¹ᵉ*) y)⁻¹ ⬝ _,
-      refine fwedge_functor_homotopy (λ i, pright_inv (f i)) y ⬝ _,
+      refine fwedge_functor_phomotopy (λ i, pright_inv (f i)) y ⬝ _,
       exact fwedge_functor_pid y
     },
-    { intro y, refine (fwedge_functor_compose (λ i, (f i)⁻¹ᵉ*) (λ i, f i) y)⁻¹ ⬝ _,
+    { intro y, refine (fwedge_functor_pcompose (λ i, (f i)⁻¹ᵉ*) (λ i, f i) y)⁻¹ ⬝ _,
-      refine fwedge_functor_homotopy (λ i, pleft_inv (f i)) y ⬝ _,
+      refine fwedge_functor_phomotopy (λ i, pleft_inv (f i)) y ⬝ _,
       exact fwedge_functor_pid y
     }
   end
 
-  definition plift_fwedge.{u v} {I : Type} {F : I → pType.{u}} : plift.{u v} (⋁ F) ≃* ⋁ (λ i, plift.{u v} (F i)) :=
+  definition plift_fwedge.{u v} {I : Type} (F : I → pType.{u}) : plift.{u v} (⋁ F) ≃* ⋁ (plift.{u v} ∘ F) :=
   calc plift.{u v} (⋁ F) ≃* ⋁ F : by exact !pequiv_plift ⁻¹ᵉ*
-                      ... ≃* ⋁ (λ i, plift.{u v} (F i)) : by exact fwedge_pequiv (λ i, !pequiv_plift)
+                     ... ≃* ⋁ (λ i, plift.{u v} (F i)) : by exact fwedge_pequiv (λ i, !pequiv_plift)
+
+  definition fwedge_down_left.{u v} {I : Type} (F : I → pType) : ⋁ (F ∘ down.{u v}) ≃* ⋁ F :=
+  let pto := @fwedge_pmap (lift.{u v} I) (F ∘ down) (⋁ F) (λ i, pinl (down i)) in
+  let pfrom := @fwedge_pmap I F (⋁ (F ∘ down.{u v})) (λ i, pinl (up.{u v} i)) in
+  begin
+    fapply pequiv_of_pmap,
+    { exact pto },
+    fapply adjointify,
+    { exact pfrom },
+    { intro x, exact calc pto (pfrom x) = fwedge_pmap (λ i, (pto ∘* pfrom) ∘* pinl i) x : by exact (fwedge_pmap_eta (pto ∘* pfrom) x)⁻¹
+                                    ... = fwedge_pmap (λ i, pto ∘* (pfrom ∘* pinl i)) x : by exact fwedge_pmap_phomotopy (λ i, passoc pto pfrom (pinl i)) x
+                                    ... = fwedge_pmap (λ i, pto ∘* pinl (up.{u v} i)) x : by exact fwedge_pmap_phomotopy (λ i, pwhisker_left pto (fwedge_pmap_beta (λ i, pinl (up.{u v} i)) i)) x
+                                    ... = fwedge_pmap pinl x : by exact fwedge_pmap_phomotopy (λ i, fwedge_pmap_beta (λ i, (pinl (down.{u v} i))) (up.{u v} i)) x
+                                    ... = x : by exact fwedge_pmap_pinl x
+    },
+    { intro x, exact calc pfrom (pto x) = fwedge_pmap (λ i, (pfrom ∘* pto) ∘* pinl i) x : by exact (fwedge_pmap_eta (pfrom ∘* pto) x)⁻¹
+                                    ... = fwedge_pmap (λ i, pfrom ∘* (pto ∘* pinl i)) x : by exact fwedge_pmap_phomotopy (λ i, passoc pfrom pto (pinl i)) x
+                                    ... = fwedge_pmap (λ i, pfrom ∘* pinl (down.{u v} i)) x : by exact fwedge_pmap_phomotopy (λ i, pwhisker_left pfrom (fwedge_pmap_beta (λ i, pinl (down.{u v} i)) i)) x
+                                    ... = fwedge_pmap pinl x : by exact fwedge_pmap_phomotopy (λ i,
+                                            begin induction i with i,
+                                              exact fwedge_pmap_beta (λ i, (pinl (up.{u v} i))) i
+                                            end
+                                          ) x
+                                    ... = x : by exact fwedge_pmap_pinl x
+    }
+  end
 
 end fwedge

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

@@ -5,7 +5,7 @@ Authors: Michael Shulman, Floris van Doorn
 
 -/
 
-import homotopy.LES_of_homotopy_groups .splice ..colim types.pointed2 .EM ..pointed_pi .smash_adjoint ..algebra.seq_colim
+import homotopy.LES_of_homotopy_groups .splice ..colim types.pointed2 .EM ..pointed_pi .smash_adjoint ..algebra.seq_colim .fwedge
 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 function
 
@@ -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]
@@ -277,20 +277,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
 
@@ -607,5 +613,17 @@ spectrify_fun (smash_prespectrum_fun f g)
   definition EM_spectrum /-[constructor]-/ (G : AbGroup) : spectrum :=
   spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*)
 
+  /- Wedge of prespectra -/
+
+open fwedge
+
+  definition fwedge_prespectrum.{u v} {I : Type.{v}} (X : I -> prespectrum.{u}) : prespectrum.{max u v} :=
+  begin
+    fconstructor,
+    { intro n, exact fwedge (λ i, X i n) },
+    { intro n, fapply fwedge_pmap,
+      intro i, exact Ω→ !pinl ∘* !glue 
+  }
+  end
 
 end spectrum