colimit, start on encode-decode proof

colim.hlean

@@ -16,12 +16,8 @@ namespace seq_colim
     : 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)) :=
- sorry
-
   definition seq_diagram [reducible] (A : ℕ → Type) : Type := Π⦃n⦄, A n → A (succ n)
+  definition pseq_diagram [reducible] (A : ℕ → Type*) : Type := Π⦃n⦄, A n →* A (succ n)
 
   structure Seq_diagram : Type :=
     (carrier : ℕ → Type)
@@ -192,8 +188,13 @@ namespace seq_colim
     seq_diagram (λn, Πx, A x n) :=
   λn f x, g (f x)
 
+  namespace seq_colim.ops
   abbreviation ι  [constructor] := @inclusion
+  abbreviation pι  [constructor] {A} (f) {n} := @pinclusion A f n
+  abbreviation pι'  [constructor] [parsing_only] := @pinclusion
   abbreviation ι' [constructor] [parsing_only] {A} (f n) := @inclusion A f n
+  end seq_colim.ops
+  open seq_colim.ops
 
   definition rep0_glue (k : ℕ) (a : A 0) : ι f (rep0 f k a) = ι f a :=
   begin
@@ -345,6 +346,122 @@ namespace seq_colim
     { esimp, apply respect_pt }
   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
