From 62c134df4e099c5cae47346456084706be65c60f Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 26 Apr 2016 16:07:15 -0400 Subject: [PATCH] whitehead corollaries --- homotopy/EM.hlean | 148 ++++++++++++++++++++++ homotopy/LES_of_homotopy_groups_old.hlean | 5 +- 2 files changed, 149 insertions(+), 4 deletions(-) create mode 100644 homotopy/EM.hlean diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean new file mode 100644 index 0000000..c948206 --- /dev/null +++ b/homotopy/EM.hlean @@ -0,0 +1,148 @@ +/- +Copyright (c) 2016 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Floris van Doorn + +Eilenberg MacLane spaces +-/ + +import homotopy.EM + +open eq is_equiv equiv is_conn is_trunc unit function pointed nat group algebra trunc trunc_index + fiber prod fin + +namespace chain_complex + open succ_str + + definition is_contr_of_is_embedding_of_is_surjective {N : succ_str} (X : chain_complex N) {n : N} + (H : is_exact_at X (S n)) [is_embedding (cc_to_fn X n)] + [H2 : is_surjective (cc_to_fn X (S (S (S n))))] : is_contr (X (S (S n))) := + begin + apply is_contr.mk pt, intro x, + have p : cc_to_fn X n (cc_to_fn X (S n) x) = cc_to_fn X n pt, + from !cc_is_chain_complex ⬝ !respect_pt⁻¹, + have q : cc_to_fn X (S n) x = pt, from is_injective_of_is_embedding p, + induction H x q with y r, + induction H2 y with z s, + exact (cc_is_chain_complex X _ z)⁻¹ ⬝ ap (cc_to_fn X _) s ⬝ r + end + +end chain_complex open chain_complex + +namespace EM + + -- MOVE to connectedness + definition is_conn_fun_to_unit_of_is_conn (n : ℕ₋₂) (A : Type) [H : is_conn n A] + : is_conn_fun n (const A unit.star) := + begin + intro u, induction u, + exact is_conn_equiv_closed n (fiber.fiber_star_equiv A)⁻¹ᵉ _, + end + + /- Whitehead Corollaries -/ + + -- replace in homotopy_group? + theorem trivial_homotopy_group_of_is_trunc' (A : Type*) {n k : ℕ} [is_trunc n A] (H : n < k) + : is_contr (π[k] A) := + begin + apply is_trunc_trunc_of_is_trunc, + apply is_contr_loop_of_is_trunc, + apply @is_trunc_of_le A n _, + apply trunc_index.le_of_succ_le_succ, + rewrite [succ_sub_two_succ k], + exact of_nat_le_of_nat H, + end + + definition is_trunc_pointed_MK [instance] [priority 1100] (n : ℕ₋₂) {A : Type} (a : A) + [H : is_trunc n A] : is_trunc n (pointed.MK A a) := + H + + definition is_contr_of_trivial_homotopy (n : ℕ₋₂) (A : Type) [is_trunc n A] [is_conn 0 A] + (H : Πk a, is_contr (π[k] (pointed.MK A a))) : is_contr A := + begin + fapply is_trunc_is_equiv_closed_rev, { exact λa, ⋆}, + apply whiteheads_principle n, + { apply is_equiv_trunc_functor_of_is_conn_fun, apply is_conn_fun_to_unit_of_is_conn}, + intro a k, + apply @is_equiv_of_is_contr, + refine trivial_homotopy_group_of_is_trunc' _ !one_le_succ, + end + + definition is_contr_of_trivial_homotopy_nat (n : ℕ) (A : Type) [is_trunc n A] [is_conn 0 A] + (H : Πk a, k ≤ n → is_contr (π[k] (pointed.MK A a))) : is_contr A := + begin + apply is_contr_of_trivial_homotopy n, + intro k a, apply @lt_ge_by_cases _ _ n k, + { intro H', exact trivial_homotopy_group_of_is_trunc' _ H'}, + { intro H', exact H k a H'} + end + + definition is_contr_of_trivial_homotopy_pointed (n : ℕ₋₂) (A : Type*) [is_trunc n A] + (H : Πk, is_contr (π[k] A)) : is_contr A := + begin + have is_conn 0 A, proof H 0 qed, + fapply is_contr_of_trivial_homotopy n A, + intro k, apply is_conn.elim -1, + cases A with A a, exact H k + end + + definition is_contr_of_trivial_homotopy_nat_pointed (n : ℕ) (A : Type*) [is_trunc n A] + (H : Πk, k ≤ n → is_contr (π[k] A)) : is_contr A := + begin + have is_conn 0 A, proof H 0 !zero_le qed, + fapply is_contr_of_trivial_homotopy_nat n A, + intro k a H', revert a, apply is_conn.elim -1, + cases A with A a, exact H k H' + end + + -- replace in homotopy_group + definition phomotopy_group_ptrunc_of_le [constructor] {k n : ℕ} (H : k ≤ n) (A : Type*) : + π*[k] (ptrunc n A) ≃* π*[k] A := + calc + π*[k] (ptrunc n A) ≃* Ω[k] (ptrunc k (ptrunc n A)) + : phomotopy_group_pequiv_loop_ptrunc k (ptrunc n A) + ... ≃* Ω[k] (ptrunc k A) + : loopn_pequiv_loopn k (ptrunc_ptrunc_pequiv_left A (of_nat_le_of_nat H)) + ... ≃* π*[k] A : (phomotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ* + + definition is_conn_fun_of_equiv_on_homotopy_groups.{u} (n : ℕ) {A B : Type.{u}} (f : A → B) + [is_equiv (trunc_functor 0 f)] + (H1 : Πa k, k ≤ n → is_equiv (homotopy_group_functor k (pmap_of_map f a))) + (H2 : Πa, is_surjective (homotopy_group_functor (succ n) (pmap_of_map f a))) : is_conn_fun n f := + have H2' : Πa k, k ≤ n → is_surjective (homotopy_group_functor (succ k) (pmap_of_map f a)), + begin + intro a k H, cases H with n' H', + { apply H2}, + { apply is_surjective_of_is_equiv, apply H1, exact succ_le_succ H'} + end, + have H3 : Πa, is_contr (ptrunc n (pfiber (pmap_of_map f a))), + begin + intro a, apply is_contr_of_trivial_homotopy_nat_pointed n, + { intro k H, apply is_trunc_equiv_closed_rev, exact phomotopy_group_ptrunc_of_le H _, + rexact @is_contr_of_is_embedding_of_is_surjective +3ℕ + (LES_of_homotopy_groups (pmap_of_map f a)) (k, 0) + (is_exact_LES_of_homotopy_groups _ _) + proof @(is_embedding_of_is_equiv _) (H1 a k H) qed + proof (H2' a k H) qed} + end, + show Πb, is_contr (trunc n (fiber f b)), + begin + intro b, + note p := right_inv (trunc_functor 0 f) (tr b), revert p, + induction (trunc_functor 0 f)⁻¹ (tr b), esimp, intro p, + induction !tr_eq_tr_equiv p with q, + rewrite -q, exact H3 a + end + + open sigma lift + definition flatten_univ.{u v} {A : Type.{u}} {B : Type.{v}} (f : A → B) : + Σ(A' B' : Type.{max u v}) (f' : A' → B') (g : A ≃ A') (h : B ≃ B'), h ∘ f ~ f' ∘ g := + ⟨lift A, lift B, lift_functor f, proof equiv_lift A qed, proof equiv_lift B qed, + proof sorry qed⟩ + + definition is_conn_inf [reducible] (A : Type) : Type := Πn, is_conn n A + definition is_conn_fun_inf [reducible] {A B : Type} (f : A → B) : Type := Πn, is_conn_fun n f + + +end EM diff --git a/homotopy/LES_of_homotopy_groups_old.hlean b/homotopy/LES_of_homotopy_groups_old.hlean index 2e6b31a..0c57021 100644 --- a/homotopy/LES_of_homotopy_groups_old.hlean +++ b/homotopy/LES_of_homotopy_groups_old.hlean @@ -307,7 +307,7 @@ namespace chain_complex namespace old | (n, fin.mk k H) := Ω[2*n + 1] (pfiber f) definition homotopy_groups2_add1 (n : ℕ) : Π(x : fin (succ 5)), - homotopy_groups2 (n+1, x) = Ω Ω(homotopy_groups2 (n, x)) + homotopy_groups2 (n+1, x) = Ω (Ω(homotopy_groups2 (n, x))) | (fin.mk 0 H) := by reflexivity | (fin.mk 1 H) := by reflexivity | (fin.mk 2 H) := by reflexivity @@ -732,7 +732,6 @@ namespace chain_complex namespace old apply homomorphism.mk (cc_to_fn (LES_of_homotopy_groups3 f) (k + 1, 3)), exact abstract begin rewrite [LES_of_homotopy_groups_fun3_3], refine @is_homomorphism_compose _ _ _ _ _ _ (π→*[2 * (k + 1) + 1] f) tinverse _ _, - { apply group_homotopy_group (2 * (k+1))}, { apply phomotopy_group_functor_mul}, { apply is_homomorphism_inverse} end end end @@ -741,7 +740,6 @@ namespace chain_complex namespace old apply homomorphism.mk (cc_to_fn (LES_of_homotopy_groups3 f) (k + 1, 4)), exact abstract begin rewrite [LES_of_homotopy_groups_fun3_4], refine @is_homomorphism_compose _ _ _ _ _ _ (π→*[2 * (k + 1) + 1] (ppoint f)) tinverse _ _, - { apply group_homotopy_group (2 * (k+1))}, { apply phomotopy_group_functor_mul}, { apply is_homomorphism_inverse} end end end @@ -753,7 +751,6 @@ namespace chain_complex namespace old (π→*[2 * (k + 1) + 1] (boundary_map f) ∘ tinverse) _ _ _, { refine @is_homomorphism_compose _ _ _ _ _ _ (π→*[2 * (k + 1) + 1] (boundary_map f)) tinverse _ _, - { apply group_homotopy_group (2 * (k+1))}, { apply phomotopy_group_functor_mul}, { apply is_homomorphism_inverse}}, { rewrite [▸*, -ap_compose', ▸*],