michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

one sorry less: parametrized_cohomology_isomorphism_shomotopy_group_spi

Browse source
This commit is contained in:
Ulrik Buchholtz 2017-07-08 12:22:31 +01:00
parent bc43e079e0
commit 1abb09b062
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
homotopy/cohomology.hlean
View file

@ -80,7 +80,13 @@ sorry /- TODO FOR SSS -/
definition parametrized_cohomology_isomorphism_shomotopy_group_spi {X : Type*} (Y : X → spectrum) 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) := {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} 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) := (Y : X → spectrum) {n m : ℤ} (p : -m = n) : upH^n[(x : X), Y x] ≃g πₛ[m] (supi X Y) :=