diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean index 781294c72..e5abcf3e3 100644 --- a/hott/algebra/homotopy_group.hlean +++ b/hott/algebra/homotopy_group.hlean @@ -37,26 +37,31 @@ namespace eq notation `π[`:95 n:0 `]`:0 := homotopy_group n - definition group_homotopy_group [instance] [constructor] [reducible] (n : ℕ) (A : Type*) - : group (π[succ n] A) := - trunc_group (Ω[succ n] A) + section + local attribute inf_group_loopn [instance] + definition group_homotopy_group [instance] [constructor] [reducible] (n : ℕ) [is_succ n] (A : Type*) + : group (π[n] A) := + trunc_group (Ω[n] A) + end definition group_homotopy_group2 [instance] (k : ℕ) (A : Type*) : group (carrier (ptrunctype.to_pType (π[k + 1] A))) := - group_homotopy_group k A + group_homotopy_group (k+1) A - definition ab_group_homotopy_group [constructor] [reducible] (n : ℕ) (A : Type*) - : ab_group (π[succ (succ n)] A) := - trunc_ab_group (Ω[succ (succ n)] A) + section + local attribute ab_inf_group_loopn [instance] + definition ab_group_homotopy_group [constructor] [reducible] (n : ℕ) [is_at_least_two n] (A : Type*) + : ab_group (π[n] A) := + trunc_ab_group (Ω[n] A) + end local attribute ab_group_homotopy_group [instance] - definition ghomotopy_group [constructor] : Π(n : ℕ) [is_succ n] (A : Type*), Group - | (succ n) x A := Group.mk (π[succ n] A) _ + definition ghomotopy_group [constructor] (n : ℕ) [is_succ n] (A : Type*) : Group := + Group.mk (π[n] A) _ - definition cghomotopy_group [constructor] : - Π(n : ℕ) [is_at_least_two n] (A : Type*), AbGroup - | (succ (succ n)) x A := AbGroup.mk (π[succ (succ n)] A) _ + definition cghomotopy_group [constructor] (n : ℕ) [is_at_least_two n] (A : Type*) : AbGroup := + AbGroup.mk (π[n] A) _ definition fundamental_group [constructor] (A : Type*) : Group := ghomotopy_group 1 A @@ -258,12 +263,12 @@ namespace eq inv_preserve_binary (homotopy_group_pequiv_loop_ptrunc (succ k) A) mul concat (@homotopy_group_pequiv_loop_ptrunc_con k A) p q - definition ghomotopy_group_ptrunc [constructor] (k : ℕ) (A : Type*) : - πg[k+1] (ptrunc (k+1) A) ≃g πg[k+1] A := + definition ghomotopy_group_ptrunc_of_le [constructor] {k n : ℕ} (H : k ≤ n) [Hk : is_succ k] (A : Type*) : + πg[k] (ptrunc n A) ≃g πg[k] A := begin fapply isomorphism_of_equiv, - { exact homotopy_group_ptrunc (k+1) A}, - { intro g₁ g₂, + { exact homotopy_group_ptrunc_of_le H A}, + { intro g₁ g₂, induction Hk with k, refine _ ⬝ !homotopy_group_pequiv_loop_ptrunc_inv_con, apply ap ((homotopy_group_pequiv_loop_ptrunc (k+1) A)⁻¹ᵉ*), refine _ ⬝ !loopn_pequiv_loopn_con , @@ -271,6 +276,10 @@ namespace eq apply homotopy_group_pequiv_loop_ptrunc_con} end + definition ghomotopy_group_ptrunc [constructor] (k : ℕ) [is_succ k] (A : Type*) : + πg[k] (ptrunc k A) ≃g πg[k] A := + ghomotopy_group_ptrunc_of_le (le.refl k) A + /- some homomorphisms -/ -- definition is_homomorphism_cast_loopn_succ_eq_in {A : Type*} (n : ℕ) : diff --git a/hott/homotopy/LES_of_homotopy_groups.hlean b/hott/homotopy/LES_of_homotopy_groups.hlean index b3c1a290f..e4b2a6847 100644 --- a/hott/homotopy/LES_of_homotopy_groups.hlean +++ b/hott/homotopy/LES_of_homotopy_groups.hlean @@ -75,12 +75,14 @@ We get the long exact sequence of homotopy groups by taking the set-truncation o import .chain_complex algebra.homotopy_group eq2 -open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc nat trunc algebra function sum +open eq pointed sigma fiber equiv is_equiv is_trunc nat trunc algebra function sum /-------------- PART 1 --------------/ namespace chain_complex + section + open sigma.ops definition fiber_sequence_helper [constructor] (v : Σ(X Y : Type*), X →* Y) : Σ(Z X : Type*), Z →* X := @@ -90,7 +92,10 @@ namespace chain_complex : Σ(Z X : Type*), Z →* X := iterate fiber_sequence_helper n v + end + section + open sigma.ops universe variable u parameters {X Y : pType.{u}} (f : X →* Y) include f @@ -470,10 +475,14 @@ namespace chain_complex PART 3 --------------/ + definition fibration_sequence [unfold 4] : fin 3 → Type* + | (fin.mk 0 H) := Y + | (fin.mk 1 H) := X + | (fin.mk 2 H) := pfiber f + | (fin.mk (n+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end + definition loop_spaces2 [reducible] : +3ℕ → Type* - | (n, fin.mk 0 H) := Ω[n] Y - | (n, fin.mk 1 H) := Ω[n] X - | (n, fin.mk k H) := Ω[n] (pfiber f) + | (n, m) := Ω[n] (fibration_sequence m) definition loop_spaces2_add1 (n : ℕ) : Π(x : fin 3), loop_spaces2 (n+1, x) = Ω (loop_spaces2 (n, x)) @@ -629,11 +638,10 @@ namespace chain_complex /-------------- PART 4 --------------/ + open prod.ops - definition homotopy_groups [reducible] : +3ℕ → Set* - | (n, fin.mk 0 H) := π[n] Y - | (n, fin.mk 1 H) := π[n] X - | (n, fin.mk k H) := π[n] (pfiber f) + definition homotopy_groups [reducible] : +3ℕ → Set* := + λnm, π[nm.1] (fibration_sequence nm.2) definition homotopy_groups_pequiv_loop_spaces2 [reducible] : Π(n : +3ℕ), ptrunc 0 (loop_spaces2 n) ≃* homotopy_groups n @@ -709,27 +717,23 @@ namespace chain_complex open group - definition group_LES_of_homotopy_groups (n : ℕ) : Π(x : fin (succ 2)), - group (LES_of_homotopy_groups (n + 1, x)) - | (fin.mk 0 H) := begin rexact group_homotopy_group n Y end - | (fin.mk 1 H) := begin rexact group_homotopy_group n X end - | (fin.mk 2 H) := begin rexact group_homotopy_group n (pfiber f) end - | (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end + definition group_LES_of_homotopy_groups (n : ℕ) [is_succ n] (x : fin (succ 2)) : + group (LES_of_homotopy_groups (n, x)) := + group_homotopy_group n (fibration_sequence x) - definition ab_group_LES_of_homotopy_groups (n : ℕ) : Π(x : fin (succ 2)), - ab_group (LES_of_homotopy_groups (n + 2, x)) - | (fin.mk 0 H) := proof ab_group_homotopy_group n Y qed - | (fin.mk 1 H) := proof ab_group_homotopy_group n X qed - | (fin.mk 2 H) := proof ab_group_homotopy_group n (pfiber f) qed - | (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end + definition pgroup_LES_of_homotopy_groups (n : ℕ) [H : is_succ n] (x : fin (succ 2)) : + pgroup (LES_of_homotopy_groups (n, x)) := + by induction H with n; exact @pgroup_of_group _ (group_LES_of_homotopy_groups (n+1) x) idp - definition Group_LES_of_homotopy_groups (x : +3ℕ) : Group.{u} := - Group.mk (LES_of_homotopy_groups (nat.succ (pr1 x), pr2 x)) - (group_LES_of_homotopy_groups (pr1 x) (pr2 x)) + definition ab_group_LES_of_homotopy_groups (n : ℕ) [is_at_least_two n] (x : fin (succ 2)) : + ab_group (LES_of_homotopy_groups (n, x)) := + ab_group_homotopy_group n (fibration_sequence x) + + definition Group_LES_of_homotopy_groups (n : +3ℕ) : Group.{u} := + πg[n.1+1] (fibration_sequence n.2) definition AbGroup_LES_of_homotopy_groups (n : +3ℕ) : AbGroup.{u} := - AbGroup.mk (LES_of_homotopy_groups (pr1 n + 2, pr2 n)) - (ab_group_LES_of_homotopy_groups (pr1 n) (pr2 n)) + πag[n.1+2] (fibration_sequence n.2) definition homomorphism_LES_of_homotopy_groups_fun : Π(k : +3ℕ), Group_LES_of_homotopy_groups (S k) →g Group_LES_of_homotopy_groups k @@ -748,6 +752,52 @@ namespace chain_complex end | (k, fin.mk (l+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end + definition LES_is_equiv_of_trivial (n : ℕ) (x : fin (succ 2)) [H : is_succ n] + (HX1 : is_contr (LES_of_homotopy_groups (stratified_pred snat' (n, x)))) + (HX2 : is_contr (LES_of_homotopy_groups (stratified_pred snat' (n+1, x)))) + : is_equiv (cc_to_fn LES_of_homotopy_groups (n, x)) := + begin + induction H with n, + induction x with m H, cases m with m, + { rexact @is_equiv_of_trivial +3ℕ LES_of_homotopy_groups (n, 2) (is_exact_LES_of_homotopy_groups (n, 2)) + proof (is_exact_LES_of_homotopy_groups (n+1, 0)) qed HX1 proof HX2 qed + proof pgroup_LES_of_homotopy_groups (n+1) 0 qed proof pgroup_LES_of_homotopy_groups (n+1) 1 qed + proof homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun (n, 0)) qed }, + cases m with m, + { rexact @is_equiv_of_trivial +3ℕ LES_of_homotopy_groups (n+1, 0) (is_exact_LES_of_homotopy_groups (n+1, 0)) + proof (is_exact_LES_of_homotopy_groups (n+1, 1)) qed HX1 proof HX2 qed + proof pgroup_LES_of_homotopy_groups (n+1) 1 qed proof pgroup_LES_of_homotopy_groups (n+1) 2 qed + proof homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun (n, 1)) qed }, cases m with m, + { rexact @is_equiv_of_trivial +3ℕ LES_of_homotopy_groups (n+1, 1) (is_exact_LES_of_homotopy_groups (n+1, 1)) + proof (is_exact_LES_of_homotopy_groups (n+1, 2)) qed HX1 proof HX2 qed + proof pgroup_LES_of_homotopy_groups (n+1) 2 qed proof pgroup_LES_of_homotopy_groups (n+2) 0 qed + proof homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun (n, 2)) qed }, + exfalso, apply lt_le_antisymm H, apply le_add_left + end + + definition LES_isomorphism_of_trivial_cod (n : ℕ) [H : is_succ n] + (HX1 : is_contr (πg[n] Y)) (HX2 : is_contr (πg[n+1] Y)) : πg[n] (pfiber f) ≃g πg[n] X := + begin + induction H with n, + refine isomorphism.mk (homomorphism_LES_of_homotopy_groups_fun (n, 1)) _, + apply LES_is_equiv_of_trivial, apply HX1, apply HX2 + end + + definition LES_isomorphism_of_trivial_dom (n : ℕ) [H : is_succ n] + (HX1 : is_contr (πg[n] X)) (HX2 : is_contr (πg[n+1] X)) : πg[n+1] (Y) ≃g πg[n] (pfiber f) := + begin + induction H with n, + refine isomorphism.mk (homomorphism_LES_of_homotopy_groups_fun (n, 2)) _, + apply LES_is_equiv_of_trivial, apply HX1, apply HX2 + end + + definition LES_isomorphism_of_trivial_pfiber (n : ℕ) + (HX1 : is_contr (π[n] (pfiber f))) (HX2 : is_contr (πg[n+1] (pfiber f))) : πg[n+1] X ≃g πg[n+1] Y := + begin + refine isomorphism.mk (homomorphism_LES_of_homotopy_groups_fun (n, 0)) _, + apply LES_is_equiv_of_trivial, apply HX1, apply HX2 + end + end /- @@ -794,22 +844,22 @@ namespace chain_complex refine _ ⬝* !apn_pcompose⁻¹*, reflexivity end | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - definition type_fibration_sequence [constructor] : type_chain_complex +3ℕ := + definition type_LES_fibration_sequence [constructor] : type_chain_complex +3ℕ := transfer_type_chain_complex (LES_of_loop_spaces2 f) fibration_sequence_fun fibration_sequence_pequiv fibration_sequence_fun_phomotopy - definition is_exact_type_fibration_sequence : is_exact_t type_fibration_sequence := + definition is_exact_type_fibration_sequence : is_exact_t type_LES_fibration_sequence := begin intro n, apply is_exact_at_t_transfer, apply is_exact_LES_of_loop_spaces2 end - definition fibration_sequence [constructor] : chain_complex +3ℕ := - trunc_chain_complex type_fibration_sequence + definition LES_fibration_sequence [constructor] : chain_complex +3ℕ := + trunc_chain_complex type_LES_fibration_sequence end diff --git a/hott/homotopy/chain_complex.hlean b/hott/homotopy/chain_complex.hlean index 055b3a25a..c947a13a7 100644 --- a/hott/homotopy/chain_complex.hlean +++ b/hott/homotopy/chain_complex.hlean @@ -49,6 +49,11 @@ definition stratified_succ {N : succ_str} {n : ℕ} (x : stratified_type N n) : stratified_type N n := (if val (pr2 x) = n then S (pr1 x) else pr1 x, cyclic_succ (pr2 x)) +/- You might need to manually change the succ_str, to use predecessor as "successor" -/ +definition stratified_pred (N : succ_str) {n : ℕ} (x : stratified_type N n) + : stratified_type N n := +(if val (pr2 x) = 0 then S (pr1 x) else pr1 x, cyclic_pred (pr2 x)) + definition stratified [reducible] [constructor] (N : succ_str) (n : ℕ) : succ_str := succ_str.mk (stratified_type N n) stratified_succ diff --git a/hott/homotopy/homotopy_group.hlean b/hott/homotopy/homotopy_group.hlean index 3939f6695..3c56158d2 100644 --- a/hott/homotopy/homotopy_group.hlean +++ b/hott/homotopy/homotopy_group.hlean @@ -7,7 +7,7 @@ Authors: Floris van Doorn, Clive Newstead import .LES_of_homotopy_groups .sphere .complex_hopf -open eq is_trunc trunc_index pointed algebra trunc nat is_conn fiber pointed unit +open eq is_trunc trunc_index pointed algebra trunc nat is_conn fiber pointed unit group namespace is_trunc @@ -53,15 +53,6 @@ namespace is_trunc [H : is_conn_fun n f] (H2 : k ≤ n) : is_contr (π[k] (pfiber f)) := @(trivial_homotopy_group_of_is_conn (pfiber f) H2) (H pt) - theorem homotopy_group_trunc_of_le (A : Type*) (n k : ℕ) (H : k ≤ n) - : π[k] (ptrunc n A) ≃* π[k] A := - begin - refine !homotopy_group_pequiv_loop_ptrunc ⬝e* _, - refine loopn_pequiv_loopn _ (ptrunc_ptrunc_pequiv_left _ _) ⬝e* _, - exact of_nat_le_of_nat H, - exact !homotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*, - end - /- Corollaries of the LES of homotopy groups -/ local attribute ab_group.to_group [coercion] local attribute is_equiv_tinverse [instance] @@ -81,16 +72,9 @@ namespace is_trunc refine is_conn_fun_of_le f (zero_le_of_nat n)}, { /- k > 0 -/ have H2' : k ≤ n, from le.trans !self_le_succ H2, - exact - @is_equiv_of_trivial _ - (LES_of_homotopy_groups f) _ - (is_exact_LES_of_homotopy_groups f (k, 2)) - (is_exact_LES_of_homotopy_groups f (succ k, 0)) - (@is_contr_HG_fiber_of_is_connected A B k n f H H2') - (@is_contr_HG_fiber_of_is_connected A B (succ k) n f H H2) - (@pgroup_of_group _ (group_LES_of_homotopy_groups f k 0) idp) - (@pgroup_of_group _ (group_LES_of_homotopy_groups f k 1) idp) - (homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun f (k, 0)))}, + exact LES_is_equiv_of_trivial f (succ k) 0 + (@is_contr_HG_fiber_of_is_connected A B k n f H H2') + (@is_contr_HG_fiber_of_is_connected A B (succ k) n f H H2) }, end theorem is_equiv_π_of_is_connected.{u v} {A : pType.{u}} {B : pType.{v}} {n k : ℕ} (f : A →* B) @@ -131,7 +115,7 @@ namespace is_trunc (H : Πa k, is_equiv (π→[k + 1] (pmap_of_map f a))) : is_equiv f := begin revert A B HA HB f H' H, induction n with n IH: intros, - { apply is_equiv_of_is_contr}, + { apply is_equiv_of_is_contr }, have Πa, is_equiv (Ω→ (pmap_of_map f a)), begin intro a, @@ -223,8 +207,6 @@ namespace is_trunc cases A with A a, exact H k H' end - - definition ab_group_homotopy_group_of_is_conn (n : ℕ) (A : Type*) [H : is_conn 1 A] : ab_group (π[n] A) := begin @@ -233,7 +215,7 @@ namespace is_trunc { unfold [homotopy_group, ptrunc], apply ab_group_of_is_contr }, cases n with n, { unfold [homotopy_group, ptrunc], apply ab_group_of_is_contr }, - exact ab_group_homotopy_group n A + exact ab_group_homotopy_group (n+2) A end definition is_contr_of_trivial_homotopy' (n : ℕ₋₂) (A : Type) [is_trunc n A] [is_conn -1 A] @@ -253,7 +235,7 @@ namespace is_trunc intro k a H2, induction a with a, apply is_trunc_equiv_closed_rev, - exact equiv_of_pequiv (homotopy_group_trunc_of_le (pointed.MK A a) _ _ H2), + exact equiv_of_pequiv (homotopy_group_ptrunc_of_le H2 (pointed.MK A a)), exact H k a H2 end @@ -266,9 +248,6 @@ namespace is_trunc cases A with A a, exact H k H2 end - - - 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))) diff --git a/hott/homotopy/sphere2.hlean b/hott/homotopy/sphere2.hlean index 3c15db76d..94a8f9051 100644 --- a/hott/homotopy/sphere2.hlean +++ b/hott/homotopy/sphere2.hlean @@ -27,22 +27,12 @@ namespace sphere fapply isomorphism_of_equiv, { fapply equiv.mk, { exact cc_to_fn (LES_of_homotopy_groups complex_phopf) (1, 2)}, - { refine @is_equiv_of_trivial _ - _ _ - (is_exact_LES_of_homotopy_groups _ (1, 1)) - (is_exact_LES_of_homotopy_groups _ (1, 2)) - _ - _ - (@pgroup_of_group _ (group_LES_of_homotopy_groups complex_phopf _ _) idp) - (@pgroup_of_group _ (group_LES_of_homotopy_groups complex_phopf _ _) idp) - _, - { rewrite [LES_of_homotopy_groups_1, ▸*], - have H : 1 ≤[ℕ] 2, from !one_le_succ, - apply trivial_homotopy_group_of_is_conn, exact H, rexact is_conn_psphere 3}, + { refine LES_is_equiv_of_trivial complex_phopf 1 2 _ _, + { have H : 1 ≤[ℕ] 2, from !one_le_succ, + apply trivial_homotopy_group_of_is_conn, exact H, rexact is_conn_psphere 3 }, { refine tr_rev (λx, is_contr (ptrunctype._trans_of_to_pType x)) (LES_of_homotopy_groups_1 complex_phopf 2) _, - apply trivial_homotopy_group_of_is_conn, apply le.refl, rexact is_conn_psphere 3}, - { exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (0, 2))}}}, + apply trivial_homotopy_group_of_is_conn, apply le.refl, rexact is_conn_psphere 3 }}}, { exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (0, 2))} end @@ -54,23 +44,13 @@ namespace sphere { exact cc_to_fn (LES_of_homotopy_groups complex_phopf) (n+3, 0)}, { have H : is_trunc 1 (pfiber complex_phopf), from @(is_trunc_equiv_closed_rev _ pfiber_complex_phopf) is_trunc_circle, - refine @is_equiv_of_trivial _ - _ _ - (is_exact_LES_of_homotopy_groups _ (n+2, 2)) - (is_exact_LES_of_homotopy_groups _ (n+3, 0)) - _ - _ - (@pgroup_of_group _ (group_LES_of_homotopy_groups complex_phopf _ _) idp) - (@pgroup_of_group _ (group_LES_of_homotopy_groups complex_phopf _ _) idp) - _, - { rewrite [▸*, LES_of_homotopy_groups_2 _ (n +[ℕ] 2)], - have H2 : 1 ≤[ℕ] n + 1, from !one_le_succ, - exact @trivial_ghomotopy_group_of_is_trunc _ _ _ H H2}, + refine LES_is_equiv_of_trivial complex_phopf (n+3) 0 _ _, + { have H2 : 1 ≤[ℕ] n + 1, from !one_le_succ, + exact @trivial_ghomotopy_group_of_is_trunc _ _ _ H H2 }, { refine tr_rev (λx, is_contr (ptrunctype._trans_of_to_pType x)) (LES_of_homotopy_groups_2 complex_phopf _) _, have H2 : 1 ≤[ℕ] n + 2, from !one_le_succ, - apply trivial_ghomotopy_group_of_is_trunc _ _ _ H2}, - { exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (n+2, 0))}}}, + apply trivial_ghomotopy_group_of_is_trunc _ _ _ H2 }}}, { exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (n+2, 0))} end diff --git a/hott/types/fin.hlean b/hott/types/fin.hlean index 4174f9413..011827035 100644 --- a/hott/types/fin.hlean +++ b/hott/types/fin.hlean @@ -595,6 +595,15 @@ end (succ_lt_succ (lt_of_le_of_ne (le_of_lt_succ (is_lt x)) H))} end + definition cyclic_pred {n : ℕ} (x : fin n) : fin n := + begin + cases n with n, + { exfalso, apply not_lt_zero _ (is_lt x)}, + { cases x with m H, cases m with m, + { exact fin.mk n (self_lt_succ n) }, + { exact fin.mk m (lt.trans (self_lt_succ m) H) }} + end + /- We want to say that fin (succ n) always has a 0 and 1. However, we want a bit more, because sometimes we want a zero of (fin a) where a is either diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index 61dfee981..cf027f091 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -791,6 +791,7 @@ namespace pointed infix ` ⬝e*p `:75 := peconcat_eq infix ` ⬝pe* `:75 := eq_peconcat + -- rename pequiv_of_eq_natural definition pequiv_of_eq_commute [constructor] {A : Type} {B C : A → Type*} (f : Πa, B a →* C a) {a₁ a₂ : A} (p : a₁ = a₂) : pequiv_of_eq (ap C p) ∘* f a₁ ~* f a₂ ∘* pequiv_of_eq (ap B p) := pcast_commute f p