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

compute fibers of postnikov tower

Browse source
This commit is contained in:
Floris van Doorn 2017-06-14 20:04:35 -04:00
parent da95ea0acb
commit b6fa4e8716
1 changed files with 32 additions and 44 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

76
homotopy/EM.hlean
View file

@ -565,58 +565,42 @@ namespace EM
open fiber EM.ops
-- definition loopn_succ_pfiber_postnikov_map (A : Type*) (k : ℕ) (n : ℕ₋₂) :
-- Ω[k+1] (pfiber (postnikov_map A (n.+1))) ≃* Ω[k] (pfiber (postnikov_map (Ω A) n)) :=
-- begin
-- exact sorry
-- end
-- definition loopn_pfiber_postnikov_map (A : Type*) (n : ℕ) :
-- Ω[n] (pfiber (postnikov_map A n)) ≃* EM1 (πg[n+1] A) :=
-- begin
-- revert A, induction n with n IH: intro A,
-- { apply pfiber_postnikov_map_zero },
-- exact loopn_succ_pfiber_postnikov_map A n n ⬝e* IH (Ω A) ⬝e*
-- EM1_pequiv_EM1 !ghomotopy_group_succ_in⁻¹ᵍ
-- end
-- move
definition pgroup_of_Group (X : Group) : pgroup X :=
pgroup_of_group _ idp
open prod chain_complex succ_str fin
definition isomorphism_of_trivial_LES {A B : Type*} (f : A →* B) (n : ℕ)
(k : fin (nat.succ 2)) (HX1 : is_contr (homotopy_groups f (n+1, k)))
(HX2 : is_contr (homotopy_groups f (n+2, k))) :
Group_LES_of_homotopy_groups f (@S +3ℕ (S (n, k))) ≃g Group_LES_of_homotopy_groups f (S (n, k)) :=
begin
induction k with k Hk,
cases k with k, rotate 1, cases k with k, rotate 1, cases k with k, rotate 1,
exfalso, apply lt_le_antisymm Hk, apply le_add_left,
all_goals exact let k := fin.mk _ Hk in let x : +3ℕ := (n, k) in let S : +3ℕ → +3ℕ := succ_str.S in
let z :=
@is_equiv_of_trivial _
(LES_of_homotopy_groups f) _
(is_exact_LES_of_homotopy_groups f (n+1, k))
(is_exact_LES_of_homotopy_groups f (S (n+1, k)))
HX1 HX2
(pgroup_of_Group (Group_LES_of_homotopy_groups f (S x)))
(pgroup_of_Group (Group_LES_of_homotopy_groups f (S (S x))))
(homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun f (S x))) in
isomorphism.mk (homomorphism_LES_of_homotopy_groups_fun f _) z
end
-- open prod chain_complex succ_str fin
-- definition isomorphism_of_trivial_LES {A B : Type*} (f : A →* B) (n : ℕ)
-- (k : fin (nat.succ 2)) (HX1 : is_contr (homotopy_groups f (n+1, k)))
-- (HX2 : is_contr (homotopy_groups f (n+2, k))) :
-- Group_LES_of_homotopy_groups f (@S +3ℕ (S (n, k))) ≃g Group_LES_of_homotopy_groups f (S (n, k)) :=
-- begin
-- induction k with k Hk,
-- cases k with k, rotate 1, cases k with k, rotate 1, cases k with k, rotate 1,
-- exfalso, apply lt_le_antisymm Hk, apply le_add_left,
-- all_goals exact let k := fin.mk _ Hk in let x : +3ℕ := (n, k) in let S : +3ℕ → +3ℕ := succ_str.S in
-- let z :=
-- @is_equiv_of_trivial _
-- (LES_of_homotopy_groups f) _
-- (is_exact_LES_of_homotopy_groups f (n+1, k))
-- (is_exact_LES_of_homotopy_groups f (S (n+1, k)))
-- HX1 HX2
-- (pgroup_of_Group (Group_LES_of_homotopy_groups f (S x)))
-- (pgroup_of_Group (Group_LES_of_homotopy_groups f (S (S x))))
-- (homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun f (S x))) in
-- isomorphism.mk (homomorphism_LES_of_homotopy_groups_fun f _) z
-- end
definition pfiber_postnikov_map_zero (A : Type*) :
pfiber (postnikov_map A 0) ≃* EM1 (πg[1] A) :=
begin
symmetry, apply EM1_pequiv,
{ symmetry, note z := isomorphism_of_trivial_LES (postnikov_map A 0) 1 0
(trivial_homotopy_group_of_is_trunc (ptrunc 0 A) !zero_lt_succ)
(trivial_homotopy_group_of_is_trunc (ptrunc 0 A) !zero_lt_succ), exact sorry
-- rexact isomorphism_of_equiv (equiv_of_isomorphism z) sorry
},
{ symmetry, refine _ ⬝g ghomotopy_group_ptrunc 1 A,
exact chain_complex.LES_isomorphism_of_trivial_cod _ _
(trivial_homotopy_group_of_is_trunc _ !zero_lt_one)
(trivial_homotopy_group_of_is_trunc _ (zero_lt_succ 1)) },
{ apply @is_conn_fun_trunc_elim, apply is_conn_fun_tr },
{ apply is_trunc_pfiber }
end
@ -624,9 +608,13 @@ namespace EM
definition pfiber_postnikov_map_succ (A : Type*) (n : ℕ) :
pfiber (postnikov_map A (n+1)) ≃* EMadd1 (πag[n+2] A) (n+1) :=
begin
apply pequiv_EMadd1_of_loopn_pequiv_EM1,
{ exact sorry },
{ apply is_conn_fun_trunc_elim, apply is_conn_fun_tr }
symmetry, apply EMadd1_pequiv,
{ refine _ ⬝g ghomotopy_group_ptrunc (n+2) A,
exact chain_complex.LES_isomorphism_of_trivial_cod _ _
(trivial_homotopy_group_of_is_trunc _ (self_lt_succ (n+1)))
(trivial_homotopy_group_of_is_trunc _ (le_succ _)) },
{ apply is_conn_fun_trunc_elim, apply is_conn_fun_tr },
{ apply is_trunc_pfiber }
end