From 057980ca1fb8cac01ee816d9f37025f5e11bd3a2 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 29 Jun 2017 15:48:43 +0100
Subject: [PATCH] start on postnikov tower of spectra

---
 algebra/module_exact_couple.hlean |   4 +-
 homotopy/EM.hlean                 |  20 ------
 homotopy/serre.hlean              | 116 ++++++++++++++++++++++++++++++
 homotopy/smash_adjoint.hlean      |   3 +
 pointed.hlean                     |   9 ++-
 susp_product.hlean                |   2 +-
 6 files changed, 126 insertions(+), 28 deletions(-)
 create mode 100644 homotopy/serre.hlean

diff --git a/algebra/module_exact_couple.hlean b/algebra/module_exact_couple.hlean
index cf45445..6843cab 100644
--- a/algebra/module_exact_couple.hlean
+++ b/algebra/module_exact_couple.hlean
@@ -633,8 +633,8 @@ namespace spectrum
 
   open int
   parameters (ub : ℤ) (lb : ℤ → ℤ)
-    (Aub : Πs n, s ≥ ub + 1 → is_equiv (f s n))
-    (Alb : Πs n, s ≤ lb n → is_contr (πₛ[n] (A s)))
+    (Aub : Π(s n : ℤ), s ≥ ub + 1 → is_equiv (f s n))
+    (Alb : Π(s n : ℤ), s ≤ lb n → is_contr (πₛ[n] (A s)))
 
   definition B : I → ℕ
   | (n, s) := max0 (s - lb n)
diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean
index 28b8b3d..aa95281 100644
--- a/homotopy/EM.hlean
+++ b/homotopy/EM.hlean
@@ -570,24 +570,4 @@ namespace EM
     abstract (EMadd1_functor_gcompose φ φ⁻¹ᵍ n)⁻¹* ⬝* EMadd1_functor_phomotopy proof right_inv φ qed n ⬝*
              EMadd1_functor_gid H n end
 
-  /- Eilenberg MacLane spaces are the fibers of the Postnikov system of a type -/
-
-  definition postnikov_map [constructor] (A : Type*) (n : ℕ₋₂) : ptrunc (n.+1) A →* ptrunc n A :=
-  ptrunc.elim (n.+1) !ptr
-
-  open fiber
-
-  definition pfiber_postnikov_map (A : Type*) (n : ℕ) : pfiber (postnikov_map A n) ≃* EM_type A (n+1) :=
-  begin
-    symmetry, apply EM_type_pequiv,
-    { symmetry, refine _ ⬝g ghomotopy_group_ptrunc (n+1) A,
-      exact chain_complex.LES_isomorphism_of_trivial_cod _ _
-        (trivial_homotopy_group_of_is_trunc _ (self_lt_succ n))
-        (trivial_homotopy_group_of_is_trunc _ (le_succ _)) },
-    { apply is_conn_fun_trunc_elim,  apply is_conn_fun_tr },
-    { have is_trunc (n+1) (ptrunc n.+1 A), from !is_trunc_trunc,
-      have is_trunc ((n+1).+1) (ptrunc n A), by do 2 apply is_trunc_succ, apply is_trunc_trunc,
-      apply is_trunc_pfiber }
-  end
-
 end EM
