From f54011335d9b0d8797338e35410339fc931bbfa5 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Sat, 1 Jul 2017 20:02:31 +0100
Subject: [PATCH] define atiyah-hirzebruch exact couple

this commit also defines str and strunc_elim
proving that the exact couple is bounded, and that it converges to the right this is still todo
---
 homotopy/serre.hlean  |  89 ++++++++++++-------------------
 homotopy/strunc.hlean | 119 ++++++++++++++++++++++++++++++------------
 move_to_lib.hlean     |  78 +++++++++++++++++----------
 pointed.hlean         |   7 ++-
 4 files changed, 177 insertions(+), 116 deletions(-)

diff --git a/homotopy/serre.hlean b/homotopy/serre.hlean
index 4946217..eb19084 100644
--- a/homotopy/serre.hlean
+++ b/homotopy/serre.hlean
@@ -1,6 +1,6 @@
 import ..algebra.module_exact_couple .strunc
 
-open eq spectrum trunc is_trunc pointed int EM algebra left_module fiber lift
+open eq spectrum trunc is_trunc pointed int EM algebra left_module fiber lift equiv is_equiv
 
 /- Eilenberg MacLane spaces are the fibers of the Postnikov system of a type -/
 
@@ -37,6 +37,14 @@ definition postnikov_map_natural {A B : Type*} (f : A →* B) (n : ℕ₋₂) :
           (ptrunc_functor (n.+1) f) (ptrunc_functor n f) :=
 !ptrunc_functor_postnikov_map ⬝* !ptrunc_elim_ptrunc_functor⁻¹*
 
+definition is_equiv_postnikov_map (A : Type*) {n k : ℕ₋₂} [HA : is_trunc k A] (H : k ≤ n) :
+  is_equiv (postnikov_map A n) :=
+begin
+  apply is_equiv_of_equiv_of_homotopy
+    (ptrunc_pequiv_ptrunc_of_is_trunc (trunc_index.le.step H) H HA),
+  intro x, induction x, reflexivity
+end
+
 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
@@ -54,63 +62,34 @@ begin
 end,
 this⁻¹ᵛ*
 
+definition is_strunc_strunc_pred (X : spectrum) (k : ℤ) : is_strunc k (strunc (k - 1) X) :=
+λn, @(is_trunc_of_le _ (maxm2_monotone (add_le_add_right (sub_one_le k) n))) !is_strunc_strunc
 
--- 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_smap [constructor] (X : spectrum) (k : ℤ) :
+  strunc k X →ₛ strunc (k - 1) X :=
+strunc_elim (str (k - 1) X) (is_strunc_strunc_pred X k)
 
--- 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_smap_phomotopy [constructor] (X : spectrum) (k : ℤ) (n : ℤ) :
+  postnikov_smap X k n ~* postnikov_map (X n) (maxm2 (k - 1 + n)) ∘*
+  sorry :=
+sorry
 
--- 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
+section atiyah_hirzebruch
+  parameters {X : Type*} (Y : X → spectrum) (s₀ : ℤ) (H : Πx, is_strunc s₀ (Y x))
 
--- 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 atiyah_hirzebruch_exact_couple : exact_couple rℤ Z2 :=
+  @exact_couple_sequence (λs, strunc s (spi X Y)) (postnikov_smap (spi X Y))
 
--- 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 is_bounded_atiyah_hirzebruch : is_bounded atiyah_hirzebruch_exact_couple :=
+  is_bounded_sequence _ s₀ (λn, n - 1)
+    begin
+      intro s n H,
+      exact sorry
+    end
+    begin
+      intro s n H, apply trivial_shomotopy_group_of_is_strunc,
+        apply is_strunc_strunc,
+      exact lt_of_le_sub_one H,
+    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
+end atiyah_hirzebruch
diff --git a/homotopy/strunc.hlean b/homotopy/strunc.hlean
index 677decd..0acf418 100644
--- a/homotopy/strunc.hlean
+++ b/homotopy/strunc.hlean
@@ -1,10 +1,9 @@
 import .spectrum .EM
 
--- TODO move this
-open trunc_index nat
-
 namespace int
 
