From e0365d2c65fc3fa9624dc6d5e2d3a8ef5cd18f6b Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 29 Jan 2018 15:30:10 -0500 Subject: [PATCH] higher_groups: finish adjunction between loop and deloop --- higher_groups.hlean | 43 ++++++++++++++++++++++++++++--------------- move_to_lib.hlean | 35 +++++++++++++++++++---------------- 2 files changed, 47 insertions(+), 31 deletions(-) diff --git a/higher_groups.hlean b/higher_groups.hlean index af8ecfb..854a98f 100644 --- a/higher_groups.hlean +++ b/higher_groups.hlean @@ -180,7 +180,7 @@ Grp.mk (ptrunctype.mk (Ω G) !is_trunc_loop_nat pt) 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 -/ +(connect_intro_pequiv _ !is_conn_pconntype)⁻¹ᵉ* /- to do: naturality -/ @@ -263,8 +263,21 @@ definition ωStabilize_of_le (H : k ≥ n + 2) (G : [n;k]Grp) : [n;ω]Grp := definition ωStabilize (G : [n;k]Grp) : [n;ω]Grp := ωStabilize_of_le !le_max_left (nStabilize !le_max_right G) +theorem ωstabilization (H : k ≥ n + 2) : is_equiv (@ωStabilize n k) := +sorry + /- to do: adjunction (and ωStabilize ∘ ωForget =?= id) -/ +definition Grp_hom (G H : [n;k]Grp) : Type := +B G →* B H + +definition is_trunc_Grp_hom (G H : [n;k]Grp) : is_trunc n (Grp_hom G H) := +is_trunc_pmap_of_is_conn _ (k.-2) _ (k + n) _ (le_of_eq (sub_one_add_plus_two_sub_one k n)⁻¹) + (is_trunc_B' H) + +definition is_set_Grp_hom (G H : [0;k]Grp) : is_set (Grp_hom G H) := +is_trunc_Grp_hom G H + definition is_trunc_Grp (n k : ℕ) : is_trunc (n + 1) [n;k]Grp := begin apply @is_trunc_equiv_closed_rev _ _ (n + 1) (Grp_equiv n k), @@ -272,18 +285,9 @@ begin apply @is_trunc_equiv_closed_rev _ _ _ (ptruncconntype_eq_equiv X Y), apply @is_trunc_equiv_closed_rev _ _ _ (pequiv.sigma_char_pmap X Y), apply @is_trunc_subtype (X →* Y) (λ f, trunctype.mk' -1 (is_equiv f)), - apply is_trunc_pmap_of_is_conn X k.-2 (n.-1) (n + k) Y, - { apply le_of_eq, exact (sub_one_add_plus_two_sub_one n k)⁻¹ ⬝ !add_plus_two_comm }, - { exact _ } + exact is_trunc_Grp_hom ((Grp_equiv n k)⁻¹ᵉ X) ((Grp_equiv n k)⁻¹ᵉ Y) 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 := @@ -298,10 +302,8 @@ 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 +definition cGrp_equivalence_Grp [constructor] : cGrp 1 ≃c category.Grp := +sorry -- set_option pp.all true -- definition cGrp_equivalence_Grp [constructor] : cGrp 1 ≃c category.Grp := @@ -320,5 +322,16 @@ sorry -- (equivalence.symm Grp_equivalence_cptruncconntype') +--has sorry +print axioms ωstabilization +print axioms Decat_adjoint_Disc_natural +print axioms cGrp_equivalence_Grp + + +-- no sorry's +print axioms Decat_adjoint_Disc +print axioms Deloop_adjoint_Loop +print axioms stabilization +print axioms is_trunc_Grp end higher_group diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 6a47a79..ce23989 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -24,6 +24,15 @@ end algebra namespace eq + -- this should maybe replace whisker_left_idp and whisker_left_idp_con + definition whisker_left_idp_square {A : Type} {a a' : A} {p q : a = a'} (r : p = q) : + square (whisker_left idp r) r (idp_con p) (idp_con q) := + begin induction r, exact hrfl end + + definition ap_con_idp_left {A B : Type} (f : A → B) {a a' : A} (p : a = a') : + square (ap_con f idp p) idp (ap02 f (idp_con p)) (idp_con (ap f p)) := + begin induction p, exact ids end + definition pathover_tr_pathover_idp_of_eq {A : Type} {B : A → Type} {a a' : A} {b : B a} {b' : B a'} {p : a = a'} (q : b =[p] b') : pathover_tr p b ⬝o pathover_idp_of_eq (tr_eq_of_pathover q) = q := @@ -1321,29 +1330,23 @@ definition connect_intro_ppoint [constructor] {k : ℕ} {X : Type*} {Y : Type*} (f : X →* connect k Y) : connect_intro H (ppoint (ptr k Y) ∘* f) ~* f := begin cases f with f f₀, - -- revert f₀, refine equiv_rect (fiber_eq_equiv' _ _)⁻¹ᵉ _ _, - -- revert f, - -- refine equiv_rect (!sigma_pi_equiv_pi_sigma ⬝e arrow_equiv_arrow_right _ !fiber.sigma_char⁻¹ᵉ) _ _, - -- intro fg pq, induction pq with p q, induction fg with f g, - -- induction Y with Y y₀, esimp at *, esimp [connect] at (f, p, q), induction p, fapply phomotopy.mk, { intro x, fapply fiber_eq, reflexivity, refine @is_conn.elim (k.-1) _ _ _ (λx', !is_trunc_eq) _ x, refine !is_conn.elim_β ⬝ _, refine _ ⬝ !idp_con⁻¹, - refine !ap_compose⁻¹ ⬝ _, - exact ap_is_constant point_eq f₀ }, - { esimp, - refine whisker_left _ !fiber_eq_eta ⬝ !fiber_eq_con ⬝ apd011 fiber_eq !idp_con _, - esimp, + symmetry, refine _ ⬝ !con_idp, exact fiber_eq_pr2 f₀ }, + { esimp, refine whisker_left _ !fiber_eq_eta ⬝ !fiber_eq_con ⬝ apd011 fiber_eq !idp_con _, esimp, apply eq_pathover_constant_left, refine whisker_right _ (whisker_right _ (whisker_right _ !is_conn.elim_β)) ⬝pv _, - exact sorry - --apply move_bot_of_left, - --- refine whisker_right _ _ ⬝ _, --- refine !is_conn.elim_β ⬝ _, - } + esimp [connect], refine _ ⬝vp !con_idp, + apply move_bot_of_left, refine !idp_con ⬝ !con_idp⁻¹ ⬝ph _, + refine !con.assoc ⬝ !con.assoc ⬝pv _, apply whisker_tl, + note r := eq_bot_of_square (transpose (whisker_left_idp_square (fiber_eq_pr2 f₀))⁻¹ᵛ), + refine !con.assoc⁻¹ ⬝ whisker_right _ r⁻¹ ⬝pv _, clear r, + apply move_top_of_left, + refine whisker_right_idp (ap_con tr idp (ap point f₀))⁻¹ᵖ ⬝pv _, + exact (ap_con_idp_left tr (ap point f₀))⁻¹ʰ } end definition connect_intro_equiv [constructor] {k : ℕ} {X : Type*} (Y : Type*) (H : is_conn k X) :