From 9ad673682d160e6fd55123d0c6f4a469016532b7 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 26 May 2017 05:17:02 -0400 Subject: [PATCH] add stuff about Postnikov towers, EM-spaces and components --- homotopy/EM.hlean | 95 +++++++++++++++++++++++++++++++++------ move_to_lib.hlean | 112 +++++++++++++++++++++++++++++++++++++++++----- 2 files changed, 184 insertions(+), 23 deletions(-) diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean index 501cac6..ae44ca1 100644 --- a/homotopy/EM.hlean +++ b/homotopy/EM.hlean @@ -499,6 +499,65 @@ namespace EM equivalence.mk (EM_cfunctor (n+2)) (is_equivalence_EM_cfunctor n) end category + /- move -/ + -- switch arguments in homotopy_group_trunc_of_le + lemma ghomotopy_group_trunc_of_le (k n : ℕ) (A : Type*) [Hk : is_succ k] (H : k ≤[ℕ] n) + : πg[k] (ptrunc n A) ≃g πg[k] A := + begin + exact sorry + end + + lemma homotopy_group_isomorphism_of_ptrunc_pequiv {A B : Type*} + (n k : ℕ) (H : n+1 ≤[ℕ] k) (f : ptrunc k A ≃* ptrunc k B) : πg[n+1] A ≃g πg[n+1] B := + (ghomotopy_group_trunc_of_le _ k A H)⁻¹ᵍ ⬝g + homotopy_group_isomorphism_of_pequiv n f ⬝g + ghomotopy_group_trunc_of_le _ k B H + + open trunc_index + lemma minus_two_add_plus_two (n : ℕ₋₂) : -2+2+n = n := + by induction n with n p; reflexivity; exact ap succ p + + definition is_trunc_succ_of_is_trunc_loop (n : ℕ₋₂) (A : Type*) (H : is_trunc (n.+1) (Ω A)) + (H2 : is_conn 0 A) : is_trunc (n.+2) A := + begin + apply is_trunc_succ_of_is_trunc_loop, apply minus_one_le_succ, + refine is_conn.elim -1 _ _, exact H + end + + lemma is_trunc_of_is_trunc_loopn (m n : ℕ) (A : Type*) (H : is_trunc n (Ω[m] A)) + (H2 : is_conn m A) : is_trunc (m + n) A := + begin + revert A H H2; induction m with m IH: intro A H H2, + { rewrite [nat.zero_add], exact H }, + rewrite [succ_add], + apply is_trunc_succ_of_is_trunc_loop, + { apply IH, + { apply is_trunc_equiv_closed _ !loopn_succ_in }, + apply is_conn_loop }, + exact is_conn_of_le _ (zero_le_of_nat (succ m)) + end + + lemma is_trunc_of_is_set_loopn (m : ℕ) (A : Type*) (H : is_set (Ω[m] A)) + (H2 : is_conn m A) : is_trunc m A := + is_trunc_of_is_trunc_loopn m 0 A H H2 + + definition pequiv_EMadd1_of_loopn_pequiv_EM1 {G : AbGroup} {X : Type*} (n : ℕ) (e : Ω[n] X ≃* EM1 G) + [H1 : is_conn n X] : X ≃* EMadd1 G n := + begin + symmetry, apply EMadd1_pequiv, + refine isomorphism_of_eq (ap (λx, πg[x+1] X) !zero_add⁻¹) ⬝g homotopy_group_add X 0 n ⬝g _ ⬝g + !fundamental_group_EM1, + exact homotopy_group_isomorphism_of_pequiv 0 e, + refine is_trunc_of_is_trunc_loopn n 1 X _ _, + apply is_trunc_equiv_closed_rev 1 e + end + + definition EM1_pequiv_EM1 {G H : Group} (φ : G ≃g H) : EM1 G ≃* EM1 H := + sorry + + definition EMadd1_pequiv_EMadd1 (n : ℕ) {G H : AbGroup} (φ : G ≃g H) : EMadd1 G n ≃* EMadd1 H n := + sorry + /- Eilenberg MacLane spaces are the fibers of the Postnikov system of a type -/ definition postnikov_map [constructor] (A : Type*) (n : ℕ₋₂) : ptrunc (n.+1) A →* ptrunc n A := @@ -507,30 +566,40 @@ 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)) := + Ω[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+1] (pfiber (postnikov_map A n)) ≃* ptrunc 0 A := + definition pfiber_postnikov_map_zero (A : Type*) : + pfiber (postnikov_map A 0) ≃* EM1 (πg[1] A) := begin - induction n with n IH, - { exact loopn_succ_pfiber_postnikov_map A 0 -1 ⬝e* !pfiber_pequiv_of_is_prop }, - exact loopn_succ_pfiber_postnikov_map A (n+1) n ⬝e* IH + symmetry, apply EM1_pequiv, + { refine !homotopy_group_component⁻¹ᵍ ⬝g _, + apply homotopy_group_isomorphism_of_ptrunc_pequiv, exact le.refl 1, symmetry, + refine !ptrunc_pequiv ⬝e* _, + exact sorry + }, + { apply @is_conn_fun_trunc_elim, apply is_conn_fun_tr } + 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 definition pfiber_postnikov_map_succ (A : Type*) (n : ℕ) : pfiber (postnikov_map A (n+1)) ≃* EMadd1 (πag[n+2] A) (n+1) := begin - symmetry, apply EMadd1_pequiv, - { }, - { apply @is_conn_fun_trunc_elim, apply is_conn_fun_tr } + apply pequiv_EMadd1_of_loopn_pequiv_EM1, + { exact sorry }, + { apply is_conn_fun_trunc_elim, apply is_conn_fun_tr } end - definition pfiber_postnikov_map_zero (A : Type*) : pfiber (postnikov_map A 0) ≃* EM1 (πg[1] A) := - begin - exact sorry - end end EM diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 8356091..2e9ca17 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -954,6 +954,7 @@ namespace fiber Ω→ (ppoint f) ∘* (loop_pfiber f)⁻¹ᵉ* ~* ppoint (Ω→ f) := (phomotopy_pinv_right_of_phomotopy (ppoint_loop_pfiber f))⁻¹* + -- rename to pfiber_pequiv_... lemma pfiber_equiv_of_phomotopy_ppoint {A B : Type*} {f g : A →* B} (h : f ~* g) : ppoint g ∘* pfiber_equiv_of_phomotopy h ~* ppoint f := begin @@ -1005,19 +1006,13 @@ namespace fiber [is_trunc n A] [is_trunc (n.+1) B] : is_trunc n (pfiber f) := is_trunc_fiber n f pt - definition fiber_equiv_of_is_prop [constructor] {A B : Type} (f : A → B) (b : B) [is_prop B] : + definition fiber_equiv_of_is_contr [constructor] {A B : Type} (f : A → B) (b : B) [is_contr B] : fiber f b ≃ A := - begin - fapply equiv.MK, - { intro f, cases f with a H, exact a }, - { intro a, apply fiber.mk a, apply is_prop.elim }, - { intro a, reflexivity }, - { intro f, cases f with a H, apply ap (fiber.mk a) !is_prop.elim } - end + !fiber.sigma_char ⬝e !sigma_equiv_of_is_contr_right - definition pfiber_pequiv_of_is_prop [constructor] {A B : Type*} (f : A →* B) [is_prop B] : + definition pfiber_pequiv_of_is_contr [constructor] {A B : Type*} (f : A →* B) [is_contr B] : pfiber f ≃* A := - pequiv_of_equiv (fiber_equiv_of_is_prop f pt) idp + pequiv_of_equiv (fiber_equiv_of_is_contr f pt) idp end fiber @@ -1181,6 +1176,103 @@ namespace is_conn cases A with A a, exact H k H2 end + /- move! -/ + open sigma.ops pointed + definition merely_constant {A B : Type} (f : A → B) : Type := + Σb, Πa, merely (f a = b) + + definition merely_constant_pmap {A B : Type*} {f : A →* B} (H : merely_constant f) (a : A) : + merely (f a = pt) := + tconcat (tconcat (H.2 a) (tinverse (H.2 pt))) (tr (respect_pt f)) + + definition merely_constant_of_is_conn {A B : Type*} (f : A →* B) [is_conn 0 A] : merely_constant f := + ⟨pt, is_conn.elim -1 _ (tr (respect_pt f))⟩ + + open sigma + definition component [constructor] (A : Type*) : Type* := + pType.mk (Σ(a : A), merely (pt = a)) ⟨pt, tr idp⟩ + + lemma is_conn_component [instance] (A : Type*) : is_conn 0 (component A) := + is_contr.mk (tr pt) + begin + intro x, induction x with x, induction x with a p, induction p with p, induction p, reflexivity + end + + definition component_incl [constructor] (A : Type*) : component A →* A := + pmap.mk pr1 idp + + definition component_intro [constructor] {A B : Type*} (f : A →* B) (H : merely_constant f) : + A →* component B := + begin + fapply pmap.mk, + { intro a, refine ⟨f a, _⟩, exact tinverse (merely_constant_pmap H a) }, + exact subtype_eq !respect_pt + end + + definition component_functor [constructor] {A B : Type*} (f : A →* B) : component A →* component B := + component_intro (f ∘* component_incl A) !merely_constant_of_is_conn + + -- definition component_elim [constructor] {A B : Type*} (f : A →* B) (H : merely_constant f) : + -- A →* component B := + -- begin + -- fapply pmap.mk, + -- { intro a, refine ⟨f a, _⟩, exact tinverse (merely_constant_pmap H a) }, + -- exact subtype_eq !respect_pt + -- end + + /- move!-/ + lemma is_equiv_ap1_of_is_embedding {A B : Type*} (f : A →* B) [is_embedding f] : + is_equiv (Ω→ f) := + sorry + + definition loop_pequiv_loop_of_is_embedding [constructor] {A B : Type*} (f : A →* B) [is_embedding f] : + Ω A ≃* Ω B := + pequiv_of_pmap (Ω→ f) (is_equiv_ap1_of_is_embedding f) + + definition loop_component (A : Type*) : Ω (component A) ≃* Ω A := + have is_embedding (component_incl A), from is_embedding_pr1 _, + loop_pequiv_loop_of_is_embedding (component_incl A) + + lemma loopn_component (n : ℕ) (A : Type*) : Ω[n+1] (component A) ≃* Ω[n+1] A := + !loopn_succ_in ⬝e* loopn_pequiv_loopn n (loop_component A) ⬝e* !loopn_succ_in⁻¹ᵉ* + + -- lemma fundamental_group_component (A : Type*) : π₁ (component A) ≃g π₁ A := + -- isomorphism_of_equiv (trunc_equiv_trunc 0 (loop_component A)) _ + + lemma homotopy_group_component (n : ℕ) (A : Type*) : πg[n+1] (component A) ≃g πg[n+1] A := + sorry + + definition is_trunc_component [instance] (n : ℕ₋₂) (A : Type*) [is_trunc n A] : is_trunc n (component A) := + begin + apply @is_trunc_sigma, intro a, cases n with n, + { apply is_contr_of_inhabited_prop, exact tr !is_prop.elim }, + { apply is_trunc_succ_of_is_prop }, + end + + definition ptrunc_component' (n : ℕ₋₂) (A : Type*) : + ptrunc (n.+2) (component A) ≃* component (ptrunc (n.+2) A) := + begin + fapply pequiv.MK, + { exact ptrunc.elim (n.+2) (component_functor !ptr) }, + { intro x, cases x with x p, induction x with a, + refine tr ⟨a, _⟩, + note q := trunc_functor -1 !tr_eq_tr_equiv p, + exact trunc_trunc_equiv_left _ !minus_one_le_succ q }, + { exact sorry }, + { exact sorry } + end + + definition ptrunc_component (n : ℕ₋₂) (A : Type*) : ptrunc n (component A) ≃* component (ptrunc n A) := + begin + cases n with n, exact sorry, + cases n with n, exact sorry, + exact ptrunc_component' n A + end + + definition pfiber_pequiv_component_of_is_contr [constructor] {A B : Type*} (f : A →* B) [is_contr B] + /- extra condition, something like trunc_functor 0 f is an embedding -/ : pfiber f ≃* component A := + sorry + end is_conn namespace circle