+  -- TODO move this
+  open trunc_index nat algebra
   section
   private definition maxm2_le.lemma₁ {n k : ℕ} : n+(1:int) + -[1+ k] ≤ n :=
   le.intro (
@@ -39,13 +38,29 @@ open int trunc eq is_trunc lift unit pointed equiv is_equiv algebra EM
 
 namespace spectrum
 
-definition ptrunc_maxm2_change_int {k l : ℤ} (X : Type*) (p : k = l)
+definition ptrunc_maxm2_change_int {k l : ℤ} (p : k = l) (X : Type*)
   : ptrunc (maxm2 k) X ≃* ptrunc (maxm2 l) X :=
 pequiv_ap (λ n, ptrunc (maxm2 n) X) p
 
-definition loop_ptrunc_maxm2_pequiv (k : ℤ) (X : Type*) :
-  Ω (ptrunc (maxm2 (k+1)) X) ≃* ptrunc (maxm2 k) (Ω X) :=
+definition is_trunc_maxm2_change_int {k l : ℤ} (X : pType) (p : k = l)
+  : is_trunc (maxm2 k) X → is_trunc (maxm2 l) X :=
+by induction p; exact id
+
+definition is_trunc_maxm2_loop {k : ℤ} {A : Type*} (H : is_trunc (maxm2 (k+1)) A) :
+  is_trunc (maxm2 k) (Ω A) :=
 begin
+  induction k with k k,
+    apply is_trunc_loop, exact H,
+  apply is_contr_loop,
+  cases k with k,
+  { exact H },
+  { apply is_trunc_succ, apply is_trunc_succ, exact H }
+end
+
+definition loop_ptrunc_maxm2_pequiv {k : ℤ} {l : ℕ₋₂} (p : maxm2 (k+1) = l) (X : Type*) :
+  Ω (ptrunc l X) ≃* ptrunc (maxm2 k) (Ω X) :=
+begin
+  induction p,
   induction k with k k,
   { exact loop_ptrunc_pequiv k X },
   { refine pequiv_of_is_contr _ _ _ !is_trunc_trunc,
@@ -55,6 +70,43 @@ begin
     { change is_set (trunc -2 X), apply _ }}
 end
 
+definition ptrunc_elim_phomotopy2 [constructor] (k : ℕ₋₂) {A B : Type*} {f g : A →* B} (H₁ : is_trunc k B)
+  (H₂ : is_trunc k B) (p : f ~* g) : @ptrunc.elim k A B H₁ f ~* @ptrunc.elim k A B H₂ g :=
+begin
+  fapply phomotopy.mk,
+  { intro x, induction x with a, exact p a },
+  { exact to_homotopy_pt p }
+end
+
+definition loop_ptrunc_maxm2_pequiv_ptrunc_elim' {k : ℤ} {l : ℕ₋₂} (p : maxm2 (k+1) = l)
+  {A B : Type*} (f : A →* B) {H : is_trunc l B} :
+  Ω→ (ptrunc.elim l f) ∘* (loop_ptrunc_maxm2_pequiv p A)⁻¹ᵉ* ~*
+  @ptrunc.elim (maxm2 k) _ _ (is_trunc_maxm2_loop (is_trunc_of_eq p⁻¹ H)) (Ω→ f) :=
+begin
+  induction p, induction k with k k,
+  { refine pwhisker_right _ (ap1_phomotopy _) ⬝* @(ap1_ptrunc_elim k f) H,
+    apply ptrunc_elim_phomotopy2, reflexivity },
+  { apply phomotopy_of_is_contr_cod, exact is_trunc_maxm2_loop H }
+end
+
+definition loop_ptrunc_maxm2_pequiv_ptrunc_elim {k : ℤ} {l : ℕ₋₂} (p : maxm2 (k+1) = l)
+  {A B : Type*} (f : A →* B) {H1 : is_trunc ((maxm2 k).+1) B } {H2 : is_trunc l B} :
+  Ω→ (ptrunc.elim l f) ∘* (loop_ptrunc_maxm2_pequiv p A)⁻¹ᵉ* ~* ptrunc.elim (maxm2 k) (Ω→ f) :=
+begin
+  induction p, induction k with k k: esimp at H1,
+  { refine pwhisker_right _ (ap1_phomotopy _) ⬝* ap1_ptrunc_elim k f,
+    apply ptrunc_elim_phomotopy2, reflexivity },
+  { apply phomotopy_of_is_contr_cod }
+end
+
+definition loop_ptrunc_maxm2_pequiv_ptr {k : ℤ} {l : ℕ₋₂} (p : maxm2 (k+1) = l) (A : Type*) :
+  Ω→ (ptr l A) ~* (loop_ptrunc_maxm2_pequiv p A)⁻¹ᵉ* ∘* ptr (maxm2 k) (Ω A) :=
+begin
+  induction p, induction k with k k,
+  { exact ap1_ptr k A },
+  { apply phomotopy_pinv_left_of_phomotopy, apply phomotopy_of_is_contr_cod, apply is_trunc_trunc }
+end
+
 definition is_trunc_of_is_trunc_maxm2 (k : ℤ) (X : Type)
   : is_trunc (maxm2 k) X → is_trunc (max0 k) X :=
 λ H, @is_trunc_of_le X _ _ (maxm2_le_maxm0 k) H
@@ -62,24 +114,12 @@ definition is_trunc_of_is_trunc_maxm2 (k : ℤ) (X : Type)
 definition strunc [constructor] (k : ℤ) (E : spectrum) : spectrum :=
 spectrum.MK (λ(n : ℤ), ptrunc (maxm2 (k + n)) (E n))
             (λ(n : ℤ), ptrunc_pequiv_ptrunc (maxm2 (k + n)) (equiv_glue E n)
-              ⬝e* (loop_ptrunc_maxm2_pequiv (k + n) (E (n+1)))⁻¹ᵉ*
-              ⬝e* (loop_pequiv_loop
-                   (ptrunc_maxm2_change_int _ (add.assoc k n 1))))
+              ⬝e* (loop_ptrunc_maxm2_pequiv (ap maxm2 (add.assoc k n 1)) (E (n+1)))⁻¹ᵉ*)
 
 definition strunc_change_int [constructor] {k l : ℤ} (E : spectrum) (p : k = l) :
   strunc k E →ₛ strunc l E :=
 begin induction p, reflexivity end
 
