progress on spectrum and colim

algebra/product_group.hlean

@@ -8,7 +8,7 @@ Constructions with groups
 
 import algebra.group_theory hit.set_quotient types.list types.sum .subgroup .quotient_group
 
-open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function
+open eq algebra is_trunc set_quotient relation sigma prod prod.ops sum list trunc function
      equiv
 namespace group
 
@@ -79,4 +79,7 @@ namespace group
 
   infix ` ×≃g `:60 := group.product_isomorphism
 
+  definition product_group_mul_eq {G H : Group} (g h : G ×g H) : g * h = product_mul g h :=
+  idp
+
 end group

colim.hlean

@@ -251,7 +251,7 @@ namespace seq_colim
 
   definition pshift_equiv_pinclusion {A : ℕ → Type*} (f : Πn, A n →* A (succ n)) (n : ℕ) :
     psquare (pinclusion f n) (pinclusion (λn, f (n+1)) n) (f n) (pshift_equiv f)  :=
-  phomotopy.mk homotopy.rfl begin 
+  phomotopy.mk homotopy.rfl begin
     refine !idp_con ⬝ _, esimp,
     induction n with n IH,
     { esimp[inclusion_pt], esimp[shift_diag], exact !idp_con⁻¹ },
@@ -259,7 +259,7 @@ namespace seq_colim
       rewrite ap_con, rewrite ap_con,
       refine _ ⬝ whisker_right _ !con.assoc,
       refine _ ⬝ (con.assoc (_ ⬝ _) _ _)⁻¹,
