From 2cc891487406a91949cf5910274213ef69aaca56 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 24 Jun 2016 09:54:00 +0100 Subject: [PATCH] feat(homotopy): add results about infty-connectedness and loops of EM-spaces --- hott/homotopy/EM.hlean | 59 ++++++++++++++++++++++++++++-- hott/homotopy/circle.hlean | 5 ++- hott/homotopy/connectedness.hlean | 49 +++++++++++++++++++++---- hott/homotopy/homotopy_group.hlean | 22 +++++++++++ hott/types/int/hott.hlean | 4 ++ hott/types/trunc.hlean | 32 +++++++++++++++- 6 files changed, 158 insertions(+), 13 deletions(-) diff --git a/hott/homotopy/EM.hlean b/hott/homotopy/EM.hlean index 40085db8d..18e7aa8e3 100644 --- a/hott/homotopy/EM.hlean +++ b/hott/homotopy/EM.hlean @@ -199,16 +199,23 @@ namespace EM rexact add_mul_le_mul_add n 1 1 end - local attribute EMadd1 [reducible] - definition is_conn_EMadd1 (G : CommGroup) (n : ℕ) : is_conn n (EMadd1 G n) := _ + section + local attribute EMadd1 [reducible] + definition is_conn_EMadd1 [instance] (G : CommGroup) (n : ℕ) : is_conn n (EMadd1 G n) := _ - definition is_trunc_EMadd1 (G : CommGroup) (n : ℕ) : is_trunc (n+1) (EMadd1 G n) := _ + definition is_trunc_EMadd1 [instance] (G : CommGroup) (n : ℕ) : is_trunc (n+1) (EMadd1 G n) := _ + end /- K(G, n) -/ definition EM (G : CommGroup) : ℕ → Type* | 0 := pType_of_Group G | (k+1) := EMadd1 G k + namespace ops + abbreviation K := EM + end ops + open ops + definition phomotopy_group_EM (G : CommGroup) (n : ℕ) : π*[n] (EM G n) ≃* pType_of_Group G := begin cases n with n, @@ -277,11 +284,55 @@ namespace EM [is_conn 0 X] [is_trunc 1 X] : pEM1 G ≃* X := begin apply pEM1_pequiv' (!trunc_equiv⁻¹ᵉ ⬝e equiv_of_isomorphism e), - intro p q, esimp, exact respect_mul e (tr p) (tr q) + intro p q, esimp, exact to_respect_mul e (tr p) (tr q) end + definition pEM1_pequiv_type {X : Type*} [is_conn 0 X] [is_trunc 1 X] : pEM1 (π₁ X) ≃* X := + pEM1_pequiv !isomorphism.refl + + definition EM_pequiv_1.{u} {G : CommGroup.{u}} {X : pType.{u}} (e : π₁ X ≃g G) + [is_conn 0 X] [is_trunc 1 X] : EM G 1 ≃* X := + begin + refine _ ⬝e* pEM1_pequiv e, + apply ptrunc_pequiv, + apply is_trunc_pEM1 + end + + definition EMadd1_pequiv_pEM1 (G : CommGroup) : EMadd1 G 0 ≃* pEM1 G := + begin apply ptrunc_pequiv, apply is_trunc_pEM1 end + + definition EM1add1_pequiv_0.{u} {G : CommGroup.{u}} {X : pType.{u}} (e : π₁ X ≃g G) + [is_conn 0 X] [is_trunc 1 X] : EMadd1 G 0 ≃* X := + EMadd1_pequiv_pEM1 G ⬝e* pEM1_pequiv e + definition KG1_pequiv.{u} {X Y : pType.{u}} (e : π₁ X ≃g π₁ Y) [is_conn 0 X] [is_trunc 1 X] [is_conn 0 Y] [is_trunc 1 Y] : X ≃* Y := (pEM1_pequiv e)⁻¹ᵉ* ⬝e* pEM1_pequiv !isomorphism.refl + open circle int + definition EM_pequiv_circle : K agℤ 1 ≃* S¹. := + !EMadd1_pequiv_pEM1 ⬝e* pEM1_pequiv fundamental_group_of_circle + + /- loops of EM-spaces -/ + definition loop_EMadd1 {G : CommGroup} (n : ℕ) : Ω (EMadd1 G (succ n)) ≃* EMadd1 G n := + begin + cases n with n, + { symmetry, apply EM1add1_pequiv_0, rexact homotopy_group_EMadd1 G 1, + -- apply is_conn_loop, apply is_conn_EMadd1, + apply is_trunc_loop, apply is_trunc_EMadd1}, + { refine loop_ptrunc_pequiv _ _ ⬝e* _, + rewrite [add_one, succ_sub_two], + have succ n + 1 ≤ 2 * succ n, from add_mul_le_mul_add n 1 1, + symmetry, refine freudenthal_pequiv _ this, } + end + + definition loop_EM (G : CommGroup) (n : ℕ) : Ω (K G (succ n)) ≃* K G n := + begin + cases n with n, + { refine _ ⬝e* pequiv_of_isomorphism (fundamental_group_pEM1 G), + refine loop_pequiv_loop (EMadd1_pequiv_pEM1 G) ⬝e* _, + symmetry, apply ptrunc_pequiv, exact _}, + { apply loop_EMadd1} + end + end EM diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean index b7b392c23..86246dd17 100644 --- a/hott/homotopy/circle.hlean +++ b/hott/homotopy/circle.hlean @@ -10,7 +10,7 @@ import .sphere import types.int.hott import algebra.homotopy_group .connectedness -open eq susp bool sphere_index is_equiv equiv is_trunc is_conn pi algebra +open eq susp bool sphere_index is_equiv equiv is_trunc is_conn pi algebra pointed definition circle : Type₀ := sphere 1 @@ -337,6 +337,9 @@ namespace circle proposition is_conn_circle [instance] : is_conn 0 S¹ := sphere.is_conn_sphere -1.+2 + definition is_conn_pcircle [instance] : is_conn 0 S¹. := !is_conn_circle + definition is_trunc_pcircle [instance] : is_trunc 1 S¹. := !is_trunc_circle + definition circle_mul [reducible] (x y : S¹) : S¹ := circle.elim y (circle_turn y) x diff --git a/hott/homotopy/connectedness.hlean b/hott/homotopy/connectedness.hlean index cffa70df5..364905ed9 100644 --- a/hott/homotopy/connectedness.hlean +++ b/hott/homotopy/connectedness.hlean @@ -2,16 +2,24 @@ Copyright (c) 2015 Ulrik Buchholtz. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Ulrik Buchholtz, Floris van Doorn + +Connectedness of types and functions -/ import types.trunc types.arrow_2 types.lift -open eq is_trunc is_equiv nat equiv trunc function fiber funext pi +open eq is_trunc is_equiv nat equiv trunc function fiber funext pi pointed + +definition is_conn [reducible] (n : ℕ₋₂) (A : Type) : Type := +is_contr (trunc n A) + +definition is_conn_fun [reducible] (n : ℕ₋₂) {A B : Type} (f : A → B) : Type := +Πb : B, is_conn n (fiber f b) + +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 namespace is_conn - definition is_conn [reducible] (n : ℕ₋₂) (A : Type) : Type := - is_contr (trunc n A) - definition is_conn_equiv_closed (n : ℕ₋₂) {A B : Type} : A ≃ B → is_conn n A → is_conn n B := begin @@ -21,9 +29,6 @@ namespace is_conn assumption end - definition is_conn_fun [reducible] (n : ℕ₋₂) {A B : Type} (f : A → B) : Type := - Πb : B, is_conn n (fiber f b) - theorem is_conn_of_le (A : Type) {n k : ℕ₋₂} (H : n ≤ k) [is_conn k A] : is_conn n A := begin apply is_contr_equiv_closed, @@ -34,6 +39,9 @@ namespace is_conn [is_conn_fun k f] : is_conn_fun n f := λb, is_conn_of_le _ H + definition is_conn_of_is_conn_succ (n : ℕ₋₂) (A : Type) [is_conn (n.+1) A] : is_conn n A := + is_trunc_trunc_of_le A -2 (trunc_index.self_le_succ n) + namespace is_conn_fun section parameters (n : ℕ₋₂) {A B : Type} {h : A → B} @@ -267,6 +275,15 @@ namespace is_conn apply is_trunc_equiv_closed, apply trunc_trunc_equiv_trunc_trunc end + definition is_conn_eq [instance] (n : ℕ₋₂) {A : Type} (a a' : A) [is_conn (n.+1) A] : + is_conn n (a = a') := + begin + apply is_trunc_equiv_closed, apply tr_eq_tr_equiv, + end + + definition is_conn_loop [instance] (n : ℕ₋₂) (A : Type*) [is_conn (n.+1) A] : is_conn n (Ω A) := + !is_conn_eq + open pointed definition is_conn_ptrunc [instance] (A : Type*) (n k : ℕ₋₂) [H : is_conn n A] : is_conn n (ptrunc k A) := @@ -330,4 +347,22 @@ namespace is_conn { apply trunc_equiv_trunc, apply fiber_lift_functor} end + open trunc_index + definition is_conn_fun_inf.mk_nat {A B : Type} {f : A → B} (H : Π(n : ℕ), is_conn_fun n f) + : is_conn_fun_inf f := + begin + intro n, + cases n with n, { exact _}, + cases n with n, { have -1 ≤ of_nat 0, from dec_star, apply is_conn_fun_of_le f this}, + rewrite -of_nat_add_two, exact _ + end + + definition is_conn_inf.mk_nat {A : Type} (H : Π(n : ℕ), is_conn n A) : is_conn_inf A := + begin + intro n, + cases n with n, { exact _}, + cases n with n, { have -1 ≤ of_nat 0, from dec_star, apply is_conn_of_le A this}, + rewrite -of_nat_add_two, exact _ + end + end is_conn diff --git a/hott/homotopy/homotopy_group.hlean b/hott/homotopy/homotopy_group.hlean index c7b2d60e7..fcc6ae4c5 100644 --- a/hott/homotopy/homotopy_group.hlean +++ b/hott/homotopy/homotopy_group.hlean @@ -244,3 +244,25 @@ namespace is_trunc end end is_trunc +open is_trunc function +/- applications to infty-connected types and maps -/ +namespace is_conn + + definition is_conn_fun_inf_of_equiv_on_homotopy_groups.{u} {A B : Type.{u}} (f : A → B) + [is_equiv (trunc_functor 0 f)] + (H1 : Πa k, is_equiv (homotopy_group_functor k (pmap_of_map f a))) : is_conn_fun_inf f := + begin + apply is_conn_fun_inf.mk_nat, intro n, apply is_conn_fun_of_equiv_on_homotopy_groups, + { intro a k H, exact H1 a k}, + { intro a, apply is_surjective_of_is_equiv} + end + + definition is_equiv_trunc_functor_of_is_conn_fun_inf.{u} (n : ℕ₋₂) {A B : Type.{u}} (f : A → B) + [is_conn_fun_inf f] : is_equiv (trunc_functor n f) := + _ + + definition is_equiv_homotopy_group_functor_of_is_conn_fun_inf.{u} {A B : pType.{u}} (f : A →* B) + [is_conn_fun_inf f] (a : A) (k : ℕ) : is_equiv (homotopy_group_functor k f) := + is_equiv_π_of_is_connected f (le.refl k) + +end is_conn diff --git a/hott/types/int/hott.hlean b/hott/types/int/hott.hlean index 36ff46209..65bd2b566 100644 --- a/hott/types/int/hott.hlean +++ b/hott/types/int/hott.hlean @@ -18,6 +18,10 @@ namespace int Group.mk ℤ (group_of_add_group _) notation `gℤ` := group_integers + + definition CommGroup_int [constructor] : CommGroup := + CommGroup.mk ℤ ⦃comm_group, group_of_add_group ℤ, mul_comm := add.comm⦄ + notation `agℤ` := CommGroup_int end definition is_equiv_succ [instance] : is_equiv succ := diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index 408b0efc5..ea82806f5 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -182,6 +182,9 @@ namespace trunc_index definition sub_two_succ_succ (n : ℕ) : n.-2.+1.+1 = n := rfl definition succ_sub_two_succ (n : ℕ) : (nat.succ n).-2.+1 = n := rfl + definition of_nat_add_two (n : ℕ₋₂) : of_nat (add_two n) = n.+2 := + begin induction n with n IH, reflexivity, exact ap succ IH end + definition of_nat_le_of_nat {n m : ℕ} (H : n ≤ m) : (of_nat n ≤ of_nat m) := begin induction H with m H IH, @@ -224,6 +227,17 @@ namespace trunc_index { exact succ_le_succ H2'}} end + definition trunc_index.decidable_le [instance] : Π(n m : ℕ₋₂), decidable (n ≤ m) := + begin + intro n, induction n with n IH: intro m, + { left, apply minus_two_le}, + cases m with m, + { right, apply not_succ_le_minus_two}, + cases IH m with H H, + { left, apply succ_le_succ H}, + right, intro H2, apply H, exact le_of_succ_le_succ H2 + end + end trunc_index open trunc_index namespace is_trunc @@ -401,6 +415,7 @@ namespace is_trunc is_trunc (n.+1) A ↔ Π(a : A), is_trunc n (a = a) := iff.intro _ (is_trunc_succ_of_is_trunc_loop Hn) + -- use loopn in name 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 @@ -417,6 +432,7 @@ namespace is_trunc apply imp_iff, reflexivity} end + -- use loopn in name theorem is_trunc_iff_is_contr_loop (n : ℕ) (A : Type) : is_trunc (n.-2.+1) A ↔ (Π(a : A), is_contr (Ω[n](pointed.Mk a))) := begin @@ -427,6 +443,7 @@ namespace is_trunc { apply is_trunc_iff_is_contr_loop_succ}, end + -- rename to is_contr_loopn_of_is_trunc theorem is_contr_loop_of_is_trunc (n : ℕ) (A : Type*) [H : is_trunc (n.-2.+1) A] : is_contr (Ω[n] A) := begin @@ -434,6 +451,7 @@ namespace is_trunc apply iff.mp !is_trunc_iff_is_contr_loop H end + -- rename to is_trunc_loopn_of_is_trunc theorem is_trunc_loop_of_is_trunc (n : ℕ₋₂) (k : ℕ) (A : Type*) [H : is_trunc n A] : is_trunc n (Ω[k] A) := begin @@ -442,6 +460,17 @@ namespace is_trunc { apply is_trunc_eq} end + definition is_trunc_loopn (k : ℕ₋₂) (n : ℕ) (A : Type*) [H : is_trunc (k+n) A] + : is_trunc k (Ω[n] A) := + begin + revert k H, induction n with n IH: intro k H, exact _, + apply is_trunc_eq, apply IH, rewrite [succ_add_nat, add_nat_succ at H], exact H + end + + definition is_set_loopn (n : ℕ) (A : Type*) [is_trunc n A] : is_set (Ω[n] A) := + have is_trunc (0+[ℕ₋₂]n) A, by rewrite [trunc_index.zero_add]; exact _, + is_trunc_loopn 0 n A + end is_trunc open is_trunc namespace trunc @@ -496,7 +525,8 @@ namespace trunc intro p, induction p, induction aa with a, esimp, exact (tr idp) end - protected definition decode {n : ℕ₋₂} (aa aa' : trunc n.+1 A) : trunc.code n aa aa' → aa = aa' := + protected definition decode [unfold 3 4 5] {n : ℕ₋₂} (aa aa' : trunc n.+1 A) : + trunc.code n aa aa' → aa = aa' := begin induction aa' with a', induction aa with a, esimp [trunc.code, trunc.rec_on], intro x,