-definition is_trunc_maxm2_loop (A : pType) (k : ℤ)
-  : is_trunc (maxm2 (k + 1)) A → is_trunc (maxm2 k) (Ω A) :=
-begin
-  intro H, induction k with k k,
-  { apply is_trunc_loop, exact H },
-  { apply is_contr_loop, cases k with k,
-    { exact H },
-    { have H2 : is_contr A, from H, apply _ } }
-end
-
 definition is_strunc [reducible] (k : ℤ) (E : spectrum) : Type :=
 Π (n : ℤ), is_trunc (maxm2 (k + n)) (E n)
 
@@ -98,13 +138,36 @@ definition is_strunc_strunc (k : ℤ) (E : spectrum)
   : is_strunc k (strunc k E) :=
 λ n, is_trunc_trunc (maxm2 (k + n)) (E n)
 
-definition is_trunc_maxm2_change_int {k l : ℤ} (X : pType) (p : k = l)
-  : is_trunc (maxm2 k) X → is_trunc (maxm2 l) X :=
-by induction p; exact id
+definition str [constructor] (k : ℤ) (E : spectrum) : E →ₛ strunc k E :=
+smap.mk (λ n, ptr (maxm2 (k + n)) (E n))
+  abstract begin
+    intro n,
+    apply psquare_of_phomotopy,
+    refine !passoc ⬝* pwhisker_left _ !ptr_natural ⬝* _,
+    refine !passoc⁻¹* ⬝* pwhisker_right _ !loop_ptrunc_maxm2_pequiv_ptr⁻¹*,
+  end end
+
+definition strunc_elim [constructor] {k : ℤ} {E F : spectrum} (f : E →ₛ F)
+  (H : is_strunc k F) : strunc k E →ₛ F :=
+smap.mk (λn, ptrunc.elim (maxm2 (k + n)) (f n))
+  abstract begin
+    intro n,
+    apply psquare_of_phomotopy,
+    symmetry,
+    refine !passoc⁻¹* ⬝* pwhisker_right _ !loop_ptrunc_maxm2_pequiv_ptrunc_elim' ⬝* _,
+    refine @(ptrunc_elim_ptrunc_functor _ _ _) _ ⬝* _,
+    refine _ ⬝* @(ptrunc_elim_pcompose _ _ _) _ _,
+      apply is_trunc_maxm2_loop,
+      refine is_trunc_of_eq _ (H (n+1)), exact ap maxm2 (add.assoc k n 1)⁻¹,
+    apply ptrunc_elim_phomotopy2,
+    apply phomotopy_of_psquare,
+    apply ptranspose,
+    apply smap.glue_square
+  end end
 
 definition strunc_functor [constructor] (k : ℤ) {E F : spectrum} (f : E →ₛ F) :
   strunc k E →ₛ strunc k F :=
