From b2ab29c3c3b6abeb40e367493a9fa89f74916bd4 Mon Sep 17 00:00:00 2001
From: spiceghello <stefano.piceghello@uib.no>
Date: Thu, 8 Jun 2017 18:28:15 -0600
Subject: [PATCH] on colim.elim o pinclusion, and corollary on spectra

---
 colim.hlean             | 36 ++++++++++++++++++++++++++++++----
 homotopy/spectrum.hlean | 43 +++++++++++++++++++++++++++--------------
 2 files changed, 60 insertions(+), 19 deletions(-)

diff --git a/colim.hlean b/colim.hlean
index 7619b49..57daa6b 100644
--- a/colim.hlean
+++ b/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)}
-    (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f ~ g n) : pseq_colim @f →* B :=
+  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 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)}
-    (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f ~* g n) : pseq_colim @f →* B :=
+  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 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
diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index 96ea66e..2565806 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -477,28 +477,41 @@ namespace spectrum
     }
   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 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 spectrify.elim_n f n },
     { 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)