From c3650048f0e5c588cf1c8a2d29308f528dc110bb Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 10 Sep 2018 18:01:44 +0200 Subject: [PATCH] fixes and additions add some properties about pointed maps and groups --- higher_groups.hlean | 4 +- homotopy/EM.hlean | 184 +++++++++++++++++---------------- homotopy/smash_adjoint.hlean | 8 +- homotopy/susp.hlean | 18 ++-- move_to_lib.hlean | 70 +++++++++++-- pointed.hlean | 142 ++++++++++++------------- pointed_pi.hlean | 118 +++++++++++++++++---- spectrum/basic.hlean | 11 +- spectrum/spectrification.hlean | 2 +- 9 files changed, 343 insertions(+), 214 deletions(-) diff --git a/higher_groups.hlean b/higher_groups.hlean index afd5f22..b4c8de3 100644 --- a/higher_groups.hlean +++ b/higher_groups.hlean @@ -28,7 +28,7 @@ is_conn_fun_prod_of_wedge n m A B definition is_trunc_ppi_of_is_conn (k n : ℕ) (X : Type*) (H : is_conn (k.-1) X) (Y : X → Type*) (H3 : Πx, is_trunc (k + n) (Y x)) : is_trunc n (Π*(x : X), Y x) := -is_conn.is_trunc_ppi_of_is_conn _ (k.-2) _ _ (le_of_eq (sub_one_add_plus_two_sub_one k n)⁻¹) _ H3 +is_conn.is_trunc_ppi_of_is_conn _ (k.-2) H _ _ (le_of_eq (sub_one_add_plus_two_sub_one k n)⁻¹) _ H3 end hide @@ -396,7 +396,7 @@ end -/ definition is_trunc_GType_hom (G H : [n;k]GType) : is_trunc n (GType_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_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_GType_hom (G H : [0;k]GType) : is_set (GType_hom G H) := diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean index ca703d0..77f5ca2 100644 --- a/homotopy/EM.hlean +++ b/homotopy/EM.hlean @@ -10,32 +10,6 @@ universe variable u namespace EM - /- move to HoTT-EM, this version doesn't require that X is connected -/ - definition EM1_map' [unfold 6] {G : Group} {X : Type*} (e : G → Ω X) - (r : Πg h, e (g * h) = e g ⬝ e h) [is_trunc 1 X] : EM1 G → X := - begin - intro x, induction x using EM.elim, - { exact Point X }, - { exact e g }, - { exact r g h } - end - - definition EM1_pmap' [constructor] {G : Group} {X : Type*} (e : G → Ω X) - (r : Πg h, e (g * h) = e g ⬝ e h) [is_trunc 1 X] : EM1 G →* X := - pmap.mk (EM1_map' e r) idp - - definition loop_EM1_pmap' {G : Group} {X : Type*} (e : G →* Ω X) - (r : Πg h, e (g * h) = e g ⬝ e h) [is_trunc 1 X] : Ω→(EM1_pmap' e r) ∘* loop_EM1 G ~* e := - begin - fapply phomotopy.mk, - { intro g, refine !idp_con ⬝ elim_pth r g }, - { apply is_set.elim } - end - - definition EMadd1_functor_succ [unfold_full] {G H : AbGroup} (φ : G →g H) (n : ℕ) : - EMadd1_functor φ (succ n) ~* ptrunc_functor (n+2) (susp_functor (EMadd1_functor φ n)) := - by reflexivity - definition EM1_functor_gid (G : Group) : EM1_functor (gid G) ~* !pid := begin fapply phomotopy.mk, @@ -183,30 +157,27 @@ namespace EM by reflexivity definition ap1_EMadd1_natural {G H : AbGroup} (φ : G →g H) (n : ℕ) : - Ω→ (EMadd1_functor φ (succ n)) ∘* loop_EMadd1 G n ~* loop_EMadd1 H n ∘* EMadd1_functor φ n := + psquare (loop_EMadd1 G n) (loop_EMadd1 H n) + (EMadd1_functor φ n) (Ω→ (EMadd1_functor φ (succ n))) := begin - refine pwhisker_right _ (ap1_phomotopy !EMadd1_functor_succ) ⬝* _, + refine _ ⬝hp* Ω⇒ !EMadd1_functor_succ, induction n with n IH, - { refine pwhisker_left _ !hopf.to_pmap_delooping_pinv ⬝* _ ⬝* - pwhisker_right _ !hopf.to_pmap_delooping_pinv⁻¹*, - refine !loop_susp_unit_natural⁻¹* ⬝h* _, - apply ap1_psquare, - apply ptr_natural }, - { refine pwhisker_left _ !loop_EMadd1_succ ⬝* _ ⬝* pwhisker_right _ !loop_EMadd1_succ⁻¹*, + { refine !hopf.to_pmap_delooping_pinv ⬝pv* _ ⬝vp* !hopf.to_pmap_delooping_pinv, + exact !loop_susp_unit_natural ⬝h* ap1_psquare !ptr_natural }, + { refine !loop_EMadd1_succ ⬝pv* _ ⬝vp* !loop_EMadd1_succ, refine _ ⬝h* !ap1_ptrunc_functor, refine (@(ptrunc_pequiv_natural (n+1+1) _) _ _)⁻¹ʰ* ⬝h* _, - refine pwhisker_left _ !to_pmap_freudenthal_pequiv ⬝* _ ⬝* - pwhisker_right _ !to_pmap_freudenthal_pequiv⁻¹*, + refine !to_pmap_freudenthal_pequiv ⬝pv* _ ⬝vp* !to_pmap_freudenthal_pequiv, apply ptrunc_functor_psquare, - exact !loop_susp_unit_natural⁻¹* } + exact !loop_susp_unit_natural } end definition apn_EMadd1_pequiv_EM1_natural {G H : AbGroup} (φ : G →g H) (n : ℕ) : - Ω→[n] (EMadd1_functor φ n) ∘* loopn_EMadd1_pequiv_EM1 G n ~* - loopn_EMadd1_pequiv_EM1 H n ∘* EM1_functor φ := + psquare (loopn_EMadd1_pequiv_EM1 G n) (loopn_EMadd1_pequiv_EM1 H n) + (EM1_functor φ) (Ω→[n] (EMadd1_functor φ n)) := begin induction n with n IH, - { reflexivity }, + { exact phomotopy.rfl }, { refine pwhisker_left _ !loopn_EMadd1_pequiv_EM1_succ ⬝* _, refine _ ⬝* pwhisker_right _ !loopn_EMadd1_pequiv_EM1_succ⁻¹*, refine _ ⬝h* !loopn_succ_in_inv_natural, @@ -214,8 +185,8 @@ namespace EM end definition homotopy_group_functor_EMadd1_functor {G H : AbGroup} (φ : G →g H) (n : ℕ) : - π→g[n+1] (EMadd1_functor φ n) ∘ ghomotopy_group_EMadd1' G n ~ - ghomotopy_group_EMadd1' H n ∘ φ := + hsquare (ghomotopy_group_EMadd1' G n) (ghomotopy_group_EMadd1' H n) + φ (π→g[n+1] (EMadd1_functor φ n)) := begin refine hwhisker_left _ (to_fun_isomorphism_trans _ _) ⬝hty _ ⬝hty hwhisker_right _ (to_fun_isomorphism_trans _ _)⁻¹ʰᵗʸ, @@ -224,14 +195,13 @@ namespace EM end definition homotopy_group_functor_EMadd1_functor' {G H : AbGroup} (φ : G →g H) (n : ℕ) : - φ ∘ (ghomotopy_group_EMadd1' G n)⁻¹ᵍ ~ - (ghomotopy_group_EMadd1' H n)⁻¹ᵍ ∘ π→g[n+1] (EMadd1_functor φ n) := + hsquare (ghomotopy_group_EMadd1' G n)⁻¹ᵍ (ghomotopy_group_EMadd1' H n)⁻¹ᵍ + (π→g[n+1] (EMadd1_functor φ n)) φ := (homotopy_group_functor_EMadd1_functor φ n)⁻¹ʰᵗʸʰ definition EM1_pmap_natural {G H : Group} {X Y : Type*} (f : X →* Y) (eX : G → Ω X) (eY : H → Ω Y) (rX : Πg h, eX (g * h) = eX g ⬝ eX h) (rY : Πg h, eY (g * h) = eY g ⬝ eY h) - [H1 : is_conn 0 X] [H2 : is_trunc 1 X] [is_conn 0 Y] [is_trunc 1 Y] - (φ : G →g H) (p : hsquare eX eY φ (Ω→ f)) : + [H2 : is_trunc 1 X] [is_trunc 1 Y] (φ : G →g H) (p : hsquare eX eY φ (Ω→ f)) : psquare (EM1_pmap eX rX) (EM1_pmap eY rY) (EM1_functor φ) f := begin fapply phomotopy.mk, @@ -247,14 +217,14 @@ namespace EM definition EM1_pequiv'_natural {G H : Group} {X Y : Type*} (f : X →* Y) (eX : G ≃* Ω X) (eY : H ≃* Ω Y) (rX : Πg h, eX (g * h) = eX g ⬝ eX h) (rY : Πg h, eY (g * h) = eY g ⬝ eY h) [H1 : is_conn 0 X] [H2 : is_trunc 1 X] [is_conn 0 Y] [is_trunc 1 Y] - (φ : G →g H) (p : Ω→ f ∘ eX ~ eY ∘ φ) : - f ∘* EM1_pequiv' eX rX ~* EM1_pequiv' eY rY ∘* EM1_functor φ := + (φ : G →g H) (p : hsquare eX eY φ (Ω→ f)) : + psquare (EM1_pequiv' eX rX) (EM1_pequiv' eY rY) (EM1_functor φ) f := EM1_pmap_natural f eX eY rX rY φ p definition EM1_pequiv_natural {G H : Group} {X Y : Type*} (f : X →* Y) (eX : G ≃g π₁ X) (eY : H ≃g π₁ Y) [H1 : is_conn 0 X] [H2 : is_trunc 1 X] [is_conn 0 Y] [is_trunc 1 Y] - (φ : G →g H) (p : π→g[1] f ∘ eX ~ eY ∘ φ) : - f ∘* EM1_pequiv eX ~* EM1_pequiv eY ∘* EM1_functor φ := + (φ : G →g H) (p : hsquare eX eY φ (π→g[1] f)) : + psquare (EM1_pequiv eX) (EM1_pequiv eY) (EM1_functor φ) f := EM1_pequiv'_natural f _ _ _ _ φ begin assert p' : ptrunc_functor 0 (Ω→ f) ∘* pequiv_of_isomorphism eX ~* @@ -262,67 +232,71 @@ namespace EM exact p' ⬝h* (ptrunc_pequiv_natural 0 (Ω→ f)), end - definition EM1_pequiv_type_natural {X Y : Type*} (f : X →* Y) [H1 : is_conn 0 X] [H2 : is_trunc 1 X] - [H3 : is_conn 0 Y] [H4 : is_trunc 1 Y] : - f ∘* EM1_pequiv_type X ~* EM1_pequiv_type Y ∘* EM1_functor (π→g[1] f) := - begin refine EM1_pequiv_natural f _ _ _ _, reflexivity end + definition EM1_pequiv_type_natural {X Y : Type*} (f : X →* Y) + [H1 : is_conn 0 X] [H2 : is_trunc 1 X] [H3 : is_conn 0 Y] [H4 : is_trunc 1 Y] : + psquare (EM1_pequiv_type X) (EM1_pequiv_type Y) (EM1_functor (π→g[1] f)) f := + begin refine EM1_pequiv_natural f _ _ _ _, exact homotopy.rfl end definition EM_up_natural {G H : AbGroup} (φ : G →g H) {X Y : Type*} (f : X →* Y) {n : ℕ} - (eX : Ω[succ (succ n)] X ≃* G) (eY : Ω[succ (succ n)] Y ≃* H) (p : φ ∘ eX ~ eY ∘ Ω→[succ (succ n)] f) - : φ ∘ EM_up eX ~ EM_up eY ∘ Ω→[succ n] (Ω→ f) := + (eX : G →* Ω[succ (succ n)] X) (eY : H →* Ω[succ (succ n)] Y) + (p : hsquare eX eY φ (Ω→[succ (succ n)] f)) + : hsquare (EM_up eX) (EM_up eY) φ (Ω→[succ n] (Ω→ f)) := begin - refine _ ⬝htyh p, - exact to_homotopy (phinverse (loopn_succ_in_natural (succ n) f)⁻¹*) + refine p ⬝htyh hsquare_of_psquare (loopn_succ_in_natural (succ n) f), end - definition EMadd1_pmap_natural {G H : AbGroup} {X Y : Type*} (f : X →* Y) (n : ℕ) (eX : Ω[succ n] X ≃* G) - (eY : Ω[succ n] Y ≃* H) (rX : Πp q, eX (p ⬝ q) = eX p * eX q) (rY : Πp q, eY (p ⬝ q) = eY p * eY q) - [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] [H3 : is_conn n Y] [H4 : is_trunc (n.+1) Y] - (φ : G →g H) (p : φ ∘ eX ~ eY ∘ Ω→[succ n] f) : - f ∘* EMadd1_pmap n eX rX ~* EMadd1_pmap n eY rY ∘* EMadd1_functor φ n := + definition EMadd1_pmap_natural {G H : AbGroup} {X Y : Type*} (f : X →* Y) (n : ℕ) + (eX : G →* Ω[succ n] X) (eY : H →* Ω[succ n] Y) (rX : Π(g h : G), eX (g * h) = eX g ⬝ eX h) + (rY : Π(g h : H), eY (g * h) = eY g ⬝ eY h) [HX : is_trunc (n.+1) X] [HY : is_trunc (n.+1) Y] + (φ : G →g H) (p : hsquare eX eY φ (Ω→[succ n] f)) : + psquare (EMadd1_pmap n eX rX) (EMadd1_pmap n eY rY) (EMadd1_functor φ n) f := begin - revert X Y f eX eY rX rY H1 H2 H3 H4 p, induction n with n IH: intros, - { apply EM1_pmap_natural, exact @hhinverse _ _ _ _ _ _ eX eY p }, + revert X Y f eX eY rX rY HX HY p, induction n with n IH: intros, + { apply EM1_pmap_natural, exact p }, { do 2 rewrite [EMadd1_pmap_succ], refine _ ⬝* pwhisker_left _ !EMadd1_functor_succ⁻¹*, refine (ptrunc_elim_pcompose ((succ n).+1) _ _)⁻¹* ⬝* _ ⬝* (ptrunc_elim_ptrunc_functor ((succ n).+1) _ _)⁻¹*, apply ptrunc_elim_phomotopy, refine _ ⬝* !susp_elim_susp_functor⁻¹*, - refine _ ⬝* susp_elim_phomotopy (IH _ _ _ _ _ (is_homomorphism_EM_up eX rX) _ (@is_conn_loop _ _ H1) - (@is_trunc_loop _ _ H2) _ _ (EM_up_natural φ f eX eY p)), + refine _ ⬝* susp_elim_phomotopy (IH _ _ _ _ _ (is_homomorphism_EM_up eX rX) _ + (@is_trunc_loop _ _ HX) _ (EM_up_natural φ f eX eY p)), apply susp_elim_natural } end - definition EMadd1_pequiv'_natural {G H : AbGroup} {X Y : Type*} (f : X →* Y) (n : ℕ) (eX : Ω[succ n] X ≃* G) - (eY : Ω[succ n] Y ≃* H) (rX : Πp q, eX (p ⬝ q) = eX p * eX q) (rY : Πp q, eY (p ⬝ q) = eY p * eY q) + definition EMadd1_pequiv'_natural {G H : AbGroup} {X Y : Type*} (f : X →* Y) (n : ℕ) + (eX : G ≃* Ω[succ n] X) (eY : H ≃* Ω[succ n] Y) (rX : Π(g h : G), eX (g * h) = eX g ⬝ eX h) + (rY : Π(g h : H), eY (g * h) = eY g ⬝ eY h) [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] [is_conn n Y] [is_trunc (n.+1) Y] - (φ : G →g H) (p : φ ∘ eX ~ eY ∘ Ω→[succ n] f) : - f ∘* EMadd1_pequiv' n eX rX ~* EMadd1_pequiv' n eY rY ∘* EMadd1_functor φ n := - begin rexact EMadd1_pmap_natural f n eX eY rX rY φ p end + (φ : G →g H) (p : hsquare eX eY φ (Ω→[succ n] f)) : + psquare (EMadd1_pequiv' n eX rX) (EMadd1_pequiv' n eY rY) (EMadd1_functor φ n) f := + EMadd1_pmap_natural f n eX eY rX rY φ p definition EMadd1_pequiv_natural_local_instance {X : Type*} (n : ℕ) [H : is_trunc (n.+1) X] : is_set (Ω[succ n] X) := @(is_set_loopn (succ n) X) H + local attribute EMadd1_pequiv_natural_local_instance [instance] - definition EMadd1_pequiv_natural {G H : AbGroup} {X Y : Type*} (f : X →* Y) (n : ℕ) (eX : πg[n+1] X ≃g G) - (eY : πg[n+1] Y ≃g H) [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] [H3 : is_conn n Y] - [H4 : is_trunc (n.+1) Y] (φ : G →g H) (p : φ ∘ eX ~ eY ∘ π→g[n+1] f) : - f ∘* EMadd1_pequiv n eX ~* EMadd1_pequiv n eY ∘* EMadd1_functor φ n := + definition EMadd1_pequiv_natural {G H : AbGroup} {X Y : Type*} (f : X →* Y) (n : ℕ) (eX : G ≃g πg[n+1] X) + (eY : H ≃g πg[n+1] Y) [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] [H3 : is_conn n Y] + [H4 : is_trunc (n.+1) Y] (φ : G →g H) (p : hsquare eX eY φ (π→g[n+1] f)) : + psquare (EMadd1_pequiv n eX) (EMadd1_pequiv n eY) (EMadd1_functor φ n) f := EMadd1_pequiv'_natural f n - ((ptrunc_pequiv 0 (Ω[succ n] X))⁻¹ᵉ* ⬝e* pequiv_of_isomorphism eX) - ((ptrunc_pequiv 0 (Ω[succ n] Y))⁻¹ᵉ* ⬝e* pequiv_of_isomorphism eY) - _ _ φ (hhconcat (to_homotopy (phinverse (ptrunc_pequiv_natural 0 (Ω→[succ n] f)))) p) + (pequiv_of_isomorphism eX ⬝e* ptrunc_pequiv 0 (Ω[succ n] X)) + (pequiv_of_isomorphism eY ⬝e* ptrunc_pequiv 0 (Ω[succ n] Y)) + _ _ φ (p ⬝htyh hsquare_of_psquare (ptrunc_pequiv_natural 0 (Ω→[succ n] f))) definition EMadd1_pequiv_succ_natural {G H : AbGroup} {X Y : Type*} (f : X →* Y) (n : ℕ) - (eX : πag[n+2] X ≃g G) (eY : πag[n+2] Y ≃g H) [is_conn (n.+1) X] [is_trunc (n.+2) X] - [is_conn (n.+1) Y] [is_trunc (n.+2) Y] (φ : G →g H) (p : φ ∘ eX ~ eY ∘ π→g[n+2] f) : - f ∘* EMadd1_pequiv_succ n eX ~* EMadd1_pequiv_succ n eY ∘* EMadd1_functor φ (n+1) := + (eX : G ≃g πag[n+2] X) (eY : H ≃g πag[n+2] Y) [is_conn (n.+1) X] [is_trunc (n.+2) X] + [is_conn (n.+1) Y] [is_trunc (n.+2) Y] (φ : G →g H) (p : hsquare eX eY φ (π→g[n+2] f)) : + psquare (EMadd1_pequiv_succ n eX) (EMadd1_pequiv_succ n eY) (EMadd1_functor φ (n+1)) f := @(EMadd1_pequiv_natural f (succ n) eX eY) _ _ _ _ φ p definition EMadd1_pequiv_type_natural {X Y : Type*} (f : X →* Y) (n : ℕ) - [H1 : is_conn (n+1) X] [H2 : is_trunc (n+1+1) X] [H3 : is_conn (n+1) Y] [H4 : is_trunc (n+1+1) Y] : - f ∘* EMadd1_pequiv_type X n ~* EMadd1_pequiv_type Y n ∘* EMadd1_functor (π→g[n+2] f) (succ n) := + [H1 : is_conn (n+1) X] [H2 : is_trunc (n+1+1) X] + [H3 : is_conn (n+1) Y] [H4 : is_trunc (n+1+1) Y] : + psquare (EMadd1_pequiv_type X n) (EMadd1_pequiv_type Y n) + (EMadd1_functor (π→g[n+2] f) (succ n)) f := EMadd1_pequiv_succ_natural f n !isomorphism.refl !isomorphism.refl (π→g[n+2] f) proof λa, idp qed @@ -338,6 +312,38 @@ namespace EM apply EMadd1_pequiv_type_natural } end + definition EM1_functor_trivial_homomorphism [constructor] (G H : Group) : + EM1_functor (trivial_homomorphism G H) ~* pconst (EM1 G) (EM1 H) := + begin + fapply phomotopy.mk, + { intro x, induction x using EM.set_rec, + { reflexivity }, + { apply eq_pathover_constant_right, apply hdeg_square, + refine !elim_pth ⬝ _, apply resp_one }}, + { reflexivity } + end + + definition EMadd1_functor_trivial_homomorphism (G H : AbGroup) (n : ℕ) : + EMadd1_functor (trivial_homomorphism G H) n ~* pconst (EMadd1 G n) (EMadd1 H n) := + begin + induction n with n h, + { exact EM1_functor_trivial_homomorphism G H }, + { refine !EMadd1_functor_succ ⬝* ptrunc_functor_phomotopy (n+2) _ ⬝* !ptrunc_functor_pconst, + refine susp_functor_phomotopy h ⬝* !susp_functor_pconst } + end + + definition EMadd1_pfunctor [constructor] (G H : AbGroup) (n : ℕ) : + (G →gg H) →* EMadd1 G n →** EMadd1 H n := + pmap.mk (λφ, EMadd1_functor φ n) (eq_of_phomotopy (EMadd1_functor_trivial_homomorphism G H n)) + + definition loopn_EMadd1_add (G : AbGroup) (n m : ℕ) : Ω[n] (EMadd1 G (m + n)) ≃* EMadd1 G m := + begin + induction n with n e, + { reflexivity }, + { refine !loopn_succ_in ⬝e* Ω≃[n] (loop_EMadd1 G (m + n))⁻¹ᵉ* ⬝e* e } + end + + /- The Eilenberg-MacLane space K(G,n) with the same homotopy group as X on level n. On paper this is written K(πₙ(X), n). The problem is that for * n = 0 the expression π₀(X) is a pointed set, and K(X,0) needs X to be a pointed set @@ -359,7 +365,7 @@ namespace EM exact EM1_pequiv e }, { have is_conn (n+1) X, from H1, have is_trunc ((n+1).+1) X, from H2, - exact EMadd1_pequiv (n+1) e⁻¹ᵍ } + exact EMadd1_pequiv (n+1) e } end -- definition EM1_functor_equiv' (X Y : Type*) [H1 : is_conn 0 X] [H2 : is_trunc 1 X] @@ -456,7 +462,7 @@ namespace EM begin cases n with n, { exact _ }, cases Y with Y H1 H2, cases Y with Y y₀, - exact is_trunc_pmap_of_is_conn X n -1 _ (pointed.MK Y y₀) !le.refl H2, + exact is_trunc_pmap_of_is_conn X n _ -1 _ (pointed.MK Y y₀) !le.refl H2, end open category functor nat_trans @@ -568,10 +574,10 @@ namespace EM equivalence.mk (EM_cfunctor.{u} (n+2)) (is_equivalence_EM_cfunctor.{u} n) end category - definition pequiv_EMadd1_of_loopn_pequiv_EM1 {G : AbGroup} {X : Type*} (n : ℕ) (e : Ω[n] X ≃* EM1 G) - [H1 : is_conn n X] : X ≃* EMadd1 G n := + definition pequiv_EMadd1_of_loopn_pequiv_EM1 {G : AbGroup} {X : Type*} (n : ℕ) + (e : Ω[n] X ≃* EM1 G) [H1 : is_conn n X] : X ≃* EMadd1 G n := begin - symmetry, apply EMadd1_pequiv, + symmetry, apply EMadd1_pequiv, symmetry, refine isomorphism_of_eq (ap (λx, πg[x+1] X) !zero_add⁻¹) ⬝g homotopy_group_add X 0 n ⬝g _ ⬝g !fundamental_group_EM1, exact homotopy_group_isomorphism_of_pequiv 0 e, diff --git a/homotopy/smash_adjoint.hlean b/homotopy/smash_adjoint.hlean index a82cbb2..560a2dd 100644 --- a/homotopy/smash_adjoint.hlean +++ b/homotopy/smash_adjoint.hlean @@ -2,7 +2,7 @@ -- informal proofs in collaboration with Egbert, Stefano, Robin, Ulrik /- the adjunction between the smash product and pointed maps -/ -import .smash .susp ..pointed ..move_to_lib ..pyoneda +import .smash .susp ..pointed_pi ..pyoneda open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc function unit sigma susp sphere @@ -595,7 +595,7 @@ namespace smash calc ppmap (⅀ A ∧ B) X ≃* ppmap (⅀ A) (ppmap B X) : smash_adjoint_pmap (⅀ A) B X ... ≃* ppmap A (Ω (ppmap B X)) : susp_adjoint_loop A (ppmap B X) - ... ≃* ppmap A (ppmap B (Ω X)) : ppmap_pequiv_ppmap_right (loop_ppmap_commute B X) + ... ≃* ppmap A (ppmap B (Ω X)) : ppmap_pequiv_ppmap_right (loop_ppmap_pequiv B X) ... ≃* ppmap (A ∧ B) (Ω X) : smash_adjoint_pmap A B (Ω X) ... ≃* ppmap (⅀ (A ∧ B)) X : susp_adjoint_loop (A ∧ B) X @@ -604,7 +604,7 @@ namespace smash (ppcompose_left f) (ppcompose_left f) := smash_adjoint_pmap_natural_right (⅀ A) B f ⬝h* susp_adjoint_loop_natural_right (ppcompose_left f) ⬝h* - ppcompose_left_psquare (loop_pmap_commute_natural_right B f) ⬝h* + ppcompose_left_psquare (loop_ppmap_pequiv_natural_right B f) ⬝h* (smash_adjoint_pmap_natural_right A B (Ω→ f))⁻¹ʰ* ⬝h* (susp_adjoint_loop_natural_right f)⁻¹ʰ* @@ -618,7 +618,7 @@ namespace smash (susp_adjoint_loop_natural_left (f ∧→ g))⁻¹ʰ*, rotate 2, exact !ppcompose_left_ppcompose_right ⬝v* - ppcompose_left_psquare (loop_pmap_commute_natural_left X g), + ppcompose_left_psquare (loop_ppmap_pequiv_natural_left X g), exact susp_adjoint_loop_natural_left f ⬝v* susp_adjoint_loop_natural_right (ppcompose_right g) end diff --git a/homotopy/susp.hlean b/homotopy/susp.hlean index 248799d..aabc70a 100644 --- a/homotopy/susp.hlean +++ b/homotopy/susp.hlean @@ -52,21 +52,25 @@ namespace susp {f₁₀ : A₀₀ →* A₂₀} {f₁₂ : A₀₂ →* A₂₂} {f₀₁ : A₀₀ →* A₀₂} {f₂₁ : A₂₀ →* A₂₂} - -- rename: susp_functor_psquare - definition suspend_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : psquare (⅀→ f₁₀) (⅀→ f₁₂) (⅀→ f₀₁) (⅀→ f₂₁) := -sorry + definition susp_functor_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare (⅀→ f₁₀) (⅀→ f₁₂) (⅀→ f₀₁) (⅀→ f₂₁) := + !susp_functor_pcompose⁻¹* ⬝* susp_functor_phomotopy p ⬝* !susp_functor_pcompose - definition susp_to_loop_psquare (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : susp A₀₀ →* A₀₂) (f₂₁ : susp A₂₀ →* A₂₂) : (psquare (⅀→ f₁₀) f₁₂ f₀₁ f₂₁) → (psquare f₁₀ (Ω→ f₁₂) ((loop_susp_pintro A₀₀ A₀₂) f₀₁) ((loop_susp_pintro A₂₀ A₂₂) f₂₁)) := + definition susp_to_loop_psquare (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) + (f₀₁ : susp A₀₀ →* A₀₂) (f₂₁ : susp A₂₀ →* A₂₂) : psquare (⅀→ f₁₀) f₁₂ f₀₁ f₂₁ → + psquare f₁₀ (Ω→ f₁₂) (loop_susp_pintro A₀₀ A₀₂ f₀₁) (loop_susp_pintro A₂₀ A₂₂ f₂₁) := begin intro p, refine pvconcat _ (ap1_psquare p), - exact loop_susp_unit_natural f₁₀ + exact (loop_susp_unit_natural f₁₀)⁻¹* end - definition loop_to_susp_square (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : A₀₀ →* Ω A₀₂) (f₂₁ : A₂₀ →* Ω A₂₂) : (psquare f₁₀ (Ω→ f₁₂) f₀₁ f₂₁) → (psquare (⅀→ f₁₀) f₁₂ ((susp_pelim A₀₀ A₀₂) f₀₁) ((susp_pelim A₂₀ A₂₂) f₂₁)) := + definition loop_to_susp_square (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) + (f₀₁ : A₀₀ →* Ω A₀₂) (f₂₁ : A₂₀ →* Ω A₂₂) : psquare f₁₀ (Ω→ f₁₂) f₀₁ f₂₁ → + psquare (⅀→ f₁₀) f₁₂ (susp_pelim A₀₀ A₀₂ f₀₁) (susp_pelim A₂₀ A₂₂ f₂₁) := begin intro p, - refine pvconcat (suspend_psquare p) _, + refine susp_functor_psquare p ⬝v* _, exact psquare_transpose (loop_susp_counit_natural f₁₂) end diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 55eb11f..36dffc8 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -38,6 +38,37 @@ namespace eq transport C (ap g₁ p) (f z) = f (transport C p z) := by induction p; reflexivity + variables {A A' B : Type} {a a₂ a₃ : A} {p p' : a = a₂} {p₂ : a₂ = a₃} + {a' a₂' a₃' : A'} {b b₂ : B} + + definition apd_eq_ap (f : A → A') (p : a = a₂) : eq_of_pathover (apd f p) = ap f p := + begin induction p, reflexivity end + + definition eq_of_pathover_idp_constant (p : b =[idpath a] b₂) : + eq_of_pathover_idp p = eq_of_pathover p := + begin induction p using idp_rec_on, reflexivity end + + definition eq_of_pathover_change_path (r : p = p') (q : a' =[p] a₂') : + eq_of_pathover (change_path r q) = eq_of_pathover q := + begin induction r, reflexivity end + + definition eq_of_pathover_cono (q : a' =[p] a₂') (q₂ : a₂' =[p₂] a₃') : + eq_of_pathover (q ⬝o q₂) = eq_of_pathover q ⬝ eq_of_pathover q₂ := + begin induction q₂, reflexivity end + + definition eq_of_pathover_invo (q : a' =[p] a₂') : + eq_of_pathover q⁻¹ᵒ = (eq_of_pathover q)⁻¹ := + begin induction q, reflexivity end + + definition eq_of_pathover_concato_eq (q : a' =[p] a₂') (q₂ : a₂' = a₃') : + eq_of_pathover (q ⬝op q₂) = eq_of_pathover q ⬝ q₂ := + begin induction q₂, reflexivity end + + definition eq_of_pathover_eq_concato (q : a' = a₂') (q₂ : a₂' =[p₂] a₃') : + eq_of_pathover (q ⬝po q₂) = q ⬝ eq_of_pathover q₂ := + begin induction q, induction q₂, reflexivity end + + end eq open eq namespace nat @@ -90,15 +121,22 @@ end nat -- ... ≃ (k ~* l) : phomotopy.sigma_char k l namespace pointed -/- move to pointed -/ -open sigma.ops +infixr ` →** `:29 := ppmap end pointed open pointed namespace trunc open trunc_index sigma.ops + definition ptrunc_functor_pconst [constructor] (n : ℕ₋₂) (X Y : Type*) : + ptrunc_functor n (pconst X Y) ~* pconst (ptrunc n X) (ptrunc n Y) := + begin + fapply phomotopy.mk, + { intro x, induction x with x, reflexivity }, + { reflexivity } + end + -- TODO: redefine loopn_ptrunc_pequiv definition apn_ptrunc_functor (n : ℕ₋₂) (k : ℕ) {A B : Type*} (f : A →* B) : Ω→[k] (ptrunc_functor (n+k) f) ∘* (loopn_ptrunc_pequiv n k A)⁻¹ᵉ* ~* @@ -240,6 +278,29 @@ end sigma open sigma namespace group +infixr ` →gg `:56 := aghomomorphism + +definition pmap_of_homomorphism2 [constructor] {G H K : AbGroup} (φ : G →g H →gg K) : + G →* H →** K := +pmap.mk (λg, pmap_of_homomorphism (φ g)) + (eq_of_phomotopy (phomotopy_of_homotopy (ap010 group_fun (to_respect_one φ)))) + +definition homomorphism_apply [constructor] (G H : AbGroup) (g : G) : + (G →gg H) →g H := +begin + fapply homomorphism.mk, + { intro φ, exact φ g }, + { intros φ φ', reflexivity } +end + +definition homomorphism_swap [constructor] {G H K : AbGroup} (φ : G →g H →gg K) : + H →g G →gg K := +begin + fapply homomorphism.mk, + { intro h, exact homomorphism_apply H K h ∘g φ }, + { intro h h', apply homomorphism_eq, intro g, exact to_respect_mul (φ g) h h' } +end + definition isomorphism.MK [constructor] {G H : Group} (φ : G →g H) (ψ : H →g G) (p : φ ∘g ψ ~ gid H) (q : ψ ∘g φ ~ gid G) : G ≃g H := isomorphism.mk φ (adjointify φ ψ p q) @@ -1132,10 +1193,6 @@ end injective_surjective -- Yuri Sulyma's code from HoTT MRC -notation `⅀→`:(max+5) := susp_functor -notation `⅀⇒`:(max+5) := susp_functor_phomotopy -notation `Ω⇒`:(max+5) := ap1_phomotopy - definition ap1_phomotopy_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : (Ω⇒ p)⁻¹* = Ω⇒ (p⁻¹*) := begin induction p using phomotopy_rec_idp, @@ -1153,7 +1210,6 @@ begin rewrite trans_refl end - namespace pointed definition pbool_pequiv_add_point_unit [constructor] : pbool ≃* unit₊ := diff --git a/pointed.hlean b/pointed.hlean index 6677ea8..9a9d76e 100644 --- a/pointed.hlean +++ b/pointed.hlean @@ -97,82 +97,82 @@ namespace pointed end /- remove some duplicates: loop_ppmap_commute, loop_ppmap_pequiv, loop_ppmap_pequiv', pfunext -/ - definition pfunext (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) := - (loop_ppmap_commute X Y)⁻¹ᵉ* + -- definition pfunext (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) := + -- (loop_ppmap_commute X Y)⁻¹ᵉ* - definition loop_phomotopy [constructor] {A B : Type*} (f : A →* B) : Type* := - pointed.MK (f ~* f) phomotopy.rfl +-- definition loop_phomotopy [constructor] {A B : Type*} (f : A →* B) : Type* := +-- pointed.MK (f ~* f) phomotopy.rfl - definition ppcompose_left_loop_phomotopy [constructor] {A B C : Type*} (g : B →* C) {f : A →* B} - {h : A →* C} (p : g ∘* f ~* h) : loop_phomotopy f →* loop_phomotopy h := - pmap.mk (λq, p⁻¹* ⬝* pwhisker_left g q ⬝* p) - (idp ◾** !pwhisker_left_refl ◾** idp ⬝ !trans_refl ◾** idp ⬝ !trans_left_inv) +-- definition ppcompose_left_loop_phomotopy [constructor] {A B C : Type*} (g : B →* C) {f : A →* B} +-- {h : A →* C} (p : g ∘* f ~* h) : loop_phomotopy f →* loop_phomotopy h := +-- pmap.mk (λq, p⁻¹* ⬝* pwhisker_left g q ⬝* p) +-- (idp ◾** !pwhisker_left_refl ◾** idp ⬝ !trans_refl ◾** idp ⬝ !trans_left_inv) - definition ppcompose_left_loop_phomotopy' [constructor] {A B C : Type*} (g : B →* C) (f : A →* B) - : loop_phomotopy f →* loop_phomotopy (g ∘* f) := - pmap.mk (λq, pwhisker_left g q) !pwhisker_left_refl +-- definition ppcompose_left_loop_phomotopy' [constructor] {A B C : Type*} (g : B →* C) (f : A →* B) +-- : loop_phomotopy f →* loop_phomotopy (g ∘* f) := +-- pmap.mk (λq, pwhisker_left g q) !pwhisker_left_refl - definition loop_ppmap_pequiv' [constructor] (A B : Type*) : - Ω(ppmap A B) ≃* loop_phomotopy (pconst A B) := - pequiv_of_equiv (pmap_eq_equiv _ _) idp +-- definition loop_ppmap_pequiv' [constructor] (A B : Type*) : +-- Ω(ppmap A B) ≃* loop_phomotopy (pconst A B) := +-- pequiv_of_equiv (pmap_eq_equiv _ _) idp - definition ppmap_loop_pequiv' [constructor] (A B : Type*) : - loop_phomotopy (pconst A B) ≃* ppmap A (Ω B) := - pequiv_of_equiv (!phomotopy.sigma_char ⬝e !pmap.sigma_char⁻¹ᵉ) idp +-- definition ppmap_loop_pequiv' [constructor] (A B : Type*) : +-- loop_phomotopy (pconst A B) ≃* ppmap A (Ω B) := +-- pequiv_of_equiv (!phomotopy.sigma_char ⬝e !pmap.sigma_char⁻¹ᵉ) idp - definition loop_ppmap_pequiv [constructor] (A B : Type*) : Ω(ppmap A B) ≃* ppmap A (Ω B) := - loop_ppmap_pequiv' A B ⬝e* ppmap_loop_pequiv' A B +-- definition loop_ppmap_pequiv [constructor] (A B : Type*) : Ω(ppmap A B) ≃* ppmap A (Ω B) := +-- loop_ppmap_pequiv' A B ⬝e* ppmap_loop_pequiv' A B - definition loop_ppmap_pequiv'_natural_right' {X X' : Type} (x₀ : X) (A : Type*) (f : X → X') : - psquare (loop_ppmap_pequiv' A _) (loop_ppmap_pequiv' A _) - (Ω→ (ppcompose_left (pmap_of_map f x₀))) - (ppcompose_left_loop_phomotopy' (pmap_of_map f x₀) !pconst) := - begin - fapply phomotopy.mk, - { esimp, intro p, - refine _ ⬝ ap011 (λx y, phomotopy_of_eq (ap1_gen _ x y _)) - proof !eq_of_phomotopy_refl⁻¹ qed proof !eq_of_phomotopy_refl⁻¹ qed, - refine _ ⬝ ap phomotopy_of_eq !ap1_gen_idp_left⁻¹, - exact !phomotopy_of_eq_pcompose_left⁻¹ }, - { refine _ ⬝ !idp_con⁻¹, exact sorry } - end +-- definition loop_ppmap_pequiv'_natural_right' {X X' : Type} (x₀ : X) (A : Type*) (f : X → X') : +-- psquare (loop_ppmap_pequiv' A _) (loop_ppmap_pequiv' A _) +-- (Ω→ (ppcompose_left (pmap_of_map f x₀))) +-- (ppcompose_left_loop_phomotopy' (pmap_of_map f x₀) !pconst) := +-- begin +-- fapply phomotopy.mk, +-- { esimp, intro p, +-- refine _ ⬝ ap011 (λx y, phomotopy_of_eq (ap1_gen _ x y _)) +-- proof !eq_of_phomotopy_refl⁻¹ qed proof !eq_of_phomotopy_refl⁻¹ qed, +-- refine _ ⬝ ap phomotopy_of_eq !ap1_gen_idp_left⁻¹, +-- exact !phomotopy_of_eq_pcompose_left⁻¹ }, +-- { refine _ ⬝ !idp_con⁻¹, exact sorry } +-- end - definition loop_ppmap_pequiv'_natural_right {X X' : Type*} (A : Type*) (f : X →* X') : - psquare (loop_ppmap_pequiv' A X) (loop_ppmap_pequiv' A X') - (Ω→ (ppcompose_left f)) (ppcompose_left_loop_phomotopy f !pcompose_pconst) := - begin - induction X' with X' x₀', induction f with f f₀, esimp at f, esimp at f₀, induction f₀, - apply psquare_of_phomotopy, - exact sorry - end +-- definition loop_ppmap_pequiv'_natural_right {X X' : Type*} (A : Type*) (f : X →* X') : +-- psquare (loop_ppmap_pequiv' A X) (loop_ppmap_pequiv' A X') +-- (Ω→ (ppcompose_left f)) (ppcompose_left_loop_phomotopy f !pcompose_pconst) := +-- begin +-- induction X' with X' x₀', induction f with f f₀, esimp at f, esimp at f₀, induction f₀, +-- apply psquare_of_phomotopy, +-- exact sorry +-- end - definition ppmap_loop_pequiv'_natural_right {X X' : Type*} (A : Type*) (f : X →* X') : - psquare (ppmap_loop_pequiv' A X) (ppmap_loop_pequiv' A X') - (ppcompose_left_loop_phomotopy f !pcompose_pconst) (ppcompose_left (Ω→ f)) := - begin - exact sorry - end +-- definition ppmap_loop_pequiv'_natural_right {X X' : Type*} (A : Type*) (f : X →* X') : +-- psquare (ppmap_loop_pequiv' A X) (ppmap_loop_pequiv' A X') +-- (ppcompose_left_loop_phomotopy f !pcompose_pconst) (ppcompose_left (Ω→ f)) := +-- begin +-- exact sorry +-- end - definition loop_pmap_commute_natural_right_direct {X X' : Type*} (A : Type*) (f : X →* X') : - psquare (loop_ppmap_pequiv A X) (loop_ppmap_pequiv A X') - (Ω→ (ppcompose_left f)) (ppcompose_left (Ω→ f)) := - begin - induction X' with X' x₀', induction f with f f₀, esimp at f, esimp at f₀, induction f₀, --- refine _ ⬝* _ ◾* _, rotate 4, - fapply phomotopy.mk, - { intro p, esimp, esimp [pmap_eq_equiv, pcompose_pconst], exact sorry }, - { exact sorry } - end +-- definition loop_pmap_commute_natural_right_direct {X X' : Type*} (A : Type*) (f : X →* X') : +-- psquare (loop_ppmap_pequiv A X) (loop_ppmap_pequiv A X') +-- (Ω→ (ppcompose_left f)) (ppcompose_left (Ω→ f)) := +-- begin +-- induction X' with X' x₀', induction f with f f₀, esimp at f, esimp at f₀, induction f₀, +-- -- refine _ ⬝* _ ◾* _, rotate 4, +-- fapply phomotopy.mk, +-- { intro p, esimp, esimp [pmap_eq_equiv, pcompose_pconst], exact sorry }, +-- { exact sorry } +-- end - definition loop_pmap_commute_natural_left {A A' : Type*} (X : Type*) (f : A' →* A) : - psquare (loop_ppmap_commute A X) (loop_ppmap_commute A' X) - (Ω→ (ppcompose_right f)) (ppcompose_right f) := - sorry +-- definition loop_pmap_commute_natural_left {A A' : Type*} (X : Type*) (f : A' →* A) : +-- psquare (loop_ppmap_commute A X) (loop_ppmap_commute A' X) +-- (Ω→ (ppcompose_right f)) (ppcompose_right f) := +-- sorry - definition loop_pmap_commute_natural_right {X X' : Type*} (A : Type*) (f : X →* X') : - psquare (loop_ppmap_commute A X) (loop_ppmap_commute A X') - (Ω→ (ppcompose_left f)) (ppcompose_left (Ω→ f)) := - loop_ppmap_pequiv'_natural_right A f ⬝h* ppmap_loop_pequiv'_natural_right A f +-- definition loop_pmap_commute_natural_right {X X' : Type*} (A : Type*) (f : X →* X') : +-- psquare (loop_ppmap_commute A X) (loop_ppmap_commute A X') +-- (Ω→ (ppcompose_left f)) (ppcompose_left (Ω→ f)) := +-- loop_ppmap_pequiv'_natural_right A f ⬝h* ppmap_loop_pequiv'_natural_right A f /- Do we want to use a structure of homotopies between pointed homotopies? Or are equalities fine? @@ -296,14 +296,6 @@ namespace pointed {f₀₃ : A₀₂ →* A₀₄} {f₂₃ : A₂₂ →* A₂₄} {f₄₃ : A₄₂ →* A₄₄} {f₁₄ f₁₄' : A₀₄ →* A₂₄} {f₃₄ : A₂₄ →* A₄₄} - definition phconst_square (f₀₁ : A₀₀ →* A₀₂) (f₂₁ : A₂₀ →* A₂₂) : - psquare (pconst A₀₀ A₂₀) (pconst A₀₂ A₂₂) f₀₁ f₂₁ := - !pcompose_pconst ⬝* !pconst_pcompose⁻¹* - - definition pvconst_square (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) : - psquare f₁₀ f₁₂ (pconst A₀₀ A₀₂) (pconst A₂₀ A₂₂) := - !pconst_pcompose ⬝* !pcompose_pconst⁻¹* - definition pvconst_square_pcompose (f₃₀ : A₂₀ →* A₄₀) (f₁₀ : A₀₀ →* A₂₀) (f₃₂ : A₂₂ →* A₄₂) (f₁₂ : A₀₂ →* A₂₂) : pvconst_square (f₃₀ ∘* f₁₀) (f₃₂ ∘* f₁₂) = pvconst_square f₁₀ f₁₂ ⬝h* pvconst_square f₃₀ f₃₂ := @@ -325,12 +317,6 @@ namespace pointed phconst_square (f₀₃ ∘* f₀₁) (f₂₃ ∘* f₁₂) = phconst_square f₀₁ f₁₂ ⬝v* phconst_square f₀₃ f₂₃ := sorry - definition ptranspose (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : psquare f₀₁ f₂₁ f₁₀ f₁₂ := - p⁻¹* - - definition hsquare_of_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : hsquare f₁₀ f₁₂ f₀₁ f₂₁ := - p - definition rfl_phomotopy_hconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : phomotopy.rfl ⬝ph* p = p := idp ◾** (ap (pwhisker_left f₁₂) !refl_symm ⬝ !pwhisker_left_refl) ⬝ !trans_refl diff --git a/pointed_pi.hlean b/pointed_pi.hlean index 21dec0b..a44015b 100644 --- a/pointed_pi.hlean +++ b/pointed_pi.hlean @@ -333,9 +333,9 @@ namespace pointed definition phomotopy {A : Type*} {P : A → Type} {x : P pt} (f g : ppi P x) : Type := ppi (λa, f a = g a) (respect_pt f ⬝ (respect_pt g)⁻¹) - variables {A : Type*} {P Q R : A → Type*} {f g h : Π*a, P a} - {B C D : A → Type} {b₀ : B pt} {c₀ : C pt} {d₀ : D pt} - {k k' l m : ppi B b₀} + variables {A A' A'' : Type*} {P Q R : A → Type*} {P' : A' → Type*} {f g h : Π*a, P a} + {B C D : A → Type} {b₀ : B pt} {c₀ : C pt} {d₀ : D pt} + {k k' l m : ppi B b₀} definition pppi_equiv_pmap [constructor] (A B : Type*) : (Π*(a : A), B) ≃ (A →* B) := by reflexivity @@ -465,6 +465,28 @@ namespace pointed (f : Π*(a : A), P a) : Π*(a : A), Q a := ppi_functor_right g (respect_pt (g pt)) f + definition ppi_compose_pmap [constructor] (g : Π*(a : A), P a) (f : A' →* A) : + Π*(a' : A'), P (f a') := + ppi.mk (λa', g (f a')) + (eq_of_pathover_idp (change_path !con.right_inv + (apd g (respect_pt f) ⬝op respect_pt g ⬝o (apd (λx, Point (P x)) (respect_pt f))⁻¹ᵒ))) +/- alternate proof for respecting the point -/ +-- (eq_tr_of_pathover (apd g (respect_pt f)) ⬝ ap (transport _ _) (respect_pt g) ⬝ +-- apdt (λx, Point (P x)) (respect_pt f)⁻¹) + + definition ppi_compose_pmap_phomotopy [constructor] (g : A →* A'') (f : A' →* A) : + ppi_compose_pmap g f ~* g ∘* f := + begin + refine phomotopy.mk homotopy.rfl _, + refine !idp_con ⬝ _, esimp, + symmetry, + refine !eq_of_pathover_idp_constant ⬝ _, + refine !eq_of_pathover_change_path ⬝ !eq_of_pathover_cono ⬝ _, + refine (!eq_of_pathover_concato_eq ⬝ !apd_eq_ap ◾ idp) ◾ + (!eq_of_pathover_invo ⬝ (!apd_eq_ap ⬝ !ap_constant)⁻²) ⬝ _, + reflexivity + end + definition pmap_compose_ppi_ppi_const [constructor] (g : Π(a : A), ppmap (P a) (Q a)) : pmap_compose_ppi g (ppi_const P) ~* ppi_const Q := proof phomotopy.mk (λa, respect_pt (g a)) !idp_con⁻¹ qed @@ -473,6 +495,17 @@ namespace pointed pmap_compose_ppi (λa, pconst (P a) (Q a)) f ~* ppi_const Q := phomotopy.mk homotopy.rfl !ap_constant⁻¹ + definition ppi_compose_pmap_ppi_const [constructor] (f : A' →* A) : + ppi_compose_pmap (ppi_const P) f ~* ppi_const (P ∘ f) := + phomotopy.mk homotopy.rfl + begin + exact (ap eq_of_pathover_idp (change_path_of_pathover _ _ _ !cono.right_inv))⁻¹, + end + + definition ppi_compose_pmap_pconst [constructor] (g : Π*(a : A), P a) : + ppi_compose_pmap g (pconst A' A) ~* pconst A' (P pt) := + phomotopy.mk (λa, respect_pt g) !idpo_concato_eq⁻¹ + definition pmap_compose_ppi2 [constructor] {g g' : Π(a : A), ppmap (P a) (Q a)} {f f' : Π*(a : A), P a} (p : Πa, g a ~* g' a) (q : f ~* f') : pmap_compose_ppi g f ~* pmap_compose_ppi g' f' := @@ -537,6 +570,18 @@ namespace pointed (Π*(a : A), P a) →* Π*(a : A), Q a := pmap.mk (pmap_compose_ppi g) (eq_of_phomotopy (pmap_compose_ppi_ppi_const g)) + definition pppi_compose_right [constructor] (f : A' →* A) : + (Π*(a : A), P a) →* Π*(a' : A'), P (f a') := + pmap.mk (λh, ppi_compose_pmap h f) (eq_of_phomotopy (ppi_compose_pmap_ppi_const f)) + + definition pppi_compose_right_phomotopy [constructor] (f : A' →* A) : + pppi_compose_right f ~* @ppcompose_right _ _ A'' f := + begin + fapply phomotopy_mk_ppmap, + { intro g, exact ppi_compose_pmap_phomotopy g f }, + { exact sorry } + end + -- pppi_compose_left is a functor in the following sense definition pppi_compose_left_pcompose (g : Π (a : A), Q a →* R a) (f : Π (a : A), P a →* Q a) : pppi_compose_left (λ a, g a ∘* f a) ~* (pppi_compose_left g ∘* pppi_compose_left f) := @@ -832,13 +877,14 @@ namespace pointed Ω (Π*a, B a) ≃* Π*(a : A), Ω (B a) := pequiv_of_equiv !ppi_eq_equiv idp - definition loop_pppi_pequiv_natural {A : Type*} {X Y : A → Type*} (f : Π (a : A), X a →* Y a) : - psquare - (Ω→ (pppi_compose_left f)) - (pppi_compose_left (λ a, Ω→ (f a))) - (loop_pppi_pequiv X) - (loop_pppi_pequiv Y) := + definition loop_pppi_pequiv_natural_right {A : Type*} {X Y : A → Type*} + (f : Π (a : A), X a →* Y a) : + psquare (loop_pppi_pequiv X) + (loop_pppi_pequiv Y) + (Ω→ (pppi_compose_left f)) + (pppi_compose_left (λ a, Ω→ (f a))) := begin + apply ptranspose, revert Y f, refine fiberwise_pointed_map_rec _ _, intro Y f, fapply phomotopy.mk, { exact ppi_eq_equiv_natural_gen (pmap_compose_ppi_ppi_const (λa, pmap_of_map (f a) pt)) @@ -846,7 +892,16 @@ namespace pointed { exact !ppi_eq_equiv_natural_gen_refl ◾ (!idp_con ⬝ !eq_of_phomotopy_refl) } end - definition loopn_pppi_pequiv [constructor] (n : ℕ) {A : Type*} (B : A → Type*) : + definition loop_pppi_pequiv_natural_left {A B : Type*} {X : A → Type*} (f : B →* A) : + psquare (loop_pppi_pequiv X) + (loop_pppi_pequiv (X ∘ f)) + (Ω→ (pppi_compose_right f)) + (pppi_compose_right f) := + begin + exact sorry + end + + definition loopn_pppi_pequiv (n : ℕ) {A : Type*} (B : A → Type*) : Ω[n] (Π*a, B a) ≃* Π*(a : A), Ω[n] (B a) := begin induction n with n IH, @@ -854,13 +909,34 @@ namespace pointed { refine loop_pequiv_loop IH ⬝e* loop_pppi_pequiv (λa, Ω[n] (B a)) } end - -- definition trivial_homotopy_group_pppi {A : Type*} {B : A → Type*} {n : ℕ} - -- (H : Πa, is_contr (Ω[n] (B a))) : is_contr (π[n] (Π*a, B a)) := - -- begin - -- apply is_trunc_trunc_of_is_trunc, - -- apply is_trunc_equiv_closed_rev, - -- apply loopn_pppi_pequiv - -- end + definition loop_ppmap_pequiv [constructor] (A B : Type*) : Ω (A →** B) ≃* A →** Ω B := + !loop_pppi_pequiv + + definition loop_ppmap_pequiv_natural_right (A : Type*) {X Y : Type*} (f : X →* Y) : + psquare (loop_ppmap_pequiv A X) + (loop_ppmap_pequiv A Y) + (Ω→ (ppcompose_left f)) + (ppcompose_left (Ω→ f)) := + begin + exact loop_pppi_pequiv_natural_right (λa, f) + end + + definition loop_ppmap_pequiv_natural_left {A B : Type*} (X : Type*) (f : A →* B) : + psquare (loop_ppmap_pequiv B X) + (loop_ppmap_pequiv A X) + (Ω→ (ppcompose_right f)) + (ppcompose_right f) := + begin + refine Ω⇒ !pppi_compose_right_phomotopy⁻¹* ⬝ph* _ ⬝hp* !pppi_compose_right_phomotopy⁻¹*, + exact loop_pppi_pequiv_natural_left f + end + + definition loopn_ppmap_pequiv (n : ℕ) (A B : Type*) : Ω[n] (A →** B) ≃* A →** Ω[n] B := + !loopn_pppi_pequiv + + definition pfunext [constructor] {A : Type*} (B : A → Type*) : + (Π*(a : A), Ω (B a)) ≃* Ω (Π*a, B a) := + (loop_pppi_pequiv B)⁻¹ᵉ* /- below is an alternate proof strategy for the naturality of loop_pppi_pequiv_natural, @@ -901,7 +977,7 @@ open is_trunc is_conn namespace is_conn section - variables (A : Type*) (n : ℕ₋₂) [H : is_conn (n.+1) A] + variables (A : Type*) (n : ℕ₋₂) (H : is_conn (n.+1) A) include H definition is_contr_ppi_match (P : A → Type*) (H : Πa, is_trunc (n.+1) (P a)) @@ -925,7 +1001,7 @@ namespace is_conn clear H2 H3, revert P H4, induction k with k IH: intro P H4, { apply is_prop_of_imp_is_contr, intro f, - apply is_contr_ppi_match A n P H4 }, + apply is_contr_ppi_match A n H P H4 }, { apply is_trunc_succ_of_is_trunc_loop (trunc_index.succ_le_succ (trunc_index.minus_two_le k)), intro f, @@ -936,8 +1012,8 @@ namespace is_conn definition is_trunc_pmap_of_is_conn (k l : ℕ₋₂) (B : Type*) (H2 : l ≤ n.+1+2+k) (H3 : is_trunc l B) : is_trunc k.+1 (A →* B) := - @is_trunc_equiv_closed _ _ k.+1 (pppi_equiv_pmap A B) - (is_trunc_ppi_of_is_conn A n k l H2 (λ a, B) _) + is_trunc_equiv_closed k.+1 (pppi_equiv_pmap A B) + (is_trunc_ppi_of_is_conn A n H k l H2 (λ a, B) _) end diff --git a/spectrum/basic.hlean b/spectrum/basic.hlean index 75e2905..0eb075f 100644 --- a/spectrum/basic.hlean +++ b/spectrum/basic.hlean @@ -235,7 +235,7 @@ namespace spectrum definition szero [constructor] {N : succ_str} (E F : gen_prespectrum N) : E →ₛ F := begin apply smap.mk (λn, pconst (E n) (F n)), - intro n, exact !hpconst_square ⬝vp* !ap1_pconst + intro n, exact !phconst_square ⬝vp* !ap1_pconst end definition stransport [constructor] {N : succ_str} {A : Type} {a a' : A} (p : a = a') @@ -588,13 +588,13 @@ namespace spectrum definition πg_glue_homotopy_π_glue (X : spectrum) (n : ℤ) : πg_glue X n ~ π_glue X n := by reflexivity - definition π_glue_square {X Y : spectrum} (f : X →ₛ Y) (n : ℤ) : + definition π_glue_natural {X Y : spectrum} (f : X →ₛ Y) (n : ℤ) : π_glue Y n ∘* π→[2] (f (2 - succ n)) ~* π→[3] (f (2 - n)) ∘* π_glue X n := begin change π→[2] (equiv_glue_neg Y n) ∘* π→[2] (f (2 - succ n)) ~* π→[2] (Ω→ (f (2 - n))) ∘* π→[2] (equiv_glue_neg X n), refine homotopy_group_functor_psquare 2 _, - refine !sglue_square ⬝v* ap1_psquare !pequiv_of_eq_commute + refine !sglue_square ⬝v* ap1_psquare !pequiv_of_eq_natural⁻¹* end definition homotopy_group_spectrum_irrel_one {n m : ℤ} {k : ℕ} (E : spectrum) (p : n + 1 = m + k) @@ -658,7 +658,7 @@ namespace spectrum definition LES_of_shomotopy_groups : chain_complex +3ℤ := splice (λ(n : ℤ), LES_of_homotopy_groups (f (2 - n))) (2, 0) - (π_glue Y) (π_glue X) (π_glue_square f) + (π_glue Y) (π_glue X) (π_glue_natural f) -- This LES is definitionally what we want: example (n : ℤ) : LES_of_shomotopy_groups (n, 0) = πₛ[n] Y := idp @@ -818,7 +818,8 @@ namespace spectrum smap.mk (λn, pppi_compose_left (λa, f a n)) begin intro n, - exact psquare_pppi_compose_left (λa, (glue_square (f a) n)) ⬝v* !loop_pppi_pequiv_natural⁻¹ᵛ* + exact psquare_pppi_compose_left (λa, (glue_square (f a) n)) ⬝v* + (ptranspose !loop_pppi_pequiv_natural_right)⁻¹ᵛ* end -- unpointed spi diff --git a/spectrum/spectrification.hlean b/spectrum/spectrification.hlean index 07b5053..ac24b02 100644 --- a/spectrum/spectrification.hlean +++ b/spectrum/spectrification.hlean @@ -221,7 +221,7 @@ namespace spectrum refine !passoc ⬝* _, refine pwhisker_left _ ((passoc _ _ (_ ∘* _))⁻¹*) ⬝* _, refine pwhisker_left _ !passoc⁻¹* ⬝* _, - refine pwhisker_left _ (pwhisker_right _ (phomotopy_pinv_right_of_phomotopy (!loopn_succ_in_natural)⁻¹*)⁻¹*) ⬝* _, + refine pwhisker_left _ (pwhisker_right _ (phomotopy_pinv_right_of_phomotopy (!loopn_succ_in_natural))⁻¹*) ⬝* _, refine pwhisker_right _ !apn_pinv ⬝* _, refine (phomotopy_pinv_left_of_phomotopy _)⁻¹*, refine apn_psquare k _,