prove the Freudenthal Suspension Theorem

homotopy/LES_applications.hlean

@@ -1,6 +1,7 @@
 import .LES_of_homotopy_groups homotopy.connectedness homotopy.homotopy_group homotopy.join
 open eq is_trunc pointed homotopy is_equiv fiber equiv trunc nat chain_complex prod fin algebra
      group trunc_index function join pushout
+
 namespace nat
   open sigma sum
   definition eq_even_or_eq_odd (n : ℕ) : (Σk, 2 * k = n) ⊎ (Σk, 2 * k + 1 = n) :=
@@ -25,61 +26,6 @@ open nat
 
 namespace is_conn
 
-  theorem is_contr_HG_fiber_of_is_connected {A B : Type*} (k n : ℕ) (f : A →* B)
-    [H : is_conn_map n f] (H2 : k ≤ n) : is_contr (π[k] (pfiber f)) :=
-  @(trivial_homotopy_group_of_is_conn (pfiber f) H2) (H pt)
-
-  -- TODO: use this for trivial_homotopy_group_of_is_conn (in homotopy.homotopy_group)
-  theorem is_conn_of_le (A : Type) {n k : ℕ₋₂} (H : n ≤ k) [is_conn k A] : is_conn n A :=
-  begin
-    apply is_contr_equiv_closed,
-    apply trunc_trunc_equiv_left _ n k H
-  end
-
-  definition zero_le_of_nat (n : ℕ) : 0 ≤[ℕ₋₂] n :=
-  of_nat_le_of_nat (zero_le n)
-
-  local attribute is_conn_map [reducible] --TODO
-  theorem is_conn_map_of_le {A B : Type} (f : A → B) {n k : ℕ₋₂} (H : n ≤ k)
-    [is_conn_map k f] : is_conn_map n f :=
-  λb, is_conn_of_le _ H
-
-  definition is_surjective_trunc_functor {A B : Type} (n : ℕ₋₂) (f : A → B) [H : is_surjective f]
-    : is_surjective (trunc_functor n f) :=
-  begin
-    cases n with n: intro b,
-    { exact tr (fiber.mk !center !is_prop.elim)},
-    { refine @trunc.rec _ _ _ _ _ b, {intro x, exact is_trunc_of_le _ !minus_one_le_succ},
-      clear b, intro b, induction H b with v, induction v with a p,
-      exact tr (fiber.mk (tr a) (ap tr p))}
-  end
-
-  definition is_surjective_cancel_right {A B C : Type} (g : B → C) (f : A → B)
-    [H : is_surjective (g ∘ f)] : is_surjective g :=
-  begin
-    intro c,
-    induction H c with v, induction v with a p,
-    exact tr (fiber.mk (f a) p)
-  end
-
-  -- Lemma 7.5.14
-  theorem is_equiv_trunc_functor_of_is_conn_map {A B : Type} (n : ℕ₋₂) (f : A → B)
-    [H : is_conn_map n f] : is_equiv (trunc_functor n f) :=
-  begin
-    fapply adjointify,
-    { intro b, induction b with b, exact trunc_functor n point (center (trunc n (fiber f b)))},
-    { intro b, induction b with b, esimp, generalize center (trunc n (fiber f b)), intro v,
-      induction v with v, induction v with a p, esimp, exact ap tr p},
-    { intro a, induction a with a, esimp, rewrite [center_eq (tr (fiber.mk a idp))]}
-  end
-
-  theorem trunc_equiv_trunc_of_is_conn_map {A B : Type} (n : ℕ₋₂) (f : A → B)
-    [H : is_conn_map n f] : trunc n A ≃ trunc n B :=
-  equiv.mk (trunc_functor n f) (is_equiv_trunc_functor_of_is_conn_map n f)
-
-  definition is_equiv_tinverse [constructor] (A : Type*) : is_equiv (@tinverse A) :=
-  by apply @is_equiv_trunc_functor; apply is_equiv_eq_inverse
-
   local attribute comm_group.to_group [coercion]
   local attribute is_equiv_tinverse [instance]
 
@@ -124,20 +70,20 @@ namespace is_conn
     [H : is_conn_map n f] : is_surjective (π→[n + 1] f) :=
   begin
     induction n using rec_on_even_odd with n,
