From 00e01fd2a66935b32cae120150c5ab95980039f9 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 18 Jan 2017 23:19:00 +0100 Subject: [PATCH] feat(homotopy): prove adjunction between smash product and pointed maps also develop library for equality reasoning on pointed homotopies. Also do the renamings like homomorphism -> is_mul_hom --- algebra/quotient_group.hlean | 16 +- homotopy/EM.hlean | 4 +- homotopy/degree.hlean | 2 +- homotopy/pushout.hlean | 12 +- homotopy/smash.hlean | 223 +++++++++++++-- homotopy/smash_adjoint.hlean | 508 +++++++++++++++++++++++++++++++++++ homotopy/smash_assoc.hlean | 1 + homotopy/spectrum.hlean | 4 +- move_to_lib.hlean | 274 +++++++++++++++++-- 9 files changed, 983 insertions(+), 61 deletions(-) create mode 100644 homotopy/smash_adjoint.hlean diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean index a00f260..c2e0b2b 100644 --- a/algebra/quotient_group.hlean +++ b/algebra/quotient_group.hlean @@ -249,12 +249,12 @@ namespace group -- FIRST ISOMORPHISM THEOREM -definition kernel_quotient_extension {A B : AbGroup} (f : A →g B) : quotient_ab_group (kernel_subgroup f) →g B := +definition kernel_quotient_extension {A B : AbGroup} (f : A →g B) : quotient_ab_group (kernel_subgroup f) →g B := begin fapply quotient_group_elim f, intro a, intro p, exact p end -definition kernel_quotient_extension_triangle {A B : AbGroup} (f : A →g B) : +definition kernel_quotient_extension_triangle {A B : AbGroup} (f : A →g B) : kernel_quotient_extension f ∘g ab_qg_map (kernel_subgroup f) ~ f := begin intro a, @@ -264,7 +264,7 @@ definition kernel_quotient_extension_triangle {A B : AbGroup} (f : A →g B) : definition is_embedding_kernel_quotient_extension {A B : AbGroup} (f : A →g B) : is_embedding (kernel_quotient_extension f) := begin - fapply is_embedding_homomorphism, + fapply is_embedding_of_is_mul_hom, intro x, note H := is_surjective_ab_qg_map (kernel_subgroup f) x, induction H, induction p, @@ -273,7 +273,7 @@ definition is_embedding_kernel_quotient_extension {A B : AbGroup} (f : A →g B) refine _ ⬝ q, symmetry, rexact kernel_quotient_extension_triangle f a - end + end definition ab_group_quotient_homomorphism (A B : AbGroup)(K : subgroup_rel A)(L : subgroup_rel B) (f : A →g B) (p : Π(a:A), K(a) → L(f a)) : quotient_ab_group K →g quotient_ab_group L := @@ -302,15 +302,15 @@ definition ab_group_triv_kernel_factor {A B C: AbGroup} (f : A →g B)(g : A intro p, intro a, intro q, - fapply p, - exact ab_group_kernel_factor f g H a q + fapply p, + exact ab_group_kernel_factor f g H a q end definition triv_kern_is_embedding {A B : AbGroup} (f : A →g B): is_trivial_subgroup _ (kernel_subgroup(f)) → is_embedding(f) := begin intro p, - fapply is_embedding_homomorphism, + fapply is_embedding_of_is_mul_hom, intro a q, apply p, exact q @@ -366,7 +366,7 @@ exact is_surjective_image_lift f definition is_embedding_kernel_quotient_to_image {A B : AbGroup} (f : A →g B) : is_embedding (ab_group_kernel_quotient_to_image f) := begin - fapply @is_embedding_factor _ (image f) B _ _ _ (ab_group_kernel_quotient_to_image f) (image_incl f) (kernel_quotient_extension f), + fapply @is_embedding_factor _ (image f) B _ _ _ (ab_group_kernel_quotient_to_image f) (image_incl f) (kernel_quotient_extension f), exact ab_group_kernel_quotient_to_image_triangle f, exact is_embedding_kernel_quotient_extension f end diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean index 9c1d300..495d1c9 100644 --- a/homotopy/EM.hlean +++ b/homotopy/EM.hlean @@ -262,7 +262,7 @@ namespace EM (ptrunc_elim_ptrunc_functor ((succ n).+1) _ _)⁻¹*, apply ptrunc_elim_phomotopy, refine _ ⬝* !psusp_elim_psusp_functor⁻¹*, - refine _ ⬝* psusp_elim_phomotopy (IH _ _ _ _ _ (is_homomorphism_EM_up eX rX) _ (@is_conn_loop _ _ H1) + refine _ ⬝* psusp_elim_phomotopy (IH _ _ _ _ _ (is_mul_hom_EM_up eX rX) _ (@is_conn_loop _ _ H1) (@is_trunc_loop _ _ H2) _ _ (EM_up_natural φ f eX eY p)), apply psusp_elim_natural } end @@ -347,7 +347,7 @@ namespace EM -- { exact EM1_pmap e⁻¹ᵉ* (equiv.inv_preserve_binary e concat mul r) }, -- rewrite [EMadd1_succ], -- exact ptrunc.elim ((succ n).+1) - -- (psusp.elim (f _ (EM_up e) (is_homomorphism_EM_up e r) _ _)), + -- (psusp.elim (f _ (EM_up e) (is_mul_hom_EM_up e r) _ _)), -- end -- definition is_set_pmap_ptruncconntype {n : ℕ₋₂} (X Y : (n.+1)-Type*[n]) : is_set (X →* Y) := diff --git a/homotopy/degree.hlean b/homotopy/degree.hlean index 7d44180..3658a37 100644 --- a/homotopy/degree.hlean +++ b/homotopy/degree.hlean @@ -5,7 +5,7 @@ open fin eq equiv group algebra sphere.ops pointed nat int trunc is_equiv functi definition eq_one_or_eq_neg_one_of_mul_eq_one {n : ℤ} (m : ℤ) (p : n * m = 1) : n = 1 ⊎ n = -1 := sorry - definition endomorphism_int_unbundled (f : ℤ → ℤ) [is_add_homomorphism f] (n : ℤ) : + definition endomorphism_int_unbundled (f : ℤ → ℤ) [is_add_hom f] (n : ℤ) : f n = f 1 * n := begin induction n using rec_nat_on with n IH n IH, diff --git a/homotopy/pushout.hlean b/homotopy/pushout.hlean index 0be70a0..6b6d76e 100644 --- a/homotopy/pushout.hlean +++ b/homotopy/pushout.hlean @@ -10,9 +10,17 @@ namespace pushout {TL' BL' TR' : Type*} {f' : TL' →* BL'} {g' : TL' →* TR'} (tl : TL ≃ TL') (bl : BL ≃* BL') (tr : TR ≃ TR') (fh : bl ∘ f ~ f' ∘ tl) (gh : tr ∘ g ~ g' ∘ tl) - include fh gh - definition ppushout_pequiv : ppushout f g ≃* ppushout f' g' := + definition ppushout_functor [constructor] (tl : TL → TL') (bl : BL →* BL') (tr : TR → TR') + (fh : bl ∘ f ~ f' ∘ tl) (gh : tr ∘ g ~ g' ∘ tl) : ppushout f g →* ppushout f' g' := + begin + fconstructor, + { exact pushout.functor tl bl tr fh gh }, + { exact ap inl (respect_pt bl) }, + end + + definition ppushout_pequiv (tl : TL ≃ TL') (bl : BL ≃* BL') (tr : TR ≃ TR') + (fh : bl ∘ f ~ f' ∘ tl) (gh : tr ∘ g ~ g' ∘ tl) : ppushout f g ≃* ppushout f' g' := pequiv_of_equiv (pushout.equiv _ _ _ _ tl bl tr fh gh) (ap inl (respect_pt bl)) end diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean index cade84a..46b0b7e 100644 --- a/homotopy/smash.hlean +++ b/homotopy/smash.hlean @@ -11,22 +11,184 @@ open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops w /- To prove: associative, A ∧ S¹ ≃ ΣA -/ -variables {A B C D : Type*} +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 := + begin + fapply pushout.functor, + { exact sum_functor f g }, + { exact prod_functor f g }, + { exact 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 [constructor] (f : A →* C) (g : B →* D) : A ∧ B →* C ∧ D := + begin + fapply pmap.mk, + { exact smash_functor' f g }, + { exact ap inl (prod_eq (respect_pt f) (respect_pt g)) }, + end + + definition functor_gluel (f : A →* C) (g : B →* D) (a : A) : + ap (smash_functor f g) (gluel a) = ap (smash.mk (f a)) (respect_pt g) ⬝ gluel (f a) := + begin + refine !pushout.elim_glue ⬝ _, esimp, apply whisker_right, + induction D with D d₀, induction g with g g₀, esimp at *, induction g₀, reflexivity + end + + definition functor_gluer (f : A →* C) (g : B →* D) (b : B) : + ap (smash_functor f g) (gluer b) = ap (λc, smash.mk c (g b)) (respect_pt f) ⬝ gluer (g b) := + begin + refine !pushout.elim_glue ⬝ _, esimp, apply whisker_right, + induction C with C c₀, induction f with f f₀, esimp at *, induction f₀, reflexivity + end + + definition functor_gluel' (f : A →* C) (g : B →* D) (a a' : A) : + ap (smash_functor f g) (gluel' a a') = ap (smash.mk (f a)) (respect_pt g) ⬝ + gluel' (f a) (f a') ⬝ (ap (smash.mk (f a')) (respect_pt g))⁻¹ := + begin + refine !ap_con ⬝ !functor_gluel ◾ (!ap_inv ⬝ !functor_gluel⁻²) ⬝ _, + refine whisker_left _ !con_inv ⬝ _, + refine !con.assoc⁻¹ ⬝ _, apply whisker_right, + apply con.assoc + end + + definition functor_gluer' (f : A →* C) (g : B →* D) (b b' : B) : + ap (smash_functor f g) (gluer' b b') = ap (λc, smash.mk c (g b)) (respect_pt f) ⬝ + gluer' (g b) (g b') ⬝ (ap (λc, smash.mk c (g b')) (respect_pt f))⁻¹ := + begin + refine !ap_con ⬝ whisker_left _ !ap_inv ⬝ _, + refine !functor_gluer ◾ !functor_gluer⁻² ⬝ _, + refine whisker_left _ !con_inv ⬝ _, + refine !con.assoc⁻¹ ⬝ _, apply whisker_right, + apply con.assoc + end + + /- the statements of the above rules becomes easier if one of the functions respects the basepoint + by reflexivity -/ + definition functor_gluel'2 {D : Type} (f : A →* C) (g : B → D) (a a' : A) : + ap (smash_functor f (pmap_of_map g pt)) (gluel' a a') = gluel' (f a) (f a') := + begin + refine !ap_con ⬝ whisker_left _ !ap_inv ⬝ _, + refine (!functor_gluel ⬝ !idp_con) ◾ (!functor_gluel ⬝ !idp_con)⁻² + end + + definition functor_gluer'2 {C : Type} (f : A → C) (g : B →* D) (b b' : B) : + ap (smash_functor (pmap_of_map f pt) g) (gluer' b b') = gluer' (g b) (g b') := + begin + refine !ap_con ⬝ whisker_left _ !ap_inv ⬝ _, + refine (!functor_gluer ⬝ !idp_con) ◾ (!functor_gluer ⬝ !idp_con)⁻² + end + + lemma functor_gluel'2_same {D : Type} (f : A →* C) (g : B → D) (a : A) : + functor_gluel'2 f (pmap_of_map g pt) a a = + ap02 (smash_functor f (pmap_of_map g pt)) (con.right_inv (gluel a)) ⬝ + (con.right_inv (gluel (f a)))⁻¹ := + begin + refine _ ⬝ whisker_right _ (eq_top_of_square (!ap_con_right_inv_sq))⁻¹, + refine _ ⬝ whisker_right _ !con_idp⁻¹, + refine _ ⬝ !con.assoc⁻¹, + apply whisker_left, + apply eq_con_inv_of_con_eq, symmetry, + apply con_right_inv_natural + end + + lemma functor_gluer'2_same {C : Type} (f : A → C) (g : B →* D) (b : B) : + functor_gluer'2 (pmap_of_map f pt) g b b = + ap02 (smash_functor (pmap_of_map f pt) g) (con.right_inv (gluer b)) ⬝ + (con.right_inv (gluer (g b)))⁻¹ := + begin + refine _ ⬝ whisker_right _ (eq_top_of_square (!ap_con_right_inv_sq))⁻¹, + refine _ ⬝ whisker_right _ !con_idp⁻¹, + refine _ ⬝ !con.assoc⁻¹, + apply whisker_left, + apply eq_con_inv_of_con_eq, symmetry, + 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 + intro x, induction x with a b a b, + { reflexivity }, + { reflexivity }, + { reflexivity }, + { apply eq_pathover, apply hdeg_square, + refine !functor_gluel ⬝ _ ⬝ (ap_compose (smash_functor f' g') _ _)⁻¹, + refine whisker_right _ !ap_con ⬝ !con.assoc ⬝ _ ⬝ ap02 _ !functor_gluel⁻¹, + refine (!ap_compose'⁻¹ ⬝ !ap_compose') ◾ proof !functor_gluel⁻¹ qed ⬝ !ap_con⁻¹, }, + { apply eq_pathover, apply hdeg_square, + refine !functor_gluer ⬝ _ ⬝ (ap_compose (smash_functor f' g') _ _)⁻¹, + refine whisker_right _ !ap_con ⬝ !con.assoc ⬝ _ ⬝ ap02 _ !functor_gluer⁻¹, + refine (!ap_compose'⁻¹ ⬝ !ap_compose') ◾ proof !functor_gluer⁻¹ qed ⬝ !ap_con⁻¹, } + end + + definition smash_functor_pcompose [constructor] (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 + fapply phomotopy.mk, + { exact smash_functor_pcompose_homotopy f' f g' g }, + { exact abstract begin induction C, induction D, induction E, induction F, + induction f with f f₀, induction f' with f' f'₀, induction g with g g₀, induction g' with g' g'₀, + esimp at *, induction f₀, induction f'₀, induction g₀, induction g'₀, reflexivity end end } + end + + definition smash_functor_phomotopy [constructor] {f f' : A →* C} {g g' : B →* D} + (h₁ : f ~* f') (h₂ : g ~* g') : smash_functor f g ~* smash_functor f' g' := + begin + induction h₁ using phomotopy_rec_on_idp, + induction h₂ using phomotopy_rec_on_idp, + reflexivity + -- fapply phomotopy.mk, + -- { intro x, induction x with a b a b, + -- { exact ap011 smash.mk (h₁ a) (h₂ b) }, + -- { reflexivity }, + -- { reflexivity }, + -- { apply eq_pathover, + -- refine !functor_gluel ⬝ph _ ⬝hp !functor_gluel⁻¹, exact sorry }, + -- { apply eq_pathover, + -- refine !functor_gluer ⬝ph _ ⬝hp !functor_gluer⁻¹, exact sorry }}, + -- { esimp, } + end + + definition smash_functor_phomotopy_refl [constructor] (f : A →* C) (g : B →* D) : + smash_functor_phomotopy (phomotopy.refl f) (phomotopy.refl g) = phomotopy.rfl := + !phomotopy_rec_on_idp_refl ⬝ !phomotopy_rec_on_idp_refl + + definition smash_functor_pid [constructor] (A B : Type*) : smash_functor (pid A) (pid B) ~* pid (A ∧ B) := + begin + fapply phomotopy.mk, + { intro x, induction x with a b a b, + { reflexivity }, + { reflexivity }, + { reflexivity }, + { apply eq_pathover_id_right, apply hdeg_square, exact !functor_gluel ⬝ !idp_con }, + { apply eq_pathover_id_right, apply hdeg_square, exact !functor_gluer ⬝ !idp_con }}, + { reflexivity } + end + + definition smash_functor_pid_pcompose [constructor] (A : Type*) (g' : C →* D) (g : B →* C) + : smash_functor (pid A) (g' ∘* g) ~* smash_functor (pid A) g' ∘* smash_functor (pid A) g := + smash_functor_phomotopy !pid_pcompose⁻¹* phomotopy.rfl ⬝* !smash_functor_pcompose + + definition smash_functor_pcompose_pid [constructor] (B : Type*) (f' : C →* D) (f : A →* C) + : 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_pequiv_smash [constructor] (f : A ≃* C) (g : B ≃* D) : A ∧ B ≃* C ∧ D := begin - fapply pequiv_of_equiv, - { fapply pushout.equiv, - { exact sum_equiv_sum f g }, - { exact prod_equiv_prod f g }, - { reflexivity }, - { 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 }}, - { exact ap inl (prod_eq (respect_pt f) (respect_pt g)) }, + fapply pequiv_of_pmap (smash_functor f g), + apply pushout.is_equiv_functor, + exact to_is_equiv (sum_equiv_sum f g) end end @@ -37,27 +199,51 @@ namespace smash definition smash_pequiv_smash_right [constructor] (A : Type*) (g : B ≃* D) : A ∧ B ≃* A ∧ D := smash_pequiv_smash pequiv.rfl g - - /- smash A B ≃ pcofiber (pprod_of_pwedge A B) -/ - theorem elim_gluel' {P : Type} {Pmk : Πa b, P} {Pl Pr : P} + definition elim_gluel' {P : Type} {Pmk : Πa b, P} {Pl Pr : P} (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (a a' : A) : ap (smash.elim Pmk Pl Pr Pgl Pgr) (gluel' a a') = Pgl a ⬝ (Pgl a')⁻¹ := - !ap_con ⬝ !elim_gluel ◾ (!ap_inv ⬝ !elim_gluel⁻²) + !ap_con ⬝ whisker_left _ !ap_inv ⬝ !elim_gluel ◾ !elim_gluel⁻² - theorem elim_gluer' {P : Type} {Pmk : Πa b, P} {Pl Pr : P} + definition elim_gluer' {P : Type} {Pmk : Πa b, P} {Pl Pr : P} (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (b b' : B) : ap (smash.elim Pmk Pl Pr Pgl Pgr) (gluer' b b') = Pgr b ⬝ (Pgr b')⁻¹ := - !ap_con ⬝ !elim_gluer ◾ (!ap_inv ⬝ !elim_gluer⁻²) + !ap_con ⬝ whisker_left _ !ap_inv ⬝ !elim_gluer ◾ !elim_gluer⁻² - theorem elim'_gluel'_pt {P : Type} {Pmk : Πa b, P} + definition elim_gluel'_same {P : Type} {Pmk : Πa b, P} {Pl Pr : P} + (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (a : A) : + elim_gluel' Pgl Pgr a a = + ap02 (smash.elim Pmk Pl Pr Pgl Pgr) (con.right_inv (gluel a)) ⬝ (con.right_inv (Pgl a))⁻¹ := + begin + refine _ ⬝ whisker_right _ (eq_top_of_square (!ap_con_right_inv_sq))⁻¹, + refine _ ⬝ whisker_right _ !con_idp⁻¹, + refine _ ⬝ !con.assoc⁻¹, + apply whisker_left, + apply eq_con_inv_of_con_eq, symmetry, + apply con_right_inv_natural + end + + definition elim_gluer'_same {P : Type} {Pmk : Πa b, P} {Pl Pr : P} + (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (b : B) : + elim_gluer' Pgl Pgr b b = + ap02 (smash.elim Pmk Pl Pr Pgl Pgr) (con.right_inv (gluer b)) ⬝ (con.right_inv (Pgr b))⁻¹ := + begin + refine _ ⬝ whisker_right _ (eq_top_of_square (!ap_con_right_inv_sq))⁻¹, + refine _ ⬝ whisker_right _ !con_idp⁻¹, + refine _ ⬝ !con.assoc⁻¹, + apply whisker_left, + apply eq_con_inv_of_con_eq, symmetry, + apply con_right_inv_natural + end + + definition elim'_gluel'_pt {P : Type} {Pmk : Πa b, P} (Pgl : Πa : A, Pmk a pt = Pmk pt pt) (Pgr : Πb : B, Pmk pt b = Pmk pt pt) (a : A) (ql : Pgl pt = idp) (qr : Pgr pt = idp) : ap (smash.elim' Pmk Pgl Pgr ql qr) (gluel' a pt) = Pgl a := !elim_gluel' ⬝ whisker_left _ ql⁻² - theorem elim'_gluer'_pt {P : Type} {Pmk : Πa b, P} + definition elim'_gluer'_pt {P : Type} {Pmk : Πa b, P} (Pgl : Πa : A, Pmk a pt = Pmk pt pt) (Pgr : Πb : B, Pmk pt b = Pmk pt pt) (b : B) (ql : Pgl pt = idp) (qr : Pgr pt = idp) : ap (smash.elim' Pmk Pgl Pgr ql qr) (gluer' b pt) = Pgr b := @@ -131,7 +317,8 @@ namespace pushout refine pushout_hcompose_equiv (sum_of_bool A B) (wedge_equiv_pushout_sum A B) _ _ ⬝e _, exact erfl, - intro x, induction x: esimp, + intro x, induction x, + reflexivity, reflexivity, exact bool_of_sum_of_bool, apply pushout_of_equiv_right end diff --git a/homotopy/smash_adjoint.hlean b/homotopy/smash_adjoint.hlean new file mode 100644 index 0000000..a0e45d9 --- /dev/null +++ b/homotopy/smash_adjoint.hlean @@ -0,0 +1,508 @@ +-- Authors: Floris van Doorn +-- in collaboration with Egbert, Stefano, Robin + + +import .smash + +open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc + function red_susp unit sigma + + +namespace smash + + variables {A B C : Type*} + + definition pinl [constructor] (A : Type*) {B : Type*} (b : B) : A →* A ∧ B := + begin + fapply pmap.mk, + { intro a, exact smash.mk a b }, + { exact gluer' b pt } + end + + definition pinl_phomotopy {A B : Type*} {b b' : B} (p : b = b') : pinl A b ~* pinl A b' := + begin + fapply phomotopy.mk, + { exact ap010 (pmap.to_fun ∘ pinl A) p }, + { induction p, apply idp_con } + end + + definition pinr [constructor] {A : Type*} (B : Type*) (a : A) : B →* A ∧ B := + begin + fapply pmap.mk, + { intro b, exact smash.mk a b }, + { exact gluel' a pt } + end + + definition smash_pmap_unit_pt [constructor] (A B : Type*) + : pinl A pt ~* pconst A (A ∧ B) := + begin + fconstructor, + { intro a, exact gluel' a pt }, + { rexact con.right_inv (gluel pt) ⬝ (con.right_inv (gluer pt))⁻¹ } + end + + definition smash_pmap_unit [constructor] (A B : Type*) : B →* ppmap A (A ∧ B) := + begin + fapply pmap.mk, + { exact pinl A }, + { apply eq_of_phomotopy, exact smash_pmap_unit_pt A B } + end + + definition smash_functor_pid_gluer' (A : Type*) {B C : Type*} (b : B) (f : B →* C) : + ap (smash_functor (pid A) f) (gluer' b pt) = gluer' (f b) (f pt) := + begin + rexact functor_gluer'2 (@id A) f b pt + end + + 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 := + begin + fapply phomotopy.mk, + { intro a, reflexivity }, + { refine !idp_con ⬝ _, + induction C with C c₀, induction f with f f₀, esimp at *, + induction f₀, rexact smash_functor_pid_gluer' A b (pmap_of_map f 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 := + begin + induction f with f f₀, induction C with C c₀, 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 }, + { refine whisker_right_idp _ ⬝ph _, + refine ap (λx, _ ⬝ x) _ ⬝ph _, + rotate 1, rexact (functor_gluel'2_same (pid A) f pt), + -- refine whisker_left _ (!con.assoc ⬝ whisker_left _ !con.left_inv ⬝ !con_idp) ⬝ph _, + refine whisker_right _ !idp_con ⬝pv _, + refine !con.assoc⁻¹ ⬝ph _, apply whisker_bl, + refine !con.assoc⁻¹ ⬝ whisker_right _ _ ⬝pv _, + rotate 1, esimp, apply whisker_left_idp_con, + refine !con.assoc ⬝pv _, apply whisker_tl, + refine whisker_right _ !idp_con ⬝pv _, + refine whisker_right _ !whisker_right_idp ⬝pv _, + refine whisker_right _ (!idp_con ⬝ !ap02_con) ⬝ !con.assoc ⬝pv _, + apply whisker_tl, + apply vdeg_square, + refine whisker_right _ !ap_inv ⬝ _, apply inv_con_eq_of_eq_con, + unfold [smash_functor_pid_gluer'], + rexact functor_gluer'2_same (pmap_of_map id (Point A)) (pmap_of_map f pt) pt } + end + + definition smash_pmap_unit_natural {A B C : Type*} (f : B →* C) : + smash_pmap_unit A C ∘* f ~* + ppcompose_left (smash_functor (pid A) f) ∘* smash_pmap_unit A B := + begin + induction A with A a₀, induction B with B b₀, induction C with C c₀, + 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₀) }, + { 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⁻¹, + refine _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹, + refine ap (λx, _ ⬝* phomotopy_of_eq (x ⬝ _)) !pcompose_eq_of_phomotopy ⬝ _, + refine ap (λx, _ ⬝* x) (!phomotopy_of_eq_con ⬝ + ap011 phomotopy.trans !phomotopy_of_eq_of_phomotopy + !phomotopy_of_eq_of_phomotopy ⬝ !trans_refl) ⬝ _, + refine _ ⬝ smash_pmap_unit_pt_natural (pmap_of_map f b₀) ⬝ _, + { exact !trans_refl⁻¹ }, + { exact !refl_trans }} + end + + definition smash_pmap_counit_map [unfold 3] {A B : Type*} (af : A ∧ (ppmap A B)) : B := + begin + induction af with a f a f, + { exact f a }, + { exact pt }, + { exact pt }, + { reflexivity }, + { exact respect_pt f } + end + + definition smash_pmap_counit [constructor] (A B : Type*) : A ∧ (ppmap A B) →* B := + begin + fapply pmap.mk, + { exact smash_pmap_counit_map }, + { reflexivity } + end + + definition smash_pmap_counit_natural {A B C : Type*} (g : B →* C) : + g ∘* smash_pmap_counit A B ~* smash_pmap_counit A C ∘* smash_functor (pid A) (ppcompose_left g) := + begin + symmetry, + fapply phomotopy.mk, + { intro af, induction af with a f a f, + { 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 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 !idp_con ⬝ph _, apply square_of_eq, + refine !idp_con ⬝ !con_inv_cancel_right⁻¹ }}, + { refine !idp_con ⬝ !idp_con ⬝ _, refine _ ⬝ !ap_compose', + refine _ ⬝ !ap_prod_elim⁻¹, esimp, + refine _ ⬝ (ap_is_constant respect_pt _)⁻¹, refine !idp_con⁻¹ } + end + + 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) := + begin + fconstructor, + { intro x, + induction x with a b a b, + { reflexivity }, + { exact gluel pt }, + { exact gluer pt }, + { 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 _, + 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 _, + apply square_of_eq, refine !idp_con ⬝ !inv_con_cancel_right⁻¹ }}, + { refine _ ⬝ !ap_compose', + refine _ ⬝ !ap_prod_elim⁻¹, refine _ ⬝ (ap_is_constant respect_pt _)⁻¹, + rexact (con.right_inv (gluer pt))⁻¹ } + end + + definition smash_pmap_counit_unit_pt [constructor] {A B : Type*} (f : A →* B) : + smash_pmap_counit A B ∘* pinl A f ~* f := + begin + fconstructor, + { intro a, reflexivity }, + { refine !idp_con ⬝ !elim_gluer'⁻¹ } + 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) := + begin + fapply phomotopy_mk_ppmap, + { intro f, exact smash_pmap_counit_unit_pt f }, + { refine !trans_refl ⬝ _, + refine _ ⬝ ap (λx, phomotopy_of_eq (x ⬝ _)) !pcompose_eq_of_phomotopy⁻¹, + refine _ ⬝ !phomotopy_of_eq_con⁻¹, + refine _ ⬝ ap011 phomotopy.trans !phomotopy_of_eq_of_phomotopy⁻¹ + !phomotopy_of_eq_of_phomotopy⁻¹, + refine _ ⬝ !trans_refl⁻¹, + fapply phomotopy_eq, + { intro a, refine !elim_gluel'⁻¹ }, + { esimp, refine whisker_right _ !whisker_right_idp ⬝ _ ⬝ !idp_con⁻¹, + refine whisker_right _ !elim_gluel'_same⁻² ⬝ _ ⬝ !elim_gluer'_same⁻¹⁻², + apply inv_con_eq_of_eq_con, refine !idp_con ⬝ _, esimp, + refine _ ⬝ !ap02_con ⬝ whisker_left _ !ap_inv, + refine !whisker_right_idp ⬝ _, + exact !idp_con }} + end + + definition smash_elim [constructor] {A B C : Type*} (f : A →* ppmap B C) : B ∧ A →* C := + smash_pmap_counit B C ∘* smash_functor (pid B) f + + definition smash_elim_inv [constructor] {A B C : Type*} (g : A ∧ B →* C) : B →* ppmap A C := + ppcompose_left g ∘* smash_pmap_unit A B + + definition smash_elim_left_inv {A B C : Type*} (f : A →* ppmap B C) : smash_elim_inv (smash_elim f) ~* f := + begin + refine !pwhisker_right !ppcompose_left_pcompose ⬝* _, + refine !passoc ⬝* _, + refine !pwhisker_left !smash_pmap_unit_natural⁻¹* ⬝* _, + refine !passoc⁻¹* ⬝* _, + refine !pwhisker_right !smash_pmap_counit_unit ⬝* _, + apply pid_pcompose + end + + definition smash_elim_right_inv {A B C : Type*} (g : A ∧ B →* C) : smash_elim (smash_elim_inv g) ~* g := + begin + refine !pwhisker_left !smash_functor_pid_pcompose ⬝* _, + refine !passoc⁻¹* ⬝* _, + refine !pwhisker_right !smash_pmap_counit_natural⁻¹* ⬝* _, + refine !passoc ⬝* _, + refine !pwhisker_left !smash_pmap_unit_counit ⬝* _, + apply pcompose_pid + end + + 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 } + end + + definition pconst_pcompose_pconst (A B C : Type*) : + pconst_pcompose (pconst A B) = pcompose_pconst (pconst B C) := + idp + + definition symm_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹*⁻¹* = p := + phomotopy_eq (λa, !inv_inv) + begin + induction p using phomotopy_rec_on_idp, induction f with f f₀, induction B with B b₀, esimp at *, + induction f₀, esimp, + end + + definition pconst_pcompose_phomotopy_pconst {A B C : Type*} {f : A →* B} (p : f ~* pconst A B) : + pconst_pcompose f = pwhisker_left (pconst B C) p ⬝* pcompose_pconst (pconst B C) := + begin + assert H : Π(p : pconst A B ~* f), + pconst_pcompose f = pwhisker_left (pconst B C) p⁻¹* ⬝* pcompose_pconst (pconst B C), + { intro p, induction p using phomotopy_rec_on_idp, reflexivity }, + refine H p⁻¹* ⬝ ap (pwhisker_left _) !symm_symm ◾** idp, + end + + 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 f, apply pconst_pcompose }, + { esimp, refine !trans_refl ⬝ _, + refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_eq_of_phomotopy ⬝ + !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹, + apply pconst_pcompose_phomotopy_pconst } + end + + definition smash_elim_natural {A B C C' : Type*} (f : C →* C') + (g : B →* ppmap A C) : f ∘* smash_elim g ~* smash_elim (ppcompose_left f ∘* g) := + begin + refine _ ⬝* pwhisker_left _ !smash_functor_pid_pcompose⁻¹*, + refine !passoc⁻¹* ⬝* pwhisker_right _ _ ⬝* !passoc, + apply smash_pmap_counit_natural + end + + definition smash_elim_inv_natural {A B C C' : Type*} (f : C →* C') + (g : A ∧ B →* C) : ppcompose_left f ∘* smash_elim_inv g ~* smash_elim_inv (f ∘* g) := + begin + refine !passoc⁻¹* ⬝* pwhisker_right _ _, + exact !ppcompose_left_pcompose⁻¹* + end + + definition smash_elim_phomotopy {A B C : Type*} {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 + 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' := + 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) := + begin + induction p using phomotopy_rec_on_idp, + refine ap02 _ !eq_of_phomotopy_refl ⬝ _, + refine !eq_of_phomotopy_refl⁻¹ ⬝ _, + apply ap eq_of_phomotopy, + refine _ ⬝ ap (pwhisker_left _) !smash_functor_phomotopy_refl⁻¹, + 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) := + begin + induction p using phomotopy_rec_on_idp, + refine ap02 _ !eq_of_phomotopy_refl ⬝ _, + refine !eq_of_phomotopy_refl⁻¹ ⬝ _, + apply ap eq_of_phomotopy, + refine _ ⬝ ap (pwhisker_right _) !ppcompose_left_phomotopy_refl⁻¹, + refine !pwhisker_right_refl⁻¹ + end + + 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) := + pmap.mk smash_elim_inv (eq_of_phomotopy !smash_elim_inv_pconst) + + 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) := + begin + fapply phomotopy_mk_ppmap, + { exact smash_elim_natural f }, + { esimp, + refine idp ◾** (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !smash_elim_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_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, + { exact smash_elim }, + { exact smash_elim_inv }, + { intro g, apply eq_of_phomotopy, exact smash_elim_right_inv g }, + { intro f, apply eq_of_phomotopy, exact smash_elim_left_inv f } + 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' A B C) (eq_of_phomotopy (smash_elim_pconst 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) := + begin + refine !passoc⁻¹* ⬝* pwhisker_right _ _, + 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) := + begin + refine _ ⬝* pwhisker_left _ !smash_functor_pid_pcompose⁻¹*, + refine !passoc⁻¹* ⬝* pwhisker_right _ _ ⬝* !passoc, + apply smash_pmap_counit_natural + 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 + + + /- associativity of smash -/ + + definition smash_assoc_elim_equiv (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 A B X)⁻¹ᵉ* + ... ≃* ppmap ((A ∧ B) ∧ C) X : (smash_adjoint_pmap (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_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 + 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_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 (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 }, + -- { }, + -- { } + -- end + + +end smash diff --git a/homotopy/smash_assoc.hlean b/homotopy/smash_assoc.hlean index ab3ceb4..406fcaf 100644 --- a/homotopy/smash_assoc.hlean +++ b/homotopy/smash_assoc.hlean @@ -1,4 +1,5 @@ -- Authors: Floris van Doorn +-- In collaboration with Stefano, Robin import .smash diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index bf041d3..8390f88 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -320,8 +320,8 @@ namespace spectrum | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end local attribute ab_group_LES_of_shomotopy_groups [instance] - definition is_homomorphism_LES_of_shomotopy_groups : - Π(v : +3ℤ), is_homomorphism (cc_to_fn LES_of_shomotopy_groups v) + definition is_mul_hom_LES_of_shomotopy_groups : + Π(v : +3ℤ), is_mul_hom (cc_to_fn LES_of_shomotopy_groups v) | (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 diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 2f3733a..41db314 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -10,9 +10,15 @@ attribute pwedge pushout.symm pushout.equiv pushout.is_equiv_functor [constructo attribute is_succ_add_right is_succ_add_left is_succ_bit0 [constructor] attribute pushout.functor [unfold 16] attribute pushout.transpose [unfold 6] +attribute ap_eq_apd10 [unfold 5] +attribute eq_equiv_eq_symm [constructor] + namespace eq + protected definition homotopy.rfl [reducible] [unfold_full] {A B : Type} {f : A → B} : f ~ f := + homotopy.refl f + definition compose_id {A B : Type} (f : A → B) : f ∘ id ~ f := by reflexivity @@ -32,7 +38,15 @@ namespace eq (r : q = idp) : ap_is_constant p q = ap02 f r ⬝ (con.right_inv (p a))⁻¹ := by cases r; exact !idp_con⁻¹ -end eq + definition con_right_inv_natural {A : Type} {a a' : A} {p p' : a = a'} (q : p = p') : + con.right_inv p = q ◾ q⁻² ⬝ con.right_inv p' := + by induction q; induction p; reflexivity + + definition whisker_right_ap {A B : Type} {a a' : A}{b₁ b₂ b₃ : B} (q : b₂ = b₃) (f : A → b₁ = b₂) + (p : a = a') : whisker_right q (ap f p) = ap (λa, f a ⬝ q) p := + by induction p; reflexivity + +end eq open eq namespace cofiber @@ -53,9 +67,13 @@ end wedge namespace pointed + definition phomotopy_of_eq_idp {A B : Type*} (f : A →* B) : phomotopy_of_eq idp = phomotopy.refl f := + idp + definition to_fun_pequiv_trans {X Y Z : Type*} (f : X ≃* Y) (g :Y ≃* Z) : f ⬝e* g ~ g ∘ f := λx, idp + -- replace pcompose2 with this definition pcompose2' {A B C : Type*} {g g' : B →* C} {f f' : A →* B} (q : g ~* g') (p : f ~* f') : g ∘* f ~* g' ∘* f' := pwhisker_right f q ⬝* pwhisker_left g' p @@ -147,6 +165,207 @@ namespace pointed (p : k ∘ f ~ g ∘ h) : h ∘ f⁻¹ᵉ ~ g⁻¹ᵉ ∘ k := λb, eq_inv_of_eq ((p (f⁻¹ᵉ b))⁻¹ ⬝ ap k (to_right_inv f b)) + definition phomotopy_of_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) : + phomotopy_of_eq (eq_of_phomotopy p) = p := + to_right_inv (pmap_eq_equiv f g) p + + definition ap_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) (a : A) : + ap (λf : A →* B, f a) (eq_of_phomotopy p) = p a := + ap010 to_homotopy (phomotopy_of_eq_of_phomotopy p) a + + definition phomotopy_rec_on_eq [recursor] {A B : Type*} {f g : A →* B} + {Q : (f ~* g) → Type} (p : f ~* g) (H : Π(q : f = g), Q (phomotopy_of_eq q)) : Q p := + phomotopy_of_eq_of_phomotopy p ▸ H (eq_of_phomotopy p) + + definition phomotopy_rec_on_idp [recursor] {A B : Type*} {f : A →* B} + {Q : Π{g}, (f ~* g) → Type} {g : A →* B} (p : f ~* g) (H : Q (phomotopy.refl f)) : Q p := + begin + induction p using phomotopy_rec_on_eq, + induction q, exact H + end + + definition phomotopy_rec_on_eq_phomotopy_of_eq {A B : Type*} {f g: A →* B} + {Q : (f ~* g) → Type} (p : f = g) (H : Π(q : f = g), Q (phomotopy_of_eq q)) : + phomotopy_rec_on_eq (phomotopy_of_eq p) H = H p := + begin + unfold phomotopy_rec_on_eq, + refine ap (λp, p ▸ _) !adj ⬝ _, + refine !tr_compose⁻¹ ⬝ _, + apply apdt + end + + definition phomotopy_rec_on_idp_refl {A B : Type*} (f : A →* B) + {Q : Π{g}, (f ~* g) → Type} (H : Q (phomotopy.refl f)) : + phomotopy_rec_on_idp phomotopy.rfl H = H := + !phomotopy_rec_on_eq_phomotopy_of_eq + + definition phomotopy_eq_equiv {A B : Type*} {f g : A →* B} (h k : f ~* g) : + (h = k) ≃ Σ(p : to_homotopy h ~ to_homotopy k), + whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h := + calc + h = k ≃ phomotopy.sigma_char _ _ h = phomotopy.sigma_char _ _ k + : eq_equiv_fn_eq (phomotopy.sigma_char f g) h k + ... ≃ Σ(p : to_homotopy h = to_homotopy k), + pathover (λp, p pt ⬝ respect_pt g = respect_pt f) (to_homotopy_pt h) p (to_homotopy_pt k) + : sigma_eq_equiv _ _ + ... ≃ Σ(p : to_homotopy h = to_homotopy k), + to_homotopy_pt h = ap (λq, q pt ⬝ respect_pt g) p ⬝ to_homotopy_pt k + : sigma_equiv_sigma_right (λp, eq_pathover_equiv_Fl p (to_homotopy_pt h) (to_homotopy_pt k)) + ... ≃ Σ(p : to_homotopy h = to_homotopy k), + ap (λq, q pt ⬝ respect_pt g) p ⬝ to_homotopy_pt k = to_homotopy_pt h + : sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _) + ... ≃ Σ(p : to_homotopy h = to_homotopy k), + whisker_right (respect_pt g) (apd10 p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h + : sigma_equiv_sigma_right (λp, equiv_eq_closed_left _ (whisker_right _ !whisker_right_ap⁻¹)) + ... ≃ Σ(p : to_homotopy h ~ to_homotopy k), + whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h + : sigma_equiv_sigma_left' eq_equiv_homotopy + + definition phomotopy_eq {A B : Type*} {f g : A →* B} {h k : f ~* g} (p : to_homotopy h ~ to_homotopy k) + (q : whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h) : h = k := + to_inv (phomotopy_eq_equiv h k) ⟨p, q⟩ + + definition phomotopy_eq' {A B : Type*} {f g : A →* B} {h k : f ~* g} (p : to_homotopy h ~ to_homotopy k) + (q : square (to_homotopy_pt h) (to_homotopy_pt k) (whisker_right (respect_pt g) (p pt)) idp) : h = k := + phomotopy_eq p (eq_of_square q)⁻¹ + + definition eq_of_phomotopy_refl {X Y : Type*} (f : X →* Y) : + eq_of_phomotopy (phomotopy.refl f) = idpath f := + begin + 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₀, + induction f with f f₀, induction g with g g₀, induction p with p p₀, + esimp at *, induction g₀, induction p₀, + reflexivity + end + + definition refl_trans {A B : Type*} {f g : A →* B} (p : f ~* g) : phomotopy.refl f ⬝* p = p := + begin + induction p using phomotopy_rec_on_idp, + induction A with A a₀, induction B with B b₀, + induction f with f f₀, esimp at *, induction f₀, + reflexivity + end + + definition trans_assoc {A B : Type*} {f g h i : A →* B} (p : f ~* g) (q : g ~* h) + (r : h ~* i) : p ⬝* q ⬝* r = p ⬝* (q ⬝* r) := + begin + 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 f with f f₀, esimp at *, induction f₀, + reflexivity + 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 + + infixl ` ◾** `:80 := pointed.trans2 + + definition phwhisker_left {A B : Type*} {f g h : A →* B} (p : f ~* g) {q q' : g ~* h} + (s : q = q') : p ⬝* q = p ⬝* q' := + idp ◾** s + + definition phwhisker_right {A B : Type*} {f g h : A →* B} {p p' : f ~* g} (q : g ~* h) + (r : p = p') : p ⬝* q = p' ⬝* q := + r ◾** idp + + 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 + + definition pcompose_eq_of_phomotopy {A B C : Type*} (g : B →* C) {f f' : A →* B} (H : f ~* f') : + ap (λf, g ∘* f) (eq_of_phomotopy H) = eq_of_phomotopy (pwhisker_left g H) := + begin + induction H using phomotopy_rec_on_idp, + refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _, + exact !pwhisker_left_refl⁻¹ + end + + definition respect_pt_pcompose {A B C : Type*} (g : B →* C) (f : A →* B) + : respect_pt (g ∘* f) = ap g (respect_pt f) ⬝ respect_pt g := + idp + + definition phomotopy_mk_ppmap [constructor] {A B C : Type*} {f g : A →* ppmap B C} (p : Πa, f a ~* g a) + (q : p pt ⬝* phomotopy_of_eq (respect_pt g) = phomotopy_of_eq (respect_pt f)) + : f ~* g := + begin + 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, + end + + definition pcompose_pconst_pcompose {A B C D : Type*} (h : C →* D) (g : B →* C) : + pcompose_pconst (h ∘* g) = + passoc h g (pconst A B) ⬝* (pwhisker_left h (pcompose_pconst g) ⬝* pcompose_pconst h) := + begin + fapply phomotopy_eq, + { intro a, exact !idp_con⁻¹ }, + { induction h with h h₀, induction g with g g₀, induction D with D d₀, induction C with C c₀, + esimp at *, induction g₀, induction h₀, reflexivity } + end + + definition ppcompose_left_pcompose [constructor] {A B C D : Type*} (h : C →* D) (g : B →* C) : + @ppcompose_left A _ _ (h ∘* g) ~* ppcompose_left h ∘* ppcompose_left g := + begin + fapply phomotopy_mk_ppmap, + { exact passoc h g }, + { esimp, + refine ap (λx, _ ⬝* x) (!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)⁻¹ } + end + + definition pcompose_pconst_phomotopy {A B C : Type*} {f f' : B →* C} (p : f ~* f') : + pwhisker_right (pconst A B) p ⬝* pcompose_pconst f' = pcompose_pconst f := + begin + fapply phomotopy_eq, + { intro a, exact to_homotopy_pt p }, + { induction p using phomotopy_rec_on_idp, induction C with C c₀, induction f with f f₀, + esimp at *, induction f₀, reflexivity } + 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 + induction p using phomotopy_rec_on_idp, + reflexivity + end + /- a more explicit proof of ppcompose_left_phomotopy, which might be useful if we need to prove properties about it + -/ + -- fapply phomotopy_mk_ppmap, + -- { intro f, exact pwhisker_right f p }, + -- { refine ap (λx, _ ⬝* x) !phomotopy_of_eq_of_phomotopy ⬝ _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹, + -- exact pcompose_pconst_phomotopy p } + + definition ppcompose_left_phomotopy_refl {A B C : Type*} (g : B →* C) : + ppcompose_left_phomotopy (phomotopy.refl g) = phomotopy.refl (@ppcompose_left A _ _ g) := + !phomotopy_rec_on_idp_refl + end pointed open pointed namespace trunc @@ -200,6 +419,9 @@ end is_equiv namespace prod + definition pprod_functor [constructor] {A B C D : Type*} (f : A →* C) (g : B →* D) : A ×* B →* C ×* D := + pmap.mk (prod_functor f g) (prod_eq (respect_pt f) (respect_pt g)) + open prod.ops definition prod_pathover_equiv {A : Type} {B C : A → Type} {a a' : A} (p : a = a') (x : B a × C a) (x' : B a' × C a') : x =[p] x' ≃ x.1 =[p] x'.1 × x.2 =[p] x'.2 := @@ -317,44 +539,40 @@ namespace group -- some extra instances for type class inference - -- definition is_homomorphism_comm_homomorphism [instance] {G G' : AbGroup} (φ : G →g G') - -- : @is_homomorphism G G' (@ab_group.to_group _ (AbGroup.struct G)) + -- definition is_mul_hom_comm_homomorphism [instance] {G G' : AbGroup} (φ : G →g G') + -- : @is_mul_hom G G' (@ab_group.to_group _ (AbGroup.struct G)) -- (@ab_group.to_group _ (AbGroup.struct G')) φ := -- homomorphism.struct φ - -- definition is_homomorphism_comm_homomorphism1 [instance] {G G' : AbGroup} (φ : G →g G') - -- : @is_homomorphism G G' _ + -- definition is_mul_hom_comm_homomorphism1 [instance] {G G' : AbGroup} (φ : G →g G') + -- : @is_mul_hom G G' _ -- (@ab_group.to_group _ (AbGroup.struct G')) φ := -- homomorphism.struct φ - -- definition is_homomorphism_comm_homomorphism2 [instance] {G G' : AbGroup} (φ : G →g G') - -- : @is_homomorphism G G' (@ab_group.to_group _ (AbGroup.struct G)) _ φ := + -- definition is_mul_hom_comm_homomorphism2 [instance] {G G' : AbGroup} (φ : G →g G') + -- : @is_mul_hom G G' (@ab_group.to_group _ (AbGroup.struct G)) _ φ := -- homomorphism.struct φ end group open group -namespace pi -- move to types.arrow +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_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 := - begin - cases f with f p, esimp [pmap_eq], - refine apd011 (apd011 pmap.mk) !eq_of_homotopy_idp _, - induction Y with Y y0, esimp at *, induction p, esimp, exact sorry - end + 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 @@ -373,7 +591,7 @@ namespace pi -- move to types.arrow { apply pmap_eq_idp} end -end pi open pi +end pointed open pointed namespace eq @@ -686,7 +904,7 @@ namespace category theorem Group_eq_equiv_lemma {G H : Group} (p : (Group.sigma_char2 G).1 = (Group.sigma_char2 H).1) : ((Group.sigma_char2 G).2 =[p] (Group.sigma_char2 H).2) ≃ - (is_homomorphism (equiv_of_eq (proof p qed : Group.carrier G = Group.carrier H))) := + (is_mul_hom (equiv_of_eq (proof p qed : Group.carrier G = Group.carrier H))) := begin refine !sigma_pathover_equiv_of_is_prop ⬝e _, induction G with G g, induction H with H h, @@ -697,7 +915,7 @@ namespace category (Group.sigma_char2 (Group.mk G (group.mk μ σ μa ε εμ με ι μι))).2.2 end - definition isomorphism.sigma_char (G H : Group) : (G ≃g H) ≃ Σ(e : G ≃ H), is_homomorphism e := + definition isomorphism.sigma_char (G H : Group) : (G ≃g H) ≃ Σ(e : G ≃ H), is_mul_hom e := begin fapply equiv.MK, { intro φ, exact ⟨equiv_of_isomorphism φ, to_respect_mul φ⟩ }, @@ -712,7 +930,7 @@ namespace category refine !sigma_eq_equiv ⬝e _, refine sigma_equiv_sigma_right Group_eq_equiv_lemma ⬝e _, transitivity (Σ(e : (Group.sigma_char2 G).1 ≃ (Group.sigma_char2 H).1), - @is_homomorphism _ _ _ _ (to_fun e)), apply sigma_ua, + @is_mul_hom _ _ _ _ (to_fun e)), apply sigma_ua, exact !isomorphism.sigma_char⁻¹ᵉ end