work on strunc

homotopy/spectrum.hlean

@@ -32,6 +32,7 @@ structure gen_spectrum (N : succ_str) :=
 
 attribute gen_spectrum.to_prespectrum [coercion]
 attribute gen_spectrum.to_is_spectrum [instance]
+attribute gen_spectrum._trans_of_to_prespectrum [unfold 2]
 
 -- Classically, spectra and prespectra use the successor structure +ℕ.
 -- But we will use +ℤ instead, to reduce case analysis later on.
@@ -240,16 +241,6 @@ namespace spectrum
   definition psp_susp (X : Type*) : gen_prespectrum +ℕ :=
     gen_prespectrum.mk (λn, psuspn n X) (λn, loop_psusp_unit (psuspn n X))
 
-  /- Truncations -/
-
-  -- We could truncate prespectra too, but since the operation
-  -- preserves spectra and isn't "correct" acting on prespectra
-  -- without spectrifying them first anyway, why bother?
-  definition strunc (k : ℕ₋₂) (E : spectrum) : spectrum :=
-    spectrum.Mk (λ(n:ℕ), ptrunc (k + n) (E n))
-      (λ(n:ℕ), (loop_ptrunc_pequiv (k + n) (E (succ n)))⁻¹ᵉ*
-               ∘*ᵉ (ptrunc_pequiv_ptrunc (k + n) (equiv_glue E (int.of_nat n))))
-
   /---------------------
     Homotopy groups
    ---------------------/

homotopy/strunc.hlean

@@ -15,6 +15,8 @@ begin
   induction k with k k, exact ptrunc k X,
   exact plift punit
 end
+-- NB the carrier of ptrunc_int k X is not definitionally 
+-- equal to trunc_int k (carrier X)
 
 definition ptrunc_int_pequiv_ptrunc_int (k : ℤ) {X Y : Type*} (e : X ≃* Y) :
   ptrunc_int k X ≃* ptrunc_int k Y :=
@@ -39,14 +41,86 @@ begin
   exact loop_pequiv_loop !pequiv_plift⁻¹ᵉ* ⬝e* !loop_punit ⬝e* !pequiv_plift
 end
 
-definition strunc_int [constructor] (k : ℤ) (E : spectrum) : spectrum :=
+definition strunc [constructor] (k : ℤ) (E : spectrum) : spectrum :=
 spectrum.MK (λ(n : ℤ), ptrunc_int (k + n) (E n))
             (λ(n : ℤ), ptrunc_int_pequiv_ptrunc_int (k + n) (equiv_glue E n) ⬝e*
                        (loop_ptrunc_int_pequiv (k + n) (E (n+1)))⁻¹ᵉ* ⬝e*
                        loop_pequiv_loop (ptrunc_int_change_int _ (add.assoc k n 1)))
 
-definition strunc_int_change_int [constructor] {k l : ℤ} (E : spectrum) (p : k = l) :
+definition strunc_change_int [constructor] {k l : ℤ} (E : spectrum) (p : k = l) :
-  strunc_int k E →ₛ strunc_int l E :=
+  strunc k E →ₛ strunc l E :=
 begin induction p, reflexivity end
 
+definition is_trunc_int.{u} (k : ℤ) (X : Type.{u}) : Type.{u} :=
+begin
+  induction k with k k,
+  { -- case ≥ 0
+    exact is_trunc k X },
+  { cases k with k,
+    { -- case = -1
+      exact is_trunc -1 X },
+    { -- case < -1
+      exact lift unit } }
+end
+
+definition is_trunc_int_change_int {k l : ℤ} (X : Type) (p : k = l)
+  : is_trunc_int k X → is_trunc_int l X :=
+begin induction p, exact id end
+
+definition is_strunc (k : ℤ) (E : spectrum) : Type :=
+Π (n : ℤ), is_trunc_int (k + n) (E n)
+
+definition is_strunc_change_int {k l : ℤ} (E : spectrum) (p : k = l)
+  : is_strunc k E → is_strunc l E :=
+begin induction p, exact id end
+
+definition is_trunc_trunc_int (k : ℤ) (X : Type)
+  : is_trunc_int k (trunc_int k X) :=
+begin
+  induction k with k k,
+  { -- case ≥ 0
+    exact is_trunc_trunc k X },
+  { cases k with k,
+    { -- case = -1
+      exact is_trunc_trunc -1 X },
+    { -- case < -1
+      exact up unit.star } }
+end
+
+definition is_trunc_ptrunc_int (k : ℤ) (X : pType)
+  : is_trunc_int k (ptrunc_int k X) :=
+begin
+  induction k with k k,
+  { -- case ≥ 0
+    exact is_trunc_trunc k X },
+  { cases k with k,
+    { -- case = -1
+      apply is_trunc_lift, apply is_trunc_unit },
+    { -- case < -1
+      exact up unit.star } }
+end
+
+definition is_strunc_strunc (k : ℤ) (E : spectrum)
+  : is_strunc k (strunc k E) :=
+λ n, is_trunc_ptrunc_int (k + n) (E n)
+
+definition is_strunc_EM_spectrum (G : AbGroup)
+  : is_strunc 0 (EM_spectrum G) :=
+begin
+  intro n, induction n with n n,
+  { -- case ≥ 0
+    apply is_trunc_int_change_int (EM G n) (zero_add n)⁻¹,
+    apply is_trunc_EM },
+  { cases n,
+    { -- case = -1
+      apply is_trunc_loop, exact ab_group.is_set_carrier G },
+    { -- case < -1
+      exact up unit.star }}
+end
+
+definition trivial_shomotopy_group_of_is_strunc (E : spectrum)
+  {n k : ℤ} (K : is_strunc n E) (H : n < k)
+  : is_contr (πₛ[k] E) :=
+sorry
+
 end spectrum