-    { cases n with n,
+    { have H3 : is_surjective (π→*[2*n + 1] f ∘* tinverse), from
-      { exact sorry},
+      @is_surjective_of_trivial _
-      { have H3 : is_surjective (π→*[2*(succ n) + 1] f ∘* tinverse), from
+        (LES_of_homotopy_groups3 f) _
-        @is_surjective_of_trivial _
+        (is_exact_LES_of_homotopy_groups3 f (n, 2))
-          (LES_of_homotopy_groups3 f) _
+        (@is_contr_HG_fiber_of_is_connected A B (2 * n) (2 * n) f H !le.refl),
-          (is_exact_LES_of_homotopy_groups3 f (succ n, 2))
+      exact @(is_surjective_cancel_right (pmap.to_fun (π→*[2*n + 1] f)) tinverse) H3},
-          (@is_contr_HG_fiber_of_is_connected A B (2 * succ n) (2 * succ n) f H !le.refl),
-        exact @(is_surjective_cancel_right (pmap.to_fun (π→*[2*(succ n) + 1] f)) tinverse) H3}},
     { exact @is_surjective_of_trivial _
         (LES_of_homotopy_groups3 f) _
         (is_exact_LES_of_homotopy_groups3 f (k, 5))
         (@is_contr_HG_fiber_of_is_connected A B (2 * k + 1) (2 * k + 1) f H !le.refl)}
   end
 
+  /- joins -/
+
   definition join_empty_right [constructor] (A : Type) : join A empty ≃ A :=
   begin
     fapply equiv.MK,
@@ -153,8 +99,6 @@ namespace is_conn
       { exact empty.elim (pr2 v)}}
   end
 
-  /- joins -/
-
   definition join_functor [unfold 7] {A A' B B' : Type} (f : A → A') (g : B → B') :
     join A B → join A' B' :=
   begin

homotopy/chain_complex.hlean

@@ -495,7 +495,6 @@ namespace chain_complex
             pt_mul := one_mul,
             mul_pt := mul_one,
             mul_left_inv_pt := mul.left_inv⦄
-
   end
 
   -- the following theorems would also be true of the replace "is_contr" by "is_prop"

homotopy/sec86.hlean

@@ -1,45 +1,259 @@
+-- TODO: in wedge connectivity and is_conn.elim, unbundle P
 
+import  homotopy.wedge types.pi .LES_applications --TODO: remove
 
-import  homotopy.wedge types.pi
+open eq homotopy is_trunc pointed susp nat pi equiv is_equiv trunc fiber trunc_index
 
-open eq homotopy is_trunc pointed susp nat pi equiv is_equiv trunc
+  definition iterated_loop_ptrunc_pequiv_con (n : ℕ₋₂) (k : ℕ) (A : Type*)
-
+    (p q : Ω[k](ptrunc (n+k) (Ω A))) :
-section freudenthal
+    iterated_loop_ptrunc_pequiv n k (Ω A) (loop_mul trunc_concat p q) =
-
+    trunc_functor2 (loop_mul concat) (iterated_loop_ptrunc_pequiv n k (Ω A) p)
-parameters {A : Type*} (n : ℕ) [is_conn n A]
+                                     (iterated_loop_ptrunc_pequiv n k (Ω A) q) :=
-
---set_option pp.notation false
-
-protected definition my_wedge_extension.ext : Π {A : Type*} {B : Type*} (n m : ℕ) [cA : is_conn n (carrier A)] [cB : is_conn m (carrier B)]
-(P : carrier A → carrier B → (m+n)-Type) (f : Π (a : carrier A), trunctype.carrier (P a (Point B)))
-(g : Π (b : carrier B), trunctype.carrier (P (Point A) b)),
-  f (Point A) = g (Point B) → (Π (a : carrier A) (b : carrier B), trunctype.carrier (P a b)) :=
-sorry
-
-definition code_fun (a : A) (q : north = north :> susp A)
-  : trunc (n * 2) (fiber (pmap.to_fun (loop_susp_unit A)) q) → trunc (n * 2) (fiber merid (q ⬝ merid a)) :=
-begin
-  intro x, induction x with x,
-  esimp at *, cases x with a' p,
---  apply my_wedge_extension.ext n n,
-  exact sorry
-end
-
-definition code (y : susp A) :  north = y → Type :=
-susp.rec_on y
-  (λp, trunc (2*n) (fiber (loop_susp_unit A) p))
-  (λq, trunc (2*n) (fiber merid q))
   begin