diff --git a/homotopy/serre.hlean b/homotopy/serre.hlean
new file mode 100644
index 0000000..4946217
--- /dev/null
+++ b/homotopy/serre.hlean
@@ -0,0 +1,116 @@
+import ..algebra.module_exact_couple .strunc
+
+open eq spectrum trunc is_trunc pointed int EM algebra left_module fiber lift
+
+/- Eilenberg MacLane spaces are the fibers of the Postnikov system of a type -/
+
+definition postnikov_map [constructor] (A : Type*) (n : ℕ₋₂) : ptrunc (n.+1) A →* ptrunc n A :=
+ptrunc.elim (n.+1) !ptr
+
+definition ptrunc_functor_postnikov_map {A B : Type*} (n : ℕ₋₂) (f : A →* B) :
+  ptrunc_functor n f ∘* postnikov_map A n ~* ptrunc.elim (n.+1) (!ptr ∘* f) :=
+begin
+  fapply phomotopy.mk,
+  { intro x, induction x with a, reflexivity },
+  { reflexivity }
+end
+
+section
+open nat is_conn group
+definition pfiber_postnikov_map (A : Type*) (n : ℕ) :
+  pfiber (postnikov_map A n) ≃* EM_type A (n+1) :=
+begin
+  symmetry, apply EM_type_pequiv,
+  { symmetry, refine _ ⬝g ghomotopy_group_ptrunc (n+1) A,
+    exact chain_complex.LES_isomorphism_of_trivial_cod _ _
+      (trivial_homotopy_group_of_is_trunc _ (self_lt_succ n))
+      (trivial_homotopy_group_of_is_trunc _ (le_succ _)) },
+  { apply is_conn_fun_trunc_elim,  apply is_conn_fun_tr },
+  { have is_trunc (n+1) (ptrunc n.+1 A), from !is_trunc_trunc,
+    have is_trunc ((n+1).+1) (ptrunc n A), by do 2 apply is_trunc_succ, apply is_trunc_trunc,
+    apply is_trunc_pfiber }
+end
+end
+
+definition postnikov_map_natural {A B : Type*} (f : A →* B) (n : ℕ₋₂) :
+  psquare (postnikov_map A n) (postnikov_map B n)
+          (ptrunc_functor (n.+1) f) (ptrunc_functor n f) :=
+!ptrunc_functor_postnikov_map ⬝* !ptrunc_elim_ptrunc_functor⁻¹*
+
+definition encode_ap1_gen_tr (n : ℕ₋₂) {A : Type*} {a a' : A} (p : a = a') :
+  trunc.encode (ap1_gen tr idp idp p) = tr p :> trunc n (a = a') :=
+by induction p; reflexivity
+
+definition ap1_postnikov_map (A : Type*) (n : ℕ₋₂) :
+  psquare (Ω→ (postnikov_map A (n.+1))) (postnikov_map (Ω A) n)
+          (loop_ptrunc_pequiv (n.+1) A) (loop_ptrunc_pequiv n A) :=
+have psquare (postnikov_map (Ω A) n) (Ω→ (postnikov_map A (n.+1)))
+             (loop_ptrunc_pequiv (n.+1) A)⁻¹ᵉ* (loop_ptrunc_pequiv n A)⁻¹ᵉ*,
+begin
+  refine _ ⬝* !ap1_ptrunc_elim⁻¹*, apply pinv_left_phomotopy_of_phomotopy,
+  fapply phomotopy.mk,
+  { intro x, induction x with p, exact !encode_ap1_gen_tr⁻¹ },
+  { reflexivity }
+end,
+this⁻¹ᵛ*
+
+
+-- definition postnikov_map_int (X : Type*) (k : ℤ) :
+--   ptrunc (maxm2 (k + 1)) X →* ptrunc (maxm2 k) X :=
+-- begin
+--   induction k with k k,
+--     exact postnikov_map X k,
+--   exact !pconst
+-- end
+
+-- definition postnikov_map_int_natural {A B : Type*} (f : A →* B) (k : ℤ) :
+--   psquare (postnikov_map_int A k) (postnikov_map_int B k)
+--           (ptrunc_int_functor (k+1) f) (ptrunc_int_functor k f) :=
+-- begin
+--   induction k with k k,
+--     exact postnikov_map_natural f k,
+--   apply psquare_of_phomotopy, exact !pcompose_pconst ⬝* !pconst_pcompose⁻¹*
+-- end
+
+-- definition postnikov_map_int_natural_pequiv {A B : Type*} (f : A ≃* B) (k : ℤ) :
+--   psquare (postnikov_map_int A k) (postnikov_map_int B k)
+--           (ptrunc_int_pequiv_ptrunc_int (k+1) f) (ptrunc_int_pequiv_ptrunc_int k f) :=
+-- begin
+--   induction k with k k,
+--     exact postnikov_map_natural f k,
+--   apply psquare_of_phomotopy, exact !pcompose_pconst ⬝* !pconst_pcompose⁻¹*
+-- end
+
+-- definition pequiv_ap_natural2 {X A : Type} (B C : X → A → Type*) {a a' : X → A}
+--   (p : a ~ a')
+--   (s : X → X) (f : Πx a, B x a →* C (s x) a) (x : X) :
+--   psquare (pequiv_ap (B x) (p x)) (pequiv_ap (C (s x)) (p x)) (f x (a x)) (f x (a' x)) :=
+-- begin induction p using homotopy.rec_on_idp, exact phrfl end
+
+-- definition pequiv_ap_natural3 {X A : Type} (B C : X → A → Type*) {a a' : A}
+--   (p : a = a')
+--   (s : X → X) (x : X) (f : Πx a, B x a →* C (s x) a) :
+--   psquare (pequiv_ap (B x) p) (pequiv_ap (C (s x)) p) (f x a) (f x a') :=
+-- begin induction p, exact phrfl end
+
+-- definition postnikov_smap (X : spectrum) (k : ℤ) :
+--   strunc (k+1) X →ₛ strunc k X :=
+-- smap.mk (λn, postnikov_map_int (X n) (k + n) ∘* ptrunc_int_change_int _ !norm_num.add_comm_middle)
+--         (λn, begin
+--                exact sorry
+-- --             exact (_ ⬝vp* !ap1_pequiv_ap) ⬝h* (!postnikov_map_int_natural_pequiv ⬝v* _ ⬝v* _) ⬝vp* !ap1_pcompose,
+--              end)
+
+
+-- section atiyah_hirzebruch
+--   parameters {X : Type*} (Y : X → spectrum)
+
+--   definition atiyah_hirzebruch_exact_couple : exact_couple rℤ spectrum.I :=
+--   @exact_couple_sequence (λs, strunc s (spi X (λx, Y x)))
+--                          (λs, !postnikov_smap ∘ₛ strunc_change_int _ !succ_pred⁻¹)
+
+-- --  parameters (k : ℕ) (H : Π(x : X) (n : ℕ), is_trunc (k + n) (Y x n))
+
+
+
+-- end atiyah_hirzebruch
diff --git a/homotopy/smash_adjoint.hlean b/homotopy/smash_adjoint.hlean
index 5c0892a..93121bc 100644
--- a/homotopy/smash_adjoint.hlean
+++ b/homotopy/smash_adjoint.hlean
@@ -570,6 +570,9 @@ namespace smash
   smash_iterate_psusp n A pbool ⬝e*
   iterate_psusp_pequiv n (smash_pbool_pequiv A)
 
+  definition smash_pcircle (A : Type*) : A ∧ pcircle ≃* psusp A :=
+  smash_sphere A 1
+
   definition sphere_smash_sphere (n m : ℕ) : psphere n ∧ psphere m ≃* psphere (n+m) :=
   smash_sphere (psphere n) m ⬝e*
   iterate_psusp_pequiv m (psphere_pequiv_iterate_psusp n) ⬝e*
diff --git a/pointed.hlean b/pointed.hlean
index 62adf6c..792beae 100644
--- a/pointed.hlean
+++ b/pointed.hlean
@@ -192,15 +192,14 @@ namespace pointed
     psquare (pequiv_ap B p) (pequiv_ap C p) (f a) (f a') :=
   begin induction p, exact phrfl end
 
-  definition pequiv_ap_natural2 {A : Type} (B C : A → Type*) {a a' : A} (p : a = a')
-    (f : Πa, B a →* C a) :
-    psquare (pequiv_ap B p) (pequiv_ap C p) (f a) (f a') :=
-  begin induction p, exact phrfl end
-
   definition loop_pequiv_punit_of_is_set (X : Type*) [is_set X] : Ω X ≃* punit :=
   pequiv_punit_of_is_contr _ (is_contr_of_inhabited_prop pt)
 
   definition loop_punit : Ω punit ≃* punit :=
   loop_pequiv_punit_of_is_set punit
 
+  definition phomotopy_of_is_contr [constructor] {X Y: Type*} (f g : X →* Y) [is_contr Y] :
+    f ~* g :=
+  phomotopy.mk (λa, !eq_of_is_contr) !eq_of_is_contr
+
 end pointed
diff --git a/susp_product.hlean b/susp_product.hlean
index ad3d9a1..7c31e4b 100644
--- a/susp_product.hlean
+++ b/susp_product.hlean
@@ -2,4 +2,4 @@ import core
 open susp smash pointed wedge prod
 
 definition susp_product (X Y : Type*) : ⅀ (X × Y) ≃* ⅀ X ∨ (⅀ Y ∨ ⅀ (X ∧ Y)) :=
-  sorry
+sorry