From 0949070096736681d64ec6fdcdf5f455b9b59dd5 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sun, 28 Jan 2018 18:05:45 -0500 Subject: [PATCH] Prove stabilization and work on equivalence of categories --- higher_groups.hlean | 87 ++++++++++++++++++++++++++++++++++++++++----- homotopy/susp.hlean | 3 ++ move_to_lib.hlean | 22 ++++++++++++ 3 files changed, 103 insertions(+), 9 deletions(-) diff --git a/higher_groups.hlean b/higher_groups.hlean index be93c76..af8ecfb 100644 --- a/higher_groups.hlean +++ b/higher_groups.hlean @@ -6,9 +6,9 @@ Authors: Ulrik Buchholtz, Egbert Rijke, Floris van Doorn Formalization of the higher groups paper -/ -import .pointed_pi +import .homotopy.EM open eq is_conn pointed is_trunc trunc equiv is_equiv trunc_index susp nat algebra - prod.ops sigma sigma.ops + prod.ops sigma sigma.ops category EM namespace higher_group set_option pp.binder_types true universe variable u @@ -120,7 +120,7 @@ definition InfGrp_eq {k : ℕ} {G H : [∞;k]Grp} (e : iB G ≃* iB H) : G = H : -- maybe to do: ωGrp ≃ Σ(X : spectrum), is_sconn n X -/- Constructions -/ +/- Constructions on higher groups -/ definition Decat (G : [n+1;k]Grp) : [n;k]Grp := Grp.mk (ptrunctype.mk (ptrunc n G) _ pt) (pconntype.mk (ptrunc (n + k) (B G)) _ pt) abstract begin @@ -182,11 +182,11 @@ definition Deloop_adjoint_Loop (G : [n;k+1]Grp) (H : [n+1;k]Grp) : ppmap (B (Deloop G)) (B H) ≃* ppmap (B G) (B (Loop H)) := (connect_intro_pequiv _ !is_conn_pconntype)⁻¹ᵉ* /- still a sorry here -/ +/- to do: naturality -/ + definition Loop_Deloop (G : [n;k+1]Grp) : Loop (Deloop G) = G := Grp_eq (connect_pequiv (is_conn_pconntype (B G))) -/- to do: adjunction, and Loop ∘ Deloop = id -/ - definition Forget (G : [n;k+1]Grp) : [n;k]Grp := have is_conn k (B G), from !is_conn_pconntype, Grp.mk G (pconntype.mk (Ω (B G)) !is_conn_loop pt) @@ -217,11 +217,36 @@ begin induction H with l H IH, exact G, exact Stabilize IH end -lemma Stabilize_pequiv (H : k ≥ n + 2) (G : [n;k]Grp) : B G ≃* Ω (B (Stabilize G)) := -sorry +definition Forget_Stabilize (H : k ≥ n + 2) (G : [n;k]Grp) : B (Forget (Stabilize G)) ≃* B G := +loop_ptrunc_pequiv _ _ ⬝e* +begin + cases k with k, + { cases H }, + { have k ≥ succ n, from le_of_succ_le_succ H, + assert this : n + succ k ≤ 2 * k, + { rewrite [two_mul, add_succ, -succ_add], exact nat.add_le_add_right this k }, + exact freudenthal_pequiv (B G) this } +end⁻¹ᵉ* ⬝e* +ptrunc_pequiv (n + k) _ + +definition Stabilize_Forget (H : k ≥ n + 1) (G : [n;k+1]Grp) : B (Stabilize (Forget G)) ≃* B G := +begin + assert lem1 : n + succ k ≤ 2 * k, + { rewrite [two_mul, add_succ, -succ_add], exact nat.add_le_add_right H k }, + have is_conn k (B G), from !is_conn_pconntype, + have Π(G' : [n;k+1]Grp), is_trunc (n + k + 1) (B G'), from is_trunc_B, + note z := is_conn_fun_loop_susp_counit (B G) (nat.le_refl (2 * k)), + refine ptrunc_pequiv_ptrunc_of_le (of_nat_le_of_nat lem1) (@(ptrunc_pequiv_ptrunc_of_is_conn_fun _ _) z) ⬝e* + !ptrunc_pequiv, +end theorem stabilization (H : k ≥ n + 2) : is_equiv (@Stabilize n k) := -sorry +begin + fapply adjointify, + { exact Forget }, + { intro G, apply Grp_eq, exact Stabilize_Forget (le.trans !self_le_succ H) _ }, + { intro G, apply Grp_eq, exact Forget_Stabilize H G } +end definition ωGrp.mk_le {n : ℕ} (k₀ : ℕ) (B : Π⦃k : ℕ⦄, k₀ ≤ k → (n+k)-Type*[k.-1]) @@ -233,7 +258,7 @@ sorry definition ωStabilize_of_le (H : k ≥ n + 2) (G : [n;k]Grp) : [n;ω]Grp := ωGrp.mk_le k (λl H', Grp_equiv n l (nStabilize H' G)) - (λl H', Stabilize_pequiv (le.trans H H') (nStabilize H' G)) + (λl H', (Forget_Stabilize (le.trans H H') (nStabilize H' G))⁻¹ᵉ*) definition ωStabilize (G : [n;k]Grp) : [n;ω]Grp := ωStabilize_of_le !le_max_left (nStabilize !le_max_right G) @@ -252,4 +277,48 @@ begin { exact _ } end +definition Grp_hom (G H : [n;k]Grp) : Type := +B G →* B H + +definition is_set_Grp_hom (G H : [0;k]Grp) : is_set (Grp_hom G H) := +is_trunc_pmap_of_is_conn _ (k.-2) _ k _ (le_of_eq (sub_one_add_plus_two_sub_one k 0)⁻¹) + (is_trunc_B' H) + +local attribute [instance] is_set_Grp_hom + +definition Grp_precategory [constructor] (k : ℕ) : precategory [0;k]Grp := +precategory.mk (λG H, Grp_hom G H) (λX Y Z g f, g ∘* f) (λX, pid (B X)) + begin intros, apply eq_of_phomotopy, exact !passoc⁻¹* end + begin intros, apply eq_of_phomotopy, apply pid_pcompose end + begin intros, apply eq_of_phomotopy, apply pcompose_pid end + +definition cGrp [constructor] (k : ℕ) : Precategory := +Precategory.mk _ (Grp_precategory k) + +definition cGrp_equivalence_cType [constructor] (k : ℕ) : cGrp k ≃c cType*[k.-1] := +sorry + +-- print category.Grp +-- set_option pp.universes true +-- print equivalence.symm +-- print equivalence.trans + +-- set_option pp.all true +-- definition cGrp_equivalence_Grp [constructor] : cGrp 1 ≃c category.Grp := +-- equivalence.trans +-- _ +-- (equivalence.symm Grp_equivalence_cptruncconntype') +-- begin +-- transitivity cptruncconntype'.{u} 0, +-- exact sorry, +-- symmetry, exact Grp_equivalence_cptruncconntype' +-- end +-- category.equivalence.{u+1 u u+1 u} (category.Category.to_Precategory.{u+1 u} category.Grp.{u}) +-- (EM.cptruncconntype'.{u} (@zero.{0} trunc_index has_zero_trunc_index)) +-- equivalence.trans +-- _ +-- (equivalence.symm Grp_equivalence_cptruncconntype') + + + end higher_group diff --git a/homotopy/susp.hlean b/homotopy/susp.hlean index 73c8b19..88a7bc9 100644 --- a/homotopy/susp.hlean +++ b/homotopy/susp.hlean @@ -78,6 +78,7 @@ sorry -- we end up not using this, because to prove that the -- composition with the first projection is loop_susp_counit A -- is hideous without HIT computations on path constructors + parameter (A) definition pullback_diagonal_prod_of_wedge : susp (Ω A) ≃ Σ (a : A) (w : wedge A A), prod_of_wedge w = (a, a) := begin @@ -116,6 +117,7 @@ sorry induction z with p q, reflexivity } end + parameter {A} -- instead we directly compare the fibers, using flattening twice definition fiber_loop_susp_counit_equiv (a : A) : fiber (loop_susp_counit A) a ≃ fiber prod_of_wedge (a, a) := @@ -166,6 +168,7 @@ sorry open is_conn trunc_index + parameter (A) -- connectivity of loop_susp_counit definition is_conn_fun_loop_susp_counit {k : ℕ} (H : k ≤ 2 * n) : is_conn_fun k (loop_susp_counit A) := diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 2002409..6a47a79 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -1209,6 +1209,11 @@ namespace is_conn open unit trunc_index nat is_trunc pointed.ops sigma.ops prod.ops +-- todo: make trunc_equiv_trunc_of_is_conn_fun a def. +definition ptrunc_pequiv_ptrunc_of_is_conn_fun {A B : Type*} (n : ℕ₋₂) (f : A →* B) + [H : is_conn_fun n f] : ptrunc n A ≃* ptrunc n B := +pequiv_of_pmap (ptrunc_functor n f) (is_equiv_trunc_functor_of_is_conn_fun n f) + definition is_conn_zero {A : Type} (a₀ : trunc 0 A) (p : Πa a' : A, ∥ a = a' ∥) : is_conn 0 A := is_conn_succ_intro a₀ (λa a', is_conn_minus_one _ (p a a')) @@ -1753,6 +1758,23 @@ end end list + +namespace susp +open trunc_index +/- move to freudenthal -/ +definition freudenthal_pequiv_trunc_index' (A : Type*) (n : ℕ) (k : ℕ₋₂) [HA : is_conn n A] + (H : k ≤ of_nat (2 * n)) : ptrunc k A ≃* ptrunc k (Ω (susp A)) := +begin + assert lem : Π(l : ℕ₋₂), l ≤ 0 → ptrunc l A ≃* ptrunc l (Ω (susp A)), + { intro l H', exact ptrunc_pequiv_ptrunc_of_le H' (freudenthal_pequiv A (zero_le (2 * n))) }, + cases k with k, { exact lem -2 (minus_two_le 0) }, + cases k with k, { exact lem -1 (succ_le_succ (minus_two_le -1)) }, + rewrite [-of_nat_add_two at *, add_two_sub_two at HA], + exact freudenthal_pequiv A (le_of_of_nat_le_of_nat H) +end + +end susp + /- namespace logic? -/ namespace decidable definition double_neg_elim {A : Type} (H : decidable A) (p : ¬ ¬ A) : A :=