-    intros,
+    revert n p q, induction k with k IH: intro n p q,
-    apply arrow_pathover_constant_right,
+    { reflexivity},
-    intro q, rewrite [transport_eq_r],
+    { exact sorry}
-    apply ua,
-    exact sorry
   end
 
-definition freudenthal_suspension  : is_conn_map (n*2) (loop_susp_unit A) :=
+  theorem elim_type_merid_inv {A : Type} (PN : Type) (PS : Type) (Pm : A → PN ≃ PS)
-sorry
+    (a : A) : transport (susp.elim_type PN PS Pm) (merid a)⁻¹ = to_inv (Pm a) :=
+  by rewrite [tr_eq_cast_ap_fn,↑susp.elim_type,ap_inv,elim_merid]; apply cast_ua_inv_fn
 
+  definition is_conn_trunc (A : Type) (n k : ℕ₋₂) [H : is_conn n A]
+    : is_conn n (trunc k A) :=
+  begin
+    apply is_trunc_equiv_closed, apply trunc_trunc_equiv_trunc_trunc
+  end
 
+  section open sphere sphere.ops
+  definition psphere_succ [unfold_full] (n : ℕ) : S. (n + 1) = psusp (S. n) := idp
+  end
 
-end freudenthal
+namespace freudenthal section
+
+  parameters {A : Type*} {n : ℕ} [is_conn n A]
+
+  --porting from Agda
+  -- definition Q (x : susp A) : Type :=
+  -- trunc (k) (north = x)
+
+  definition up (a : A) : north = north :> susp A := -- up a = loop_susp_unit A a
+  merid a ⬝ (merid pt)⁻¹
+
+  definition code_merid : A → ptrunc (n + n) A → ptrunc (n + n) A :=
+  begin
+    have is_conn n (ptrunc (n + n) A), from !is_conn_trunc,
+    refine wedge_extension.ext n n (λ x y, ttrunc (n + n) A) _ _ _,
+    { exact tr},
+    { exact id},
+    { reflexivity}
+  end
+
+  definition code_merid_β_left (a : A) : code_merid a pt = tr a :=
+  by apply wedge_extension.β_left
+
+  definition code_merid_β_right (b : ptrunc (n + n) A) : code_merid pt b = b :=
+  by apply wedge_extension.β_right
+
+  definition code_merid_coh : code_merid_β_left pt = code_merid_β_right pt :=
+  begin
+    symmetry, apply eq_of_inv_con_eq_idp, apply wedge_extension.coh
+  end
+
+  definition is_equiv_code_merid (a : A) : is_equiv (code_merid a) :=
+  begin
+    refine @is_conn.elim (n.-1) _ _ _ _ a,
+    { intro a, apply is_trunc_of_le, apply minus_one_le_succ},
+    { esimp, exact homotopy_closed id (homotopy.symm (code_merid_β_right))}
+  end
+
+  definition code_merid_equiv [constructor] (a : A) : trunc (n + n) A ≃ trunc (n + n) A :=
+  equiv.mk _ (is_equiv_code_merid a)
+
+  definition code_merid_inv_pt (x : trunc (n + n) A) : (code_merid_equiv pt)⁻¹ x = x :=
+  begin
+    refine ap010 @(is_equiv.inv _) _ x ⬝ _,
+    { exact homotopy_closed id (homotopy.symm code_merid_β_right)},
+    { apply is_conn.elim_β},
+    { reflexivity}
+  end
+
+  definition code [unfold 4] : susp A → Type :=
+  susp.elim_type (trunc (n + n) A) (trunc (n + n) A) code_merid_equiv
+
+  definition is_trunc_code (x : susp A) : is_trunc (n + n) (code x) :=
+  begin
+    induction x with a: esimp,
+    { exact _},
+    { exact _},
+    { apply is_prop.elimo}
+  end
+  local attribute is_trunc_code [instance]
+
+  definition decode_north [unfold 4] : code north → trunc (n + n) (north = north :> susp A) :=
+  trunc_functor (n + n) up
+
+  definition decode_north_pt : decode_north (tr pt) = tr idp :=
+  ap tr !con.right_inv
+
+  definition decode_south [unfold 4] : code south → trunc (n + n) (north = south :> susp A) :=
+  trunc_functor (n + n) merid
+
+  definition encode' {x : susp A} (p : north = x) : code x :=
+  transport code p (tr pt)
+
+  definition encode [unfold 5] {x : susp A} (p : trunc (n + n) (north = x)) : code x :=
+  begin
+    induction p with p,
+    exact transport code p (tr pt)
+  end
+
+  theorem encode_decode_north (c : code north) : encode (decode_north c) = c :=
+  begin
+    have H : Πc, is_trunc (n + n) (encode (decode_north c) = c), from _,
+    esimp at *,
+    induction c with a,
+    rewrite [↑[encode, decode_north, up, code], con_tr, elim_type_merid, ▸*,
+             code_merid_β_left, elim_type_merid_inv, ▸*, code_merid_inv_pt]
+  end
+
+  definition decode_coh_f (a : A) : tr (up pt) =[merid a] decode_south (code_merid a (tr pt)) :=
+  begin
+    refine _ ⬝op ap decode_south (code_merid_β_left a)⁻¹,
+    apply trunc_pathover,
+    apply eq_pathover,
+    refine !ap_constant ⬝ph _ ⬝hp !ap_id⁻¹,
+    apply square_of_eq,
+    exact whisker_right !con.right_inv (merid a)
+  end
+
+  definition decode_coh_g (a' : A) : tr (up a') =[merid pt] decode_south (code_merid pt (tr a')) :=
+  begin
+    refine _ ⬝op ap decode_south (code_merid_β_right (tr a'))⁻¹,
+    apply trunc_pathover,
+    apply eq_pathover,
+    refine !ap_constant ⬝ph _ ⬝hp !ap_id⁻¹,
+    apply square_of_eq, refine !inv_con_cancel_right ⬝ !idp_con⁻¹
+  end
+
+  definition decode_coh_equality {A : Type} {a a' : A} (p : a = a')
+    : whisker_right (con.right_inv p) p = inv_con_cancel_right p p ⬝ (idp_con p)⁻¹ :=
+  by induction p; reflexivity
+
+  theorem decode_coh (a : A) : decode_north =[merid a] decode_south :=
+  begin
+    apply arrow_pathover_left, intro c, esimp at *,
+    induction c with a',
+    rewrite [↑code, elim_type_merid, ▸*],
+    refine wedge_extension.ext n n _ _ _ _ a a',
+    { exact _},
+    { exact decode_coh_f},
+    { exact decode_coh_g},
+    { clear a a', unfold [decode_coh_f, decode_coh_g], refine ap011 concato_eq _ _,
+      { apply ap (λp, trunc_pathover (eq_pathover (_ ⬝ph square_of_eq p ⬝hp _))),
+        apply decode_coh_equality},
+      { apply ap (λp, ap decode_south p⁻¹), apply code_merid_coh}}
+  end
+
+  definition decode [unfold 4] {x : susp A} (c : code x) : trunc (n + n) (north = x) :=
+  begin
+    induction x with a,
+    { exact decode_north c},
+    { exact decode_south c},
+    { exact decode_coh a}
+  end
+
+  theorem decode_encode {x : susp A} (p : trunc (n + n) (north = x)) : decode (encode p) = p :=
+  begin
+    induction p with p, induction p, esimp, apply decode_north_pt
+  end
+
+  parameters (A n)
+  definition equiv' : trunc (n + n) A ≃ trunc (n + n) (Ω (psusp A)) :=
+  equiv.MK decode_north encode decode_encode encode_decode_north
+
+  definition pequiv' : ptrunc (n + n) A ≃* ptrunc (n + n) (Ω (psusp A)) :=
+  pequiv_of_equiv equiv' decode_north_pt
+
+  -- can we get this?
+  -- definition freudenthal_suspension  : is_conn_map (n+n) (loop_susp_unit A) :=
+  -- begin
+  --   intro p, esimp at *, fapply is_contr.mk,
+  --   { note c := encode (tr p), esimp at *, induction c with a, },
+  --   { exact sorry}
+  -- end
+
+-- {- Used to prove stability in iterated suspensions -}
+-- module FreudenthalIso
+--   {i} (n : ℕ₋₂) (k : ℕ) (t : k ≠ O) (kle : ⟨ k ⟩ ≤T S (n +2+ S n))
+--   (X : Ptd i) (cX : is-connected (S (S n)) (fst X)) where
+
+--   open FreudenthalEquiv n (⟨ k ⟩) kle (fst X) (snd X) cX public
+
+--   hom : Ω^-Group k t (⊙Trunc ⟨ k ⟩ X) Trunc-level
+--      →ᴳ Ω^-Group k t (⊙Trunc ⟨ k ⟩ (⊙Ω (⊙Susp X))) Trunc-level
+--   hom = record {
+--     f = fst F;
+--     pres-comp = ap^-conc^ k t (decodeN , decodeN-pt) }
+--     where F = ap^ k (decodeN , decodeN-pt)
+
+--   iso : Ω^-Group k t (⊙Trunc ⟨ k ⟩ X) Trunc-level
+--      ≃ᴳ Ω^-Group k t (⊙Trunc ⟨ k ⟩ (⊙Ω (⊙Susp X))) Trunc-level
+--   iso = (hom , is-equiv-ap^ k (decodeN , decodeN-pt) (snd eq))
+
+end end freudenthal
+
+open algebra
+definition freudenthal_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n)
+  : ptrunc k A ≃* ptrunc k (Ω (psusp A)) :=
+have H' : k ≤[ℕ₋₂] n + n,
+  by rewrite [mul.comm at H, -algebra.zero_add n at {1}]; exact of_nat_le_of_nat H,
+ptrunc_pequiv_ptrunc_of_le H' (freudenthal.pequiv' A n)
+
+definition freudenthal_equiv {A : Type*} {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n)
+  : trunc k A ≃ trunc k (Ω (psusp A)) :=
+freudenthal_pequiv A H
+
+namespace sphere
+  open ops algebra pointed function
+
+  definition stability_pequiv (k n : ℕ) (H : k + 2 ≤ 2 * n) : π*[k + 1] (S. (n+1)) ≃* π*[k] (S. n) :=
+  begin
+    have H' : k ≤ 2 * pred n,
+    begin
+      rewrite [mul_pred_right], change pred (pred (k + 2)) ≤ pred (pred (2 * n)),
+      apply pred_le_pred, apply pred_le_pred, exact H
+    end,
+    have is_conn (of_nat (pred n)) (S. n),
+    begin
+      cases n with n,
+      { exfalso, exact not_succ_le_zero _ H},
+      { esimp, apply is_conn_psphere}
+    end,
+    refine pequiv_of_eq (ap (ptrunc 0) (loop_space_succ_eq_in (S. (n+1)) k)) ⬝e* _,
+    rewrite psphere_succ,
+    refine !phomotopy_group_pequiv_loop_ptrunc ⬝e* _,
+    refine loopn_pequiv_loopn k (freudenthal_pequiv _ H')⁻¹ᵉ* ⬝e* _,
+    exact !phomotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*,
+  end
+print phomotopy_group_pequiv_loop_ptrunc
+print iterated_loop_ptrunc_pequiv
+  definition to_fun_stability_pequiv (k n : ℕ) (H : k + 2 ≤ 2 * n) --(p : π*[k + 1] (S. (n+1)))
+    : stability_pequiv k n H = _ ∘ _ ∘ cast (ap (ptrunc 0) (loop_space_succ_eq_in (S. (n+1)) k)) :=
+  sorry
+
+  -- definition stability (k n : ℕ) (H : k + 3 ≤ 2 * n) : πg[k+1 +1] (S. (n+1)) = πg[k+1] (S. n) :=
+  -- begin
+  --   fapply Group_eq,
+  --   { refine equiv_of_pequiv (stability_pequiv _ _ _), rewrite succ_add, exact H},
+  --   { intro g h, esimp, }
+  -- end
+
+end sphere
+
+/-
+  changes in book:
+  proof 8.6.15: also mention that we ignore multiplication
+  proof 8.4.4: respects points
+  proof 8.4.8: do k=0 separately
+-/