progress on spectrify

colim.hlean

@@ -1,6 +1,6 @@
 -- authors: Floris van Doorn, Egbert Rijke
 
-import hit.colimit types.fin homotopy.chain_complex .move_to_lib
+import hit.colimit types.fin homotopy.chain_complex types.pointed2
 open seq_colim pointed algebra eq is_trunc nat is_equiv equiv sigma sigma.ops chain_complex
 
 namespace seq_colim
@@ -8,7 +8,7 @@ namespace seq_colim
   definition pseq_colim [constructor] {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) : Type* :=
   pointed.MK (seq_colim f) (@sι _ _ 0 pt)
 
-  definition inclusion_pt [constructor] {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ)
+  definition inclusion_pt {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ)
     : inclusion f (Point (X n)) = Point (pseq_colim f) :=
   begin
     induction n with n p,
@@ -249,6 +249,10 @@ namespace seq_colim
     { exact ap (ι _) !respect_pt }
   end
 
+  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 refine !idp_con ⬝ _, esimp, exact sorry end
+
   section functor
   variable {f}
   variables {A' : ℕ → Type} {f' : seq_diagram A'}
@@ -305,6 +309,30 @@ 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 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_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) :=
+  sorry
+
+  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 : ℕ) :
+    pseq_colim_equiv_constant p ∘* pinclusion f n ~* pinclusion f' n  :=
+  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)),
@@ -327,19 +355,6 @@ namespace seq_colim
   equiv.mk _ !is_equiv_seq_colim_rec
   end functor
 
-  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 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.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 :=
   begin
@@ -361,6 +376,7 @@ namespace seq_colim
   theorem prep0_succ_lemma {A : ℕ → Type*} (f : pseq_diagram A) (n : ℕ)
     (p : rep0 (λn x, f x) n pt = rep0 (λn x, f x) n pt)
     (q : prep0 f n (Point (A 0)) = Point (A n))
+
     : loop_equiv_eq_closed (ap (@f n) q ⬝ respect_pt (@f n))
     (ap (@f n) p) = Ω→(@f n) (loop_equiv_eq_closed q p) :=
   by rewrite [▸*, con_inv, ↑ap1_gen, +ap_con, ap_inv, +con.assoc]
@@ -466,6 +482,10 @@ namespace seq_colim
     { exact sorry }
   end
 
+  definition pseq_colim_loop_pinclusion {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ) :
+    pseq_colim_loop f ∘* Ω→ (pinclusion f n) ~* pinclusion (λn, Ω→(f n)) n :=
+  sorry
+
   -- open succ_str
   -- definition pseq_colim_succ_str_change_index' {N : succ_str} {B : N → Type*} (n : N) (m : ℕ)
   --   (h : Πn, B n →* B (S n)) :

homotopy/spectrum.hlean

@@ -396,8 +396,8 @@ namespace spectrum
   definition spectrify_pequiv {N : succ_str} (X : gen_prespectrum N) (n : N) :
     spectrify_type X n ≃* Ω (spectrify_type X (S n)) :=
   begin
-    refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*,
     refine !pshift_equiv ⬝e* _,
+    refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*,
     transitivity pseq_colim (λk, spectrify_type_fun' X (succ k) (S n +' k)), rotate 1,
     refine pseq_colim_equiv_constant (λn, !ap1_pcompose⁻¹*),
     fapply pseq_colim_pequiv,
@@ -426,7 +426,13 @@ namespace spectrum
   begin
     fapply smap.mk,
     { intro n, exact pinclusion _ 0 },
-    { intro n, exact sorry }
+    { 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,
+      exact sorry
+}
   end
 
   definition spectrify.elim {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N}