+
+  definition respect_pt_prep0_succ {A : ℕ → Type*} (f : pseq_diagram A) (k : ℕ)
+    : respect_pt (prep0 f (succ k)) = ap (@f k) (respect_pt (prep0 f k)) ⬝ respect_pt (@f k) :=
+  by reflexivity
+
+  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, +ap_con, ap_inv, +con.assoc]
+
+  definition succ_add_tr_rep {n : ℕ} (k : ℕ) (x : A n)
+    : transport A (succ_add n k) (rep f k (f x)) = rep f (succ k) x :=
+  begin
+    induction k with k p,
+      reflexivity,
+      exact tr_ap A succ (succ_add n k) _ ⬝ (fn_tr_eq_tr_fn (succ_add n k) f _)⁻¹ ⬝ ap (@f _) p,
+  end
+
+  definition succ_add_tr_rep_succ {n : ℕ} (k : ℕ) (x : A n)
+    : succ_add_tr_rep f (succ k) x = tr_ap A succ (succ_add n k) _ ⬝
+        (fn_tr_eq_tr_fn (succ_add n k) f _)⁻¹ ⬝ ap (@f _) (succ_add_tr_rep f k x) :=
+  by reflexivity
+
+  definition code_glue_equiv [constructor] {n : ℕ} (k : ℕ) (x y : A n)
+    : rep f k (f x) = rep f k (f y) ≃ rep f (succ k) x = rep f (succ k) y :=
+  begin
+    refine eq_equiv_fn_eq_of_equiv (equiv_ap A (succ_add n k)) _ _ ⬝e _,
+    apply eq_equiv_eq_closed,
+      exact succ_add_tr_rep f k x,
+      exact succ_add_tr_rep f k y
+  end
+
+  theorem code_glue_equiv_ap {n : ℕ} {k : ℕ} {x y : A n} (p : rep f k (f x) = rep f k (f y))
+    : code_glue_equiv f (succ k) x y (ap (@f _) p) = ap (@f _) (code_glue_equiv f k x y p) :=
+  begin
+    rewrite [▸*, +ap_con, ap_inv, +succ_add_tr_rep_succ, con_inv, inv_con_inv_right, +con.assoc],
+    apply whisker_left,
+    rewrite [- +con.assoc], apply whisker_right, rewrite [- +ap_compose'],
+    note s := (eq_top_of_square (natural_square
+      (λx, fn_tr_eq_tr_fn (succ_add n k) f x ⬝ (tr_ap A succ (succ_add n k) (f x))⁻¹) p))⁻¹,
+    rewrite [inv_con_inv_right at s, -con.assoc at s], exact s
+  end
+
+  section
+  parameters {X : ℕ → Type} (g : seq_diagram X) (x : X 0)
+
+  definition rep_eq_diag ⦃n : ℕ⦄ (y : X n) : seq_diagram (λk, rep g k (rep0 g n x) = rep g k y) :=
+  proof λk, ap (@g (n + k)) qed
+
+  definition code_incl ⦃n : ℕ⦄ (y : X n) : Type :=
+  seq_colim (rep_eq_diag y)
+
+  definition code [unfold 4] : seq_colim g → Type :=
+  seq_colim.elim_type g code_incl
+  begin
+    intro n y,
+    refine _ ⬝e !shift_equiv⁻¹ᵉ,
+    fapply seq_colim_equiv,
+    { intro k, exact code_glue_equiv g k (rep0 g n x) y },
+    { intro k p, exact code_glue_equiv_ap g p }
+  end
+
+  definition encode [unfold 5] (y : seq_colim g) (p : ι g x = y) : code y :=
+  transport code p (ι' _ 0 idp)
+
+  definition decode [unfold 4] (y : seq_colim g) (c : code y) : ι g x = y :=
+  begin
+    induction y,
+    { esimp at c, exact sorry},
+    { exact sorry }
+  end
+
+  definition decode_encode (y : seq_colim g) (p : ι g x = y) : decode y (encode y p) = p :=
+  sorry
+
+  definition encode_decode (y : seq_colim g) (c : code y) : encode y (decode y c) = c :=
+  sorry
+
+  definition seq_colim_eq_equiv_code [constructor] (y : seq_colim g) : (ι g x = y) ≃ code y :=
+  equiv.MK (encode y) (decode y) (encode_decode y) (decode_encode y)
+
+  definition seq_colim_eq {n : ℕ} (y : X n) : (ι g x = ι g y) ≃ seq_colim (rep_eq_diag y) :=
+  proof seq_colim_eq_equiv_code (ι g y) qed
+
+  end
+
+  definition rep0_eq_diag {X : ℕ → Type} (f : seq_diagram X) (x y : X 0)
+    : seq_diagram (λk, rep0 f k x = rep0 f k y) :=
+  proof λk, ap (@f (k)) qed
+
+  definition seq_colim_eq0 {X : ℕ → Type} (f : seq_diagram X) (x y : X 0) :
+    (ι f x = ι f y) ≃ seq_colim (rep0_eq_diag f x y)  :=
+  begin
+    refine !seq_colim_eq ⬝e _,
+    fapply seq_colim_equiv,
+    { intro n, exact sorry},
+    { intro n p, exact sorry }
+  end
+
+
+  definition pseq_colim_loop {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) :
+    Ω (pseq_colim f) ≃* pseq_colim (λn, Ω→(f n)) :=
+  begin
+    fapply pequiv_of_equiv,
+    { refine !seq_colim_eq0 ⬝e _,
+      fapply seq_colim_equiv,
+      { intro n, exact loop_equiv_eq_closed (respect_pt (prep0 f n)) },
+      { intro n p, apply prep0_succ_lemma }},
+    { exact sorry }
+  end
+
   -- 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

@@ -123,6 +123,7 @@ namespace spectrum
   ------------------------------
 
   -- These make sense for any succ_str.
+
   structure smap {N : succ_str} (E F : gen_prespectrum N) :=
     (to_fun : Π(n:N), E n →* F n)
     (glue_square : Π(n:N), glue F n ∘* to_fun n ~* Ω→ (to_fun (S n)) ∘* glue E n)
@@ -243,13 +244,16 @@ namespace spectrum
 
   definition sfiber {N : succ_str} {X Y : gen_spectrum N} (f : X →ₛ Y) : gen_spectrum N :=
     spectrum.MK (λn, pfiber (f n))
-      (λn, pfiber_loop_space (f (S n)) ∘*ᵉ pfiber_equiv_of_square (sglue_square f n))
+      (λn, pfiber_loop_space (f (S n)) ∘*ᵉ pfiber_equiv_of_square _ _ (sglue_square f n))
 
-  /- the map from the fiber to the domain. The fact that the square commutes requires work -/
+  /- the map from the fiber to the domain -/
   definition spoint {N : succ_str} {X Y : gen_spectrum N} (f : X →ₛ Y) : sfiber f →ₛ X :=
   smap.mk (λn, ppoint (f n))
     begin
-      intro n, exact sorry
+      intro n,
+      refine _ ⬝* !passoc,
+      refine _ ⬝* pwhisker_right _ !ap1_ppoint_phomotopy⁻¹*,
+      rexact (pfiber_equiv_of_square_ppoint (equiv_glue X n) (equiv_glue Y n) (sglue_square f n))⁻¹*
     end
 
   definition π_glue (X : spectrum) (n : ℤ) : π[2] (X (2 - succ n)) ≃* π[3] (X (2 - n)) :=
@@ -386,6 +390,15 @@ namespace spectrum
   definition spectrify_type {N : succ_str} (X : gen_prespectrum N) (n : N) : Type* :=
   pseq_colim (spectrify_type_fun X n)
 
+  /-
+    Let Y = spectify X. Then
+    Ω Y (n+1) ≡ Ω colim_k Ω^k X ((n + 1) + k)
+          ... = colim_k Ω^{k+1} X ((n + 1) + k)
+          ... = colim_k Ω^{k+1} X (n + (k + 1))
+          ... = colim_k Ω^k X(n + k)
+          ... ≡ Y n
+  -/
+
   definition spectrify_pequiv {N : succ_str} (X : gen_prespectrum N) (n : N) :
     spectrify_type X n ≃* Ω (spectrify_type X (S n)) :=
   begin
@@ -396,7 +409,7 @@ namespace spectrum
     fapply pseq_colim_pequiv,
     { intro n, apply loopn_pequiv_loopn, apply pequiv_ap X, apply succ_str.add_succ },
     { intro k, apply to_homotopy,
-      refine !passoc⁻¹* ⬝* _, refine pwhisker_right _ (loopn_succ_in_inv_apn (succ k) _) ⬝* _,
+      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⁻¹* }

homotopy/splice.hlean

@@ -20,9 +20,9 @@ such that the evident squares commute, we can obtain a single sequence
 
 However, in this formalization, we will only do this for k = 3, because we get more definitional
 equalities in this specific case than in the general case. The reason is that we need to check
-whether a term `x : fin (succ k)` represents `n`. If we do this in general using
+whether a term `x : fin (succ k)` represents `k`. If we do this in general using
-if x = n then ... else ...
+if x = k then ... else ...
-we don't get definitionally that x = n and the successor of x is 0, which means that when defining
+we don't get definitionally that x = k and the successor of x is 0, which means that when defining
 maps G_{n,m} -> G_{n+1,m+k-1} we need to transport along those paths, which is annoying.
 
 So far, the splicing seems to be only needed for k = 3, so it seems to be sufficient.

move_to_lib.hlean

@@ -7,7 +7,8 @@ open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc
 
 attribute equiv.symm equiv.trans is_equiv.is_equiv_ap fiber.equiv_postcompose
           fiber.equiv_precompose pequiv.to_pmap pequiv._trans_of_to_pmap ghomotopy_group_succ_in
-          isomorphism_of_eq pmap_bool_equiv sphere_equiv_bool psphere_pequiv_pbool [constructor]
+          isomorphism_of_eq pmap_bool_equiv sphere_equiv_bool psphere_pequiv_pbool fiber_eq_equiv
+          [constructor]
 attribute is_equiv.eq_of_fn_eq_fn' [unfold 3]
 attribute isomorphism._trans_of_to_hom [unfold 3]
 attribute homomorphism.struct [unfold 3]
@@ -90,11 +91,21 @@ namespace pi -- move to types.arrow
     { apply pmap_eq_idp}
   end
 
-
 end pi open pi
 
 namespace eq
 
+  -- types.eq
+  definition loop_equiv_eq_closed [constructor] {A : Type} {a a' : A} (p : a = a')
+    : (a = a) ≃ (a' = a') :=
+  eq_equiv_eq_closed p p
+
+  -- init.path
+  definition tr_ap {A B : Type} {x y : A} (P : B → Type) (f : A → B) (p : x = y) (z : P (f x)) :
+    transport P (ap f p) z = transport (P ∘ f) p z :=
+  (tr_compose P f p z)⁻¹
+
+
   definition pathover_eq_Fl' {A B : Type} {f : A → B} {a₁ a₂ : A} {b : B} (p : a₁ = a₂) (q : f a₂ = b) : (ap f p) ⬝ q =[p] q :=
   by induction p; induction q; exact idpo
 
@@ -298,16 +309,6 @@ 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
-
   definition papply [constructor] {A : Type*} (B : Type*) (a : A) : ppmap A B →* B :=
   pmap.mk (λ(f : A →* B), f a) idp
 
@@ -337,30 +338,52 @@ namespace pointed
     ppmap A B →* Ω[n] B :=
   papply _ p ∘* papn_pt n A B
 
-  definition loopn_succ_in_natural {A B : Type*} {n : ℕ} (f : A →* B) :
+  definition loopn_succ_in_natural {A B : Type*} (n : ℕ) (f : A →* B) :
     loopn_succ_in B n ∘* Ω→[n+1] f ~* Ω→[n] (Ω→ f) ∘* loopn_succ_in A n :=
   !apn_succ_phomotopy_in
 
-  definition loopn_succ_in_inv_natural {A B : Type*} {n : ℕ} (f : A →* B) :
+  definition loopn_succ_in_inv_natural {A B : Type*} (n : ℕ) (f : A →* B) :
-    (loopn_succ_in B n)⁻¹ᵉ* ∘* Ω→[n] (Ω→ f) ~* Ω→[n+1] f ∘* (loopn_succ_in A n)⁻¹ᵉ* :=
+    Ω→[n + 1] f ∘* (loopn_succ_in A n)⁻¹ᵉ* ~* (loopn_succ_in B n)⁻¹ᵉ* ∘* Ω→[n] (Ω→ f):=
-  sorry
+  begin
+    apply pinv_right_phomotopy_of_phomotopy,
+    refine _ ⬝* !passoc⁻¹*,
+    apply phomotopy_pinv_left_of_phomotopy,
+    apply apn_succ_phomotopy_in
+  end
 
 end pointed open pointed
 
 namespace fiber
 
+  definition pfiber.sigma_char [constructor] {A B : Type*} (f : A →* B)
+    : pfiber f ≃* pointed.MK (Σa, f a = pt) ⟨pt, respect_pt f⟩ :=
+  pequiv_of_equiv (fiber.sigma_char f pt) idp
+
+  definition ppoint_sigma_char [constructor] {A B : Type*} (f : A →* B)
+    : ppoint f ~* pmap.mk pr1 idp ∘* pfiber.sigma_char f :=
+  !phomotopy.refl
+
   definition pfiber_loop_space {A B : Type*} (f : A →* B) : pfiber (Ω→ f) ≃* Ω (pfiber f) :=
     pequiv_of_equiv
-    (calc pfiber (Ω→ f) ≃ Σ(p : Point A = Point A), ap1 f p = rfl                                : (fiber.sigma_char (ap1 f) (Point (Ω B)))
+    (calc pfiber (Ω→ f) ≃ Σ(p : Point A = Point A), ap1 f p = rfl
-                    ... ≃ Σ(p : Point A = Point A), (respect_pt f) = ap f p ⬝ (respect_pt f)      : (sigma_equiv_sigma_right (λp,
+                          : (fiber.sigma_char (ap1 f) (Point (Ω B)))
-                              calc (ap1 f p = rfl) ≃ !respect_pt⁻¹ ⬝ (ap f p ⬝ !respect_pt) = rfl : equiv_eq_closed_left _ (con.assoc _ _ _)
+                    ... ≃ Σ(p : Point A = Point A), (respect_pt f) = ap f p ⬝ (respect_pt f)
-                                               ... ≃ ap f p ⬝ (respect_pt f) = (respect_pt f)     : eq_equiv_inv_con_eq_idp
+                          : (sigma_equiv_sigma_right (λp,
-                                               ... ≃ (respect_pt f) = ap f p ⬝ (respect_pt f)     : eq_equiv_eq_symm))
+                              calc (ap1 f p = rfl) ≃ !respect_pt⁻¹ ⬝ (ap f p ⬝ !respect_pt) = rfl
-                    ... ≃ fiber.mk (Point A) (respect_pt f) = fiber.mk pt (respect_pt f)          : fiber_eq_equiv
+                                                     : equiv_eq_closed_left _ (con.assoc _ _ _)
-                    ... ≃ Ω (pfiber f)                                                            : erfl)
+                                               ... ≃ ap f p ⬝ (respect_pt f) = (respect_pt f)
-    (begin cases f with f p, cases A with A a, cases B with B b, esimp at p, esimp at f, induction p, reflexivity end)
+                                                     : eq_equiv_inv_con_eq_idp
+                                               ... ≃ (respect_pt f) = ap f p ⬝ (respect_pt f)
+                                                     : eq_equiv_eq_symm))
+                    ... ≃ fiber.mk (Point A) (respect_pt f) = fiber.mk pt (respect_pt f)
+                          : fiber_eq_equiv
+                    ... ≃ Ω (pfiber f)
+                          : erfl)
+    (begin cases f with f p, cases A with A a, cases B with B b, esimp at p, esimp at f,
+           induction p, reflexivity end)
 
-  definition pfiber_equiv_of_phomotopy {A B : Type*} {f g : A →* B} (h : f ~* g) : pfiber f ≃* pfiber g :=
+  definition pfiber_equiv_of_phomotopy {A B : Type*} {f g : A →* B} (h : f ~* g)
+    : pfiber f ≃* pfiber g :=
   begin
     fapply pequiv_of_equiv,
     { refine (fiber.sigma_char f pt ⬝e _ ⬝e (fiber.sigma_char g pt)⁻¹ᵉ),
@@ -371,12 +394,14 @@ namespace fiber
       rewrite idp_con, apply inv_con_eq_of_eq_con, symmetry, exact (to_homotopy_pt h) }
   end
 
-  definition transport_fiber_equiv [constructor] {A B : Type} (f : A → B) {b1 b2 : B} (p : b1 = b2) : fiber f b1 ≃ fiber f b2 :=
+  definition transport_fiber_equiv [constructor] {A B : Type} (f : A → B) {b1 b2 : B} (p : b1 = b2)
+    : fiber f b1 ≃ fiber f b2 :=
     calc fiber f b1 ≃ Σa, f a = b1 : fiber.sigma_char
                ...  ≃ Σa, f a = b2 : sigma_equiv_sigma_right (λa, equiv_eq_closed_right (f a) p)
                ...  ≃ fiber f b2   : fiber.sigma_char
 
-  definition pequiv_postcompose {A B B' : Type*} (f : A →* B) (g : B ≃* B') : pfiber (g ∘* f) ≃* pfiber f :=
+  definition pequiv_postcompose {A B B' : Type*} (f : A →* B) (g : B ≃* B')
+    : pfiber (g ∘* f) ≃* pfiber f :=
   begin
     fapply pequiv_of_equiv, esimp,
     refine transport_fiber_equiv (g ∘* f) (respect_pt g)⁻¹ ⬝e fiber.equiv_postcompose f g (Point B),
@@ -384,7 +409,8 @@ namespace fiber
     rewrite [con.assoc, con.right_inv, con_idp, -ap_compose'], apply ap_con_eq_con
   end
 
-  definition pequiv_precompose {A A' B : Type*} (f : A →* B) (g : A' ≃* A) : pfiber (f ∘* g) ≃* pfiber f :=
+  definition pequiv_precompose {A A' B : Type*} (f : A →* B) (g : A' ≃* A)
+    : pfiber (f ∘* g) ≃* pfiber f :=
   begin
     fapply pequiv_of_equiv, esimp,
     refine fiber.equiv_precompose f g (Point B),
@@ -393,12 +419,23 @@ namespace fiber
     { apply pathover_eq_Fl' }
   end
 
-  definition pfiber_equiv_of_square {A B C D : Type*} {f : A →* B} {g : C →* D} {h : A ≃* C} {k : B ≃* D} (s : k ∘* f ~* g ∘* h)
+  definition pfiber_equiv_of_square {A B C D : Type*} {f : A →* B} {g : C →* D} (h : A ≃* C)
-    : pfiber f ≃* pfiber g :=
+    (k : B ≃* D) (s : k ∘* f ~* g ∘* h) : pfiber f ≃* pfiber g :=
     calc pfiber f ≃* pfiber (k ∘* f) : pequiv_postcompose
               ... ≃* pfiber (g ∘* h) : pfiber_equiv_of_phomotopy s
               ... ≃* pfiber g : pequiv_precompose
 
+  definition ap1_ppoint_phomotopy {A B : Type*} (f : A →* B)
+    : Ω→ (ppoint f) ∘* pfiber_loop_space f ~* ppoint (Ω→ f) :=
+  begin
+    exact sorry
+  end
+
+  definition pfiber_equiv_of_square_ppoint {A B C D : Type*} {f : A →* B} {g : C →* D}
+    (h : A ≃* C) (k : B ≃* D) (s : k ∘* f ~* g ∘* h)
+    : ppoint g ∘* pfiber_equiv_of_square h k s ~* h ∘* ppoint f :=
+  sorry
+
 end fiber
 
 namespace eq --algebra.homotopy_group
@@ -689,7 +726,7 @@ namespace new_sphere
     { revert A, induction n with n IH: intro A,
       { reflexivity },
       { intro f, refine ap !loopn_succ_in⁻¹ᵉ* (IH (Ω A) _ ⬝ !apn_pcompose _) ⬝ _,
-        exact !loopn_succ_in_inv_natural _ }}
+        exact !loopn_succ_in_inv_natural⁻¹* _ }}
   end
 
 end new_sphere
@@ -709,4 +746,3 @@ namespace sphere
   -- end
 
 end sphere
-