From 85b04639cb3895f3cb584cf23a12f31cc9b9363f Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 30 Jan 2018 20:28:15 -0500 Subject: [PATCH] higher groups: prove naturality of all adjunctions --- higher_groups.hlean | 34 +++++++++++++++++++++++----- move_to_lib.hlean | 54 ++++++++++++++++++++++++++++++++++++++++++++- pointed.hlean | 9 ++++++++ pointed_pi.hlean | 30 +++++++++++++++++++++++++ 4 files changed, 120 insertions(+), 7 deletions(-) diff --git a/higher_groups.hlean b/higher_groups.hlean index 93a4077..4879795 100644 --- a/higher_groups.hlean +++ b/higher_groups.hlean @@ -149,12 +149,12 @@ definition Decat_adjoint_Disc (G : [n+1;k]Grp) (H : [n;k]Grp) : pmap_ptrunc_pequiv (n + k) (B G) (B H) definition Decat_adjoint_Disc_natural {G G' : [n+1;k]Grp} {H H' : [n;k]Grp} - (eG : B G' ≃* B G) (eH : B H ≃* B H') : + (g : B G' →* B G) (h : B H →* B H') : psquare (Decat_adjoint_Disc G H) (Decat_adjoint_Disc G' H') - (ppcompose_left eH ∘* ppcompose_right (ptrunc_functor _ eG)) - (ppcompose_left eH ∘* ppcompose_right eG) := -sorry + (ppcompose_left h ∘* ppcompose_right (ptrunc_functor _ g)) + (ppcompose_left h ∘* ppcompose_right g) := +pmap_ptrunc_pequiv_natural (n + k) g h definition Decat_Disc (G : [n;k]Grp) : Decat (Disc G) = G := Grp_eq !ptrunc_pequiv @@ -195,6 +195,14 @@ 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)⁻¹ᵉ* +definition Deloop_adjoint_Loop_natural {G G' : [n;k+1]Grp} {H H' : [n+1;k]Grp} + (g : B G' →* B G) (h : B H →* B H') : + psquare (Deloop_adjoint_Loop G H) + (Deloop_adjoint_Loop G' H') + (ppcompose_left h ∘* ppcompose_right g) + (ppcompose_left (connect_functor k h) ∘* ppcompose_right g) := +(connect_intro_pequiv_natural g h _ _)⁻¹ʰ* + /- to do: naturality -/ definition Loop_Deloop (G : [n;k+1]Grp) : Loop (Deloop G) = G := @@ -223,6 +231,19 @@ definition Stabilize_adjoint_Forget (G : [n;k]Grp) (H : [n;k+1]Grp) : have is_trunc (n + k + 1) (B H), from !is_trunc_B, pmap_ptrunc_pequiv (n + k + 1) (⅀ (B G)) (B H) ⬝e* susp_adjoint_loop (B G) (B H) +definition Stabilize_adjoint_Forget_natural {G G' : [n;k]Grp} {H H' : [n;k+1]Grp} + (g : B G' →* B G) (h : B H →* B H') : + psquare (Stabilize_adjoint_Forget G H) + (Stabilize_adjoint_Forget G' H') + (ppcompose_left h ∘* ppcompose_right (ptrunc_functor (n+k+1) (⅀→ g))) + (ppcompose_left (Ω→ h) ∘* ppcompose_right g) := +begin + have is_trunc (n + k + 1) (B H), from !is_trunc_B, + have is_trunc (n + k + 1) (B H'), from !is_trunc_B, + refine pmap_ptrunc_pequiv_natural (n+k+1) (⅀→ g) h ⬝h* _, + exact susp_adjoint_loop_natural_left g ⬝v* susp_adjoint_loop_natural_right h +end + /- to do: naturality -/ definition ωForget (k : ℕ) (G : [n;ω]Grp) : [n;k]Grp := @@ -348,14 +369,15 @@ sorry --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 Decat_adjoint_Disc_natural print axioms Deloop_adjoint_Loop +print axioms Deloop_adjoint_Loop_natural print axioms Stabilize_adjoint_Forget +print axioms Stabilize_adjoint_Forget_natural print axioms stabilization print axioms is_trunc_Grp diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 8a8570e..1a0841d 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -1129,6 +1129,33 @@ pmap.mk (fiber_functor g h H (respect_pt h)) exact !con.assoc ⬝ to_homotopy_pt H end +definition ppoint_natural {A A' B B' : Type*} {f : A →* B} {f' : A' →* B'} + (g : A →* A') (h : B →* B') (H : psquare g h f f') : + psquare (ppoint f) (ppoint f') (pfiber_functor g h H) g := +begin + fapply phomotopy.mk, + { intro x, reflexivity }, + { refine !idp_con ⬝ _ ⬝ !idp_con⁻¹, esimp, apply point_fiber_eq } +end + +/- if we need this: do pfiber_functor_pcompose and so on first -/ +-- definition psquare_pfiber_functor [constructor] {A₁ A₂ A₃ A₄ B₁ B₂ B₃ B₄ : Type*} +-- {f₁ : A₁ →* B₁} {f₂ : A₂ →* B₂} {f₃ : A₃ →* B₃} {f₄ : A₄ →* B₄} +-- {g₁₂ : A₁ →* A₂} {g₃₄ : A₃ →* A₄} {g₁₃ : A₁ →* A₃} {g₂₄ : A₂ →* A₄} +-- {h₁₂ : B₁ →* B₂} {h₃₄ : B₃ →* B₄} {h₁₃ : B₁ →* B₃} {h₂₄ : B₂ →* B₄} +-- (H₁₂ : psquare g₁₂ h₁₂ f₁ f₂) (H₃₄ : psquare g₃₄ h₃₄ f₃ f₄) +-- (H₁₃ : psquare g₁₃ h₁₃ f₁ f₃) (H₂₄ : psquare g₂₄ h₂₄ f₂ f₄) +-- (G : psquare g₁₂ g₃₄ g₁₃ g₂₄) (H : psquare h₁₂ h₃₄ h₁₃ h₂₄) +-- /- pcube H₁₂ H₃₄ H₁₃ H₂₄ G H -/ : +-- psquare (pfiber_functor g₁₂ h₁₂ H₁₂) (pfiber_functor g₃₄ h₃₄ H₃₄) +-- (pfiber_functor g₁₃ h₁₃ H₁₃) (pfiber_functor g₂₄ h₂₄ H₂₄) := +-- begin +-- fapply phomotopy.mk, +-- { intro x, induction x with x p, induction B₁ with B₁ b₁₀, induction f₁ with f₁ f₁₀, esimp at *, +-- induction p, esimp [fiber_functor], }, +-- { } +-- end + -- TODO: use this in pfiber_pequiv_of_phomotopy definition fiber_equiv_of_homotopy {A B : Type} {f g : A → B} (h : f ~ g) (b : B) : fiber f b ≃ fiber g b := @@ -1361,7 +1388,7 @@ definition connect_intro_equiv [constructor] {k : ℕ} {X : Type*} (Y : Type*) ( (X →* connect k Y) ≃ (X →* Y) := begin fapply equiv.MK, - { intro f, exact ppoint (ptr k Y) ∘* f }, + { intro f, exact ppoint (ptr k Y) ∘* f }, { intro g, exact connect_intro H g }, { intro g, apply eq_of_phomotopy, exact ppoint_connect_intro H g }, { intro f, apply eq_of_phomotopy, exact connect_intro_ppoint H f } @@ -1386,6 +1413,31 @@ loopn_pfiber (k+1) (ptr k X) ⬝e* definition is_conn_of_is_conn_succ_nat (n : ℕ) (A : Type) [is_conn (n+1) A] : is_conn n A := is_conn_of_is_conn_succ n A +definition connect_functor (k : ℕ) {X Y : Type*} (f : X →* Y) : connect k X →* connect k Y := +pfiber_functor f (ptrunc_functor k f) (ptr_natural k f)⁻¹* + +definition connect_intro_pequiv_natural {k : ℕ} {X X' : Type*} {Y Y' : Type*} (f : X' →* X) + (g : Y →* Y') (H : is_conn k X) (H' : is_conn k X') : + psquare (connect_intro_pequiv Y H) (connect_intro_pequiv Y' H') + (ppcompose_left (connect_functor k g) ∘* ppcompose_right f) + (ppcompose_left g ∘* ppcompose_right f) := +begin + refine _ ⬝v* _, exact connect_intro_pequiv Y H', + { fapply phomotopy.mk, + { intro h, apply eq_of_phomotopy, apply passoc }, + { xrewrite [▸*, pcompose_right_eq_of_phomotopy, pcompose_left_eq_of_phomotopy, + -+eq_of_phomotopy_trans], + apply ap eq_of_phomotopy, apply passoc_pconst_middle }}, + { fapply phomotopy.mk, + { intro h, apply eq_of_phomotopy, + refine !passoc⁻¹* ⬝* pwhisker_right h (ppoint_natural _ _ _) ⬝* !passoc }, + { xrewrite [▸*, +pcompose_left_eq_of_phomotopy, -+eq_of_phomotopy_trans], + apply ap eq_of_phomotopy, + refine !trans_assoc ⬝ idp ◾** !passoc_pconst_right ⬝ _, + refine !trans_assoc ⬝ idp ◾** !pcompose_pconst_phomotopy ⬝ _, + apply symm_trans_eq_of_eq_trans, symmetry, apply passoc_pconst_right }} +end + end is_conn namespace misc diff --git a/pointed.hlean b/pointed.hlean index ee9240b..fd5b27f 100644 --- a/pointed.hlean +++ b/pointed.hlean @@ -202,6 +202,15 @@ namespace pointed -- definition phomotopy_eq_equiv_phomotopy2 : p = q ≃ p ~*2 q := -- sorry + definition pconst_pcompose_phomotopy {A B C : Type*} {f f' : A →* B} (p : f ~* f') : + pwhisker_left (pconst B C) p ⬝* pconst_pcompose f' = pconst_pcompose f := + begin + fapply phomotopy_eq, + { intro a, apply ap_constant }, + { induction p using phomotopy_rec_idp, induction B with B b₀, induction f with f f₀, + esimp at *, induction f₀, reflexivity } + end + /- Homotopy between a function and its eta expansion -/ definition pmap_eta [constructor] {X Y : Type*} (f : X →* Y) : f ~* pmap.mk f (respect_pt f) := diff --git a/pointed_pi.hlean b/pointed_pi.hlean index 26aee60..446f324 100644 --- a/pointed_pi.hlean +++ b/pointed_pi.hlean @@ -940,3 +940,33 @@ namespace is_conn end end is_conn + + +/- TODO: move, these facts use some of these pointed properties -/ + +namespace trunc + +lemma pmap_ptrunc_pequiv_natural [constructor] (n : ℕ₋₂) {A A' B B' : Type*} + [H : is_trunc n B] [H : is_trunc n B'] (f : A' →* A) (g : B →* B') : + psquare (pmap_ptrunc_pequiv n A B) (pmap_ptrunc_pequiv n A' B') + (ppcompose_left g ∘* ppcompose_right (ptrunc_functor n f)) + (ppcompose_left g ∘* ppcompose_right f) := +begin + refine _ ⬝v* _, exact pmap_ptrunc_pequiv n A' B, + { fapply phomotopy.mk, + { intro h, apply eq_of_phomotopy, + exact !passoc ⬝* pwhisker_left h (ptr_natural n f)⁻¹* ⬝* !passoc⁻¹* }, + { xrewrite [▸*, +pcompose_right_eq_of_phomotopy, -+eq_of_phomotopy_trans], + apply ap eq_of_phomotopy, + refine !trans_assoc ⬝ idp ◾** (!trans_assoc⁻¹ ⬝ (eq_bot_of_phsquare (phtranspose + (passoc_pconst_left (ptrunc_functor n f) (ptr n A'))))⁻¹) ⬝ _, + refine !trans_assoc ⬝ idp ◾** !pconst_pcompose_phomotopy ⬝ _, + apply passoc_pconst_left }}, + { fapply phomotopy.mk, + { intro h, apply eq_of_phomotopy, exact !passoc⁻¹* }, + { xrewrite [▸*, pcompose_right_eq_of_phomotopy, pcompose_left_eq_of_phomotopy, + -+eq_of_phomotopy_trans], + apply ap eq_of_phomotopy, apply symm_trans_eq_of_eq_trans, symmetry, + apply passoc_pconst_middle }} +end +end trunc