continue on spectrification

colim.hlean

@@ -8,6 +8,14 @@ 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 : ℕ)
+    : inclusion f (Point (X n)) = Point (pseq_colim f) :=
+  by induction n with n p; reflexivity; exact (ap (sι f) !respect_pt)⁻¹ ⬝ !glue ⬝ p
+
+  definition pinclusion [constructor] {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ)
+    : X n →* pseq_colim f :=
+  pmap.mk (inclusion f) (inclusion_pt f n)
+
   -- TODO: we need to prove this
   definition pseq_colim_loop {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) :
     Ω (pseq_colim f) ≃* pseq_colim (λn, Ω→(f n)) :=

homotopy/smash.hlean

@@ -203,6 +203,7 @@ namespace smash
     { exact gluel' pt a ⬝ ap (smash.mk a) loop ⬝ gluel' a pt },
   end
 
+exit -- the definitions below compile, but take a long time to do so and have sorry's in them
   definition smash_pcircle_of_psusp_of_smash_pcircle_pt [unfold 3] (a : A) (x : S¹*) :
     smash_pcircle_of_psusp (psusp_of_smash_pcircle (smash.mk a x)) = smash.mk a x :=
   begin
@@ -232,7 +233,6 @@ namespace smash
     { apply square_of_eq, exact whisker_right !con.right_inv _ },
     { apply square_pathover', exact sorry }
   end
-exit
 
   definition smash_pcircle_pequiv [constructor] (A : Type*) : smash A S¹* ≃* psusp A :=
   begin

homotopy/spectrum.hlean

@@ -50,6 +50,11 @@ namespace spectrum
   definition equiv_glue {N : succ_str} (E : gen_prespectrum N) [H : is_spectrum E] (n:N) : (E n) ≃* (Ω (E (S n))) :=
     pequiv_of_pmap (glue E n) (is_spectrum.is_equiv_glue E n)
 
+  -- a square when we compose glue with transporting over a path in N
+  definition glue_ptransport {N : succ_str} (X : gen_prespectrum N) {n n' : N} (p : n = n') :
+    glue X n' ∘* ptransport X p ~* Ω→ (ptransport X (ap S p)) ∘* glue X n :=
+  by induction p; exact !pcompose_pid ⬝* !pid_pcompose⁻¹* ⬝* pwhisker_right _ !ap1_pid⁻¹*
+
   -- Sometimes an ℕ-indexed version does arise naturally, however, so
   -- we give a standard way to extend an ℕ-indexed (pre)spectrum to a
   -- ℤ-indexed one.
@@ -151,12 +156,20 @@ namespace spectrum
 
   infixr ` ∘ₛ `:60 := scompose
 
-  definition szero {N : succ_str} (E F : gen_prespectrum N) : E →ₛ F :=
+  definition szero [constructor] {N : succ_str} (E F : gen_prespectrum N) : E →ₛ F :=
     smap.mk (λn, pconst (E n) (F n))
       (λn, calc glue F n ∘* pconst (E n) (F n) ~* pconst (E n) (Ω(F (S n)))                    : pcompose_pconst
                                          ...   ~* pconst (Ω(E (S n))) (Ω(F (S n))) ∘* glue E n : pconst_pcompose
                                          ...   ~* Ω→(pconst (E (S n)) (F (S n))) ∘* glue E n   : pwhisker_right (glue E n) (ap1_pconst _ _))
 
+  definition stransport [constructor] {N : succ_str} {A : Type} {a a' : A} (p : a = a')
+  (E : A → gen_prespectrum N) : E a →ₛ E a' :=
+  smap.mk (λn, ptransport (λa, E a n) p)
+          begin
+            intro n, induction p,
+            exact !pcompose_pid ⬝* !pid_pcompose⁻¹* ⬝* pwhisker_right _ !ap1_pid⁻¹*,
+          end
+
   structure shomotopy {N : succ_str} {E F : gen_prespectrum N} (f g : E →ₛ F) :=
     (to_phomotopy : Πn, f n ~* g n)
     (glue_homotopy : Πn, pwhisker_left (glue F n) (to_phomotopy n) ⬝* glue_square g n
@@ -378,15 +391,15 @@ namespace spectrum
   begin
     refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*,
     refine !pshift_equiv ⬝e* _,
-    refine _ ⬝e* pseq_colim_equiv_constant (λn, !ap1_pcompose⁻¹*),
-    transitivity pseq_colim (λk, spectrify_type_fun' X (succ k) (S n +' k)),
-    rotate 1, --exact pseq_colim_equiv_constant (λn, !ap1_pcompose⁻¹*),
-    reflexivity,
-    transitivity pseq_colim (λk, spectrify_type_fun' X (succ k) (n +' succ k)),
-    reflexivity,
+    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,
     { intro n, apply loopn_pequiv_loopn, apply pequiv_ap X, apply succ_str.add_succ },
