From 4d39e86f272e551aa8ef543ca94dad249c632ecd Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 28 Nov 2017 08:26:13 +0100 Subject: [PATCH] Mostly formalize the pentagon of the smash product, fix the order of the arguments in the adjunction --- homotopy/pushout.hlean | 76 ++++- homotopy/smash.hlean | 548 ++++++++++++++++++++++----------- homotopy/smash_adjoint.hlean | 580 ++++++++++++++++++++--------------- pointed.hlean | 6 + 4 files changed, 789 insertions(+), 421 deletions(-) diff --git a/homotopy/pushout.hlean b/homotopy/pushout.hlean index fde01fb..0d35477 100644 --- a/homotopy/pushout.hlean +++ b/homotopy/pushout.hlean @@ -1,5 +1,5 @@ -import ..algebra.exactness homotopy.cofiber homotopy.wedge +import ..algebra.exactness homotopy.cofiber homotopy.wedge homotopy.smash open eq function is_trunc sigma prod lift is_equiv equiv pointed sum unit bool cofiber @@ -811,4 +811,78 @@ namespace pushout end + variables {A B : Type*} + open smash + + definition prod_of_wedge [unfold 3] (v : wedge A B) : A × B := + begin + induction v with a b , + { exact (a, pt) }, + { exact (pt, b) }, + { reflexivity } + end + + definition wedge_of_sum [unfold 3] (v : A + B) : wedge A B := + begin + induction v with a b, + { exact pushout.inl a }, + { exact pushout.inr b } + end + + definition prod_of_wedge_of_sum [unfold 3] (v : A + B) : + prod_of_wedge (wedge_of_sum v) = prod_of_sum v := + begin + induction v with a b, + { reflexivity }, + { reflexivity } + end + + definition eq_inl_pushout_wedge_of_sum [unfold 3] (v : wedge A B) : + inl pt = inl v :> pushout wedge_of_sum bool_of_sum := + begin + induction v with a b, + { exact glue (sum.inl pt) ⬝ (glue (sum.inl a))⁻¹, }, + { exact ap inl (glue ⋆) ⬝ glue (sum.inr pt) ⬝ (glue (sum.inr b))⁻¹, }, + { apply eq_pathover_constant_left, + refine !con.right_inv ⬝pv _ ⬝vp !con_inv_cancel_right⁻¹, exact square_of_eq idp } + end + + variables (A B) + definition eq_inr_pushout_wedge_of_sum [unfold 3] (b : bool) : + inl pt = inr b :> pushout (@wedge_of_sum A B) bool_of_sum := + begin + induction b, + { exact glue (sum.inl pt) }, + { exact ap inl (glue ⋆) ⬝ glue (sum.inr pt) } + end + + definition is_contr_pushout_wedge_of_sum : is_contr (pushout (@wedge_of_sum A B) bool_of_sum) := + begin + apply is_contr.mk (pushout.inl pt), + intro x, induction x with v b w, + { apply eq_inl_pushout_wedge_of_sum }, + { apply eq_inr_pushout_wedge_of_sum }, + { apply eq_pathover_constant_left_id_right, + induction w with a b, + { apply whisker_rt, exact vrfl }, + { apply whisker_rt, exact vrfl }} + end + + definition bool_of_sum_of_bool {A B : Type*} (b : bool) : bool_of_sum (sum_of_bool A B b) = b := + by induction b: reflexivity + + /- a different proof, using pushout lemmas, and the fact that the wedge is the pushout of + A + B <-- 2 --> 1 -/ + definition pushout_wedge_of_sum_equiv_unit : pushout (@wedge_of_sum A B) bool_of_sum ≃ unit := + begin + refine pushout_hcompose_equiv (sum_of_bool A B) (wedge_equiv_pushout_sum A B ⬝e !pushout.symm) + _ _ ⬝e _, + exact erfl, + intro x, induction x, + reflexivity, reflexivity, + exact bool_of_sum_of_bool, + apply pushout_of_equiv_right + end + + end pushout diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean index 137b92a..7e3334e 100644 --- a/homotopy/smash.hlean +++ b/homotopy/smash.hlean @@ -9,10 +9,8 @@ open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops w /- To prove: Σ(X ∧ Y) ≃ X ★ Y (?) (notation means suspension, smash, join) -/ - /- To prove: A ∧ S¹ ≃ ΣA -/ - - /- associativity is proven in smash_adjoint -/ -variables {A A' B B' C C' D E F : Type*} + /- associativity and A ∧ S¹ ≃ ΣA is proven in smash_adjoint -/ +variables {A A' A'' B B' B'' C C' D E F : Type*} namespace smash @@ -233,6 +231,8 @@ namespace smash reflexivity end + infixr ` ∧~ `:78 := smash_functor_phomotopy + /- a more explicit proof, if we ever need it -/ -- definition smash_functor_homotopy [unfold 11] {f f' : A →* C} {g g' : B →* D} -- (h₁ : f ~* f') (h₂ : g ~* g') : f ∧→ g ~ f' ∧→ g' := @@ -317,6 +317,17 @@ namespace smash exact !smash_functor_phomotopy_refl⁻¹ end + definition smash_functor_eq_of_phomotopy_left (g : B →* D) {f f' : A →* C} + (p : f ~* f') : ap (λf, smash_functor f g) (eq_of_phomotopy p) = + eq_of_phomotopy (smash_functor_phomotopy p phomotopy.rfl) := + begin + induction p using phomotopy_rec_idp, + refine ap02 _ !eq_of_phomotopy_refl ⬝ _, + refine !eq_of_phomotopy_refl⁻¹ ⬝ _, + apply ap eq_of_phomotopy, + exact !smash_functor_phomotopy_refl⁻¹ + end + /- the functorial action preserves compositions, the interchange law -/ definition smash_functor_pcompose_homotopy [unfold 11] {C D E F : Type} (f' : C → E) (f : A → C) (g' : D → F) (g : B → D) : @@ -348,7 +359,11 @@ namespace smash end definition smash_functor_split (f : A →* C) (g : B →* D) : - f ∧→ g ~* (pid C) ∧→ g ∘* f ∧→ (pid B) := + f ∧→ g ~* f ∧→ pid D ∘* pid A ∧→ g := + smash_functor_phomotopy !pcompose_pid⁻¹* !pid_pcompose⁻¹* ⬝* !smash_functor_pcompose + + definition smash_functor_split_rev (f : A →* C) (g : B →* D) : + f ∧→ g ~* pid C ∧→ g ∘* f ∧→ pid B := smash_functor_phomotopy !pid_pcompose⁻¹* !pcompose_pid⁻¹* ⬝* !smash_functor_pcompose /- An alternative proof which doesn't start by applying inductions, so which is more explicit -/ @@ -429,6 +444,337 @@ namespace smash !smash_functor_pcompose⁻¹* ⬝* smash_functor_phomotopy p q ⬝* !smash_functor_pcompose end + + /- f ∧ g is a pointed equivalence if f and g are -/ + definition smash_functor_using_pushout [unfold 7] (f : A →* C) (g : B →* D) : A ∧ B → C ∧ D := + begin + fapply pushout.functor (sum_functor f g) (prod_functor f g) id, + { intro v, induction v with a b, + exact prod_eq idp (respect_pt g), + exact prod_eq (respect_pt f) idp }, + { intro v, induction v with a b: reflexivity } + end + + definition smash_functor_homotopy_pushout_functor (f : A →* C) (g : B →* D) : + f ∧→ g ~ smash_functor_using_pushout f g := + begin + intro x, induction x, + { reflexivity }, + { reflexivity }, + { reflexivity }, + { apply eq_pathover, refine !elim_gluel ⬝ph _ ⬝hp !pushout.elim_glue⁻¹, + apply hdeg_square, esimp, apply whisker_right, exact !ap_ap011⁻¹ }, + { apply eq_pathover, refine !elim_gluer ⬝ph _ ⬝hp !pushout.elim_glue⁻¹, + apply hdeg_square, esimp, apply whisker_right, exact !ap_ap011⁻¹ } + end + + local attribute is_equiv_sum_functor [instance] + definition smash_pequiv [constructor] (f : A ≃* C) (g : B ≃* D) : A ∧ B ≃* C ∧ D := + begin + fapply pequiv_of_pmap (f ∧→ g), + refine @homotopy_closed _ _ _ _ _ (smash_functor_homotopy_pushout_functor f g)⁻¹ʰᵗʸ, + apply pushout.is_equiv_functor + end + + infixr ` ∧≃ `:80 := smash_pequiv + + + definition smash_pequiv_left [constructor] (B : Type*) (f : A ≃* C) : A ∧ B ≃* C ∧ B := + f ∧≃ pequiv.rfl + + definition smash_pequiv_right [constructor] (A : Type*) (g : B ≃* D) : A ∧ B ≃* A ∧ D := + pequiv.rfl ∧≃ g + + /- f ∧ g is constant if f is constant -/ + definition smash_functor_pconst_left_homotopy [unfold 6] {B' : Type} (f : B → B') (x : A ∧ B) : + (pconst A A' ∧→ pmap_of_map f pt) x = pt := + begin + induction x with a b a b, + { exact gluer' (f b) pt }, + { exact (gluel pt)⁻¹ }, + { exact (gluer pt)⁻¹ᵖ }, + { apply eq_pathover, note x := functor_gluel2 (λx : A, Point A') f a, + refine x ⬝ph _, refine _ ⬝hp !ap_constant⁻¹, apply square_of_eq, + rexact con.right_inv (gluer (f pt)) ⬝ (con.right_inv (gluel pt))⁻¹ }, + { apply eq_pathover, note x := functor_gluer2 (λx : A, Point A') f b, + refine x ⬝ph _, refine _ ⬝hp !ap_constant⁻¹, apply square_of_eq, reflexivity } + end + + definition smash_functor_pconst_left (f : B →* B') : pconst A A' ∧→ f ~* pconst (A ∧ B) (A' ∧ B') := + begin + induction B' with B', induction f with f f₀, esimp at *, induction f₀, + fapply phomotopy.mk, + { exact smash_functor_pconst_left_homotopy f }, + { rexact con.right_inv (gluer (f pt)) } + end + + definition smash_functor_pconst_left_phomotopy {f f' : B →* B'} (p : f ~* f') : + phomotopy.refl (pconst A A') ∧~ p ⬝* smash_functor_pconst_left f' = smash_functor_pconst_left f := + begin + induction p using phomotopy_rec_idp, + exact !smash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans + end + + /- This makes smash_functor into a pointed map (B →* B') →* (A ∧ B →* A ∧ B') -/ + + definition smash_functor_left [constructor] (A A' B : Type*) : + ppmap A A' →* ppmap (A ∧ B) (A' ∧ B) := + pmap.mk (λf, f ∧→ pid B) (eq_of_phomotopy (smash_functor_pconst_left (pid B))) + + /- We want to show that smash_functor_left is natural in A, B and C. + + For this we need two coherence rules. Given the function h := (f' ∘ f) ∧→ (g' ∘ g) and suppose + that either f' or f is constant. There are two ways to show that h is constant: either by using + exchange, or directly. We need to show that these two proofs result in the same pointed + homotopy. First we do the case where f is constant -/ + + private definition my_squarel {A : Type} {a₁ a₂ a₃ : A} (p₁ : a₁ = a₃) (p₂ : a₂ = a₃) : + square (p₁ ⬝ p₂⁻¹) p₂⁻¹ p₁ idp := + proof square_of_eq idp qed + + private definition my_squarer {A : Type} {a₁ a₂ a₃ : A} (p₁ : a₁ = a₃) (p₂ : a₁ = a₂) : + square (p₁ ⬝ p₁⁻¹) p₂⁻¹ p₂ idp := + proof square_of_eq (con.right_inv p₁ ⬝ (con.right_inv p₂)⁻¹) qed + + private definition my_cube_fillerl {A B C : Type} {g : B → C} {f : A → B} {a₁ a₂ : A} {b₀ : B} + {p : f ~ λa, b₀} {q : Πa, g (f a) = g b₀} (r : (λa, ap g (p a)) ~ q) : + cube (hrfl ⬝hp (r a₁)⁻¹) hrfl + (my_squarel (q a₁) (q a₂)) (aps g (my_squarel (p a₁) (p a₂))) + (hrfl ⬝hp (!ap_con ⬝ whisker_left _ !ap_inv ⬝ (r a₁) ◾ (r a₂)⁻²)⁻¹) + (hrfl ⬝hp (r a₂)⁻²⁻¹ ⬝hp !ap_inv⁻¹) := + begin + induction r using homotopy.rec_on_idp, induction p using homotopy.rec_on_idp_left, exact idc + end + + private definition my_cube_fillerr {B C : Type} {g : B → C} {b₀ bl br : B} + {pl : b₀ = bl} {pr : b₀ = br} {ql : g b₀ = g bl} {qr : g b₀ = g br} + (sl : ap g pl = ql) (sr : ap g pr = qr) : + cube (hrfl ⬝hp sr⁻¹) hrfl + (my_squarer ql qr) (aps g (my_squarer pl pr)) + (hrfl ⬝hp (!ap_con ⬝ whisker_left _ !ap_inv ⬝ sl ◾ sl⁻²)⁻¹) + (hrfl ⬝hp sr⁻²⁻¹ ⬝hp !ap_inv⁻¹) := + begin + induction sr, induction sl, induction pr, induction pl, exact idc + end + + definition smash_functor_pcompose_pconst2_homotopy {A A' A'' B B' B'' : Type} + (a₀ : A) (b₀ : B) (a₀' : A') (f' : A' → A'') (g' : B' → B'') (g : B → B') + (x : pointed.MK A a₀ ∧ pointed.MK B b₀) : + square (smash_functor_pcompose_homotopy f' (λ a, a₀') g' g x) + idp + (smash_functor_pconst_left_homotopy (λ a, g' (g a)) x) + (ap (smash_functor' (pmap.mk f' (refl (f' a₀'))) (pmap.mk g' (refl (g' (g b₀))))) + (smash_functor_pconst_left_homotopy g x)) := + begin + induction x with a b a b, + { refine _ ⬝hp (functor_gluer'2 f' g' (g b) (g b₀))⁻¹, exact hrfl }, + { refine _ ⬝hp !ap_inv⁻¹, refine _ ⬝hp !functor_gluel2⁻²⁻¹, exact hrfl }, + { refine _ ⬝hp !ap_inv⁻¹, refine _ ⬝hp !functor_gluer2⁻²⁻¹, exact hrfl }, + { exact abstract begin apply square_pathover, + refine !rec_eq_gluel ⬝p1 _ ⬝1p !natural_square_refl⁻¹, + refine !rec_eq_gluel ⬝p2 _ ⬝2p !natural_square_ap_fn⁻¹, + apply whisker001, apply whisker021, + apply move201, refine _ ⬝1p !eq_hconcat_hdeg_square⁻¹, + apply move221, refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹, + refine ap (hconcat_eq _) !ap_inv ⬝p1 _ ⬝2p (ap (aps _) !rec_eq_gluel ⬝ !aps_eq_hconcat)⁻¹, + apply whisker021, refine _ ⬝2p !aps_hconcat_eq⁻¹, apply move221, + refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹, + refine _ ⬝1p ap hdeg_square (eq_bot_of_square (transpose !ap02_ap_constant)), + apply my_cube_fillerr end end }, + { exact abstract begin apply square_pathover, + refine !rec_eq_gluer ⬝p1 _ ⬝1p !natural_square_refl⁻¹, + refine !rec_eq_gluer ⬝p2 _ ⬝2p !natural_square_ap_fn⁻¹, + apply whisker001, apply whisker021, + apply move201, refine _ ⬝1p !eq_hconcat_hdeg_square⁻¹, + apply move221, refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹, + refine ap (hconcat_eq _) !ap_inv ⬝p1 _ ⬝2p (ap (aps _) !rec_eq_gluer ⬝ !aps_eq_hconcat)⁻¹, + apply whisker021, refine _ ⬝2p !aps_hconcat_eq⁻¹, apply move221, + refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹, + refine _ ⬝1p ap hdeg_square (eq_bot_of_square (transpose !ap02_ap_constant)), + apply my_cube_fillerl end end } + end + + definition smash_functor_pcompose_pconst2 (f' : A' →* A'') (g' : B' →* B'') (g : B →* B') : + phsquare (smash_functor_pcompose f' (pconst A A') g' g) + (smash_functor_pconst_left (g' ∘* g)) + (smash_functor_phomotopy (pcompose_pconst f') phomotopy.rfl) + (pwhisker_left (f' ∧→ g') (smash_functor_pconst_left g) ⬝* + pcompose_pconst (f' ∧→ g')) := + begin + induction A with A a₀, induction B with B b₀, + induction A' with A' a₀', induction B' with B' b₀', + induction A'' with A'' a₀'', induction B'' with B'' b₀'', + induction f' with f' f'₀, induction g' with g' g₀', induction g with g g₀, + esimp at *, induction f'₀, induction g₀', induction g₀, + refine !smash_functor_phomotopy_refl ⬝ph** _, refine _ ⬝ !refl_trans⁻¹, + fapply phomotopy_eq, + { intro x, refine eq_of_square _ ⬝ !con_idp, + exact smash_functor_pcompose_pconst2_homotopy a₀ b₀ a₀' f' g' g x }, + { refine _ ⬝ !idp_con⁻¹, + refine whisker_right _ (!whisker_right_idp ⬝ !eq_of_square_hrfl_hconcat_eq) ⬝ _, + refine !con.assoc ⬝ _, apply con_eq_of_eq_inv_con, + refine whisker_right _ _ ⬝ _, rotate 1, rexact functor_gluer'2_same f' g' (g b₀), + refine !inv_con_cancel_right ⬝ _, + exact sorry, -- TODO: FIX, the proof below should work (with some small changes) + -- refine _ ⬝ whisker_left _ _, + -- rotate 2, refine ap (whisker_left _) _, symmetry, exact !idp_con ⬝ !idp_con ⬝ !whisker_right_idp ⬝ !idp_con, + -- symmetry, apply whisker_left_idp + } + end + + /- a version where the left maps are identities -/ + definition smash_functor_pcompose_pconst2_pid (f' : A' →* A'') : + phsquare (smash_functor_pcompose_pid B f' (pconst A A')) + (smash_functor_pconst_left (pid B)) + (pcompose_pconst f' ∧~ phomotopy.rfl) + (pwhisker_left (f' ∧→ pid B) (smash_functor_pconst_left (pid B)) ⬝* + pcompose_pconst (f' ∧→ pid B)) := + (!smash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans) ⬝pv** + smash_functor_pcompose_pconst2 f' (pid B) (pid B) + + /- a small rewrite of the previous -/ + -- definition smash_functor_pcompose_pid_pconst' (f' : A' →* A'') : + -- pwhisker_left (f' ∧→ pid B) (smash_functor_pconst_left (pid B)) ⬝* + -- pcompose_pconst (f' ∧→ pid B) = + -- (smash_functor_pcompose_pid B f' (pconst A A'))⁻¹* ⬝* + -- (pcompose_pconst f' ∧~ phomotopy.rfl ⬝* + -- smash_functor_pconst_left (pid B)) := + -- begin + -- apply eq_symm_trans_of_trans_eq, + -- exact smash_functor_pcompose_pid_pconst f' + -- end + + /- if f' is constant -/ + definition smash_functor_pcompose_pconst1_homotopy [unfold 13] {A A' A'' B B' B'' : Type} + (a₀ : A) (b₀ : B) (a₀'' : A'') (f : A → A') (g' : B' → B'') (g : B → B') + (x : pointed.MK A a₀ ∧ pointed.MK B b₀) : + square (smash_functor_pcompose_homotopy (λa', a₀'') f g' g x) + idp + (smash_functor_pconst_left_homotopy (λ a, g' (g a)) x) + (smash_functor_pconst_left_homotopy g' + ((pmap_of_map f a₀ ∧→ pmap_of_map g b₀) x)) := + begin + induction x with a b a b, + { exact hrfl }, + { exact hrfl }, + { exact hrfl }, + { exact abstract begin apply square_pathover, + refine !rec_eq_gluel ⬝p1 _ ⬝1p !natural_square_refl⁻¹, + refine !rec_eq_gluel ⬝p2 _ ⬝2p + (natural_square_compose (smash_functor_pconst_left_homotopy g') _ _)⁻¹ᵖ, + apply whisker001, apply whisker021, + apply move201, refine _ ⬝1p !eq_hconcat_hdeg_square⁻¹, + apply move221, refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹, + refine ap (hconcat_eq _) !ap_inv ⬝p1 _ ⬝2p (natural_square_eq2 _ !functor_gluel2)⁻¹ᵖ, + apply whisker021, + refine _ ⬝1p ap hdeg_square (eq_of_square (!ap_constant_compose⁻¹ʰ) ⬝ !idp_con)⁻¹, + apply move221, refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹, + refine _ ⬝2p !rec_eq_gluel⁻¹, apply whisker021, + apply move221, refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹, + refine _ ⬝1p ap hdeg_square (eq_bot_of_square (transpose !ap02_constant)), + exact rfl2 end end }, + { exact abstract begin apply square_pathover, + refine !rec_eq_gluer ⬝p1 _ ⬝1p !natural_square_refl⁻¹, + refine !rec_eq_gluer ⬝p2 _ ⬝2p + (natural_square_compose (smash_functor_pconst_left_homotopy g') _ _)⁻¹ᵖ, + apply whisker001, apply whisker021, + apply move201, refine _ ⬝1p !eq_hconcat_hdeg_square⁻¹, + apply move221, refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹, + refine ap (hconcat_eq _) !ap_inv ⬝p1 _ ⬝2p (natural_square_eq2 _ !functor_gluer2)⁻¹ᵖ, + apply whisker021, + refine _ ⬝1p ap hdeg_square (eq_of_square (!ap_constant_compose⁻¹ʰ) ⬝ !idp_con)⁻¹, + apply move221, refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹, + refine _ ⬝2p !rec_eq_gluer⁻¹, apply whisker021, + apply move221, refine _ ⬝1p !hdeg_square_hconcat_eq⁻¹, + refine _ ⬝1p ap hdeg_square (eq_bot_of_square (transpose !ap02_constant)), + exact rfl2 end end }, + end + + definition smash_functor_pcompose_pconst1 (f : A →* A') (g' : B' →* B'') (g : B →* B') : + phsquare (smash_functor_pcompose (pconst A' A'') f g' g) + (smash_functor_pconst_left (g' ∘* g)) + (pconst_pcompose f ∧~ phomotopy.rfl) + (pwhisker_right (f ∧→ g) (smash_functor_pconst_left g') ⬝* + pconst_pcompose (f ∧→ g)) := + begin + induction A with A a₀, induction B with B b₀, + induction A' with A' a₀', induction B' with B' b₀', + induction A'' with A'' a₀'', induction B'' with B'' b₀'', + induction f with f f₀, induction g' with g' g₀', induction g with g g₀, + esimp at *, induction f₀, induction g₀', induction g₀, + refine !smash_functor_phomotopy_refl ⬝ph** _, refine _ ⬝ !refl_trans⁻¹, + fapply phomotopy_eq, + { intro x, refine eq_of_square (smash_functor_pcompose_pconst1_homotopy a₀ b₀ a₀'' f g' g x) }, + { refine whisker_right _ (!whisker_right_idp ⬝ !eq_of_square_hrfl) ⬝ _, + have H : Π{A : Type} {a a' : A} (p : a = a'), + idp_con (p ⬝ p⁻¹) ⬝ con.right_inv p = idp ⬝ + whisker_left idp (idp ⬝ (idp ⬝ proof whisker_right idp (idp_con (p ⬝ p⁻¹ᵖ))⁻¹ᵖ qed ⬝ + whisker_left idp (con.right_inv p))), by intros; induction p; reflexivity, + rexact H (gluer (g' (g b₀))) } + end + + /- a version where the left maps are identities -/ + definition smash_functor_pcompose_pconst1_pid (f : A →* A') : + phsquare (smash_functor_pcompose_pid B (pconst A' A'') f) + (smash_functor_pconst_left (pid B)) + (pconst_pcompose f ∧~ phomotopy.rfl) + (pwhisker_right (f ∧→ pid B) (smash_functor_pconst_left (pid B)) ⬝* + pconst_pcompose (f ∧→ pid B)) := + (!smash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans) ⬝pv** + smash_functor_pcompose_pconst1 f (pid B) (pid B) + + /- Using these lemmas we show that smash_functor_left is natural in all arguments -/ + + definition smash_functor_left_natural_left (f : A' →* A) : + psquare (smash_functor_left A B C) (smash_functor_left A' B C) + (ppcompose_right f) (ppcompose_right (f ∧→ pid C)) := + begin + refine _⁻¹*, + fapply phomotopy_mk_ppmap, + { intro g, exact smash_functor_pcompose_pid C g f }, + { refine idp ◾** (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_right_eq_of_phomotopy ⬝ + !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy) ⬝ _ , + refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !smash_functor_eq_of_phomotopy_left ⬝ + !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹, + apply smash_functor_pcompose_pconst1_pid } + end + + definition smash_functor_left_natural_middle (f : B →* B') : + psquare (smash_functor_left A B C) (smash_functor_left A B' C) + (ppcompose_left f) (ppcompose_left (f ∧→ pid C)) := + begin + refine _⁻¹*, + fapply phomotopy_mk_ppmap, + { exact smash_functor_pcompose_pid C f }, + { refine idp ◾** (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_left_eq_of_phomotopy ⬝ + !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy) ⬝ _ , + refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !smash_functor_eq_of_phomotopy_left ⬝ + !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹, + apply smash_functor_pcompose_pconst2_pid } + end + + definition smash_functor_left_natural_right (f : C →* C') : + psquare (smash_functor_left A B C) (ppcompose_right (pid A ∧→ f)) + (smash_functor_left A B C') (ppcompose_left (pid B ∧→ f)) := + begin + refine _⁻¹*, + fapply phomotopy_mk_ppmap, + { intro g, exact smash_functor_psquare proof phomotopy.rfl qed proof phomotopy.rfl qed }, + { esimp, + refine idp ◾** (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_left_eq_of_phomotopy ⬝ + !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy) ⬝ _ , + refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_right_eq_of_phomotopy ⬝ + !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹, + apply eq_of_phsquare, + refine (phmove_bot_of_left _ !smash_functor_pcompose_pconst1⁻¹ʰ**) ⬝h** + (!smash_functor_phomotopy_refl ⬝pv** !phhrfl) ⬝h** !smash_functor_pcompose_pconst2 ⬝vp** _, + refine !trans_assoc ⬝ !trans_assoc ⬝ idp ◾** _ ⬝ !trans_refl, + refine idp ◾** !refl_trans ⬝ !trans_left_inv } + end + + + /- the following is not really used, but a symmetric version of the natural equivalence + smash_functor_left -/ /- f ∧ g is constant if g is constant -/ definition smash_functor_pconst_right_homotopy [unfold 6] {C : Type} (f : A → C) (x : A ∧ B) : (pmap_of_map f pt ∧→ pconst B D) x = pt := @@ -474,36 +820,7 @@ namespace smash exchange, or directly. We need to show that these two proofs result in the same pointed homotopy. First we do the case where g is constant -/ - private definition my_squarel {A : Type} {a₁ a₂ a₃ : A} (p₁ : a₁ = a₃) (p₂ : a₂ = a₃) : - square (p₁ ⬝ p₂⁻¹) p₂⁻¹ p₁ idp := - proof square_of_eq idp qed - - private definition my_squarer {A : Type} {a₁ a₂ a₃ : A} (p₁ : a₁ = a₃) (p₂ : a₁ = a₂) : - square (p₁ ⬝ p₁⁻¹) p₂⁻¹ p₂ idp := - proof square_of_eq (con.right_inv p₁ ⬝ (con.right_inv p₂)⁻¹) qed - - private definition my_cube_fillerl {A B C : Type} {g : B → C} {f : A → B} {a₁ a₂ : A} {b₀ : B} - {p : f ~ λa, b₀} {q : Πa, g (f a) = g b₀} (r : (λa, ap g (p a)) ~ q) : - cube (hrfl ⬝hp (r a₁)⁻¹) hrfl - (my_squarel (q a₁) (q a₂)) (aps g (my_squarel (p a₁) (p a₂))) - (hrfl ⬝hp (!ap_con ⬝ whisker_left _ !ap_inv ⬝ (r a₁) ◾ (r a₂)⁻²)⁻¹) - (hrfl ⬝hp (r a₂)⁻²⁻¹ ⬝hp !ap_inv⁻¹) := - begin - induction r using homotopy.rec_on_idp, induction p using homotopy.rec_on_idp_left, exact idc - end - - private definition my_cube_fillerr {B C : Type} {g : B → C} {b₀ bl br : B} - {pl : b₀ = bl} {pr : b₀ = br} {ql : g b₀ = g bl} {qr : g b₀ = g br} - (sl : ap g pl = ql) (sr : ap g pr = qr) : - cube (hrfl ⬝hp sr⁻¹) hrfl - (my_squarer ql qr) (aps g (my_squarer pl pr)) - (hrfl ⬝hp (!ap_con ⬝ whisker_left _ !ap_inv ⬝ sl ◾ sl⁻²)⁻¹) - (hrfl ⬝hp sr⁻²⁻¹ ⬝hp !ap_inv⁻¹) := - begin - induction sr, induction sl, induction pr, induction pl, exact idc - end - - definition smash_functor_pcompose_pconst_homotopy {A B C D E F : Type} + definition smash_functor_pcompose_pconst4_homotopy {A B C D E F : Type} (a₀ : A) (b₀ : B) (d₀ : D) (f' : C → E) (f : A → C) (g : D → F) (x : pointed.MK A a₀ ∧ pointed.MK B b₀) : square (smash_functor_pcompose_homotopy f' f g (λ a, d₀) x) @@ -540,7 +857,7 @@ namespace smash apply my_cube_fillerr end end } end - definition smash_functor_pcompose_pconst (f' : C →* E) (f : A →* C) (g : D →* F) : + definition smash_functor_pcompose_pconst4 (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)) @@ -554,7 +871,7 @@ namespace smash refine !smash_functor_phomotopy_refl ⬝ph** _, refine _ ⬝ !refl_trans⁻¹, fapply phomotopy_eq, { intro x, refine eq_of_square _ ⬝ !con_idp, - exact smash_functor_pcompose_pconst_homotopy a₀ b₀ d₀ f' f g x, }, + exact smash_functor_pcompose_pconst4_homotopy a₀ b₀ d₀ f' f g x, }, { refine _ ⬝ !idp_con⁻¹, refine whisker_right _ (!whisker_right_idp ⬝ !eq_of_square_hrfl_hconcat_eq) ⬝ _, refine !con.assoc ⬝ _, apply con_eq_of_eq_inv_con, @@ -568,29 +885,29 @@ namespace smash end /- a version where the left maps are identities -/ - definition smash_functor_pid_pcompose_pconst (g : D →* F) : + definition smash_functor_pcompose_pconst4_pid (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 (pid A ∧→ g) (smash_functor_pconst_right (pid A)) ⬝* pcompose_pconst (pid A ∧→ g)) := (!smash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans) ⬝pv** - smash_functor_pcompose_pconst (pid A) (pid A) g + smash_functor_pcompose_pconst4 (pid A) (pid A) g /- a small rewrite of the previous -/ - definition smash_functor_pid_pcompose_pconst' (g : D →* F) : - pwhisker_left (pid A ∧→ g) (smash_functor_pconst_right (pid A)) ⬝* - pcompose_pconst (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_pid_pcompose_pconst g - end + -- definition smash_functor_pid_pcompose_pconst' (g : D →* F) : + -- pwhisker_left (pid A ∧→ g) (smash_functor_pconst_right (pid A)) ⬝* + -- pcompose_pconst (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_pid_pcompose_pconst g + -- end /- if g' is constant -/ - definition smash_functor_pconst_pcompose_homotopy [unfold 13] {A B C D E F : Type} + definition smash_functor_pcompose_pconst3_homotopy [unfold 13] {A B C D E F : Type} (a₀ : A) (b₀ : B) (x₀ : F) (f' : C → E) (f : A → C) (g : B → D) (x : pointed.MK A a₀ ∧ pointed.MK B b₀) : square (smash_functor_pcompose_homotopy f' f (λ a, x₀) g x) @@ -635,7 +952,7 @@ namespace smash exact rfl2 end end }, end - definition smash_functor_pconst_pcompose (f' : C →* E) (f : A →* C) (g : B →* D) : + definition smash_functor_pcompose_pconst3 (f' : C →* E) (f : A →* C) (g : B →* D) : phsquare (smash_functor_pcompose f' f (pconst D F) g) (smash_functor_pconst_right (f' ∘* f)) (smash_functor_phomotopy phomotopy.rfl (pconst_pcompose g)) @@ -648,7 +965,7 @@ namespace smash esimp at *, induction f'₀, induction f₀, induction g₀, refine !smash_functor_phomotopy_refl ⬝ph** _, refine _ ⬝ !refl_trans⁻¹, fapply phomotopy_eq, - { intro x, refine eq_of_square (smash_functor_pconst_pcompose_homotopy a₀ b₀ x₀ f' f g x) }, + { intro x, refine eq_of_square (smash_functor_pcompose_pconst3_homotopy a₀ b₀ x₀ f' f g x) }, { refine whisker_right _ (!whisker_right_idp ⬝ !eq_of_square_hrfl) ⬝ _, have H : Π{A : Type} {a a' : A} (p : a = a'), idp_con (p ⬝ p⁻¹) ⬝ con.right_inv p = idp ⬝ @@ -658,14 +975,14 @@ namespace smash end /- a version where the left maps are identities -/ - definition smash_functor_pid_pconst_pcompose (g : B →* D) : + definition smash_functor_pcompose_pconst3_pid (g : B →* D) : phsquare (smash_functor_pid_pcompose A (pconst D F) g) (smash_functor_pconst_right (pid A)) (smash_functor_phomotopy phomotopy.rfl (pconst_pcompose g)) (pwhisker_right (pid A ∧→ g) (smash_functor_pconst_right (pid A)) ⬝* pconst_pcompose (pid A ∧→ g)) := (!smash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans) ⬝pv** - smash_functor_pconst_pcompose (pid A) (pid A) g + smash_functor_pcompose_pconst3 (pid A) (pid A) g /- Using these lemmas we show that smash_functor_right is natural in all arguments -/ definition smash_functor_right_natural_right (f : C →* C') : @@ -679,7 +996,7 @@ namespace smash !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy) ⬝ _ , refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !smash_functor_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹, - apply smash_functor_pid_pcompose_pconst } + apply smash_functor_pcompose_pconst4_pid } end definition smash_functor_right_natural_middle (f : B' →* B) : @@ -693,7 +1010,7 @@ namespace smash !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy) ⬝ _ , refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !smash_functor_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹, - apply smash_functor_pid_pconst_pcompose } + apply smash_functor_pcompose_pconst3_pid } end definition smash_functor_right_natural_left (f : A →* A') : @@ -709,129 +1026,16 @@ namespace smash refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_right_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹, apply eq_of_phsquare, - refine (phmove_bot_of_left _ !smash_functor_pconst_pcompose⁻¹ʰ**) ⬝h** - (!smash_functor_phomotopy_refl ⬝pv** !phhrfl) ⬝h** !smash_functor_pcompose_pconst ⬝vp** _, + refine (phmove_bot_of_left _ !smash_functor_pcompose_pconst3⁻¹ʰ**) ⬝h** + (!smash_functor_phomotopy_refl ⬝pv** !phhrfl) ⬝h** !smash_functor_pcompose_pconst4 ⬝vp** _, refine !trans_assoc ⬝ !trans_assoc ⬝ idp ◾** _ ⬝ !trans_refl, refine idp ◾** !refl_trans ⬝ !trans_left_inv } end - /- f ∧ g is a pointed equivalence if f and g are -/ - definition smash_functor_using_pushout [unfold 7] (f : A →* C) (g : B →* D) : A ∧ B → C ∧ D := - begin - fapply pushout.functor (sum_functor f g) (prod_functor f g) id, - { intro v, induction v with a b, - exact prod_eq idp (respect_pt g), - exact prod_eq (respect_pt f) idp }, - { intro v, induction v with a b: reflexivity } - end - - definition smash_functor_homotopy_pushout_functor (f : A →* C) (g : B →* D) : - f ∧→ g ~ smash_functor_using_pushout f g := - begin - intro x, induction x, - { reflexivity }, - { reflexivity }, - { reflexivity }, - { apply eq_pathover, refine !elim_gluel ⬝ph _ ⬝hp !pushout.elim_glue⁻¹, - apply hdeg_square, esimp, apply whisker_right, exact !ap_ap011⁻¹ }, - { apply eq_pathover, refine !elim_gluer ⬝ph _ ⬝hp !pushout.elim_glue⁻¹, - apply hdeg_square, esimp, apply whisker_right, exact !ap_ap011⁻¹ } - end - - local attribute is_equiv_sum_functor [instance] - definition smash_pequiv [constructor] (f : A ≃* C) (g : B ≃* D) : A ∧ B ≃* C ∧ D := - begin - fapply pequiv_of_pmap (f ∧→ g), - refine @homotopy_closed _ _ _ _ _ (smash_functor_homotopy_pushout_functor f g)⁻¹ʰᵗʸ, - apply pushout.is_equiv_functor - end - - definition smash_pequiv_left [constructor] (B : Type*) (f : A ≃* C) : A ∧ B ≃* C ∧ B := - smash_pequiv f pequiv.rfl - - definition smash_pequiv_right [constructor] (A : Type*) (g : B ≃* D) : A ∧ B ≃* A ∧ D := - smash_pequiv pequiv.rfl g - /- A ∧ B ≃* pcofiber (pprod_of_wedge A B) -/ - definition prod_of_wedge [unfold 3] (v : wedge A B) : A × B := - begin - induction v with a b , - { exact (a, pt) }, - { exact (pt, b) }, - { reflexivity } - end - - definition wedge_of_sum [unfold 3] (v : A + B) : wedge A B := - begin - induction v with a b, - { exact pushout.inl a }, - { exact pushout.inr b } - end - - definition prod_of_wedge_of_sum [unfold 3] (v : A + B) : prod_of_wedge (wedge_of_sum v) = prod_of_sum v := - begin - induction v with a b, - { reflexivity }, - { reflexivity } - end - -end smash open smash - -namespace pushout - - definition eq_inl_pushout_wedge_of_sum [unfold 3] (v : wedge A B) : - inl pt = inl v :> pushout wedge_of_sum bool_of_sum := - begin - induction v with a b, - { exact glue (sum.inl pt) ⬝ (glue (sum.inl a))⁻¹, }, - { exact ap inl (glue ⋆) ⬝ glue (sum.inr pt) ⬝ (glue (sum.inr b))⁻¹, }, - { apply eq_pathover_constant_left, - refine !con.right_inv ⬝pv _ ⬝vp !con_inv_cancel_right⁻¹, exact square_of_eq idp } - end - - variables (A B) - definition eq_inr_pushout_wedge_of_sum [unfold 3] (b : bool) : - inl pt = inr b :> pushout (@wedge_of_sum A B) bool_of_sum := - begin - induction b, - { exact glue (sum.inl pt) }, - { exact ap inl (glue ⋆) ⬝ glue (sum.inr pt) } - end - - definition is_contr_pushout_wedge_of_sum : is_contr (pushout (@wedge_of_sum A B) bool_of_sum) := - begin - apply is_contr.mk (pushout.inl pt), - intro x, induction x with v b w, - { apply eq_inl_pushout_wedge_of_sum }, - { apply eq_inr_pushout_wedge_of_sum }, - { apply eq_pathover_constant_left_id_right, - induction w with a b, - { apply whisker_rt, exact vrfl }, - { apply whisker_rt, exact vrfl }} - end - - definition bool_of_sum_of_bool {A B : Type*} (b : bool) : bool_of_sum (sum_of_bool A B b) = b := - by induction b: reflexivity - - /- a different proof, using pushout lemmas, and the fact that the wedge is the pushout of - A + B <-- 2 --> 1 -/ - definition pushout_wedge_of_sum_equiv_unit : pushout (@wedge_of_sum A B) bool_of_sum ≃ unit := - begin - refine pushout_hcompose_equiv (sum_of_bool A B) (wedge_equiv_pushout_sum A B ⬝e !pushout.symm) - _ _ ⬝e _, - exact erfl, - intro x, induction x, - reflexivity, reflexivity, - exact bool_of_sum_of_bool, - apply pushout_of_equiv_right - end - -end pushout open pushout - -namespace smash - variables (A B) + open pushout definition smash_equiv_cofiber : smash A B ≃ cofiber (@prod_of_wedge A B) := begin diff --git a/homotopy/smash_adjoint.hlean b/homotopy/smash_adjoint.hlean index c910498..8bd2d9d 100644 --- a/homotopy/smash_adjoint.hlean +++ b/homotopy/smash_adjoint.hlean @@ -1,8 +1,8 @@ -- Authors: Floris van Doorn --- in collaboration with Egbert, Stefano, Robin, Ulrik +-- 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 +import .smash .susp ..pointed ..move_to_lib ..pyoneda open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc function unit sigma susp sphere @@ -12,62 +12,59 @@ namespace smash variables {A A' B B' C C' X X' : Type*} /- we start by defining the unit of the adjunction -/ - definition pinl [constructor] (A : Type*) {B : Type*} (b : B) : A →* A ∧ B := + definition pinr [constructor] {A : Type*} (B : Type*) (a : A) : B →* A ∧ B := begin fapply pmap.mk, - { intro a, exact smash.mk a b }, - { exact gluer' b pt } + { intro b, exact smash.mk a b }, + { exact gluel' a pt } end - definition pinl_phomotopy {b b' : B} (p : b = b') : pinl A b ~* pinl A b' := + definition pinr_phomotopy {a a' : A} (p : a = a') : pinr B a ~* pinr B a' := begin fapply phomotopy.mk, - { exact ap010 (pmap.to_fun ∘ pinl A) p }, + { exact ap010 (pmap.to_fun ∘ pinr B) p }, { induction p, apply idp_con } end definition smash_pmap_unit_pt [constructor] (A B : Type*) - : pinl A pt ~* pconst A (A ∧ B) := + : pinr B pt ~* pconst B (A ∧ B) := begin fapply phomotopy.mk, - { intro a, exact gluel' a pt }, - { rexact con.right_inv (gluel pt) ⬝ (con.right_inv (gluer pt))⁻¹ } + { intro b, exact gluer' b pt }, + { rexact con.right_inv (gluer pt) ⬝ (con.right_inv (gluel pt))⁻¹ } end - /- We chose an unfortunate order of arguments, but it might be bothersome to change it-/ - definition smash_pmap_unit [constructor] (A B : Type*) : B →* ppmap A (A ∧ B) := + definition smash_pmap_unit [constructor] (A B : Type*) : A →* ppmap B (A ∧ B) := begin fapply pmap.mk, - { exact pinl A }, + { exact pinr B }, { apply eq_of_phomotopy, exact smash_pmap_unit_pt A B } end - /- The unit is natural in the second argument -/ - definition smash_functor_pid_pinl' [constructor] {A B C : Type*} (b : B) (f : B →* C) : - pinl A (f b) ~* smash_functor (pid A) f ∘* pinl A b := + /- The unit is natural in the first argument -/ + definition smash_functor_pid_pinr' [constructor] (B : Type*) (f : A →* A') (a : A) : + pinr B (f a) ~* smash_functor f (pid B) ∘* pinr B a := begin fapply phomotopy.mk, - { intro a, reflexivity }, + { intro b, reflexivity }, { refine !idp_con ⬝ _, - induction C with C c₀, induction f with f f₀, esimp at *, - induction f₀, rexact functor_gluer'2 (@id A) f b pt } + induction A' with A' a₀', induction f with f f₀, esimp at *, + induction f₀, rexact functor_gluel'2 f (@id B) a pt } end - definition smash_pmap_unit_pt_natural [constructor] (f : B →* C) : - smash_functor_pid_pinl' pt f ⬝* - pwhisker_left (smash_functor (pid A) f) (smash_pmap_unit_pt A B) ⬝* - pcompose_pconst (smash_functor (pid A) f) = - pinl_phomotopy (respect_pt f) ⬝* smash_pmap_unit_pt A C := + definition smash_pmap_unit_pt_natural [constructor] (B : Type*) (f : A →* A') : + smash_functor_pid_pinr' B f pt ⬝* pwhisker_left (smash_functor f (pid B)) (smash_pmap_unit_pt A B) ⬝* + pcompose_pconst (f ∧→ (pid B)) = pinr_phomotopy (respect_pt f) ⬝* smash_pmap_unit_pt A' B := begin - induction f with f f₀, induction C with C c₀, esimp at *, + induction f with f f₀, induction A' with A' a₀', esimp at *, induction f₀, refine _ ⬝ !refl_trans⁻¹, refine !trans_refl ⬝ _, fapply phomotopy_eq', - { intro a, refine !idp_con ⬝ _, - rexact functor_gluel'2 (pid A) f a pt }, + { intro b, refine !idp_con ⬝ _, + rexact functor_gluer'2 f (pid B) b pt }, { refine whisker_right_idp _ ⬝ph _, refine ap (λx, _ ⬝ x) _ ⬝ph _, - rotate 1, rexact (functor_gluel'2_same (pid A) f pt), + rotate 1, rexact (functor_gluer'2_same f (pid B) pt), refine whisker_right _ !idp_con ⬝pv _, refine !con.assoc⁻¹ ⬝ph _, apply whisker_bl, refine whisker_left _ !to_homotopy_pt_mk ⬝pv _, @@ -80,16 +77,16 @@ namespace smash apply whisker_tl, apply vdeg_square, refine whisker_right _ !ap_inv ⬝ _, apply inv_con_eq_of_eq_con, - rexact functor_gluer'2_same (pmap_of_map id (Point A)) (pmap_of_map f pt) pt } + rexact functor_gluel'2_same (pmap_of_map f pt) (pmap_of_map id (Point B)) pt } end - definition smash_pmap_unit_natural (f : B →* C) : - smash_pmap_unit A C ∘* f ~* - ppcompose_left (smash_functor (pid A) f) ∘* smash_pmap_unit A B := + definition smash_pmap_unit_natural (B : Type*) (f : A →* A') : + psquare (smash_pmap_unit A B) (smash_pmap_unit A' B) f (ppcompose_left (f ∧→ pid B)) := begin - induction A with A a₀, induction B with B b₀, induction C with C c₀, + apply ptranspose, + induction A with A a₀, induction B with B b₀, induction A' with A' a₀', induction f with f f₀, esimp at *, induction f₀, fapply phomotopy_mk_ppmap, - { esimp [pcompose], intro b, exact smash_functor_pid_pinl' b (pmap_of_map f b₀) }, + { intro a, exact smash_functor_pid_pinr' _ (pmap_of_map f a₀) a }, { refine ap (λx, _ ⬝* phomotopy_of_eq x) !respect_pt_pcompose ⬝ _ ⬝ ap phomotopy_of_eq !respect_pt_pcompose⁻¹, esimp, refine _ ⬝ ap phomotopy_of_eq !idp_con⁻¹, @@ -97,23 +94,26 @@ namespace smash refine ap (λx, _ ⬝* phomotopy_of_eq (x ⬝ _)) !pcompose_left_eq_of_phomotopy ⬝ _, refine ap (λx, _ ⬝* x) (!phomotopy_of_eq_con ⬝ !phomotopy_of_eq_of_phomotopy ◾** !phomotopy_of_eq_of_phomotopy ⬝ !trans_refl) ⬝ _, - refine _ ⬝ smash_pmap_unit_pt_natural (pmap_of_map f b₀) ⬝ _, + refine _ ⬝ smash_pmap_unit_pt_natural _ (pmap_of_map f a₀) ⬝ _, { exact !trans_refl⁻¹ }, { exact !refl_trans }} end + /- The unit is also dinatural in the first argument, but that's easier to prove after the adjunction. + We don't need it for the adjunction -/ + /- The counit -/ - definition smash_pmap_counit_map [unfold 3] (af : A ∧ (ppmap A B)) : B := + definition smash_pmap_counit_map [unfold 3] (fb : ppmap B C ∧ B) : C := begin - induction af with a f a f, - { exact f a }, + induction fb with f b f b, + { exact f b }, { exact pt }, { exact pt }, - { reflexivity }, - { exact respect_pt f } + { exact respect_pt f }, + { reflexivity } end - definition smash_pmap_counit [constructor] (A B : Type*) : A ∧ (ppmap A B) →* B := + definition smash_pmap_counit [constructor] (B C : Type*) : ppmap B C ∧ B →* C := begin fapply pmap.mk, { exact smash_pmap_counit_map }, @@ -121,35 +121,35 @@ namespace smash end /- The counit is natural in both arguments -/ - definition smash_pmap_counit_natural_right (g : B →* C) : g ∘* smash_pmap_counit A B ~* - smash_pmap_counit A C ∘* smash_functor (pid A) (ppcompose_left g) := + definition smash_pmap_counit_natural_right (B : Type*) (g : C →* C') : + psquare (smash_pmap_counit B C) (smash_pmap_counit B C') (ppcompose_left g ∧→ pid B) g := begin - symmetry, + apply ptranspose, fapply phomotopy.mk, - { intro af, induction af with a f a f, + { intro fb, induction fb with f b f b, { reflexivity }, { exact (respect_pt g)⁻¹ }, { exact (respect_pt g)⁻¹ }, { apply eq_pathover, - refine ap_compose (smash_pmap_counit A C) _ _ ⬝ph _ ⬝hp (ap_compose g _ _)⁻¹, + refine ap_compose (smash_pmap_counit B C') _ _ ⬝ph _ ⬝hp (ap_compose g _ _)⁻¹, refine ap02 _ !functor_gluel ⬝ph _ ⬝hp ap02 _ !elim_gluel⁻¹, - refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluel ⬝ph _⁻¹ʰ, - apply square_of_eq_bot, refine !idp_con ⬝ _, - induction C with C c₀, induction g with g g₀, esimp at *, - induction g₀, refine ap02 _ !eq_of_phomotopy_refl }, - { apply eq_pathover, - refine ap_compose (smash_pmap_counit A C) _ _ ⬝ph _ ⬝hp (ap_compose g _ _)⁻¹, - refine ap02 _ !functor_gluer ⬝ph _ ⬝hp ap02 _ !elim_gluer⁻¹, - refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluer ⬝ph _, + refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluel ⬝ph _, refine !idp_con ⬝ph _, apply square_of_eq, - refine !idp_con ⬝ !con_inv_cancel_right⁻¹ }}, + refine !idp_con ⬝ !con_inv_cancel_right⁻¹ }, + { apply eq_pathover, + refine ap_compose (smash_pmap_counit B C') _ _ ⬝ph _ ⬝hp (ap_compose g _ _)⁻¹, + refine ap02 _ !functor_gluer ⬝ph _ ⬝hp ap02 _ !elim_gluer⁻¹, + refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluer ⬝ph _⁻¹ʰ, + apply square_of_eq_bot, refine !idp_con ⬝ _, + induction C' with C' c₀', induction g with g g₀, esimp at *, + induction g₀, refine ap02 _ !eq_of_phomotopy_refl }}, { refine !idp_con ⬝ !idp_con ⬝ _, refine _ ⬝ !ap_compose', refine _ ⬝ (ap_is_constant respect_pt _)⁻¹, refine !idp_con⁻¹ } end - definition smash_pmap_counit_natural_left (g : A →* A') : - smash_pmap_counit A' B ∘* g ∧→ (pid (ppmap A' B)) ~* - smash_pmap_counit A B ∘* (pid A) ∧→ (ppcompose_right g) := + definition smash_pmap_counit_natural_left (g : B →* B') : + psquare (pid (ppmap B' C) ∧→ g) (smash_pmap_counit B C) + (ppcompose_right g ∧→ pid B) (smash_pmap_counit B' C) := begin fapply phomotopy.mk, { intro af, induction af with a f a f, @@ -157,23 +157,23 @@ namespace smash { reflexivity }, { reflexivity }, { apply eq_pathover, apply hdeg_square, - refine ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ (!elim_gluel ⬝ !idp_con) ⬝ - !elim_gluel ⬝ _, + refine ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ !elim_gluel ⬝ !ap_con ⬝ + !ap_compose'⁻¹ ◾ !elim_gluel ⬝ _, refine (ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ !elim_gluel ⬝ !ap_con ⬝ - !ap_compose'⁻¹ ◾ !elim_gluel ⬝ !con_idp ⬝ _)⁻¹, - refine !to_fun_eq_of_phomotopy ⬝ _, reflexivity }, + !ap_compose'⁻¹ ◾ !elim_gluel ⬝ !idp_con)⁻¹ }, { apply eq_pathover, apply hdeg_square, - refine ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ !elim_gluer ⬝ !ap_con ⬝ - !ap_compose'⁻¹ ◾ !elim_gluer ⬝ _, + refine ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ (!elim_gluer ⬝ !idp_con) ⬝ + !elim_gluer ⬝ _, refine (ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ !elim_gluer ⬝ !ap_con ⬝ - !ap_compose'⁻¹ ◾ !elim_gluer ⬝ !idp_con)⁻¹ }}, + !ap_compose'⁻¹ ◾ !elim_gluer ⬝ !con_idp ⬝ _)⁻¹, + refine !to_fun_eq_of_phomotopy ⬝ _, reflexivity }}, { refine !idp_con ⬝ _, refine !ap_compose'⁻¹ ⬝ _ ⬝ !ap_ap011⁻¹, esimp, - refine !to_fun_eq_of_phomotopy ⬝ _, exact !ap_constant⁻¹, } + refine !to_fun_eq_of_phomotopy ⬝ _, exact !ap_constant⁻¹ } end /- The unit-counit laws -/ definition smash_pmap_unit_counit (A B : Type*) : - smash_pmap_counit A (A ∧ B) ∘* smash_functor (pid A) (smash_pmap_unit A B) ~* pid (A ∧ B) := + smash_pmap_counit B (A ∧ B) ∘* smash_pmap_unit A B ∧→ pid B ~* pid (A ∧ B) := begin fapply phomotopy.mk, { intro x, @@ -184,27 +184,27 @@ namespace smash { apply eq_pathover_id_right, refine ap_compose smash_pmap_counit_map _ _ ⬝ ap02 _ !functor_gluel ⬝ph _, refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluel ⬝ph _, - refine !ap_eq_of_phomotopy ⬝ph _, + refine !idp_con ⬝ph _, apply square_of_eq, refine !idp_con ⬝ !inv_con_cancel_right⁻¹ }, { apply eq_pathover_id_right, refine ap_compose smash_pmap_counit_map _ _ ⬝ ap02 _ !functor_gluer ⬝ph _, refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluer ⬝ph _, - refine !idp_con ⬝ph _, + refine !ap_eq_of_phomotopy ⬝ph _, apply square_of_eq, refine !idp_con ⬝ !inv_con_cancel_right⁻¹ }}, { refine _ ⬝ !ap_compose', refine _ ⬝ (ap_is_constant respect_pt _)⁻¹, - rexact (con.right_inv (gluer pt))⁻¹ } + rexact (con.right_inv (gluel pt))⁻¹ } end definition smash_pmap_counit_unit_pt [constructor] (f : A →* B) : - smash_pmap_counit A B ∘* pinl A f ~* f := + smash_pmap_counit A B ∘* pinr A f ~* f := begin fapply phomotopy.mk, { intro a, reflexivity }, - { refine !idp_con ⬝ !elim_gluer'⁻¹ } + { refine !idp_con ⬝ !elim_gluel'⁻¹ } end definition smash_pmap_counit_unit (A B : Type*) : - ppcompose_left (smash_pmap_counit A B) ∘* smash_pmap_unit A (ppmap A B) ~* pid (ppmap A B) := + ppcompose_left (smash_pmap_counit A B) ∘* smash_pmap_unit (ppmap A B) A ~* pid (ppmap A B) := begin fapply phomotopy_mk_ppmap, { intro f, exact smash_pmap_counit_unit_pt f }, @@ -214,9 +214,9 @@ namespace smash refine _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹ ◾** !phomotopy_of_eq_of_phomotopy⁻¹, refine _ ⬝ !trans_refl⁻¹, fapply phomotopy_eq, - { intro a, esimp, refine !elim_gluel'⁻¹ }, + { intro a, esimp, refine !elim_gluer'⁻¹ }, { esimp, refine whisker_right _ !whisker_right_idp ⬝ _ ⬝ !idp_con⁻¹, - refine whisker_right _ !elim_gluel'_same⁻² ⬝ _ ⬝ !elim_gluer'_same⁻¹⁻², + refine whisker_right _ !elim_gluer'_same⁻² ⬝ _ ⬝ !elim_gluel'_same⁻¹⁻², apply inv_con_eq_of_eq_con, refine !idp_con ⬝ _, esimp, refine _ ⬝ !ap02_con ⬝ whisker_left _ !ap_inv, refine !whisker_right_idp ⬝ _, @@ -224,10 +224,10 @@ namespace smash end /- The underlying (unpointed) functions of the equivalence A →* (B →* C) ≃* A ∧ B →* C) -/ - definition smash_elim [constructor] (f : A →* ppmap B C) : B ∧ A →* C := - smash_pmap_counit B C ∘* smash_functor (pid B) f + definition smash_elim [constructor] (f : A →* ppmap B C) : A ∧ B →* C := + smash_pmap_counit B C ∘* f ∧→ pid B - definition smash_elim_inv [constructor] (g : A ∧ B →* C) : B →* ppmap A C := + definition smash_elim_inv [constructor] (g : A ∧ B →* C) : A →* ppmap B C := ppcompose_left g ∘* smash_pmap_unit A B /- They are inverses, constant on the constant function and natural -/ @@ -235,7 +235,7 @@ namespace smash begin refine !pwhisker_right !ppcompose_left_pcompose ⬝* _, refine !passoc ⬝* _, - refine !pwhisker_left !smash_pmap_unit_natural⁻¹* ⬝* _, + refine !pwhisker_left !smash_pmap_unit_natural ⬝* _, refine !passoc⁻¹* ⬝* _, refine !pwhisker_right !smash_pmap_counit_unit ⬝* _, apply pid_pcompose @@ -243,7 +243,7 @@ namespace smash definition smash_elim_right_inv (g : A ∧ B →* C) : smash_elim (smash_elim_inv g) ~* g := begin - refine !pwhisker_left !smash_functor_pid_pcompose ⬝* _, + refine !pwhisker_left !smash_functor_pcompose_pid ⬝* _, refine !passoc⁻¹* ⬝* _, refine !pwhisker_right !smash_pmap_counit_natural_right⁻¹* ⬝* _, refine !passoc ⬝* _, @@ -252,13 +252,13 @@ namespace smash end definition smash_elim_pconst (A B C : Type*) : - smash_elim (pconst B (ppmap A C)) ~* pconst (A ∧ B) C := + smash_elim (pconst A (ppmap B C)) ~* pconst (A ∧ B) C := begin - refine pwhisker_left _ (smash_functor_pconst_right (pid A)) ⬝* !pcompose_pconst + refine pwhisker_left _ (smash_functor_pconst_left (pid B)) ⬝* !pcompose_pconst end definition smash_elim_inv_pconst (A B C : Type*) : - smash_elim_inv (pconst (A ∧ B) C) ~* pconst B (ppmap A C) := + smash_elim_inv (pconst (A ∧ B) C) ~* pconst A (ppmap B C) := begin fapply phomotopy_mk_ppmap, { intro f, apply pconst_pcompose }, @@ -268,10 +268,10 @@ namespace smash apply pconst_pcompose_phomotopy_pconst } end - definition smash_elim_natural_right {A B C C' : Type*} (f : C →* C') - (g : B →* ppmap A C) : f ∘* smash_elim g ~* smash_elim (ppcompose_left f ∘* g) := + definition smash_elim_natural_right (f : C →* C') (g : A →* ppmap B C) : + f ∘* smash_elim g ~* smash_elim (ppcompose_left f ∘* g) := begin - refine _ ⬝* pwhisker_left _ !smash_functor_pid_pcompose⁻¹*, + refine _ ⬝* pwhisker_left _ !smash_functor_pcompose_pid⁻¹*, refine !passoc⁻¹* ⬝* pwhisker_right _ _ ⬝* !passoc, apply smash_pmap_counit_natural_right end @@ -283,27 +283,27 @@ namespace smash exact !ppcompose_left_pcompose⁻¹* end - definition smash_elim_natural_left (f : A →* A') (g : B →* B') - (h : B' →* ppmap A' C) : smash_elim h ∘* (f ∧→ g) ~* smash_elim (ppcompose_right f ∘* h ∘* g) := + definition smash_elim_natural_left (f : A →* A') (g : B →* B') (h : A' →* ppmap B' C) : + smash_elim h ∘* (f ∧→ g) ~* smash_elim (ppcompose_right g ∘* h ∘* f) := begin - refine !smash_functor_pid_pcompose ⬝ph* _, + refine !smash_functor_pcompose_pid ⬝ph* _, refine _ ⬝v* !smash_pmap_counit_natural_left, - refine smash_functor_psquare (pvrefl f) !pid_pcompose⁻¹* + refine smash_functor_psquare !pid_pcompose⁻¹* (phrefl g) end - definition smash_elim_phomotopy {f f' : A →* ppmap B C} - (p : f ~* f') : smash_elim f ~* smash_elim f' := + definition smash_elim_phomotopy {f f' : A →* ppmap B C} (p : f ~* f') : + smash_elim f ~* smash_elim f' := begin apply pwhisker_left, - exact smash_functor_phomotopy phomotopy.rfl p + exact smash_functor_phomotopy p phomotopy.rfl end - definition smash_elim_inv_phomotopy {f f' : A ∧ B →* C} - (p : f ~* f') : smash_elim_inv f ~* smash_elim_inv f' := + definition smash_elim_inv_phomotopy {f f' : A ∧ B →* C} (p : f ~* f') : + smash_elim_inv f ~* smash_elim_inv f' := pwhisker_right _ (ppcompose_left_phomotopy p) - definition smash_elim_eq_of_phomotopy {f f' : A →* ppmap B C} - (p : f ~* f') : ap smash_elim (eq_of_phomotopy p) = eq_of_phomotopy (smash_elim_phomotopy p) := + definition smash_elim_eq_of_phomotopy {f f' : A →* ppmap B C} (p : f ~* f') : + ap smash_elim (eq_of_phomotopy p) = eq_of_phomotopy (smash_elim_phomotopy p) := begin induction p using phomotopy_rec_idp, refine ap02 _ !eq_of_phomotopy_refl ⬝ _, @@ -325,38 +325,46 @@ namespace smash end /- The pointed maps of the equivalence A →* (B →* C) ≃* A ∧ B →* C -/ - definition smash_pelim [constructor] (A B C : Type*) : ppmap A (ppmap B C) →* ppmap (B ∧ A) C := - ppcompose_left (smash_pmap_counit B C) ∘* smash_functor_right B A (ppmap B C) + definition smash_pelim (A B C : Type*) : ppmap A (ppmap B C) →* ppmap (A ∧ B) C := + ppcompose_left (smash_pmap_counit B C) ∘* smash_functor_left A (ppmap B C) B - definition smash_pelim_inv [constructor] (A B C : Type*) : - ppmap (B ∧ A) C →* ppmap A (ppmap B C) := + definition smash_pelim_inv (A B C : Type*) : + ppmap (A ∧ B) C →* ppmap A (ppmap B C) := pmap.mk smash_elim_inv (eq_of_phomotopy !smash_elim_inv_pconst) /- The forward function is natural in all three arguments -/ + definition smash_pelim_natural_left (B C : Type*) (f : A' →* A) : + psquare (smash_pelim A B C) (smash_pelim A' B C) + (ppcompose_right f) (ppcompose_right (f ∧→ pid B)) := + smash_functor_left_natural_left f ⬝h* !ppcompose_left_ppcompose_right + + definition smash_pelim_natural_middle (A C : Type*) (f : B' →* B) : + psquare (smash_pelim A B C) (smash_pelim A B' C) + (ppcompose_left (ppcompose_right f)) (ppcompose_right (pid A ∧→ f)) := + pwhisker_tl _ !ppcompose_left_ppcompose_right ⬝* + (!smash_functor_left_natural_right⁻¹* ⬝pv* + smash_functor_left_natural_middle (ppcompose_right f) ⬝h* + ppcompose_left_psquare !smash_pmap_counit_natural_left) + definition smash_pelim_natural_right (f : C →* C') : psquare (smash_pelim A B C) (smash_pelim A B C') (ppcompose_left (ppcompose_left f)) (ppcompose_left f) := - smash_functor_right_natural_right (ppcompose_left f) ⬝h* - ppcompose_left_psquare (smash_pmap_counit_natural_right f) - - definition smash_pelim_natural_left (B C : Type*) (f : A' →* A) : - psquare (smash_pelim A B C) (smash_pelim A' B C) - (ppcompose_right f) (ppcompose_right (pid B ∧→ f)) := - smash_functor_right_natural_middle f ⬝h* !ppcompose_left_ppcompose_right - - definition smash_pelim_natural_middle (A C : Type*) (g : B' →* B) : - psquare (smash_pelim A B C) (smash_pelim A B' C) - (ppcompose_left (ppcompose_right g)) (ppcompose_right (g ∧→ pid A)) := - pwhisker_tl _ !ppcompose_left_ppcompose_right ⬝* - (!smash_functor_right_natural_left⁻¹* ⬝pv* - smash_functor_right_natural_right (ppcompose_right g) ⬝h* - ppcompose_left_psquare !smash_pmap_counit_natural_left) + smash_functor_left_natural_middle (ppcompose_left f) ⬝h* + ppcompose_left_psquare (smash_pmap_counit_natural_right _ f) definition smash_pelim_natural_lm (C : Type*) (f : A' →* A) (g : B' →* B) : psquare (smash_pelim A B C) (smash_pelim A' B' C) - (ppcompose_left (ppcompose_right g) ∘* ppcompose_right f) (ppcompose_right (g ∧→ f)) := + (ppcompose_left (ppcompose_right g) ∘* ppcompose_right f) (ppcompose_right (f ∧→ g)) := smash_pelim_natural_left B C f ⬝v* smash_pelim_natural_middle A' C g ⬝hp* - ppcompose_right_phomotopy proof !smash_functor_split qed ⬝* !ppcompose_right_pcompose + ppcompose_right_phomotopy (smash_functor_split f g) ⬝* !ppcompose_right_pcompose + + definition smash_pelim_pid (B C : Type*) : + smash_pelim (ppmap B C) B C !pid ~* smash_pmap_counit B C := + pwhisker_left _ !smash_functor_pid ⬝* !pcompose_pid + + definition smash_pelim_inv_pid (A B : Type*) : + smash_pelim_inv A B (A ∧ B) !pid ~* smash_pmap_unit A B := + pwhisker_right _ !ppcompose_left_pid ⬝* !pid_pcompose /- The equivalence (note: the forward function of smash_adjoint_pmap is smash_pelim_inv) -/ definition is_equiv_smash_elim [constructor] (A B C : Type*) : is_equiv (@smash_elim A B C) := @@ -368,29 +376,22 @@ namespace smash end definition smash_adjoint_pmap_inv [constructor] (A B C : Type*) : - ppmap B (ppmap A C) ≃* ppmap (A ∧ B) C := - pequiv_of_pmap (smash_pelim B A C) (is_equiv_smash_elim B A C) + ppmap A (ppmap B C) ≃* ppmap (A ∧ B) C := + pequiv_of_pmap (smash_pelim A B C) (is_equiv_smash_elim A B C) definition smash_adjoint_pmap [constructor] (A B C : Type*) : - ppmap (A ∧ B) C ≃* ppmap B (ppmap A C) := + ppmap (A ∧ B) C ≃* ppmap A (ppmap B C) := (smash_adjoint_pmap_inv A B C)⁻¹ᵉ* /- The naturality of the equivalence is a direct consequence of the earlier naturalities -/ definition smash_adjoint_pmap_natural_right_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) := - begin - refine !passoc⁻¹* ⬝* pwhisker_right _ _, - exact !ppcompose_left_pcompose⁻¹* - end + smash_elim_inv_natural_right f g definition smash_adjoint_pmap_inv_natural_right_pt {A B C C' : Type*} (f : C →* C') - (g : B →* ppmap A C) : f ∘* (smash_adjoint_pmap A B C)⁻¹ᵉ* g ~* + (g : A →* ppmap B C) : f ∘* (smash_adjoint_pmap A B C)⁻¹ᵉ* g ~* (smash_adjoint_pmap A B C')⁻¹ᵉ* (ppcompose_left f ∘* g) := - begin - refine _ ⬝* pwhisker_left _ !smash_functor_pid_pcompose⁻¹*, - refine !passoc⁻¹* ⬝* pwhisker_right _ _ ⬝* !passoc, - apply smash_pmap_counit_natural_right - end + smash_elim_natural_right f g definition smash_adjoint_pmap_inv_natural_right [constructor] {A B C C' : Type*} (f : C →* C') : ppcompose_left f ∘* smash_adjoint_pmap_inv A B C ~* @@ -404,161 +405,244 @@ namespace smash definition smash_adjoint_pmap_natural_lm (C : Type*) (f : A →* A') (g : B →* B') : psquare (smash_adjoint_pmap A' B' C) (smash_adjoint_pmap A B C) - (ppcompose_right (f ∧→ g)) (ppcompose_left (ppcompose_right f) ∘* ppcompose_right g) := - proof (!smash_pelim_natural_lm)⁻¹ʰ* qed + (ppcompose_right (f ∧→ g)) (ppcompose_left (ppcompose_right g) ∘* ppcompose_right f) := + (smash_pelim_natural_lm C f g)⁻¹ʰ* + + definition smash_elim_inv_natural_middle (f : B' →* B) + (g : A ∧ B →* C) : ppcompose_right f ∘* smash_elim_inv g ~* smash_elim_inv (g ∘* pid A ∧→ f) := + !pcompose_pid⁻¹* ⬝* !passoc ⬝* phomotopy_of_eq (smash_adjoint_pmap_natural_lm C (pid A) f g) + + definition smash_pmap_unit_natural_left (f : B →* B') : + ppcompose_left (pid A ∧→ f) ∘* smash_pmap_unit A B ~* + ppcompose_right f ∘* smash_pmap_unit A B' := + begin + refine pwhisker_left _ !smash_pelim_inv_pid⁻¹* ⬝* _ ⬝* pwhisker_left _ !smash_pelim_inv_pid, + refine !smash_elim_inv_natural_right ⬝* _ ⬝* !smash_elim_inv_natural_middle⁻¹*, + refine pap smash_elim_inv (!pcompose_pid ⬝* !pid_pcompose⁻¹*), + end /- Corollary: associativity of smash -/ - definition smash_assoc_elim_equiv (A B C X : Type*) : + definition smash_assoc_elim_pequiv (A B C X : Type*) : ppmap (A ∧ (B ∧ C)) X ≃* ppmap ((A ∧ B) ∧ C) X := 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_inv A B X) - ... ≃* ppmap ((A ∧ B) ∧ C) X : smash_adjoint_pmap_inv (A ∧ B) C X + ppmap (A ∧ (B ∧ C)) X + ≃* ppmap A (ppmap (B ∧ C) X) : smash_adjoint_pmap A (B ∧ C) X + ... ≃* ppmap A (ppmap B (ppmap C X)) : pequiv_ppcompose_left (smash_adjoint_pmap B C X) + ... ≃* ppmap (A ∧ B) (ppmap C X) : smash_adjoint_pmap_inv A B (ppmap C 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 := - smash_elim (ppcompose_left (smash_adjoint_pmap A B X)⁻¹ᵉ* (smash_elim_inv (smash_elim_inv f))) + -- definition smash_assoc_elim_pequiv_fn (A B C X : Type*) (f : A ∧ (B ∧ C) →* X) : + -- (A ∧ B) ∧ C →* X := + -- smash_elim (ppcompose_left (smash_adjoint_pmap A B X)⁻¹ᵉ* (smash_elim_inv (smash_elim_inv f))) - definition smash_assoc_elim_natural_right (A B C : Type*) (f : X →* X') : - psquare (smash_assoc_elim_equiv A B C X) (smash_assoc_elim_equiv A B C X') - (ppcompose_left f) (ppcompose_left f) := - !smash_adjoint_pmap_natural_right ⬝h* - !smash_adjoint_pmap_natural_right ⬝h* - ppcompose_left_psquare !smash_adjoint_pmap_inv_natural_right ⬝h* - !smash_adjoint_pmap_inv_natural_right - - /- - We could prove the following two pointed homotopies by applying smash_assoc_elim_natural_right - to g, but we give a more explicit proof - -/ - definition smash_assoc_elim_natural_right_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 - refine !smash_adjoint_pmap_inv_natural_right_pt ⬝* _, - apply smash_elim_phomotopy, - refine !passoc⁻¹* ⬝* _, - refine pwhisker_right _ !smash_adjoint_pmap_inv_natural_right ⬝* _, - refine !passoc ⬝* _, - apply pwhisker_left, - refine !smash_adjoint_pmap_natural_right_pt ⬝* _, - apply smash_elim_inv_phomotopy, - refine !smash_adjoint_pmap_natural_right_pt - end - - definition smash_assoc_elim_inv_natural_right_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 - refine !smash_adjoint_pmap_inv_natural_right_pt ⬝* _, - apply smash_elim_phomotopy, - refine !passoc⁻¹* ⬝* _, - refine pwhisker_right _ !smash_pmap_counit_natural_right ⬝* _, - 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_right f) ⬝* _, - refine !passoc ⬝* _, - apply pwhisker_left, - apply smash_elim_inv_natural_right - end - - definition smash_assoc (A B C : Type*) : A ∧ (B ∧ C) ≃* (A ∧ B) ∧ C := - begin - fapply pequiv.MK, - { exact !smash_assoc_elim_equiv⁻¹ᵉ* !pid }, - { exact !smash_assoc_elim_equiv !pid }, - { refine !smash_assoc_elim_inv_natural_right_pt ⬝* _, - refine pap !smash_assoc_elim_equiv⁻¹ᵉ* !pcompose_pid ⬝* _, - apply phomotopy_of_eq, apply to_left_inv !smash_assoc_elim_equiv }, - { refine !smash_assoc_elim_natural_right_pt ⬝* _, - refine pap !smash_assoc_elim_equiv !pcompose_pid ⬝* _, - apply phomotopy_of_eq, apply to_right_inv !smash_assoc_elim_equiv } - end - - /- the associativity of smash is natural in all arguments -/ definition smash_assoc_elim_natural_left (X : Type*) - (f : A →* A') (g : B →* B') (h : C →* C') : - psquare (smash_assoc_elim_equiv A' B' C' X) (smash_assoc_elim_equiv A B C X) + (f : A' →* A) (g : B' →* B) (h : C' →* C) : + psquare (smash_assoc_elim_pequiv A B C X) (smash_assoc_elim_pequiv A' B' C' X) (ppcompose_right (f ∧→ g ∧→ h)) (ppcompose_right ((f ∧→ g) ∧→ h)) := begin - refine !smash_adjoint_pmap_natural_lm ⬝h* _ ⬝h* - (!ppcompose_left_ppcompose_right ⬝v* ppcompose_left_psquare !smash_pelim_natural_lm) ⬝h* - !smash_pelim_natural_lm, - refine !ppcompose_left_ppcompose_right⁻¹* ⬝ph* _, - refine _ ⬝hp* pwhisker_right _ (ppcompose_left_phomotopy !ppcompose_left_ppcompose_right⁻¹* ⬝* + refine !smash_adjoint_pmap_natural_lm ⬝h* + (!ppcompose_left_ppcompose_right ⬝v* ppcompose_left_psquare !smash_adjoint_pmap_natural_lm) ⬝h* + _ ⬝h* !smash_pelim_natural_lm, + refine pwhisker_right _ (ppcompose_left_phomotopy !ppcompose_left_ppcompose_right⁻¹* ⬝* !ppcompose_left_pcompose) ⬝* !passoc ⬝* pwhisker_left _ !ppcompose_left_ppcompose_right⁻¹* ⬝* - !passoc⁻¹*, - refine _ ⬝v* !smash_adjoint_pmap_natural_lm, - refine !smash_adjoint_pmap_natural_right + !passoc⁻¹* ⬝ph* _, + refine _ ⬝hp* !ppcompose_left_ppcompose_right⁻¹*, + refine !smash_pelim_natural_right ⬝v* !smash_pelim_natural_lm end + definition smash_assoc_elim_natural_right (A B C : Type*) (f : X →* X') : + psquare (smash_assoc_elim_pequiv A B C X) (smash_assoc_elim_pequiv A B C X') + (ppcompose_left f) (ppcompose_left f) := + !smash_adjoint_pmap_natural_right ⬝h* + ppcompose_left_psquare !smash_adjoint_pmap_natural_right ⬝h* + !smash_adjoint_pmap_inv_natural_right ⬝h* + !smash_adjoint_pmap_inv_natural_right + + definition smash_assoc_elim_natural_right_pt (f : X →* X') (g : A ∧ (B ∧ C) →* X) : + f ∘* smash_assoc_elim_pequiv A B C X g ~* smash_assoc_elim_pequiv A B C X' (f ∘* g) := + phomotopy_of_eq (smash_assoc_elim_natural_right A B C f g) + + definition smash_assoc_elim_inv_natural_right_pt (f : X →* X') (g : (A ∧ B) ∧ C →* X) : + f ∘* (smash_assoc_elim_pequiv A B C X)⁻¹ᵉ* g ~* + (smash_assoc_elim_pequiv A B C X')⁻¹ᵉ* (f ∘* g) := + phomotopy_of_eq ((smash_assoc_elim_natural_right A B C f)⁻¹ʰ* g) + + definition smash_assoc (A B C : Type*) : (A ∧ B) ∧ C ≃* A ∧ (B ∧ C) := + pyoneda (smash_assoc_elim_pequiv A B C) (λX X' f, smash_assoc_elim_natural_right A B C f) + -- begin + -- fapply pequiv.MK, + -- { exact !smash_assoc_elim_pequiv !pid }, + -- { exact !smash_assoc_elim_pequiv⁻¹ᵉ* !pid }, + -- { refine !smash_assoc_elim_natural_right_pt ⬝* _, + -- refine pap !smash_assoc_elim_pequiv !pcompose_pid ⬝* _, + -- apply phomotopy_of_eq, apply to_right_inv !smash_assoc_elim_pequiv }, + -- { refine !smash_assoc_elim_inv_natural_right_pt ⬝* _, + -- refine pap !smash_assoc_elim_pequiv⁻¹ᵉ* !pcompose_pid ⬝* _, + -- apply phomotopy_of_eq, apply to_left_inv !smash_assoc_elim_pequiv } + -- end + + definition pcompose_smash_assoc {A B C X : Type*} (f : A ∧ (B ∧ C) →* X) : + f ∘* smash_assoc A B C ~* smash_assoc_elim_pequiv A B C X f := + smash_assoc_elim_natural_right_pt f !pid ⬝* pap !smash_assoc_elim_pequiv !pcompose_pid + + definition pcompose_smash_assoc_pinv {A B C X : Type*} (f : (A ∧ B) ∧ C →* X) : + f ∘* (smash_assoc A B C)⁻¹ᵉ* ~* (smash_assoc_elim_pequiv A B C X)⁻¹ᵉ* f := + smash_assoc_elim_inv_natural_right_pt f !pid ⬝* pap !smash_assoc_elim_pequiv⁻¹ᵉ* !pcompose_pid + + /- the associativity of smash is natural in all arguments -/ definition smash_assoc_natural (f : A →* A') (g : B →* B') (h : C →* C') : - psquare (smash_assoc A B C) (smash_assoc A' B' C') (f ∧→ (g ∧→ h)) ((f ∧→ g) ∧→ h) := + psquare (smash_assoc A B C) (smash_assoc A' B' C') ((f ∧→ g) ∧→ h) (f ∧→ (g ∧→ h)) := begin - refine !smash_assoc_elim_inv_natural_right_pt ⬝* _, - refine pap !smash_assoc_elim_equiv⁻¹ᵉ* (!pcompose_pid ⬝* !pid_pcompose⁻¹*) ⬝* _, - rexact phomotopy_of_eq ((smash_assoc_elim_natural_left _ f g h)⁻¹ʰ* !pid)⁻¹ + refine !pcompose_smash_assoc ⬝* _, + refine pap !smash_assoc_elim_pequiv !pid_pcompose⁻¹* ⬝* _, + rexact phomotopy_of_eq (smash_assoc_elim_natural_left _ f g h !pid)⁻¹ + end + + /- we prove the pentagon for the associativity -/ + definition smash_assoc_elim_left_pequiv (A B C D X : Type*) : + ppmap (D ∧ (A ∧ (B ∧ C))) X ≃* ppmap (D ∧ ((A ∧ B) ∧ C)) X := + calc ppmap (D ∧ (A ∧ (B ∧ C))) X + ≃* ppmap D (ppmap (A ∧ (B ∧ C)) X) : smash_adjoint_pmap D (A ∧ (B ∧ C)) X + ... ≃* ppmap D (ppmap ((A ∧ B) ∧ C) X) : pequiv_ppcompose_left (smash_assoc_elim_pequiv A B C X) + ... ≃* ppmap (D ∧ ((A ∧ B) ∧ C)) X : smash_adjoint_pmap_inv D ((A ∧ B) ∧ C) X + + definition smash_assoc_elim_right_pequiv (A B C D X : Type*) : + ppmap ((A ∧ (B ∧ C)) ∧ D) X ≃* ppmap (((A ∧ B) ∧ C) ∧ D) X := + calc ppmap ((A ∧ (B ∧ C)) ∧ D) X + ≃* ppmap (A ∧ (B ∧ C)) (ppmap D X) : smash_adjoint_pmap (A ∧ (B ∧ C)) D X + ... ≃* ppmap ((A ∧ B) ∧ C) (ppmap D X) : smash_assoc_elim_pequiv A B C (ppmap D X) + ... ≃* ppmap (((A ∧ B) ∧ C) ∧ D) X : smash_adjoint_pmap_inv ((A ∧ B) ∧ C) D X + + definition smash_assoc_elim_right_natural_right (A B C D : Type*) (f : X →* X') : + psquare (smash_assoc_elim_right_pequiv A B C D X) (smash_assoc_elim_right_pequiv A B C D X') + (ppcompose_left f) (ppcompose_left f) := + smash_adjoint_pmap_natural_right f ⬝h* + smash_assoc_elim_natural_right A B C (ppcompose_left f) ⬝h* + smash_adjoint_pmap_inv_natural_right f + + definition smash_assoc_smash_functor (A B C D : Type*) : + smash_assoc A B C ∧→ pid D ~* !smash_assoc_elim_right_pequiv (pid _) := + begin + symmetry, + refine pap (!smash_adjoint_pmap_inv ∘* !smash_assoc_elim_pequiv) !smash_pelim_inv_pid ⬝* _, + refine pap !smash_adjoint_pmap_inv !pcompose_smash_assoc⁻¹* ⬝* _, + refine pwhisker_left _ !smash_functor_pcompose_pid ⬝* _, + refine !passoc⁻¹* ⬝* _, + exact pwhisker_right _ !smash_pmap_unit_counit ⬝* !pid_pcompose, + end + + definition ppcompose_right_smash_assoc (A B C X : Type*) : + ppcompose_right (smash_assoc A B C) ~* smash_assoc_elim_pequiv A B C X := + sorry -- one hole left + + definition smash_functor_smash_assoc (A B C D : Type*) : + pid A ∧→ smash_assoc B C D ~* !smash_assoc_elim_left_pequiv (pid _) := + begin + symmetry, + refine pap (!smash_adjoint_pmap_inv ∘* ppcompose_left _) !smash_pelim_inv_pid ⬝* _, + refine pap !smash_adjoint_pmap_inv (pwhisker_right _ !ppcompose_right_smash_assoc⁻¹* ⬝* + !smash_pmap_unit_natural_left⁻¹*) ⬝* _, + refine phomotopy_of_eq (smash_adjoint_pmap_inv_natural_right (pid A ∧→ smash_assoc B C D) + !smash_pmap_unit)⁻¹ ⬝* _, + refine pwhisker_left _ _ ⬝* !pcompose_pid, + apply smash_pmap_unit_counit + end + + definition smash_assoc_pentagon (A B C D : Type*) : + smash_assoc A B (C ∧ D) ∘* smash_assoc (A ∧ B) C D ~* + pid A ∧→ smash_assoc B C D ∘* smash_assoc A (B ∧ C) D ∘* smash_assoc A B C ∧→ pid D := + begin + refine !pcompose_smash_assoc ⬝* _, + refine pap (!smash_adjoint_pmap_inv ∘* !smash_adjoint_pmap_inv ∘* + ppcompose_left !smash_adjoint_pmap) + (phomotopy_of_eq (to_left_inv !smash_adjoint_pmap_inv _)) ⬝* _, + refine pap (!smash_adjoint_pmap_inv ∘* !smash_adjoint_pmap_inv) + (phomotopy_of_eq (!smash_pelim_natural_right _)) ⬝* _, + symmetry, + refine !smash_functor_smash_assoc ◾* pwhisker_left _ !smash_assoc_smash_functor ⬝* _, + refine !passoc⁻¹* ⬝* _, + refine phomotopy_of_eq (smash_assoc_elim_right_natural_right A B C D _ _) ⬝* + pap !smash_assoc_elim_right_pequiv (!pcompose_pid ⬝* !pcompose_smash_assoc) ⬝* _, + apply phomotopy_of_eq, + apply ap (!smash_adjoint_pmap_inv ∘ !smash_adjoint_pmap_inv ∘ !smash_adjoint_pmap_inv), + refine ap (ppcompose_left _ ∘ !smash_adjoint_pmap) (to_left_inv !smash_adjoint_pmap_inv _) ⬝ _, + refine ap (ppcompose_left _) (to_left_inv !smash_adjoint_pmap_inv _) ⬝ _, + refine ap (ppcompose_left _ ∘ ppcompose_left _) (to_left_inv !smash_adjoint_pmap_inv _) ⬝ _, + refine ap (ppcompose_left _) ((ppcompose_left_pcompose _ _ _)⁻¹ ⬝ + ppcompose_left_phomotopy !pinv_pcompose_cancel_left _) ⬝ _, + refine (ppcompose_left_pcompose _ _ _)⁻¹ ⬝ + ppcompose_left_phomotopy !pinv_pcompose_cancel_left _ ⬝ _, + exact ppcompose_left_pcompose _ _ _, end /- Corollary 2: smashing with a suspension -/ - definition smash_susp_elim_equiv (A B X : Type*) : - ppmap (A ∧ susp B) X ≃* ppmap (susp (A ∧ B)) X := + definition smash_susp_elim_pequiv (A B X : Type*) : + ppmap (⅀ A ∧ B) X ≃* ppmap (⅀ (A ∧ B)) X := calc - ppmap (A ∧ susp B) X ≃* ppmap (susp B) (ppmap A X) : smash_adjoint_pmap A (susp B) X - ... ≃* ppmap B (Ω (ppmap A X)) : susp_adjoint_loop B (ppmap A X) - ... ≃* ppmap B (ppmap A (Ω X)) : pequiv_ppcompose_left (loop_ppmap_commute A X) + 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)) : pequiv_ppcompose_left (loop_ppmap_commute B X) ... ≃* ppmap (A ∧ B) (Ω X) : smash_adjoint_pmap A B (Ω X) - ... ≃* ppmap (susp (A ∧ B)) X : susp_adjoint_loop (A ∧ B) X + ... ≃* ppmap (⅀ (A ∧ B)) X : susp_adjoint_loop (A ∧ B) X definition smash_susp_elim_natural_right (A B : Type*) (f : X →* X') : - psquare (smash_susp_elim_equiv A B X) (smash_susp_elim_equiv A B X') + psquare (smash_susp_elim_pequiv A B X) (smash_susp_elim_pequiv A B X') (ppcompose_left f) (ppcompose_left f) := smash_adjoint_pmap_natural_right f ⬝h* susp_adjoint_loop_natural_right (ppcompose_left f) ⬝h* - ppcompose_left_psquare (loop_pmap_commute_natural_right A f) ⬝h* + ppcompose_left_psquare (loop_pmap_commute_natural_right B f) ⬝h* (smash_adjoint_pmap_natural_right (Ω→ f))⁻¹ʰ* ⬝h* (susp_adjoint_loop_natural_right f)⁻¹ʰ* definition smash_susp_elim_natural_left (X : Type*) (f : A' →* A) (g : B' →* B) : - psquare (smash_susp_elim_equiv A B X) (smash_susp_elim_equiv A' B' X) - (ppcompose_right (f ∧→ susp_functor g)) (ppcompose_right (susp_functor (f ∧→ g))) := + psquare (smash_susp_elim_pequiv A B X) (smash_susp_elim_pequiv A' B' X) + (ppcompose_right (⅀→ f ∧→ g)) (ppcompose_right (susp_functor (f ∧→ g))) := begin - refine smash_adjoint_pmap_natural_lm X f (susp_functor g) ⬝h* + refine smash_adjoint_pmap_natural_lm X (⅀→ f) g ⬝h* _ ⬝h* _ ⬝h* (smash_adjoint_pmap_natural_lm (Ω X) f g)⁻¹ʰ* ⬝h* (susp_adjoint_loop_natural_left (f ∧→ g))⁻¹ʰ*, rotate 2, - exact !ppcompose_left_ppcompose_right ⬝v* ppcompose_left_psquare (loop_pmap_commute_natural_left X f), - exact susp_adjoint_loop_natural_left g ⬝v* susp_adjoint_loop_natural_right (ppcompose_right f) + exact !ppcompose_left_ppcompose_right ⬝v* + ppcompose_left_psquare (loop_pmap_commute_natural_left X g), + exact susp_adjoint_loop_natural_left f ⬝v* susp_adjoint_loop_natural_right (ppcompose_right g) end - definition smash_susp (A B : Type*) : A ∧ ⅀ B ≃* ⅀(A ∧ B) := + definition susp_smash_rev (A B : Type*) : ⅀ (A ∧ B) ≃* ⅀ A ∧ B := + pyoneda (smash_susp_elim_pequiv A B) (λX X' f, smash_susp_elim_natural_right A B f) + -- begin + -- fapply pequiv.MK, + -- { exact !smash_susp_elim_pequiv⁻¹ᵉ* !pid }, + -- { exact !smash_susp_elim_pequiv !pid }, + -- { refine phomotopy_of_eq (!smash_susp_elim_natural_right⁻¹ʰ* _) ⬝* _, + -- refine pap !smash_susp_elim_pequiv⁻¹ᵉ* !pcompose_pid ⬝* _, + -- apply phomotopy_of_eq, apply to_left_inv !smash_susp_elim_pequiv }, + -- { refine phomotopy_of_eq (!smash_susp_elim_natural_right _) ⬝* _, + -- refine pap !smash_susp_elim_pequiv !pcompose_pid ⬝* _, + -- apply phomotopy_of_eq, apply to_right_inv !smash_susp_elim_pequiv } + -- end + + definition susp_smash_rev_natural (f : A →* A') (g : B →* B') : + psquare (susp_smash_rev A B) (susp_smash_rev A' B') (⅀→ (f ∧→ g)) (⅀→ f ∧→ g) := begin - fapply pequiv.MK, - { exact !smash_susp_elim_equiv⁻¹ᵉ* !pid }, - { exact !smash_susp_elim_equiv !pid }, - { refine phomotopy_of_eq (!smash_susp_elim_natural_right⁻¹ʰ* _) ⬝* _, - refine pap !smash_susp_elim_equiv⁻¹ᵉ* !pcompose_pid ⬝* _, - apply phomotopy_of_eq, apply to_left_inv !smash_susp_elim_equiv }, - { refine phomotopy_of_eq (!smash_susp_elim_natural_right _) ⬝* _, - refine pap !smash_susp_elim_equiv !pcompose_pid ⬝* _, - apply phomotopy_of_eq, apply to_right_inv !smash_susp_elim_equiv } + refine phomotopy_of_eq (smash_susp_elim_natural_right _ _ _ _) ⬝* _, + refine pap !smash_susp_elim_pequiv (!pcompose_pid ⬝* !pid_pcompose⁻¹*) ⬝* _, + rexact phomotopy_of_eq (smash_susp_elim_natural_left _ f g !pid)⁻¹ end - definition smash_susp_natural (f : A →* A') (g : B →* B') : - psquare (smash_susp A B) (smash_susp A' B') (f ∧→ (susp_functor g)) (susp_functor (f ∧→ g)) := - begin - refine phomotopy_of_eq (!smash_susp_elim_natural_right⁻¹ʰ* _) ⬝* _, - refine pap !smash_susp_elim_equiv⁻¹ᵉ* (!pcompose_pid ⬝* !pid_pcompose⁻¹*) ⬝* _, - rexact phomotopy_of_eq ((smash_susp_elim_natural_left _ f g)⁻¹ʰ* !pid)⁻¹ - end + definition susp_smash (A B : Type*) : ⅀ A ∧ B ≃* ⅀ (A ∧ B) := + (susp_smash_rev A B)⁻¹ᵉ* + + definition smash_susp (A B : Type*) : A ∧ ⅀ B ≃* ⅀ (A ∧ B) := + calc A ∧ ⅀ B + ≃* ⅀ B ∧ A : smash_comm A (⅀ B) + ... ≃* ⅀(B ∧ A) : susp_smash B A + ... ≃* ⅀(A ∧ B) : susp_pequiv (smash_comm B A) + + definition susp_smash_move (A B : Type*) : ⅀ A ∧ B ≃* A ∧ ⅀ B := + susp_smash A B ⬝e* (smash_susp A B)⁻¹ᵉ* -print axioms smash_susp_natural definition smash_iterate_susp (n : ℕ) (A B : Type*) : A ∧ iterate_susp n B ≃* iterate_susp n (A ∧ B) := begin @@ -568,11 +652,11 @@ print axioms smash_susp_natural end definition smash_sphere (A : Type*) (n : ℕ) : A ∧ sphere n ≃* iterate_susp n A := - smash_pequiv pequiv.rfl (sphere_pequiv_iterate_susp n) ⬝e* + pequiv.rfl ∧≃ (sphere_pequiv_iterate_susp n) ⬝e* smash_iterate_susp n A pbool ⬝e* iterate_susp_pequiv n (smash_pbool_pequiv A) - definition smash_pcircle (A : Type*) : A ∧ pcircle ≃* susp A := + definition smash_pcircle (A : Type*) : A ∧ S¹* ≃* susp A := smash_sphere A 1 definition sphere_smash_sphere (n m : ℕ) : sphere n ∧ sphere m ≃* sphere (n+m) := diff --git a/pointed.hlean b/pointed.hlean index 807e2d3..7ee1e98 100644 --- a/pointed.hlean +++ b/pointed.hlean @@ -33,6 +33,12 @@ namespace pointed -- apply equiv_eq_closed_right, exact !idp_con⁻¹ } -- end + definition ppcompose_left_pid [constructor] (A B : Type*) : ppcompose_left (pid B) ~* pid (ppmap A B) := + phomotopy_mk_ppmap (λf, pid_pcompose f) (!trans_refl ⬝ !phomotopy_of_eq_of_phomotopy⁻¹) + + definition ppcompose_right_pid [constructor] (A B : Type*) : ppcompose_right (pid A) ~* pid (ppmap A B) := + phomotopy_mk_ppmap (λf, pcompose_pid f) (!trans_refl ⬝ !phomotopy_of_eq_of_phomotopy⁻¹) + /- 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)⁻¹ᵉ*