diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean index 9949e34..fb07352 100644 --- a/homotopy/cohomology.hlean +++ b/homotopy/cohomology.hlean @@ -80,7 +80,13 @@ 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) := -sorry /- TODO FOR SSS -/ +begin + apply isomorphism.trans (trunc_ppi_loop_isomorphism (λx, Ω (Y x (n + 2))))⁻¹ᵍ, + apply homotopy_group_isomorphism_of_pequiv 0, esimp, + have q : sub 2 m = n + 2, + from (int.add_comm (of_nat 2) (-m) ⬝ ap (λk, k + of_nat 2) p), + rewrite q, symmetry, apply ppi_loop_pequiv +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) :=