-    { intro n, apply to_homotopy, exact sorry }
+    { intro k, apply to_homotopy,
+      refine !passoc⁻¹* ⬝* _, refine pwhisker_right _ (loopn_succ_in_inv_apn (succ k) _) ⬝* _,
+      refine !passoc ⬝* _ ⬝* !passoc⁻¹*, apply pwhisker_left,
+      refine !apn_pcompose⁻¹* ⬝* _ ⬝* !apn_pcompose, apply apn_phomotopy,
+      exact !glue_ptransport⁻¹* }
   end
 
   definition spectrify [constructor] {N : succ_str} (X : gen_prespectrum N) : gen_spectrum N :=
@@ -396,13 +409,21 @@ namespace spectrum
     : X n →* Ω[k] (X (n +' k)) :=
   by induction k with k f; reflexivity; exact !loopn_succ_in⁻¹ᵉ* ∘* Ω→[k] (glue X (n +' k)) ∘* f
 
-  -- note: the forward map is (currently) not definitionally equal to gluen.
+  -- note: the forward map is (currently) not definitionally equal to gluen. Is that a problem?
   definition equiv_gluen {N : succ_str} (X : gen_spectrum N) (n : N) (k : ℕ)
     : X n ≃* Ω[k] (X (n +' k)) :=
   by induction k with k f; reflexivity; exact f ⬝e* loopn_pequiv_loopn k (equiv_glue X (n +' k))
                                                 ⬝e* !loopn_succ_in⁻¹ᵉ*
 
   definition spectrify_map {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N}
+    (f : X →ₛ Y) : X →ₛ spectrify X :=
+  begin
+    fapply smap.mk,
+    { intro n, exact pinclusion _ 0},
+    { intro n, exact sorry}
+  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,

move_to_lib.hlean

@@ -172,6 +172,15 @@ namespace pointed
     : B a →* B a' :=
   pmap.mk (transport B p) (apdt (λa, Point (B a)) p)
 
+  definition ptransport_change_eq [constructor] {A : Type} (B : A → Type*) {a a' : A} {p q : a = a'}
+    (r : p = q) : ptransport B p ~* ptransport B q :=
+  phomotopy.mk (λb, ap (λp, transport B p b) r) begin induction r, exact !idp_con end
+
+  definition pnatural_square {A B : Type} (X : B → Type*) {f g : A → B}
+    (h : Πa, X (f a) →* X (g a)) {a a' : A} (p : a = a') :
+    h a' ∘* ptransport X (ap f p) ~* ptransport X (ap g p) ∘* h a :=
+  by induction p; exact !pcompose_pid ⬝* !pid_pcompose⁻¹*
+
   definition pequiv_ap [constructor] {A : Type} (B : A → Type*) {a a' : A} (p : a = a')
     : B a ≃* B a' :=
   pequiv_of_pmap (ptransport B p) !is_equiv_tr
@@ -279,6 +288,16 @@ namespace pointed
     {a₁ a₂ : A} (p : a₁ = a₂) : pequiv_of_eq (ap C p) ∘* f a₁ ~* f a₂ ∘* pequiv_of_eq (ap B p) :=
   pcast_commute f p
 
+  -- TODO: make the name apn_succ_phomotopy_in consistent with this
+  definition loopn_succ_in_inv_apn {A B : Type*} (n : ℕ) (f : A →* B) :
+    Ω→[n + 1] f ∘* (loopn_succ_in A n)⁻¹ᵉ* ~* (loopn_succ_in B n)⁻¹ᵉ* ∘* Ω→[n] (Ω→ f):=
+  begin
+    apply pinv_right_phomotopy_of_phomotopy,
+    refine _ ⬝* !passoc⁻¹*,
+    apply phomotopy_pinv_left_of_phomotopy,
+    apply apn_succ_phomotopy_in
+  end
+
 end pointed
 
 namespace fiber