prove two of the sorry's in cohomology

homotopy/cohomology.hlean

@@ -70,14 +70,6 @@ definition cohomology_equiv_shomotopy_group_sp_cotensor (X : Type*) (Y : spectru
 trunc_equiv_trunc 0 (!pfunext ⬝e loop_pequiv_loop !pfunext ⬝e loopn_pequiv_loopn 2
   (pequiv_of_eq (ap (λn, ppmap X (Y n)) (add.comm n 2 ⬝ ap (add 2) !neg_neg⁻¹))))
 
-definition cohomology_isomorphism_shomotopy_group_sp_cotensor (X : Type*) (Y : spectrum) {n m : ℤ}
-  (p : -m = n) : H^n[X, Y] ≃g πₛ[m] (sp_cotensor X Y) :=
-sorry /- TODO FOR SSS -/
-
-definition unreduced_cohomology_isomorphism_shomotopy_group_sp_ucotensor (X : Type) (Y : spectrum)
-  {n m : ℤ} (p : -m = n) : uH^n[X, Y] ≃g πₛ[m] (sp_ucotensor X Y) :=
-sorry /- TODO FOR SSS -/
-
 definition parametrized_cohomology_isomorphism_shomotopy_group_spi {X : Type*} (Y : X → spectrum)
   {n m : ℤ} (p : -m = n) : pH^n[(x : X), Y x] ≃g πₛ[m] (spi X Y) :=
 begin
@@ -90,8 +82,25 @@ end
 
 definition unreduced_parametrized_cohomology_isomorphism_shomotopy_group_supi {X : Type}
   (Y : X → spectrum) {n m : ℤ} (p : -m = n) : upH^n[(x : X), Y x] ≃g πₛ[m] (supi X Y) :=
+begin
+  refine parametrized_cohomology_isomorphism_shomotopy_group_spi (add_point_spectrum Y) p ⬝g _,
+  apply shomotopy_group_isomorphism_of_pequiv, intro k,
+  apply pppi_add_point_over
+end
+
+definition cohomology_isomorphism_shomotopy_group_sp_cotensor (X : Type*) (Y : spectrum) {n m : ℤ}
+  (p : -m = n) : H^n[X, Y] ≃g πₛ[m] (sp_cotensor X Y) :=
 sorry /- TODO FOR SSS -/
 
+definition unreduced_cohomology_isomorphism_shomotopy_group_sp_ucotensor (X : Type) (Y : spectrum)
+  {n m : ℤ} (p : -m = n) : uH^n[X, Y] ≃g πₛ[m] (sp_ucotensor X Y) :=
+begin
+  refine cohomology_isomorphism_shomotopy_group_sp_cotensor X₊ Y p ⬝g _,
+  apply shomotopy_group_isomorphism_of_pequiv, intro k, apply ppmap_add_point
+end
+
+
+
 /- functoriality -/
 
 definition cohomology_functor [constructor] {X X' : Type*} (f : X' →* X) (Y : spectrum)
@@ -133,7 +142,10 @@ sorry /- TODO FOR SSS -/
 
 definition parametrized_cohomology_isomorphism_right {X : Type*} {Y Y' : X → spectrum}
   (e : Πx n, Y x n ≃* Y' x n) (n : ℤ) : pH^n[(x : X), Y x] ≃g pH^n[(x : X), Y' x] :=
-sorry /- TODO FOR SSS -/
+parametrized_cohomology_isomorphism_shomotopy_group_spi Y !neg_neg ⬝g
+shomotopy_group_isomorphism_of_pequiv (-n) (λk, ppi_pequiv_right sorry) ⬝g
+(parametrized_cohomology_isomorphism_shomotopy_group_spi Y' !neg_neg)⁻¹ᵍ
+--sorry /- TODO FOR SSS -/
 
 definition unreduced_parametrized_cohomology_isomorphism_right {X : Type} {Y Y' : X → spectrum}
   (e : Πx n, Y x n ≃* Y' x n) (n : ℤ) : upH^n[(x : X), Y x] ≃g upH^n[(x : X), Y' x] :=

homotopy/spectrum.hlean

@@ -1235,19 +1235,23 @@ spectrify_fun (smash_prespectrum_fun f g)
   spectrum.MK (λn, plift punit) (λn, pequiv_of_is_contr _ _ _ _)
 
   definition shomotopy_group_sunit.{u} (n : ℤ) : πₛ[n] sunit.{u} ≃g trivial_ab_group_lift.{u} :=
-  have H : 0 <[ℕ] 2, from !zero_lt_succ,
-  isomorphism_of_is_contr (@trivial_homotopy_group_of_is_trunc _ _ _ !is_trunc_lift H)
-    !is_trunc_lift
+  phomotopy_group_plift_punit 2
+
+  definition add_point_spectrum [constructor] {X : Type} (Y : X → spectrum) (x : X₊) : spectrum :=
+  spectrum.MK (λn, add_point_over (λx, Y x n) x)
+    begin
+      intro n, induction x with x,
+        apply pequiv_of_is_contr,
+          apply is_trunc_lift,
+        apply is_contr_loop_of_is_contr, apply is_trunc_lift,
+      exact equiv_glue (Y x) n
+    end
 
   open option
-  definition add_point_spectrum [unfold 3] {X : Type} (Y : X → spectrum) : X₊ → spectrum
-  | (some x) := Y x
-  | none     := sunit
-
   definition shomotopy_group_add_point_spectrum {X : Type} (Y : X → spectrum) (n : ℤ) :
     Π(x : X₊), πₛ[n] (add_point_spectrum Y x) ≃g add_point_AbGroup (λ (x : X), πₛ[n] (Y x)) x
   | (some x) := by reflexivity
-  | none     := shomotopy_group_sunit n
+  | none     := proof phomotopy_group_plift_punit 2 qed
 
   /- The Eilenberg-MacLane spectrum -/
 

pointed.hlean

@@ -4,7 +4,7 @@
 
 import types.pointed2 .move_to_lib
 
-open pointed eq equiv function is_equiv unit is_trunc trunc nat algebra sigma group
+open pointed eq equiv function is_equiv unit is_trunc trunc nat algebra sigma group lift option
 
 namespace pointed
 
@@ -227,5 +227,20 @@ namespace pointed
   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
 
+  definition add_point_over [unfold 3] {A : Type} (B : A → Type*) : A₊ → Type*
+  | (some a) := B a
+  | none     := plift punit
+
+  definition phomotopy_group_plift_punit.{u} (n : ℕ) [H : is_at_least_two n] :
+    πag[n] (plift.{0 u} punit) ≃g trivial_ab_group_lift.{u} :=
+  begin
+    induction H with n,
+    have H : 0 <[ℕ] n+2, from !zero_lt_succ,
+    have is_set unit, from _,
+    have is_trunc (trunc_index.of_nat 0) punit, from this,
+    exact isomorphism_of_is_contr (@trivial_homotopy_group_of_is_trunc _ _ _ !is_trunc_lift H)
+      !is_trunc_lift
+  end
+
 
 end pointed

pointed_pi.hlean

@@ -6,7 +6,7 @@ Authors: Ulrik Buchholtz, Floris van Doorn
 
 import homotopy.connectedness types.pointed2 .move_to_lib .pointed
 
-open eq pointed equiv sigma is_equiv trunc
+open eq pointed equiv sigma is_equiv trunc option
 
 /-
   In this file we define dependent pointed maps and properties of them.
@@ -153,8 +153,6 @@ namespace pointed
                    : sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _)
             ...  ≃ (k ~~* l) : ppi_homotopy.sigma_char k l
 
-
-  variables
   -- the same as pmap_eq
   variables {k l}
   definition ppi_eq (h : k ~~* l) : k = l :=
@@ -471,6 +469,28 @@ namespace pointed
   -- definition pppi_ppmap {A C : Type*} {B : A → Type*} :
   --   ppmap (/- dependent smash of B -/) C ≃* Π*(a : A), ppmap (B a) C :=
 
+  definition ppi_add_point_over {A : Type} (B : A → Type*) :
+    (Π*a, add_point_over B a) ≃ Πa, B a :=
+  begin
+    fapply equiv.MK,
+    { intro f a, exact f (some a) },
+    { intro f, fconstructor,
+        intro a, cases a, exact pt, exact f a,
+        reflexivity },
+    { intro f, reflexivity },
+    { intro f, cases f with f p, apply ppi_eq, fapply ppi_homotopy.mk,
+      { intro a, cases a, exact p⁻¹, reflexivity },
+      { exact con.left_inv p }},
+  end
+
+  definition pppi_add_point_over {A : Type} (B : A → Type*) :
+    (Π*a, add_point_over B a) ≃* Πᵘ*a, B a :=
+  pequiv_of_equiv (ppi_add_point_over B) idp
+
+  definition ppmap_add_point {A : Type} (B : Type*) :
+    ppmap A₊ B ≃* A →ᵘ* B :=
+  pequiv_of_equiv (pmap_equiv_left A B) idp
+
   -- TODO: homotopy_of_eq and apd10 should be the same
   -- TODO: there is also apd10_eq_of_homotopy in both pi and eq(?)