-smap.mk (λn, ptrunc_functor (maxm2 (k + n)) (f n)) sorry
+strunc_elim (str k F ∘ₛ f) (is_strunc_strunc k F)
 
 definition is_strunc_EM_spectrum (G : AbGroup)
   : is_strunc 0 (EM_spectrum G) :=
@@ -121,11 +184,6 @@ begin
       apply is_trunc_loop, apply is_trunc_succ, exact IH }}
 end
 
-definition strunc_elim [constructor] {k : ℤ} {E F : spectrum} (f : E →ₛ F)
-  (H : is_strunc k F) : strunc k E →ₛ F :=
-smap.mk (λn, ptrunc.elim (maxm2 (k + n)) (f n))
-        (λn, sorry)
-
 definition trivial_shomotopy_group_of_is_strunc (E : spectrum)
   {n k : ℤ} (K : is_strunc n E) (H : n < k)
   : is_contr (πₛ[k] E) :=
@@ -139,11 +197,6 @@ have I : m < 2, from
   (is_trunc_of_is_trunc_maxm2 m (E (2 - k)) (K (2 - k)))
   (nat.succ_le_succ (max0_le_of_le (le_sub_one_of_lt I)))
 
-definition str [constructor] (k : ℤ) (E : spectrum) : E →ₛ strunc k E :=
-smap.mk (λ n, ptr (maxm2 (k + n)) (E n))
-  (λ n, sorry)
-
-
 structure truncspectrum (n : ℤ) :=
   (carrier : spectrum)
   (struct : is_strunc n carrier)
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 217faf4..dee29bd 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -209,38 +209,24 @@ namespace int
     { exact nat.zero_le m }
   end
 
-  section
-  -- is there a way to get this from int.add_assoc?
-  private definition maxm2_monotone.lemma₁ {n k : ℕ}
-    : k + n + (1:int) = k + (1:int) + n :=
-  begin
-    induction n with n IH,
-    { reflexivity },
-    { exact ap (λ z, z + 1) IH }
-  end
+  definition not_neg_succ_le_of_nat {n m : ℕ} : ¬m ≤ -[1+n] :=
+  by cases m: exact id
 
-  private definition maxm2_monotone.lemma₂ {n k : ℕ} : ¬ n ≤ -[1+ k] :=
-  int.not_le_of_gt (lt.intro
-    (calc -[1+ k] + (succ (k + n))
-         = -(k+1) + (k + n + 1) : by reflexivity
-     ... = -(k+1) + (k + 1 + n) : maxm2_monotone.lemma₁
-     ... = (-(k+1) + (k+1)) + n : int.add_assoc
-     ... = (0:int) + n          : by rewrite int.add_left_inv
-     ... = n                    : int.zero_add))
-
-  definition maxm2_monotone {n k : ℤ} : n ≤ k → maxm2 n ≤ maxm2 k :=
+  definition maxm2_monotone {n m : ℤ} (H : n ≤ m) : maxm2 n ≤ maxm2 m :=
   begin
-    intro H,
     induction n with n n,