-      xrewrite [-IH], 
+      xrewrite [-IH],
       esimp[shift_up], rewrite [elim_glue,  ap_inv, -ap_compose'], esimp,
       rewrite [-+con.assoc], apply whisker_right,
       rewrite con.assoc, apply !eq_inv_con_of_con_eq,
@@ -285,7 +285,6 @@ namespace seq_colim
   !elim_glue
 
   omit p
-
   definition is_equiv_seq_colim_functor [constructor] [H : Πn, is_equiv (@g n)]
      : is_equiv (seq_colim_functor @g p) :=
   adjointify _ (seq_colim_functor (λn, (@g _)⁻¹) (λn a, inv_commute' g f f' p a))
@@ -323,25 +322,34 @@ namespace seq_colim
     : Π(x : seq_colim f), P x :=
   by induction v with Pincl Pglue; exact seq_colim.rec f Pincl Pglue
 
-  definition pseq_colim_pequiv [constructor] {A A' : ℕ → Type*} {f : Π{n}, A n →* A (n+1)}
-    {f' : Π{n}, A' n →* A' (n+1)} (g : Π{n}, A n ≃* A' n)
-    (p : Π⦃n⦄, g ∘* f ~ f' ∘* g) : pseq_colim @f ≃* pseq_colim @f' :=
-  pequiv_of_equiv (seq_colim_equiv @g p) (ap (ι _) (respect_pt g))
+  definition pseq_colim_pequiv' [constructor] {A A' : ℕ → Type*} {f : Πn, A n →* A (n+1)}
+    {f' : Πn, A' n →* A' (n+1)} (g : Πn, A n ≃* A' n)
+    (p : Π⦃n⦄, g (n+1) ∘* f n ~ f' n ∘* g n) : pseq_colim @f ≃* pseq_colim @f' :=
+  pequiv_of_equiv (seq_colim_equiv g p) (ap (ι _) (respect_pt (g _)))
+
+  definition pseq_colim_pequiv [constructor] {A A' : ℕ → Type*} {f : Πn, A n →* A (n+1)}
+    {f' : Πn, A' n →* A' (n+1)} (g : Πn, A n ≃* A' n)
+    (p : Πn, g (n+1) ∘* f n ~* f' n ∘* g n) : pseq_colim @f ≃* pseq_colim @f' :=
+  pseq_colim_pequiv' g (λn, @p n)
 
   definition seq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Π⦃n⦄, A n → A (n+1)}
     (p : Π⦃n⦄ (a : A n), f a = f' a) : seq_colim f ≃ seq_colim f' :=
   seq_colim_equiv (λn, erfl) p
 
-  definition pseq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Π{n}, A n →* A (n+1)}
-    (p : Π⦃n⦄, f ~ f') : pseq_colim @f ≃* pseq_colim @f' :=
-  pseq_colim_pequiv (λn, pequiv.rfl) p
+  definition pseq_colim_equiv_constant' [constructor] {A : ℕ → Type*} {f f' : Πn, A n →* A (n+1)}
+    (p : Π⦃n⦄, f n ~ f' n) : pseq_colim @f ≃* pseq_colim @f' :=
+  pseq_colim_pequiv' (λn, pequiv.rfl) p
 
-  definition pseq_colim_pequiv_pinclusion {A A' : ℕ → Type*} {f : Π(n), A n →* A (n+1)}
-    {f' : Π(n), A' n →* A' (n+1)} (g : Π(n), A n ≃* A' n)
+  definition pseq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Πn, A n →* A (n+1)}
+    (p : Πn, f n ~* f' n) : pseq_colim @f ≃* pseq_colim @f' :=
+  pseq_colim_pequiv (λn, pequiv.rfl) (λn, !pid_pcompose ⬝* p n ⬝* !pcompose_pid⁻¹*)
+
+  definition pseq_colim_pequiv_pinclusion {A A' : ℕ → Type*} {f : Πn, A n →* A (n+1)}
+    {f' : Πn, A' n →* A' (n+1)} (g : Πn, A n ≃* A' n)
     (p : Π⦃n⦄, g (n+1) ∘* f n ~* f' n ∘* g n) (n : ℕ) :
     psquare (pinclusion f n) (pinclusion f' n) (g n) (pseq_colim_pequiv g p) :=
-  phomotopy.mk homotopy.rfl begin 
-    esimp, refine !idp_con ⬝ _, 
+  phomotopy.mk homotopy.rfl begin
+    esimp, refine !idp_con ⬝ _,
     induction n with n IH,
     { esimp[inclusion_pt], exact !idp_con⁻¹ },
     { esimp[inclusion_pt], rewrite [+ap_con, -+ap_inv, +con.assoc, +seq_colim_functor_glue],
@@ -360,8 +368,8 @@ namespace seq_colim
     }
   end
 
-  definition seq_colim_equiv_constant_pinclusion {A : ℕ → Type*} {f f' : Π⦃n⦄, A n →* A (n+1)}
-    (p : Π⦃n⦄ (a : A n), f a = f' a) (n : ℕ) :
+  definition seq_colim_equiv_constant_pinclusion {A : ℕ → Type*} {f f' : Πn, A n →* A (n+1)}
+    (p : Πn, f n ~* f' n) (n : ℕ) :
     pseq_colim_equiv_constant p ∘* pinclusion f n ~* pinclusion f' n  :=
   begin
     sorry

homotopy/spectrum.hlean

@@ -381,6 +381,10 @@ namespace spectrum
     spectrify_type_term X n k →* spectrify_type_term X n (k+1) :=
   spectrify_type_fun' X k (n +' k)
 
+  definition spectrify_type_fun_zero {N : succ_str} (X : gen_prespectrum N) (n : N) :
+    spectrify_type_fun X n 0 ~* glue X n :=
+  !pid_pcompose
+
   definition spectrify_type {N : succ_str} (X : gen_prespectrum N) (n : N) : Type* :=
   pseq_colim (spectrify_type_fun X n)
 
@@ -400,11 +404,11 @@ namespace spectrum
     transitivity pseq_colim (λk, spectrify_type_fun' X (succ k) (S n +' k)),
     fapply pseq_colim_pequiv,
     { intro n, apply loopn_pequiv_loopn, apply pequiv_ap X, apply succ_str.add_succ },
-    { intro k, apply to_homotopy,
+    { exact abstract begin intro k, apply to_homotopy,
       refine !passoc⁻¹* ⬝* _, refine pwhisker_right _ (loopn_succ_in_inv_natural (succ k) _) ⬝* _,
       refine !passoc ⬝* _ ⬝* !passoc⁻¹*, apply pwhisker_left,
       refine !apn_pcompose⁻¹* ⬝* _ ⬝* !apn_pcompose, apply apn_phomotopy,
-      exact !glue_ptransport⁻¹* },
+      exact !glue_ptransport⁻¹* end end },
     refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*,
     refine pseq_colim_equiv_constant (λn, !ap1_pcompose⁻¹*),
   end
@@ -429,10 +433,9 @@ namespace spectrum
     { intro n, apply phomotopy_of_psquare, refine !pid_pcompose⁻¹* ⬝ph* _,
       refine !pid_pcompose⁻¹* ⬝ph* _,
       --pshift_equiv_pinclusion (spectrify_type_fun X n) 0
-      refine _ ⬝v* _,
-      rotate 1, exact pshift_equiv_pinclusion (spectrify_type_fun X n) 0,
---      refine !passoc⁻¹* ⬝* pwhisker_left _ _ ⬝* _,
-      exact sorry
+      refine !passoc ⬝* pwhisker_left _ (pshift_equiv_pinclusion (spectrify_type_fun X n) 0) ⬝* _,
+      --refine !passoc ⬝* pwhisker_left _ _ ⬝* _,
+      --rotate 1, exact phomotopy_of_psquare !pseq_colim_pequiv_pinclusion
 }
   end