From 013ca8d5f28f88c5d4a4fc6ea79bd0bc58537d56 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 1 Mar 2017 20:38:13 -0500 Subject: [PATCH] make progress on naturality of smash-pmap adjunction The only fact left to be proven is a property (which is an equality of phomotopies) of the functorial action of the smash product --- homotopy/EM.hlean | 16 +- homotopy/smash.hlean | 58 ++++- homotopy/smash_adjoint.hlean | 186 ++++++--------- homotopy/spectrum.hlean | 60 ++--- move_to_lib.hlean | 451 +++++++++++++++++++++++++---------- 5 files changed, 486 insertions(+), 285 deletions(-) diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean index 5814010..0161ab0 100644 --- a/homotopy/EM.hlean +++ b/homotopy/EM.hlean @@ -193,20 +193,20 @@ namespace EM begin refine hwhisker_left _ (to_fun_isomorphism_trans _ _) ⬝hty _ ⬝hty hwhisker_right _ (to_fun_isomorphism_trans _ _)⁻¹ʰᵗʸ, - refine htyhcompose _ (homotopy_group_homomorphism_psquare 1 (apn_EMadd1_pequiv_EM1_natural φ n)), + refine _ ⬝htyh (homotopy_group_homomorphism_psquare 1 (apn_EMadd1_pequiv_EM1_natural φ n)), apply homotopy_group_functor_EM1_functor 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) := - htyhinverse (homotopy_group_functor_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 : Ω→ f ∘ eX ~ eY ∘ φ) : - f ∘* EM1_pmap eX rX ~* EM1_pmap eY rY ∘* EM1_functor φ := + (φ : G →g H) (p : hsquare eX eY φ (Ω→ f)) : + psquare (EM1_pmap eX rX) (EM1_pmap eY rY) (EM1_functor φ) f := begin fapply phomotopy.mk, { intro x, induction x using EM.set_rec, @@ -245,7 +245,7 @@ namespace EM (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) := begin - refine htyhcompose _ p, + refine _ ⬝htyh p, exact to_homotopy (phinverse (loopn_succ_in_natural (succ n) f)⁻¹*) end @@ -256,7 +256,7 @@ namespace EM f ∘* EMadd1_pmap n eX rX ~* EMadd1_pmap n eY rY ∘* EMadd1_functor φ n := 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 @htyhinverse _ _ _ _ eX eY _ _ p }, + { apply EM1_pmap_natural, exact @hhinverse _ _ _ _ _ _ eX eY 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) _ _)⁻¹*, @@ -286,7 +286,7 @@ namespace EM 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) - _ _ φ (htyhcompose (to_homotopy (phinverse (ptrunc_pequiv_natural 0 (Ω→[succ n] f)))) p) + _ _ φ (hhcompose (to_homotopy (phinverse (ptrunc_pequiv_natural 0 (Ω→[succ n] f)))) p) 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] @@ -450,7 +450,7 @@ namespace EM { fapply natural_iso.mk, { fapply nat_trans.mk, { intro G, exact (fundamental_group_EM1' G)⁻¹ᵍ }, - { intro G H φ, apply homomorphism_eq, exact htyhinverse (homotopy_group_functor_EM1_functor φ) }}, + { intro G H φ, apply homomorphism_eq, exact hhinverse (homotopy_group_functor_EM1_functor φ) }}, { intro G, fapply iso.is_iso.mk, { exact fundamental_group_EM1' G }, { apply homomorphism_eq, diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean index 75337bf..52c651d 100644 --- a/homotopy/smash.hlean +++ b/homotopy/smash.hlean @@ -15,7 +15,6 @@ variables {A B C D E F : Type*} namespace smash - section open pushout definition smash_functor' [unfold 7] (f : A →* C) (g : B →* D) : A ∧ B → C ∧ D := @@ -114,7 +113,6 @@ namespace smash apply con_right_inv_natural end - definition smash_functor_pcompose_homotopy (f' : C →* E) (f : A →* C) (g' : D →* F) (g : B →* D) : smash_functor (f' ∘* f) (g' ∘* g) ~ smash_functor f' g' ∘* smash_functor f g := begin @@ -184,6 +182,60 @@ namespace smash : smash_functor (f' ∘* f) (pid B) ~* smash_functor f' (pid B) ∘* smash_functor f (pid B) := smash_functor_phomotopy phomotopy.rfl !pid_pcompose⁻¹* ⬝* !smash_functor_pcompose + definition smash_functor_pconst_right_homotopy [unfold 6] (f : A →* C) (x : A ∧ B) : + smash_functor f (pconst B D) x = pt := + begin + induction x with a b a b, + { exact gluel' (f a) pt }, + { exact (gluel pt)⁻¹ }, + { exact (gluer pt)⁻¹ }, + { apply eq_pathover_constant_right, refine !functor_gluel ⬝ !idp_con ⬝ph _, + apply square_of_eq, reflexivity }, + { apply eq_pathover_constant_right, refine !functor_gluer ⬝ph _, + apply whisker_lb, apply square_of_eq, exact !ap_mk_left⁻¹ } + end + + definition smash_functor_pconst_right [constructor] (f : A →* C) : + smash_functor f (pconst B D) ~* pconst (A ∧ B) (C ∧ D) := + begin + fapply phomotopy.mk, + { exact smash_functor_pconst_right_homotopy f }, + { refine (ap_mk_left (respect_pt f))⁻¹ ⬝ _, + induction C with C c₀, induction f with f f₀, esimp at *, induction f₀, reflexivity } + end + + definition smash_functor_pconst_right_pcompose (f' : C →* E) (f : A →* C) (g : D →* F) : + phsquare (smash_functor_pcompose f' f g (pconst B D)) + (smash_functor_pconst_right (f' ∘* f)) + (smash_functor_phomotopy phomotopy.rfl (pcompose_pconst g)) + (pwhisker_left (smash_functor f' g) (smash_functor_pconst_right f) ⬝* + pcompose_pconst (smash_functor f' g)) := + begin + exact sorry + end + + definition smash_functor_pconst_right_pid_pcompose (g : D →* F) : + phsquare (smash_functor_pid_pcompose A g (pconst B D)) + (smash_functor_pconst_right (pid A)) + (smash_functor_phomotopy phomotopy.rfl (pcompose_pconst g)) + (pwhisker_left (smash_functor (pid A) g) (smash_functor_pconst_right (pid A)) ⬝* + pcompose_pconst (smash_functor (pid A) g)) := + begin + refine (_ ◾** idp ⬝ !refl_trans) ⬝pv** smash_functor_pconst_right_pcompose (pid A) (pid A) g, + apply smash_functor_phomotopy_refl, + end + + definition smash_functor_pconst_right_pid_pcompose' (g : D →* F) : + pwhisker_left (smash_functor (pid A) g) (smash_functor_pconst_right (pid A)) ⬝* + pcompose_pconst (smash_functor (pid A) g) = + (smash_functor_pid_pcompose A g (pconst B D))⁻¹* ⬝* + (smash_functor_phomotopy phomotopy.rfl (pcompose_pconst g) ⬝* + smash_functor_pconst_right (pid A)) := + begin + apply eq_symm_trans_of_trans_eq, + exact smash_functor_pconst_right_pid_pcompose g + end + definition smash_pequiv_smash [constructor] (f : A ≃* C) (g : B ≃* D) : A ∧ B ≃* C ∧ D := begin fapply pequiv_of_pmap (smash_functor f g), @@ -191,8 +243,6 @@ namespace smash exact to_is_equiv (sum_equiv_sum f g) end - end - definition smash_pequiv_smash_left [constructor] (B : Type*) (f : A ≃* C) : A ∧ B ≃* C ∧ B := smash_pequiv_smash f pequiv.rfl diff --git a/homotopy/smash_adjoint.hlean b/homotopy/smash_adjoint.hlean index 9ede3d1..b3fceea 100644 --- a/homotopy/smash_adjoint.hlean +++ b/homotopy/smash_adjoint.hlean @@ -241,18 +241,19 @@ namespace smash definition smash_elim_pconst (A B C : Type*) : smash_elim (pconst B (ppmap A C)) ~* pconst (A ∧ B) C := begin - fconstructor, - { intro x, induction x with a b a b, - { reflexivity }, - { reflexivity }, - { reflexivity }, - { apply eq_pathover_constant_right, apply hdeg_square, - refine ap_compose smash_pmap_counit_map _ _ ⬝ ap02 _ !functor_gluel ⬝ !ap_con ⬝ - !ap_compose'⁻¹ ◾ !elim_gluel}, - { apply eq_pathover_constant_right, apply hdeg_square, - refine ap_compose smash_pmap_counit_map _ _ ⬝ ap02 _ !functor_gluer ⬝ !ap_con ⬝ - !ap_compose'⁻¹ ◾ !elim_gluer }}, - { reflexivity } + refine pwhisker_left _ (smash_functor_pconst_right (pid A)) ⬝* !pcompose_pconst + -- fconstructor, + -- { intro x, induction x with a b a b, + -- { reflexivity }, + -- { reflexivity }, + -- { reflexivity }, + -- { apply eq_pathover_constant_right, apply hdeg_square, + -- refine ap_compose smash_pmap_counit_map _ _ ⬝ ap02 _ !functor_gluel ⬝ !ap_con ⬝ + -- !ap_compose'⁻¹ ◾ !elim_gluel}, + -- { apply eq_pathover_constant_right, apply hdeg_square, + -- refine ap_compose smash_pmap_counit_map _ _ ⬝ ap02 _ !functor_gluer ⬝ !ap_con ⬝ + -- !ap_compose'⁻¹ ◾ !elim_gluer }}, + -- { reflexivity } end definition pconst_pcompose_pconst (A B C : Type*) : @@ -302,18 +303,18 @@ namespace smash end definition smash_elim_phomotopy {A B C : Type*} {f f' : A →* ppmap B C} - (p : f ~* f'): smash_elim f ~* smash_elim f' := + (p : f ~* f') : smash_elim f ~* smash_elim f' := begin apply pwhisker_left, exact smash_functor_phomotopy phomotopy.rfl p end definition smash_elim_inv_phomotopy {A B C : Type*} {f f' : A ∧ B →* C} - (p : f ~* f'): smash_elim_inv f ~* smash_elim_inv f' := + (p : f ~* f') : smash_elim_inv f ~* smash_elim_inv f' := pwhisker_right _ (ppcompose_left_phomotopy p) definition smash_elim_eq_of_phomotopy {A B C : Type*} {f f' : A →* ppmap B C} - (p : f ~* f'): ap smash_elim (eq_of_phomotopy p) = eq_of_phomotopy (smash_elim_phomotopy p) := + (p : f ~* f') : ap smash_elim (eq_of_phomotopy p) = eq_of_phomotopy (smash_elim_phomotopy p) := begin induction p using phomotopy_rec_on_idp, refine ap02 _ !eq_of_phomotopy_refl ⬝ _, @@ -323,8 +324,8 @@ namespace smash refine !pwhisker_left_refl⁻¹ end - definition smash_elim_inv_eq_of_phomotopy {A B C : Type*} {f f' : A ∧ B →* C} - (p : f ~* f'): ap smash_elim_inv (eq_of_phomotopy p) = eq_of_phomotopy (smash_elim_inv_phomotopy p) := + definition smash_elim_inv_eq_of_phomotopy {A B C : Type*} {f f' : A ∧ B →* C} (p : f ~* f') : + ap smash_elim_inv (eq_of_phomotopy p) = eq_of_phomotopy (smash_elim_inv_phomotopy p) := begin induction p using phomotopy_rec_on_idp, refine ap02 _ !eq_of_phomotopy_refl ⬝ _, @@ -337,9 +338,31 @@ namespace smash definition smash_pelim [constructor] (A B C : Type*) : ppmap A (ppmap B C) →* ppmap (B ∧ A) C := pmap.mk smash_elim (eq_of_phomotopy !smash_elim_pconst) - definition smash_pelim_inv [constructor] (A B C : Type*) : ppmap (B ∧ A) C →* ppmap A (ppmap B C) := + definition smash_pelim_inv [constructor] (A B C : Type*) : + ppmap (B ∧ A) C →* ppmap A (ppmap B C) := pmap.mk smash_elim_inv (eq_of_phomotopy !smash_elim_inv_pconst) + theorem smash_elim_natural_pconst {A B C C' : Type*} (f : C →* C') : + smash_elim_natural f (pconst A (ppmap B C)) ⬝* + (smash_elim_phomotopy (pcompose_pconst (ppcompose_left f)) ⬝* + smash_elim_pconst B A C') = + pwhisker_left f (smash_elim_pconst B A C) ⬝* + pcompose_pconst f := + begin + refine idp ◾** (!trans_assoc⁻¹ ⬝ (!pwhisker_left_trans⁻¹ ◾** idp)) ⬝ _, + refine !trans_assoc⁻¹ ⬝ _, + refine (!trans_assoc ⬝ (idp ◾** (!pwhisker_left_trans⁻¹ ⬝ + ap (pwhisker_left _) (smash_functor_pconst_right_pid_pcompose' (ppcompose_left f))⁻¹ ⬝ + !pwhisker_left_trans))) ◾** idp ⬝ _, + refine (!trans_assoc⁻¹ ⬝ (!passoc_phomotopy_right⁻¹ʰ** ⬝h** + !pwhisker_right_pwhisker_left ⬝h** !passoc_phomotopy_right) ◾** idp) ◾** idp ⬝ _, + refine !trans_assoc ⬝ !trans_assoc ⬝ idp ◾**_ ⬝ !trans_assoc⁻¹ ⬝ !pwhisker_left_trans⁻¹ ◾** idp, + refine !trans_assoc ⬝ !trans_assoc ⬝ (eq_symm_trans_of_trans_eq _)⁻¹, + refine !pcompose_pconst_pcompose⁻¹ ⬝ _, + refine _ ⬝ idp ◾** (!pcompose_pconst_pcompose), + refine !pcompose_pconst_phomotopy⁻¹ + end + definition smash_pelim_natural {A B C C' : Type*} (f : C →* C') : ppcompose_left f ∘* smash_pelim A B C ~* smash_pelim A B C' ∘* ppcompose_left (ppcompose_left f) := @@ -351,55 +374,9 @@ namespace smash !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy) ⬝ _ , refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹, - exact sorry } + exact smash_elim_natural_pconst f } end - definition smash_pelim_inv_natural {A B C C' : Type*} (f : C →* C') : - ppcompose_left (ppcompose_left f) ∘* smash_pelim_inv A B C ~* - smash_pelim_inv A B C' ∘* ppcompose_left f := - begin - fapply phomotopy_mk_ppmap, - { exact smash_elim_inv_natural f }, - { esimp, - refine idp ◾** (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !smash_elim_inv_eq_of_phomotopy ⬝ - !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy) ⬝ _, - refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_eq_of_phomotopy ⬝ - !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹, - exact sorry - } - end - - - -- definition smash_adjoint_pmap_2 [constructor] (A B C : Type*) : (A ∧ B →* C) ≃ B →* ppmap A C := - -- begin - -- fapply equiv.MK, - -- { exact smash_elim_inv }, - -- { exact smash_elim }, - -- { intro f, apply eq_of_phomotopy, exact smash_elim_left_inv f }, - -- { intro g, apply eq_of_phomotopy, exact smash_elim_right_inv g } - -- end - - -- definition smash_adjoint_pmap_1 [constructor] (A B C : Type*) : (A ∧ B →* C) ≃ A →* ppmap B C := - -- pequiv_ppcompose_right (smash_comm B A) ⬝e smash_adjoint_pmap_2 B A C - - -- definition smash_elim_inv_pconst {A B C : Type*} : - -- smash_elim_inv (pconst (A ∧ B) C) ~* pconst B (ppmap A C) := - -- begin - -- fapply phomotopy_mk_ppmap, - -- { intro b, exact pconst_pcompose (pinl A b) }, - -- { refine !trans_refl ⬝ _ ⬝ !phomotopy_of_eq_con⁻¹, - -- refine _ ⬝ ap011 phomotopy.trans (!phomotopy_of_eq_of_phomotopy⁻¹ ⬝ - -- ap phomotopy_of_eq !pcompose_eq_of_phomotopy⁻¹) !phomotopy_of_eq_of_phomotopy⁻¹, - -- fapply phomotopy_eq, - -- { intro a, exact !ap_constant⁻¹ }, - -- { refine whisker_right _ !whisker_right_idp ⬝ _, esimp, } - -- } - -- end - - -- definition smash_adjoint_pmap' [constructor] (A B C : Type*) : ppmap (A ∧ B) C ≃* ppmap B (ppmap A C) := - -- pequiv_of_equiv (smash_adjoint_pmap_2 A B C) (eq_of_phomotopy begin esimp end) - - definition smash_adjoint_pmap' [constructor] (A B C : Type*) : B →* ppmap A C ≃ A ∧ B →* C := begin fapply equiv.MK, @@ -409,9 +386,13 @@ namespace smash { intro f, apply eq_of_phomotopy, exact smash_elim_left_inv f } end + definition smash_adjoint_pmap_inv [constructor] (A B C : Type*) : + ppmap B (ppmap A C) ≃* ppmap (A ∧ B) C := + pequiv_of_equiv (smash_adjoint_pmap' A B C) (eq_of_phomotopy (smash_elim_pconst A B C)) + definition smash_adjoint_pmap [constructor] (A B C : Type*) : ppmap (A ∧ B) C ≃* ppmap B (ppmap A C) := - (pequiv_of_equiv (smash_adjoint_pmap' A B C) (eq_of_phomotopy (smash_elim_pconst A B C)))⁻¹ᵉ* + (smash_adjoint_pmap_inv A B C)⁻¹ᵉ* definition smash_adjoint_pmap_natural_pt {A B C C' : Type*} (f : C →* C') (g : A ∧ B →* C) : ppcompose_left f ∘* smash_adjoint_pmap A B C g ~* smash_adjoint_pmap A B C' (f ∘* g) := @@ -420,15 +401,6 @@ namespace smash exact !ppcompose_left_pcompose⁻¹* end - definition smash_adjoint_pmap_natural [constructor] {A B C C' : Type*} (f : C →* C') : - ppcompose_left (ppcompose_left f) ∘* smash_adjoint_pmap A B C ~* - smash_adjoint_pmap A B C' ∘* ppcompose_left f := - begin - fapply phomotopy_mk_ppmap, - { exact smash_adjoint_pmap_natural_pt f }, - { exact sorry } - end - definition smash_adjoint_pmap_inv_natural_pt {A B C C' : Type*} (f : C →* C') (g : B →* ppmap A C) : f ∘* (smash_adjoint_pmap A B C)⁻¹ᵉ* g ~* (smash_adjoint_pmap A B C')⁻¹ᵉ* (ppcompose_left f ∘* g) := @@ -439,17 +411,14 @@ namespace smash end definition smash_adjoint_pmap_inv_natural [constructor] {A B C C' : Type*} (f : C →* C') : - ppcompose_left f ∘* (smash_adjoint_pmap A B C)⁻¹ᵉ* ~* - (smash_adjoint_pmap A B C')⁻¹ᵉ* ∘* ppcompose_left (ppcompose_left f) := - begin - exact sorry - end - -- begin - -- refine _ ⬝* pwhisker_left _ !smash_functor_pid_pcompose⁻¹*, - -- refine !passoc⁻¹* ⬝* pwhisker_right _ _ ⬝* !passoc, - -- apply smash_pmap_counit_natural - -- end + ppcompose_left f ∘* smash_adjoint_pmap_inv A B C ~* + smash_adjoint_pmap_inv A B C' ∘* ppcompose_left (ppcompose_left f) := + smash_pelim_natural f + definition smash_adjoint_pmap_natural [constructor] {A B C C' : Type*} (f : C →* C') : + ppcompose_left (ppcompose_left f) ∘* smash_adjoint_pmap A B C ~* + smash_adjoint_pmap A B C' ∘* ppcompose_left f := + (smash_adjoint_pmap_inv_natural f)⁻¹ʰ* /- associativity of smash -/ @@ -458,8 +427,8 @@ namespace smash calc ppmap (A ∧ (B ∧ C)) X ≃* ppmap (B ∧ C) (ppmap A X) : smash_adjoint_pmap A (B ∧ C) X ... ≃* ppmap C (ppmap B (ppmap A X)) : smash_adjoint_pmap B C (ppmap A X) - ... ≃* ppmap C (ppmap (A ∧ B) X) : pequiv_ppcompose_left (smash_adjoint_pmap A B X)⁻¹ᵉ* - ... ≃* ppmap ((A ∧ B) ∧ C) X : (smash_adjoint_pmap (A ∧ B) C X)⁻¹ᵉ* + ... ≃* ppmap C (ppmap (A ∧ B) X) : pequiv_ppcompose_left (smash_adjoint_pmap_inv A B X) + ... ≃* ppmap ((A ∧ B) ∧ C) X : smash_adjoint_pmap_inv (A ∧ B) C X definition smash_assoc_elim_equiv_fn (A B C X : Type*) (f : A ∧ (B ∧ C) →* X) : (A ∧ B) ∧ C →* X := @@ -479,35 +448,26 @@ namespace smash refine !smash_adjoint_pmap_natural_pt end - definition smash_assoc_elim_inv_natural_pt {A B C X X' : Type*} (f : X →* X') (g : (A ∧ B) ∧ C →* X) : + definition smash_assoc_elim_inv_natural_pt {A B C X X' : Type*} (f : X →* X') + (g : (A ∧ B) ∧ C →* X) : f ∘* (smash_assoc_elim_equiv A B C X)⁻¹ᵉ* g ~* (smash_assoc_elim_equiv A B C X')⁻¹ᵉ* (f ∘* g) := begin - exact sorry + refine !smash_adjoint_pmap_inv_natural_pt ⬝* _, + apply smash_elim_phomotopy, + refine !passoc⁻¹* ⬝* _, + refine pwhisker_right _ !smash_pmap_counit_natural ⬝* _, + refine !passoc ⬝* _, + apply pwhisker_left, + refine !smash_functor_pid_pcompose⁻¹* ⬝* _, + apply smash_functor_phomotopy phomotopy.rfl, + refine !passoc⁻¹* ⬝* _, + refine pwhisker_right _ !smash_adjoint_pmap_natural ⬝* _, + refine !passoc ⬝* _, + apply pwhisker_left, + apply smash_elim_inv_natural end - definition smash_assoc_elim_natural {A B C X X' : Type*} (f : X →* X') : - ppcompose_left f ∘* smash_assoc_elim_equiv A B C X ~* - smash_assoc_elim_equiv A B C X' ∘* ppcompose_left f := - begin - exact sorry - -- refine !smash_adjoint_pmap_inv_natural_pt ⬝* _, - -- apply smash_elim_phomotopy, - -- refine !passoc⁻¹* ⬝* _, - -- refine pwhisker_right _ !smash_adjoint_pmap_inv_natural ⬝* _, - -- refine !passoc ⬝* _, - -- apply pwhisker_left, - -- refine !smash_adjoint_pmap_natural_pt ⬝* _, - -- apply smash_elim_inv_phomotopy, - -- refine !smash_adjoint_pmap_natural_pt - end - - -- definition smash_assoc_to (A B C : Type*) : A ∧ (B ∧ C) →* (A ∧ B) ∧ C := - -- begin - - -- end - - - -- TODO: remove pap + -- TODO: maybe do it without pap / phomotopy_of_eq definition smash_assoc (A B C : Type*) : A ∧ (B ∧ C) ≃* (A ∧ B) ∧ C := begin fapply pequiv.MK2, @@ -521,5 +481,5 @@ namespace smash apply phomotopy_of_eq, apply to_right_inv !smash_assoc_elim_equiv } end - +print axioms smash_assoc end smash diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index e6dde02..90bb71a 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -7,14 +7,12 @@ Authors: Michael Shulman, Floris van Doorn import homotopy.LES_of_homotopy_groups .splice homotopy.susp ..move_to_lib ..colim ..pointed_pi open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group - seq_colim + seq_colim succ_str /--------------------- Basic definitions ---------------------/ -open succ_str - /- The basic definitions of spectra and prespectra make sense for any successor-structure. -/ structure gen_prespectrum (N : succ_str) := @@ -210,13 +208,13 @@ namespace spectrum -- read off the homotopy groups without any tedious case-analysis of -- n. We increment by 2 in order to ensure that they are all -- automatically abelian groups. - definition shomotopy_group [constructor] (n : ℤ) (E : spectrum) : AbGroup := πag[0+2] (E (2 - n)) + definition shomotopy_group [constructor] (n : ℤ) (E : spectrum) : AbGroup := πag[2] (E (2 - n)) notation `πₛ[`:95 n:0 `]`:0 := shomotopy_group n definition shomotopy_group_fun [constructor] (n : ℤ) {E F : spectrum} (f : E →ₛ F) : πₛ[n] E →g πₛ[n] F := - π→g[1+1] (f (2 - n)) + π→g[2] (f (2 - n)) notation `πₛ→[`:95 n:0 `]`:0 := shomotopy_group_fun n @@ -257,41 +255,34 @@ namespace spectrum rexact (pfiber_equiv_of_square_ppoint (equiv_glue X n) (equiv_glue Y n) (sglue_square f n))⁻¹* end - definition π_glue (X : spectrum) (n : ℤ) : π[2] (X (2 - succ n)) ≃* π[3] (X (2 - n)) := + definition scompose_spoint {N : succ_str} {X Y : gen_spectrum N} (f : X →ₛ Y) + : f ∘ₛ spoint f ~ₛ szero (sfiber f) Y := begin - refine homotopy_group_pequiv 2 (equiv_glue X (2 - succ n)) ⬝e* _, - assert H : succ (2 - succ n) = 2 - n, exact ap succ !sub_sub⁻¹ ⬝ sub_add_cancel (2-n) 1, - exact pequiv_of_eq (ap (λn, π[2] (Ω (X n))) H), + fapply shomotopy.mk, + { intro n, exact pcompose_ppoint (f n) }, + { intro n, exact sorry } end - definition πg_glue (X : spectrum) (n : ℤ) : πg[1+1] (X (2 - succ n)) ≃g πg[2+1] (X (2 - n)) := - begin - refine homotopy_group_isomorphism_of_pequiv 1 (equiv_glue X (2 - succ n)) ⬝g _, - assert H : succ (2 - succ n) = 2 - n, exact ap succ !sub_sub⁻¹ ⬝ sub_add_cancel (2-n) 1, - exact isomorphism_of_eq (ap (λn, πg[1+1] (Ω (X n))) H), - end + definition equiv_glue_neg (X : spectrum) (n : ℤ) : X (2 - succ n) ≃* Ω (X (2 - n)) := + have H : succ (2 - succ n) = 2 - n, from ap succ !sub_sub⁻¹ ⬝ sub_add_cancel (2-n) 1, + equiv_glue X (2 - succ n) ⬝e* loop_pequiv_loop (pequiv_of_eq (ap X H)) + + definition π_glue (X : spectrum) (n : ℤ) : π[2] (X (2 - succ n)) ≃* π[3] (X (2 - n)) := + homotopy_group_pequiv 2 (equiv_glue_neg X n) + + definition πg_glue (X : spectrum) (n : ℤ) : πg[2] (X (2 - succ n)) ≃g πg[3] (X (2 - n)) := + by rexact homotopy_group_isomorphism_of_pequiv _ (equiv_glue_neg X n) definition πg_glue_homotopy_π_glue (X : spectrum) (n : ℤ) : πg_glue X n ~ π_glue X n := - begin - intro x, - esimp [πg_glue, π_glue], - apply ap (λp, cast p _), - refine !ap_compose'⁻¹ ⬝ !ap_compose' - end + by reflexivity definition π_glue_square {X Y : spectrum} (f : X →ₛ Y) (n : ℤ) : π_glue Y n ∘* π→[2] (f (2 - succ n)) ~* π→[3] (f (2 - n)) ∘* π_glue X n := begin - refine !passoc ⬝* _, - assert H1 : homotopy_group_pequiv 2 (equiv_glue Y (2 - succ n)) ∘* π→[2] (f (2 - succ n)) - ~* π→[2] (Ω→ (f (succ (2 - succ n)))) ∘* homotopy_group_pequiv 2 (equiv_glue X (2 - succ n)), - { refine !homotopy_group_functor_compose⁻¹* ⬝* _, - refine homotopy_group_functor_phomotopy 2 !sglue_square ⬝* _, - apply homotopy_group_functor_compose }, - refine pwhisker_left _ H1 ⬝* _, clear H1, - refine !passoc⁻¹* ⬝* _ ⬝* !passoc, - apply pwhisker_right, - refine !pequiv_of_eq_commute ⬝* by reflexivity + 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 end section @@ -324,8 +315,7 @@ namespace spectrum | (n, fin.mk 0 H) := proof homomorphism.struct (πₛ→[n] f) qed | (n, fin.mk 1 H) := proof homomorphism.struct (πₛ→[n] (spoint f)) qed | (n, fin.mk 2 H) := proof homomorphism.struct - (homomorphism_LES_of_homotopy_groups_fun (f (2 - n)) (1, 2) ∘g - homomorphism_change_fun (πg_glue Y n) _ (πg_glue_homotopy_π_glue Y n)) qed + (homomorphism_LES_of_homotopy_groups_fun (f (2 - n)) (1, 2) ∘g πg_glue Y n) qed | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end -- In the comments below is a start on an explicit description of the LES for spectra @@ -433,8 +423,8 @@ namespace spectrum (f : X →ₛ Y) : X →ₛ spectrify X := begin fapply smap.mk, - { intro n, exact pinclusion _ 0}, - { intro n, exact sorry} + { intro n, exact pinclusion _ 0 }, + { intro n, exact sorry } end definition spectrify.elim {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N} diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 11fe09c..efb8931 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -73,6 +73,78 @@ namespace eq (p : a = a') : whisker_right q (ap f p) = ap (λa, f a ⬝ q) p := by induction p; reflexivity + infix ` ⬝hty `:75 := homotopy.trans + postfix `⁻¹ʰᵗʸ`:(max+1) := homotopy.symm + + definition hassoc {A B C D : Type} (h : C → D) (g : B → C) (f : A → B) : (h ∘ g) ∘ f ~ h ∘ (g ∘ f) := + λa, idp + + -- to algebra.homotopy_group + definition homotopy_group_homomorphism_pcompose (n : ℕ) [H : is_succ n] {A B C : Type*} (g : B →* C) + (f : A →* B) : π→g[n] (g ∘* f) ~ π→g[n] g ∘ π→g[n] f := + begin + induction H with n, exact to_homotopy (homotopy_group_functor_compose (succ n) g f) + end + + definition apn_pinv (n : ℕ) {A B : Type*} (f : A ≃* B) : + Ω→[n] f⁻¹ᵉ* ~* (loopn_pequiv_loopn n f)⁻¹ᵉ* := + begin + refine !to_pinv_pequiv_MK2⁻¹* + end + + -- definition homotopy_group_homomorphism_pinv (n : ℕ) {A B : Type*} (f : A ≃* B) : + -- π→g[n+1] f⁻¹ᵉ* ~ (homotopy_group_isomorphism_of_pequiv n f)⁻¹ᵍ := + -- begin + -- -- refine ptrunc_functor_phomotopy 0 !apn_pinv ⬝hty _, + -- -- intro x, esimp, + -- end + + -- definition natural_square_tr_eq {A B : Type} {a a' : A} {f g : A → B} + -- (p : f ~ g) (q : a = a') : natural_square p q = square_of_pathover (apd p q) := + -- idp + + + section hsquare + variables {A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type} + {f₁₀ : A₀₀ → A₂₀} {f₃₀ : A₂₀ → A₄₀} + {f₀₁ : A₀₀ → A₀₂} {f₂₁ : A₂₀ → A₂₂} {f₄₁ : A₄₀ → A₄₂} + {f₁₂ : A₀₂ → A₂₂} {f₃₂ : A₂₂ → A₄₂} + {f₀₃ : A₀₂ → A₀₄} {f₂₃ : A₂₂ → A₂₄} {f₄₃ : A₄₂ → A₄₄} + {f₁₄ : A₀₄ → A₂₄} {f₃₄ : A₂₄ → A₄₄} + + definition hsquare [reducible] (f₁₀ : A₀₀ → A₂₀) (f₁₂ : A₀₂ → A₂₂) + (f₀₁ : A₀₀ → A₀₂) (f₂₁ : A₂₀ → A₂₂) : Type := + f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁ + + definition hsquare_of_homotopy (p : f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁) : hsquare f₁₀ f₁₂ f₀₁ f₂₁ := + p + + definition homotopy_of_hsquare (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁ := + p + + definition hhcompose (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) : + hsquare (f₃₀ ∘ f₁₀) (f₃₂ ∘ f₁₂) f₀₁ f₄₁ := + hwhisker_right f₁₀ q ⬝hty hwhisker_left f₃₂ p + + definition hvcompose (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₁₂ f₁₄ f₀₃ f₂₃) : + hsquare f₁₀ f₁₄ (f₀₃ ∘ f₀₁) (f₂₃ ∘ f₂₁) := + (hhcompose p⁻¹ʰᵗʸ q⁻¹ʰᵗʸ)⁻¹ʰᵗʸ + + definition hhinverse {f₁₀ : A₀₀ ≃ A₂₀} {f₁₂ : A₀₂ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : + hsquare f₁₀⁻¹ᵉ f₁₂⁻¹ᵉ f₂₁ f₀₁ := + λb, eq_inv_of_eq ((p (f₁₀⁻¹ᵉ b))⁻¹ ⬝ ap f₂₁ (to_right_inv f₁₀ b)) + + definition hvinverse {f₀₁ : A₀₀ ≃ A₀₂} {f₂₁ : A₂₀ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : + hsquare f₁₂ f₁₀ f₀₁⁻¹ᵉ f₂₁⁻¹ᵉ := + (hhinverse p⁻¹ʰᵗʸ)⁻¹ʰᵗʸ + + infix ` ⬝htyh `:73 := hhcompose + infix ` ⬝htyv `:73 := hvcompose + postfix `⁻¹ʰᵗʸʰ`:(max+1) := hhinverse + postfix `⁻¹ʰᵗʸᵛ`:(max+1) := hvinverse + + end hsquare + end eq open eq namespace wedge @@ -130,36 +202,49 @@ namespace pointed -- pequiv_of_equiv (pi_equiv_pi_right g) -- begin esimp, apply eq_of_homotopy, intros a, esimp, exact (respect_pt (g a)) end + section psquare /- - Squares of pointed homotopies + Squares of pointed maps We treat expressions of the form - k ∘* f ~* g ∘* h + psquare f g h k :≡ k ∘* f ~* g ∘* h as squares, where f is the top, g is the bottom, h is the left face and k is the right face. Then the following are operations on squares -/ - definition psquare {A B C D : Type*} (f : A →* B) (g : C →* D) (h : A ≃* C) (k : B ≃* D) : Type := - k ∘* f ~* g ∘* h + variables {A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*} + {f₁₀ : A₀₀ →* A₂₀} {f₃₀ : A₂₀ →* A₄₀} + {f₀₁ : A₀₀ →* A₀₂} {f₂₁ : A₂₀ →* A₂₂} {f₄₁ : A₄₀ →* A₄₂} + {f₁₂ : A₀₂ →* A₂₂} {f₃₂ : A₂₂ →* A₄₂} + {f₀₃ : A₀₂ →* A₀₄} {f₂₃ : A₂₂ →* A₂₄} {f₄₃ : A₄₂ →* A₄₄} + {f₁₄ : A₀₄ →* A₂₄} {f₃₄ : A₂₄ →* A₄₄} - definition phcompose {A B C D B' D' : Type*} {f : A →* B} {g : C →* D} {h : A →* C} {k : B →* D} - {f' : B →* B'} {g' : D →* D'} {k' : B' →* D'} (p : k ∘* f ~* g ∘* h) - (q : k' ∘* f' ~* g' ∘* k) : k' ∘* (f' ∘* f) ~* (g' ∘* g) ∘* h := - !passoc⁻¹* ⬝* pwhisker_right f q ⬝* !passoc ⬝* pwhisker_left g' p ⬝* !passoc⁻¹* + definition psquare [reducible] (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) + (f₀₁ : A₀₀ →* A₀₂) (f₂₁ : A₂₀ →* A₂₂) : Type := + f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁ - definition pvcompose {A B C D C' D' : Type*} {f : A →* B} {g : C →* D} {h : A →* C} {k : B →* D} - {g' : C' →* D'} {h' : C →* C'} {k' : D →* D'} (p : k ∘* f ~* g ∘* h) - (q : k' ∘* g ~* g' ∘* h') : (k' ∘* k) ∘* f ~* g' ∘* (h' ∘* h) := + definition psquare_of_phomotopy (p : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁) : psquare f₁₀ f₁₂ f₀₁ f₂₁ := + p + + definition phomotopy_of_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁ := + p + + definition phcompose (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₃₀ f₃₂ f₂₁ f₄₁) : + psquare (f₃₀ ∘* f₁₀) (f₃₂ ∘* f₁₂) f₀₁ f₄₁ := + !passoc⁻¹* ⬝* pwhisker_right f₁₀ q ⬝* !passoc ⬝* pwhisker_left f₃₂ p ⬝* !passoc⁻¹* + + definition pvcompose (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) : + psquare f₁₀ f₁₄ (f₀₃ ∘* f₀₁) (f₂₃ ∘* f₂₁) := (phcompose p⁻¹* q⁻¹*)⁻¹* - definition phinverse {A B C D : Type*} {f : A ≃* B} {g : C ≃* D} {h : A →* C} {k : B →* D} - (p : k ∘* f ~* g ∘* h) : h ∘* f⁻¹ᵉ* ~* g⁻¹ᵉ* ∘* k := - !pid_pcompose⁻¹* ⬝* pwhisker_right _ (pleft_inv g)⁻¹* ⬝* !passoc ⬝* + definition phinverse {f₁₀ : A₀₀ ≃* A₂₀} {f₁₂ : A₀₂ ≃* A₂₂} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare f₁₀⁻¹ᵉ* f₁₂⁻¹ᵉ* f₂₁ f₀₁ := + !pid_pcompose⁻¹* ⬝* pwhisker_right _ (pleft_inv f₁₂)⁻¹* ⬝* !passoc ⬝* pwhisker_left _ (!passoc⁻¹* ⬝* pwhisker_right _ p⁻¹* ⬝* !passoc ⬝* pwhisker_left _ !pright_inv ⬝* !pcompose_pid) - definition pvinverse {A B C D : Type*} {f : A →* B} {g : C →* D} {h : A ≃* C} {k : B ≃* D} - (p : k ∘* f ~* g ∘* h) : k⁻¹ᵉ* ∘* g ~* f ∘* h⁻¹ᵉ* := + definition pvinverse {f₀₁ : A₀₀ ≃* A₀₂} {f₂₁ : A₂₀ ≃* A₂₂} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare f₁₂ f₁₀ f₀₁⁻¹ᵉ* f₂₁⁻¹ᵉ* := (phinverse p⁻¹*)⁻¹* infix ` ⬝h* `:73 := phcompose @@ -167,34 +252,31 @@ namespace pointed postfix `⁻¹ʰ*`:(max+1) := phinverse postfix `⁻¹ᵛ*`:(max+1) := pvinverse - definition ap1_psquare {A B C D : Type*} {f : A →* B} {g : C →* D} {h : A →* C} {k : B →* D} - (p : k ∘* f ~* g ∘* h) : Ω→ k ∘* Ω→ f ~* Ω→ g ∘* Ω→ h := + definition ap1_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare (Ω→ f₁₀) (Ω→ f₁₂) (Ω→ f₀₁) (Ω→ f₂₁) := !ap1_pcompose⁻¹* ⬝* ap1_phomotopy p ⬝* !ap1_pcompose - definition apn_psquare (n : ℕ) {A B C D : Type*} {f : A →* B} {g : C →* D} {h : A →* C} {k : B →* D} - (p : k ∘* f ~* g ∘* h) : Ω→[n] k ∘* Ω→[n] f ~* Ω→[n] g ∘* Ω→[n] h := + definition apn_psquare (n : ℕ) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare (Ω→[n] f₁₀) (Ω→[n] f₁₂) (Ω→[n] f₀₁) (Ω→[n] f₂₁) := !apn_pcompose⁻¹* ⬝* apn_phomotopy n p ⬝* !apn_pcompose - definition ptrunc_functor_psquare (n : ℕ₋₂) {A B C D : Type*} {f : A →* B} {g : C →* D} {h : A →* C} - {k : B →* D} (p : k ∘* f ~* g ∘* h) : - ptrunc_functor n k ∘* ptrunc_functor n f ~* ptrunc_functor n g ∘* ptrunc_functor n h := + definition ptrunc_functor_psquare (n : ℕ₋₂) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare (ptrunc_functor n f₁₀) (ptrunc_functor n f₁₂) + (ptrunc_functor n f₀₁) (ptrunc_functor n f₂₁) := !ptrunc_functor_pcompose⁻¹* ⬝* ptrunc_functor_phomotopy n p ⬝* !ptrunc_functor_pcompose - definition homotopy_group_homomorphism_psquare (n : ℕ) [H : is_succ n] {A B C D : Type*} - {f : A →* B} {g : C →* D} {h : A →* C} {k : B →* D} (p : k ∘* f ~* g ∘* h) : - π→g[n] k ∘ π→g[n] f ~ π→g[n] g ∘ π→g[n] h := + definition homotopy_group_functor_psquare (n : ℕ) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare (π→[n] f₁₀) (π→[n] f₁₂) (π→[n] f₀₁) (π→[n] f₂₁) := + !homotopy_group_functor_compose⁻¹* ⬝* homotopy_group_functor_phomotopy n p ⬝* + !homotopy_group_functor_compose + + definition homotopy_group_homomorphism_psquare (n : ℕ) [H : is_succ n] + (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : hsquare (π→g[n] f₁₀) (π→g[n] f₁₂) (π→g[n] f₀₁) (π→g[n] f₂₁) := begin induction H with n, exact to_homotopy (ptrunc_functor_psquare 0 (apn_psquare (succ n) p)) end - definition htyhcompose {A B C D B' D' : Type} {f : A → B} {g : C → D} {h : A → C} {k : B → D} - {f' : B → B'} {g' : D → D'} {k' : B' → D'} (p : k ∘ f ~ g ∘ h) - (q : k' ∘ f' ~ g' ∘ k) : k' ∘ (f' ∘ f) ~ (g' ∘ g) ∘ h := - λa, q (f a) ⬝ ap g' (p a) - - definition htyhinverse {A B C D : Type} {f : A ≃ B} {g : C ≃ D} {h : A → C} {k : B → D} - (p : k ∘ f ~ g ∘ h) : h ∘ f⁻¹ᵉ ~ g⁻¹ᵉ ∘ k := - λb, eq_inv_of_eq ((p (f⁻¹ᵉ b))⁻¹ ⬝ ap k (to_right_inv f b)) + end psquare definition phomotopy_of_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) : phomotopy_of_eq (eq_of_phomotopy p) = p := @@ -266,22 +348,6 @@ namespace pointed apply to_inv_eq_of_eq, reflexivity end - definition pwhisker_left_refl {A B C : Type*} (g : B →* C) (f : A →* B) : - pwhisker_left g (phomotopy.refl f) = phomotopy.refl (g ∘* f) := - begin - induction A with A a₀, induction B with B b₀, induction C with C c₀, - induction f with f f₀, induction g with g g₀, - esimp at *, induction g₀, induction f₀, reflexivity - end - - definition pwhisker_right_refl {A B C : Type*} (f : A →* B) (g : B →* C) : - pwhisker_right f (phomotopy.refl g) = phomotopy.refl (g ∘* f) := - begin - induction A with A a₀, induction B with B b₀, induction C with C c₀, - induction f with f f₀, induction g with g g₀, - esimp at *, induction g₀, induction f₀, reflexivity - end - definition trans_refl {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* phomotopy.refl g = p := begin induction A with A a₀, induction B with B b₀, @@ -304,11 +370,28 @@ namespace pointed induction r using phomotopy_rec_on_idp, induction q using phomotopy_rec_on_idp, induction p using phomotopy_rec_on_idp, - induction A with A a₀, induction B with B b₀, + induction B with B b₀, induction f with f f₀, esimp at *, induction f₀, reflexivity end + definition refl_symm {A B : Type*} (f : A →* B) : phomotopy.rfl⁻¹* = phomotopy.refl f := + begin + induction B with B b₀, + induction f with f f₀, esimp at *, induction f₀, + reflexivity + end + + definition trans_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* p⁻¹* = phomotopy.rfl := + begin + induction p using phomotopy_rec_on_idp, exact !refl_trans ⬝ !refl_symm + end + + definition symm_trans {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹* ⬝* p = phomotopy.rfl := + begin + induction p using phomotopy_rec_on_idp, exact !trans_refl ⬝ !refl_symm + end + definition trans2 {A B : Type*} {f g h : A →* B} {p p' : f ~* g} {q q' : g ~* h} (r : p = p') (s : q = q') : p ⬝* q = p' ⬝* q' := ap011 phomotopy.trans r s @@ -323,6 +406,149 @@ namespace pointed (r : p = p') : p ⬝* q = p' ⬝* q := r ◾** idp + definition pwhisker_left_refl {A B C : Type*} (g : B →* C) (f : A →* B) : + pwhisker_left g (phomotopy.refl f) = phomotopy.refl (g ∘* f) := + begin + induction A with A a₀, induction B with B b₀, induction C with C c₀, + induction f with f f₀, induction g with g g₀, + esimp at *, induction g₀, induction f₀, reflexivity + end + + definition pwhisker_right_refl {A B C : Type*} (f : A →* B) (g : B →* C) : + pwhisker_right f (phomotopy.refl g) = phomotopy.refl (g ∘* f) := + begin + induction A with A a₀, induction B with B b₀, induction C with C c₀, + induction f with f f₀, induction g with g g₀, + esimp at *, induction g₀, induction f₀, reflexivity + end + + definition pwhisker_left_trans {A B C : Type*} (g : B →* C) {f₁ f₂ f₃ : A →* B} + (p : f₁ ~* f₂) (q : f₂ ~* f₃) : + pwhisker_left g (p ⬝* q) = pwhisker_left g p ⬝* pwhisker_left g q := + begin + induction p using phomotopy_rec_on_idp, + induction q using phomotopy_rec_on_idp, + refine _ ⬝ !pwhisker_left_refl⁻¹ ◾** !pwhisker_left_refl⁻¹, + refine ap (pwhisker_left g) !trans_refl ⬝ !pwhisker_left_refl ⬝ !trans_refl⁻¹ + end + + definition pwhisker_right_trans {A B C : Type*} (f : A →* B) {g₁ g₂ g₃ : B →* C} + (p : g₁ ~* g₂) (q : g₂ ~* g₃) : + pwhisker_right f (p ⬝* q) = pwhisker_right f p ⬝* pwhisker_right f q := + begin + induction p using phomotopy_rec_on_idp, + induction q using phomotopy_rec_on_idp, + refine _ ⬝ !pwhisker_right_refl⁻¹ ◾** !pwhisker_right_refl⁻¹, + refine ap (pwhisker_right f) !trans_refl ⬝ !pwhisker_right_refl ⬝ !trans_refl⁻¹ + end + + definition trans_eq_of_eq_symm_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} + {r : f ~* h} (s : q = p⁻¹* ⬝* r) : p ⬝* q = r := + idp ◾** s ⬝ !trans_assoc⁻¹ ⬝ trans_symm p ◾** idp ⬝ !refl_trans + + definition eq_symm_trans_of_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} + {r : f ~* h} (s : p ⬝* q = r) : q = p⁻¹* ⬝* r := + !refl_trans⁻¹ ⬝ !symm_trans⁻¹ ◾** idp ⬝ !trans_assoc ⬝ idp ◾** s + + definition trans_eq_of_eq_trans_symm {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} + {r : f ~* h} (s : p = r ⬝* q⁻¹*) : p ⬝* q = r := + s ◾** idp ⬝ !trans_assoc ⬝ idp ◾** symm_trans q ⬝ !trans_refl + + definition eq_trans_symm_of_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} + {r : f ~* h} (s : p ⬝* q = r) : p = r ⬝* q⁻¹* := + !trans_refl⁻¹ ⬝ idp ◾** !trans_symm⁻¹ ⬝ !trans_assoc⁻¹ ⬝ s ◾** idp + + section phsquare + /- + Squares of pointed homotopies + -/ + + variables {A B : Type*} {f₀₀ f₂₀ f₄₀ f₀₂ f₂₂ f₄₂ f₀₄ f₂₄ f₄₄ : A →* B} + {p₁₀ : f₀₀ ~* f₂₀} {p₃₀ : f₂₀ ~* f₄₀} + {p₀₁ : f₀₀ ~* f₀₂} {p₂₁ : f₂₀ ~* f₂₂} {p₄₁ : f₄₀ ~* f₄₂} + {p₁₂ : f₀₂ ~* f₂₂} {p₃₂ : f₂₂ ~* f₄₂} + {p₀₃ : f₀₂ ~* f₀₄} {p₂₃ : f₂₂ ~* f₂₄} {p₄₃ : f₄₂ ~* f₄₄} + {p₁₄ : f₀₄ ~* f₂₄} {p₃₄ : f₂₄ ~* f₄₄} + + definition phsquare [reducible] (p₁₀ : f₀₀ ~* f₂₀) (p₁₂ : f₀₂ ~* f₂₂) + (p₀₁ : f₀₀ ~* f₀₂) (p₂₁ : f₂₀ ~* f₂₂) : Type := + p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂ + + definition phsquare_of_eq (p : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂) : phsquare p₁₀ p₁₂ p₀₁ p₂₁ := p + definition eq_of_phsquare (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂ := p + + definition phhcompose (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (q : phsquare p₃₀ p₃₂ p₂₁ p₄₁) : + phsquare (p₁₀ ⬝* p₃₀) (p₁₂ ⬝* p₃₂) p₀₁ p₄₁ := + !trans_assoc ⬝ idp ◾** q ⬝ !trans_assoc⁻¹ ⬝ p ◾** idp ⬝ !trans_assoc + + definition phvcompose (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (q : phsquare p₁₂ p₁₄ p₀₃ p₂₃) : + phsquare p₁₀ p₁₄ (p₀₁ ⬝* p₀₃) (p₂₁ ⬝* p₂₃) := + (phhcompose p⁻¹ q⁻¹)⁻¹ + + /- + The names are very baroque. The following stands for + "pointed homotopy path-horizontal composition" (i.e. composition on the left with a path) + The names are obtained by using the ones for squares, and putting "ph" in front of it. + In practice, use the notation ⬝ph** defined below, which might be easier to remember + -/ + definition phphcompose {p₀₁'} (p : p₀₁' = p₀₁) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : + phsquare p₁₀ p₁₂ p₀₁' p₂₁ := + by induction p; exact q + + definition phhpcompose {p₂₁'} (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (p : p₂₁ = p₂₁') : + phsquare p₁₀ p₁₂ p₀₁ p₂₁' := + by induction p; exact q + + definition phpvcompose {p₁₀'} (p : p₁₀' = p₁₀) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : + phsquare p₁₀' p₁₂ p₀₁ p₂₁ := + by induction p; exact q + + definition phvpcompose {p₁₂'} (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (p : p₁₂ = p₁₂') : + phsquare p₁₀ p₁₂' p₀₁ p₂₁ := + by induction p; exact q + + definition phhinverse (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : phsquare p₁₀⁻¹* p₁₂⁻¹* p₂₁ p₀₁ := + begin + refine (eq_symm_trans_of_trans_eq _)⁻¹, + refine !trans_assoc⁻¹ ⬝ _, + refine (eq_trans_symm_of_trans_eq _)⁻¹, + exact (eq_of_phsquare p)⁻¹ + end + + definition phvinverse (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : phsquare p₁₂ p₁₀ p₀₁⁻¹* p₂₁⁻¹* := + (phhinverse p⁻¹)⁻¹ + + infix ` ⬝h** `:71 := phhcompose + infix ` ⬝v** `:72 := phvcompose + infix ` ⬝ph** `:73 := phphcompose + infix ` ⬝hp** `:73 := phhpcompose + infix ` ⬝pv** `:73 := phpvcompose + infix ` ⬝vp** `:73 := phvpcompose + postfix `⁻¹ʰ**`:(max+1) := phhinverse + postfix `⁻¹ᵛ**`:(max+1) := phvinverse + + definition passoc_phomotopy_right {A B C D : Type*} (h : C →* D) (g : B →* C) {f f' : A →* B} + (p : f ~* f') : phsquare (passoc h g f) (passoc h g f') + (pwhisker_left (h ∘* g) p) (pwhisker_left h (pwhisker_left g p)) := + begin + induction p using phomotopy_rec_on_idp, + refine idp ◾** (ap (pwhisker_left h) !pwhisker_left_refl ⬝ !pwhisker_left_refl) ⬝ _ ⬝ + !pwhisker_left_refl⁻¹ ◾** idp, + exact !trans_refl ⬝ !refl_trans⁻¹ + end + + definition pwhisker_right_pwhisker_left {A B C : Type*} {g g' : B →* C} {f f' : A →* B} + (p : g ~* g') (q : f ~* f') : + phsquare (pwhisker_right f p) (pwhisker_right f' p) (pwhisker_left g q) (pwhisker_left g' q) := + begin + induction p using phomotopy_rec_on_idp, + induction q using phomotopy_rec_on_idp, + exact !pwhisker_right_refl ◾** !pwhisker_left_refl ⬝ + !pwhisker_left_refl⁻¹ ◾** !pwhisker_right_refl⁻¹ + end + + end phsquare + definition phomotopy_of_eq_con {A B : Type*} {f g h : A →* B} (p : f = g) (q : g = h) : phomotopy_of_eq (p ⬝ q) = phomotopy_of_eq p ⬝* phomotopy_of_eq q := begin induction q, induction p, exact !trans_refl⁻¹ end @@ -346,7 +572,7 @@ namespace pointed apply phomotopy.mk (λa, eq_of_phomotopy (p a)), apply eq_of_fn_eq_fn (pmap_eq_equiv _ _), esimp [pmap_eq_equiv], refine !phomotopy_of_eq_con ⬝ _, - refine ap (λx, x ⬝* _) !phomotopy_of_eq_of_phomotopy ⬝ q, + refine !phomotopy_of_eq_of_phomotopy ◾** idp ⬝ q, end definition pcompose_pconst_pcompose {A B C D : Type*} (h : C →* D) (g : B →* C) : @@ -365,7 +591,7 @@ namespace pointed fapply phomotopy_mk_ppmap, { exact passoc h g }, { esimp, - refine ap (λx, _ ⬝* x) (!phomotopy_of_eq_con ⬝ ap011 phomotopy.trans + refine idp ◾** (!phomotopy_of_eq_con ⬝ ap011 phomotopy.trans (ap phomotopy_of_eq !pcompose_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) !phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹, exact (pcompose_pconst_pcompose h g)⁻¹ } @@ -380,6 +606,14 @@ namespace pointed esimp at *, induction f₀, reflexivity } end + definition ppcompose_left_pconst [constructor] (A B C : Type*) : + @ppcompose_left A _ _ (pconst B C) ~* pconst (ppmap A B) (ppmap A C) := + begin + fapply phomotopy_mk_ppmap, + { exact pconst_pcompose }, + { refine idp ◾** !phomotopy_of_eq_idp ⬝ !phomotopy_of_eq_of_phomotopy⁻¹ } + end + definition ppcompose_left_phomotopy [constructor] {A B C : Type*} {g g' : B →* C} (p : g ~* g') : @ppcompose_left A _ _ g ~* ppcompose_left g' := begin @@ -397,6 +631,39 @@ namespace pointed ppcompose_left_phomotopy (phomotopy.refl g) = phomotopy.refl (@ppcompose_left A _ _ g) := !phomotopy_rec_on_idp_refl + -- definition pmap_eq_equiv {X Y : Type*} (f g : X →* Y) : (f = g) ≃ (f ~* g) := + -- begin + -- refine eq_equiv_fn_eq_of_equiv (@pmap.sigma_char X Y) f g ⬝e _, + -- refine !sigma_eq_equiv ⬝e _, + -- refine _ ⬝e (phomotopy.sigma_char f g)⁻¹ᵉ, + -- fapply sigma_equiv_sigma, + -- { esimp, apply eq_equiv_homotopy }, + -- { induction g with g gp, induction Y with Y y0, esimp, intro p, induction p, esimp at *, + -- refine !pathover_idp ⬝e _, refine _ ⬝e !eq_equiv_eq_symm, + -- apply equiv_eq_closed_right, exact !idp_con⁻¹ } + -- end + + definition pmap_eq_idp {X Y : Type*} (f : X →* Y) : + pmap_eq (λx, idpath (f x)) !idp_con⁻¹ = idpath f := + ap (λx, eq_of_phomotopy (phomotopy.mk _ x)) !inv_inv ⬝ eq_of_phomotopy_refl f + + definition pfunext [constructor] (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) := + begin + fapply pequiv_of_equiv, + { fapply equiv.MK: esimp, + { intro f, fapply pmap_eq, + { intro x, exact f x }, + { exact (respect_pt f)⁻¹ }}, + { intro p, fapply pmap.mk, + { intro x, exact ap010 pmap.to_fun p x }, + { note z := apd respect_pt p, + note z2 := square_of_pathover z, + refine eq_of_hdeg_square z2 ⬝ !ap_constant }}, + { intro p, exact sorry }, + { intro p, exact sorry }}, + { apply pmap_eq_idp} + end + end pointed open pointed namespace trunc @@ -586,80 +853,14 @@ namespace group end group open group - -namespace pointed -- move to types.pointed - - -- definition pmap_eq_equiv {X Y : Type*} (f g : X →* Y) : (f = g) ≃ (f ~* g) := - -- begin - -- refine eq_equiv_fn_eq_of_equiv (@pmap.sigma_char X Y) f g ⬝e _, - -- refine !sigma_eq_equiv ⬝e _, - -- refine _ ⬝e (phomotopy.sigma_char f g)⁻¹ᵉ, - -- fapply sigma_equiv_sigma, - -- { esimp, apply eq_equiv_homotopy }, - -- { induction g with g gp, induction Y with Y y0, esimp, intro p, induction p, esimp at *, - -- refine !pathover_idp ⬝e _, refine _ ⬝e !eq_equiv_eq_symm, - -- apply equiv_eq_closed_right, exact !idp_con⁻¹ } - -- end - - definition pmap_eq_idp {X Y : Type*} (f : X →* Y) : - pmap_eq (λx, idpath (f x)) !idp_con⁻¹ = idpath f := - ap (λx, eq_of_phomotopy (phomotopy.mk _ x)) !inv_inv ⬝ eq_of_phomotopy_refl f - - definition pfunext [constructor] (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) := - begin - fapply pequiv_of_equiv, - { fapply equiv.MK: esimp, - { intro f, fapply pmap_eq, - { intro x, exact f x }, - { exact (respect_pt f)⁻¹ }}, - { intro p, fapply pmap.mk, - { intro x, exact ap010 pmap.to_fun p x }, - { note z := apd respect_pt p, - note z2 := square_of_pathover z, - refine eq_of_hdeg_square z2 ⬝ !ap_constant }}, - { intro p, exact sorry }, - { intro p, exact sorry }}, - { apply pmap_eq_idp} - end - -end pointed open pointed - -namespace eq - - infix ` ⬝hty `:75 := homotopy.trans - postfix `⁻¹ʰᵗʸ`:(max+1) := homotopy.symm - - definition hassoc {A B C D : Type} (h : C → D) (g : B → C) (f : A → B) : (h ∘ g) ∘ f ~ h ∘ (g ∘ f) := - λa, idp - - -- to algebra.homotopy_group - definition homotopy_group_homomorphism_pcompose (n : ℕ) [H : is_succ n] {A B C : Type*} (g : B →* C) - (f : A →* B) : π→g[n] (g ∘* f) ~ π→g[n] g ∘ π→g[n] f := - begin - induction H with n, exact to_homotopy (homotopy_group_functor_compose (succ n) g f) - end - - definition apn_pinv (n : ℕ) {A B : Type*} (f : A ≃* B) : - Ω→[n] f⁻¹ᵉ* ~* (loopn_pequiv_loopn n f)⁻¹ᵉ* := - begin - refine !to_pinv_pequiv_MK2⁻¹* - end - - -- definition homotopy_group_homomorphism_pinv (n : ℕ) {A B : Type*} (f : A ≃* B) : - -- π→g[n+1] f⁻¹ᵉ* ~ (homotopy_group_isomorphism_of_pequiv n f)⁻¹ᵍ := - -- begin - -- -- refine ptrunc_functor_phomotopy 0 !apn_pinv ⬝hty _, - -- -- intro x, esimp, - -- end - - -- definition natural_square_tr_eq {A B : Type} {a a' : A} {f g : A → B} - -- (p : f ~ g) (q : a = a') : natural_square p q = square_of_pathover (apd p q) := - -- idp - -end eq open eq - namespace fiber + definition pcompose_ppoint {A B : Type*} (f : A →* B) : f ∘* ppoint f ~* pconst (pfiber f) B := + begin + fapply phomotopy.mk, + { exact point_eq }, + { exact !idp_con⁻¹ } + end definition ap1_ppoint_phomotopy {A B : Type*} (f : A →* B) : Ω→ (ppoint f) ∘* pfiber_loop_space f ~* ppoint (Ω→ f) :=