-    { induction k with k k,
-      { exact trunc_index.of_nat_monotone (le_of_of_nat_le_of_nat H) },
-      { exact empty.elim (maxm2_monotone.lemma₂ H) } },
-    { induction k with k k,
-      { apply minus_two_le },
-      { apply le.tr_refl } }
-  end
+    { induction m with m m,
+      { apply of_nat_le_of_nat, exact le_of_of_nat_le_of_nat H },
+      { exfalso, exact not_neg_succ_le_of_nat H }},
+    { apply minus_two_le }
   end
 
+  definition sub_nat_le (n : ℤ) (m : ℕ) : n - m ≤ n :=
+  le.intro !sub_add_cancel
+
+  definition sub_one_le (n : ℤ) : n - 1 ≤ n :=
+  sub_nat_le n 1
+
 end int
 
 namespace pmap
@@ -286,6 +272,44 @@ namespace trunc
     { apply idp_con }
   end
 
+  definition ptrunc_elim_ptr_phomotopy_pid (n : ℕ₋₂) (A : Type*):
+    ptrunc.elim n (ptr n A) ~* pid (ptrunc n A) :=
+  begin
+    fapply phomotopy.mk,
+    { intro a, induction a with a, reflexivity },
+    { apply idp_con }
+  end
+
+  definition is_trunc_of_eq {n m : ℕ₋₂} (p : n = m) {A : Type} (H : is_trunc n A) : is_trunc m A :=
+  transport (λk, is_trunc k A) p H
+
+  definition is_trunc_ptrunc_of_is_trunc [instance] [priority 500] (A : Type*)
+    (n m : ℕ₋₂) [H : is_trunc n A] : is_trunc n (ptrunc m A) :=
+  is_trunc_trunc_of_is_trunc A n m
+
+  definition ptrunc_pequiv_ptrunc_of_is_trunc {n m k : ℕ₋₂} {A : Type*}
+    (H1 : n ≤ m) (H2 : n ≤ k) (H : is_trunc n A) : ptrunc m A ≃* ptrunc k A :=
+  have is_trunc m A, from is_trunc_of_le A H1,
+  have is_trunc k A, from is_trunc_of_le A H2,
+  pequiv.MK (ptrunc.elim _ (ptr k A)) (ptrunc.elim _ (ptr m A))
+    abstract begin
+      refine !ptrunc_elim_pcompose⁻¹* ⬝* _,
+      exact ptrunc_elim_phomotopy _ !ptrunc_elim_ptr ⬝* !ptrunc_elim_ptr_phomotopy_pid,
+    end end
+    abstract begin
+      refine !ptrunc_elim_pcompose⁻¹* ⬝* _,
+      exact ptrunc_elim_phomotopy _ !ptrunc_elim_ptr ⬝* !ptrunc_elim_ptr_phomotopy_pid,
+    end end
+
+  definition ptrunc_change_index {k l : ℕ₋₂} (p : k = l) (X : Type*)
+    : ptrunc k X ≃* ptrunc l X :=
+  pequiv_ap (λ n, ptrunc n X) p
+
+  definition ptrunc_functor_le {k l : ℕ₋₂} (p : l ≤ k) (X : Type*)
+    : ptrunc k X →* ptrunc l X :=
+  have is_trunc k (ptrunc l X), from is_trunc_of_le _ p,
+  ptrunc.elim _ (ptr l X)
+
 end trunc
 
 namespace sigma
diff --git a/pointed.hlean b/pointed.hlean
index f1e1e85..355125e 100644
--- a/pointed.hlean
+++ b/pointed.hlean
@@ -204,10 +204,15 @@ namespace pointed
   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] :
+  definition phomotopy_of_is_contr_cod [constructor] {X Y : Type*} (f g : X →* Y) [is_contr Y] :
     f ~* g :=
   phomotopy.mk (λa, !eq_of_is_contr) !eq_of_is_contr
 
+  definition phomotopy_of_is_contr_dom [constructor] {X Y : Type*} (f g : X →* Y) [is_contr X] :
+    f ~* g :=
+  phomotopy.mk (λa, ap f !is_prop.elim ⬝ respect_pt f ⬝ (respect_pt g)⁻¹ ⬝ ap g !is_prop.elim)
+    begin rewrite [▸*, is_prop_elim_self, +ap_idp, idp_con, con_idp, inv_con_cancel_right] end
+
 
 
 end pointed