From 45d808ce7ffbc19a1dabd9f297d89e5d93be9fa6 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 18 Nov 2015 18:08:38 -0500 Subject: [PATCH] feat(homotopy/circle): give all higher homotopy groups of the circle --- hott/algebra/homotopy_group.hlean | 50 +++++++++++++++++++++++++------ hott/algebra/hott.hlean | 14 +++++++-- hott/homotopy/circle.hlean | 15 ++++++---- hott/init/trunc.hlean | 2 ++ hott/types/int/basic.hlean | 2 +- hott/types/pointed.hlean | 15 ++++++++++ hott/types/trunc.hlean | 11 ++++++- hott/types/unit.hlean | 16 ++++++++++ 8 files changed, 106 insertions(+), 19 deletions(-) diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean index f8708d525..9c0a38d33 100644 --- a/hott/algebra/homotopy_group.hlean +++ b/hott/algebra/homotopy_group.hlean @@ -6,41 +6,41 @@ Authors: Floris van Doorn homotopy groups of a pointed space -/ -import types.pointed .trunc_group +import types.pointed .trunc_group .hott types.trunc open nat eq pointed trunc is_trunc algebra namespace eq - definition homotopy_group [reducible] (n : ℕ) (A : Pointed) : Type := + definition homotopy_group [reducible] (n : ℕ) (A : Type*) : Type := trunc 0 (Ω[n] A) notation `π[`:95 n:0 `] `:0 A:95 := homotopy_group n A - definition pointed_homotopy_group [instance] [constructor] (n : ℕ) (A : Pointed) + definition pointed_homotopy_group [instance] [constructor] (n : ℕ) (A : Type*) : pointed (π[n] A) := pointed.mk (tr rfln) - definition group_homotopy_group [instance] [constructor] (n : ℕ) (A : Pointed) + definition group_homotopy_group [instance] [constructor] (n : ℕ) (A : Type*) : group (π[succ n] A) := trunc_group concat inverse idp con.assoc idp_con con_idp con.left_inv - definition comm_group_homotopy_group [constructor] (n : ℕ) (A : Pointed) + definition comm_group_homotopy_group [constructor] (n : ℕ) (A : Type*) : comm_group (π[succ (succ n)] A) := trunc_comm_group concat inverse idp con.assoc idp_con con_idp con.left_inv eckmann_hilton local attribute comm_group_homotopy_group [instance] - definition Pointed_homotopy_group [constructor] (n : ℕ) (A : Pointed) : Pointed := + definition Pointed_homotopy_group [constructor] (n : ℕ) (A : Type*) : Type* := Pointed.mk (π[n] A) - definition Group_homotopy_group [constructor] (n : ℕ) (A : Pointed) : Group := + definition Group_homotopy_group [constructor] (n : ℕ) (A : Type*) : Group := Group.mk (π[succ n] A) _ - definition CommGroup_homotopy_group [constructor] (n : ℕ) (A : Pointed) : CommGroup := + definition CommGroup_homotopy_group [constructor] (n : ℕ) (A : Type*) : CommGroup := CommGroup.mk (π[succ (succ n)] A) _ - definition fundamental_group [constructor] (A : Pointed) : Group := + definition fundamental_group [constructor] (A : Type*) : Group := Group_homotopy_group zero A notation `πP[`:95 n:0 `] `:0 A:95 := Pointed_homotopy_group n A @@ -49,5 +49,37 @@ namespace eq prefix `π₁`:95 := fundamental_group + open equiv unit + theorem trivial_homotopy_of_is_hset (A : Type*) [H : is_hset A] (n : ℕ) : πG[n+1] A = G0 := + begin + apply trivial_group_of_is_contr, + apply is_trunc_trunc_of_is_trunc, + apply is_contr_loop_of_is_trunc, + apply is_trunc_succ_succ_of_is_hset + end + + definition homotopy_group_succ_out (A : Type*) (n : ℕ) : πG[ n +1] A = π₁ Ω[n] A := idp + + definition homotopy_group_succ_in (A : Type*) (n : ℕ) : πG[succ n +1] A = πG[n +1] Ω A := + begin + fapply Group_eq, + { apply equiv_of_eq, exact ap (λ(X : Type*), trunc 0 X) (loop_space_succ_eq_in A (succ n))}, + { exact abstract [irreducible] begin refine trunc.rec _, intro p, refine trunc.rec _, intro q, + rewrite [▸*,-+tr_eq_cast_ap, +trunc_transport, ↑[group_homotopy_group, group.to_monoid, + monoid.to_semigroup, semigroup.to_has_mul, trunc_mul], trunc_transport], apply ap tr, + apply loop_space_succ_eq_in_concat end end}, + end + + definition homotopy_group_add (A : Type*) (n m : ℕ) : πG[n+m +1] A = πG[n +1] Ω[m] A := + begin + revert A, induction m with m IH: intro A, + { reflexivity}, + { esimp [Iterated_loop_space, nat.add], refine !homotopy_group_succ_in ⬝ _, refine !IH ⬝ _, + exact ap (Group_homotopy_group n) !loop_space_succ_eq_in⁻¹} + end + + theorem trivial_homotopy_of_is_hset_loop_space {A : Type*} {n : ℕ} (m : ℕ) (H : is_hset (Ω[n] A)) + : πG[m+n+1] A = G0 := + !homotopy_group_add ⬝ !trivial_homotopy_of_is_hset end eq diff --git a/hott/algebra/hott.hlean b/hott/algebra/hott.hlean index 4e4593c36..370c21f72 100644 --- a/hott/algebra/hott.hlean +++ b/hott/algebra/hott.hlean @@ -6,7 +6,7 @@ Author: Floris van Doorn Theorems about algebra specific to HoTT -/ -import .group arity types.pi hprop_trunc +import .group arity types.pi hprop_trunc types.unit open equiv eq equiv.ops is_trunc @@ -30,7 +30,7 @@ namespace algebra from λg, !mul_inv_cancel_right⁻¹, cases G with Gm Gs Gh1 G1 Gh2 Gh3 Gi Gh4, cases H with Hm Hs Hh1 H1 Hh2 Hh3 Hi Hh4, - rewrite [↑[semigroup.to_has_mul,group.to_has_inv] at (same_mul,foo)] , + rewrite [↑[semigroup.to_has_mul,group.to_has_inv] at (same_mul,foo)], have same_mul : Gm = Hm, from eq_of_homotopy2 same_mul', cases same_mul, have same_one : G1 = H1, from calc @@ -49,7 +49,8 @@ namespace algebra cases ps, cases ph1, cases ph2, cases ph3, cases ph4, reflexivity end - definition group_pathover {G : group A} {H : group B} {f : A ≃ B} : (Π(g h : A), f (g * h) = f g * f h) → G =[ua f] H := + definition group_pathover {G : group A} {H : group B} {f : A ≃ B} + : (Π(g h : A), f (g * h) = f g * f h) → G =[ua f] H := begin revert H, eapply (rec_on_ua_idp' f), @@ -67,4 +68,11 @@ namespace algebra apply group_pathover, exact resp_mul end + definition trivial_group_of_is_contr (G : Group) [H : is_contr G] : G = G0 := + begin + fapply Group_eq, + { apply equiv_unit_of_is_contr}, + { intros, reflexivity} + end + end algebra diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean index 13e11aa25..03fc4df63 100644 --- a/hott/homotopy/circle.hlean +++ b/hott/homotopy/circle.hlean @@ -192,8 +192,7 @@ namespace circle definition transport_code_loop (a : ℤ) : transport circle.code loop a = succ a := ap10 !elim_type_loop a - definition transport_code_loop_inv (a : ℤ) - : transport circle.code loop⁻¹ a = pred a := + definition transport_code_loop_inv (a : ℤ) : transport circle.code loop⁻¹ a = pred a := ap10 !elim_type_loop_inv a protected definition encode [unfold 2] {x : circle} (p : base = x) : circle.code x := @@ -228,15 +227,14 @@ namespace circle definition base_eq_base_equiv [constructor] : base = base ≃ ℤ := circle_eq_equiv base - definition decode_add (a b : ℤ) : - base_eq_base_equiv⁻¹ a ⬝ base_eq_base_equiv⁻¹ b = base_eq_base_equiv⁻¹ (a + b) := + definition decode_add (a b : ℤ) : circle.decode a ⬝ circle.decode b = circle.decode (a + b) := !power_con_power definition encode_con (p q : base = base) : circle.encode (p ⬝ q) = circle.encode p + circle.encode q := preserve_binary_of_inv_preserve base_eq_base_equiv concat add decode_add p q --the carrier of π₁(S¹) is the set-truncation of base = base. - open core algebra trunc equiv.ops + open algebra trunc equiv.ops definition fg_carrier_equiv_int : π[1](S¹.) ≃ ℤ := trunc_equiv_trunc 0 base_eq_base_equiv ⬝e !trunc_equiv @@ -251,6 +249,13 @@ namespace circle apply encode_con, end + open nat + definition homotopy_group_of_circle (n : ℕ) : πG[n+1 +1] S¹. = G0 := + begin + refine @trivial_homotopy_of_is_hset_loop_space S¹. 1 n _, + apply is_trunc_equiv_closed_rev, apply base_eq_base_equiv + end + definition eq_equiv_Z (x : S¹) : x = x ≃ ℤ := begin induction x, diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index ea2c877b4..4767025f2 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -280,6 +280,7 @@ namespace is_trunc open equiv -- A contractible type is equivalent to [Unit]. *) + variable (A) definition equiv_unit_of_is_contr [H : is_contr A] : A ≃ unit := equiv.MK (λ (x : A), ⋆) (λ (u : unit), center A) @@ -287,6 +288,7 @@ namespace is_trunc (λ (x : A), center_eq x) /- interaction with pathovers -/ + variable {A} variables {C : A → Type} {a a₂ : A} (p : a = a₂) (c : C a) (c₂ : C a₂) diff --git a/hott/types/int/basic.hlean b/hott/types/int/basic.hlean index b8b5a24d5..03e87fc1a 100644 --- a/hott/types/int/basic.hlean +++ b/hott/types/int/basic.hlean @@ -83,7 +83,7 @@ definition mul (a b : ℤ) : ℤ := /- notation -/ -notation `-[` n `+1]` := int.neg_succ_of_nat n -- for pretty-printing output +notation `-[`:95 n:0 `+1]`:0 := int.neg_succ_of_nat n -- for pretty-printing output prefix - := int.neg infix + := int.add infix * := int.mul diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index 12920b4bd..099e92d5f 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -60,6 +60,9 @@ namespace pointed definition Bool [constructor] : Type* := pointed.mk' bool + definition Unit [constructor] : Type* := + Pointed.mk unit.star + definition pointed_fun_closed [constructor] (f : A → B) [H : pointed A] : pointed B := pointed.mk (f pt) @@ -243,6 +246,18 @@ namespace pointed idp variable {A} + + /- the equality [loop_space_succ_eq_in] preserves concatenation -/ + theorem loop_space_succ_eq_in_concat {n : ℕ} (p q : Ω[succ (succ n)] A) : + transport carrier (ap Loop_space (loop_space_succ_eq_in A n)) (p ⬝ q) + = transport carrier (ap Loop_space (loop_space_succ_eq_in A n)) p + ⬝ transport carrier (ap Loop_space (loop_space_succ_eq_in A n)) q := + begin + rewrite [-+tr_compose, ↑function.compose], + rewrite [+@transport_eq_FlFr_D _ _ _ _ Point Point, +con.assoc], apply whisker_left, + rewrite [-+con.assoc], apply whisker_right, rewrite [con_inv_cancel_right, ▸*, -ap_con] + end + definition loop_space_loop_irrel (p : point A = point A) : Ω(Pointed.mk p) = Ω[2] A := begin intros, fapply Pointed_eq, diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index 9c4a85448..c239b5974 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -145,7 +145,7 @@ namespace is_trunc theorem is_trunc_succ_iff_is_trunc_loop (A : Type) (Hn : -1 ≤ n) : is_trunc (n.+1) A ↔ Π(a : A), is_trunc n (a = a) := iff.intro _ (is_trunc_succ_of_is_trunc_loop Hn) ---set_option pp.all true + theorem is_trunc_iff_is_contr_loop_succ (n : ℕ) (A : Type) : is_trunc n A ↔ Π(a : A), is_contr (Ω[succ n](Pointed.mk a)) := begin @@ -171,6 +171,11 @@ namespace is_trunc { apply is_trunc_iff_is_contr_loop_succ}, end + theorem is_contr_loop_of_is_trunc (n : ℕ) (A : Type*) [H : is_trunc (n.-2.+1) A] : + is_contr (Ω[n] A) := + by induction A; exact iff.mp !is_trunc_iff_is_contr_loop _ _ + + end is_trunc open is_trunc namespace trunc @@ -231,6 +236,10 @@ namespace trunc : P a := !trunc_equiv (f a) + /- transport over a truncated family -/ + definition trunc_transport {a a' : A} {P : A → Type} (p : a = a') (n : trunc_index) (x : P a) + : transport (λa, trunc n (P a)) p (tr x) = tr (p ▸ x) := + by induction p; reflexivity end trunc open trunc diff --git a/hott/types/unit.hlean b/hott/types/unit.hlean index 92f60dfc7..dc121d685 100644 --- a/hott/types/unit.hlean +++ b/hott/types/unit.hlean @@ -6,6 +6,8 @@ Authors: Floris van Doorn Theorems about the unit type -/ +import algebra.group + open equiv option eq namespace unit @@ -32,3 +34,17 @@ namespace unit end end unit + +open unit is_trunc + +namespace algebra + + definition trivial_group [constructor] : group unit := + group.mk (λx y, star) _ (λx y z, idp) star (unit.rec idp) (unit.rec idp) (λx, star) (λx, idp) + + definition Trivial_group [constructor] : Group := + Group.mk _ trivial_group + + notation `G0` := Trivial_group + +end algebra