diff --git a/colim.hlean b/colim.hlean index 9a6bb9d..5aaf1b5 100644 --- a/colim.hlean +++ b/colim.hlean @@ -363,7 +363,7 @@ namespace seq_colim (q : prep0 f n (Point (A 0)) = Point (A n)) : loop_equiv_eq_closed (ap (@f n) q ⬝ respect_pt (@f n)) (ap (@f n) p) = Ω→(@f n) (loop_equiv_eq_closed q p) := - by rewrite [▸*, con_inv, +ap_con, ap_inv, +con.assoc] + by rewrite [▸*, con_inv, ↑ap1_gen, +ap_con, ap_inv, +con.assoc] definition succ_add_tr_rep {n : ℕ} (k : ℕ) (x : A n) : transport A (succ_add n k) (rep f k (f x)) = rep f (succ k) x := diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean index d062ac0..4fc57e2 100644 --- a/homotopy/cohomology.hlean +++ b/homotopy/cohomology.hlean @@ -49,8 +49,8 @@ definition ap1_pmap_mul {X Y : Type*} (f g : X →* Ω Y) : begin fconstructor, { intro p, esimp, - refine ap1_gen_con_left p (respect_pt f) (respect_pt f) - (respect_pt g) (respect_pt g) ⬝ _, + refine ap1_gen_con_left (respect_pt f) (respect_pt f) + (respect_pt g) (respect_pt g) p ⬝ _, refine !whisker_right_idp ◾ !whisker_left_idp2, }, { refine !con.assoc ⬝ _, refine _ ◾ idp ⬝ _, rotate 1, diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean index b57168e..58659c7 100644 --- a/homotopy/smash.hlean +++ b/homotopy/smash.hlean @@ -510,7 +510,7 @@ namespace smash idp (smash_functor_pconst_right_homotopy (λ a, f' (f a)) x) (ap (smash_functor' (pmap.mk f' (refl (f' (f a₀)))) (pmap.mk g (refl (g d₀)))) - (smash_functor_pconst_right_homotopy f x)) := + (smash_functor_pconst_right_homotopy f x)) := begin induction x with a b a b, { refine _ ⬝hp (functor_gluel'2 f' g (f a) (f a₀))⁻¹, exact hrfl }, diff --git a/homotopy/smash_adjoint.hlean b/homotopy/smash_adjoint.hlean index 52fb13a..1c129a0 100644 --- a/homotopy/smash_adjoint.hlean +++ b/homotopy/smash_adjoint.hlean @@ -2,10 +2,10 @@ -- in collaboration with Egbert, Stefano, Robin, Ulrik /- the adjunction between the smash product and pointed maps -/ -import .smash +import .smash .susp open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc - function red_susp unit sigma + function red_susp unit sigma susp namespace smash @@ -214,7 +214,7 @@ namespace smash refine _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹ ◾** !phomotopy_of_eq_of_phomotopy⁻¹, refine _ ⬝ !trans_refl⁻¹, fapply phomotopy_eq, - { intro a, refine !elim_gluel'⁻¹ }, + { intro a, esimp, 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, @@ -392,7 +392,7 @@ namespace smash apply smash_pmap_counit_natural_right end - definition smash_adjoint_pmap_inv_natural_right [constructor] {A B C C' : Type*} (f : C →* C') : + 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 ~* smash_adjoint_pmap_inv A B C' ∘* ppcompose_left (ppcompose_left f) := smash_pelim_natural_right f @@ -504,4 +504,29 @@ namespace smash rexact phomotopy_of_eq ((smash_assoc_elim_equiv_natural_left _ f g h)⁻¹ʰ* !pid)⁻¹ end + /- Corollary 2: smashing with a suspension -/ + definition smash_psusp_elim_equiv (A B X : Type*) : + ppmap (A ∧ psusp B) X ≃* ppmap (psusp (A ∧ B)) X := + calc + ppmap (A ∧ psusp B) X ≃* ppmap (psusp B) (ppmap A X) : smash_adjoint_pmap A (psusp B) X + ... ≃* ppmap B (Ω (ppmap A X)) : psusp_adjoint_loop' B (ppmap A X) + ... ≃* ppmap B (ppmap A (Ω X)) : pequiv_ppcompose_left (loop_pmap_commute A X) + ... ≃* ppmap (A ∧ B) (Ω X) : smash_adjoint_pmap A B (Ω X) + ... ≃* ppmap (psusp (A ∧ B)) X : psusp_adjoint_loop' (A ∧ B) X + + definition loop_pmap_commute_natural_right (A : Type*) (f : X →* X') : + psquare (loop_pmap_commute A X) (loop_pmap_commute A X') + (Ω→ (ppcompose_left f)) (ppcompose_left (Ω→ f)) := + sorry + + + definition smash_psusp_elim_equiv_natural_right (A B : Type*) (f : X →* X') : + psquare (smash_psusp_elim_equiv A B X) (smash_psusp_elim_equiv A B X') + (ppcompose_left f) (ppcompose_left f) := + smash_adjoint_pmap_natural_right f ⬝h* + psusp_adjoint_loop_natural_right (ppcompose_left f) ⬝h* + ppcompose_left_psquare (loop_pmap_commute_natural_right A f) ⬝h* + (smash_adjoint_pmap_natural_right (Ω→ f))⁻¹ʰ* ⬝h* + (psusp_adjoint_loop_natural_right f)⁻¹ʰ* + end smash diff --git a/homotopy/susp.hlean b/homotopy/susp.hlean new file mode 100644 index 0000000..17c0da3 --- /dev/null +++ b/homotopy/susp.hlean @@ -0,0 +1,137 @@ +import ..pointed + +open susp eq pointed function is_equiv + variables {X X' Y Y' Z : Type*} + +-- move + definition pap1 [constructor] (X Y : Type*) : ppmap X Y →* ppmap (Ω X) (Ω Y) := + pmap.mk ap1 (eq_of_phomotopy !ap1_pconst) + + definition ap1_gen_const {A B : Type} {a₁ a₂ : A} (b : B) (p : a₁ = a₂) : + ap1_gen (const A b) idp idp p = idp := + ap1_gen_idp_left (const A b) p ⬝ ap_constant p b + + definition ap1_gen_compose_const_left + {A B C : Type} (c : C) (f : A → B) {a₁ a₂ : A} (p : a₁ = a₂) : + ap1_gen_compose (const B c) f idp idp idp idp p ⬝ + ap1_gen_const c (ap1_gen f idp idp p) = + ap1_gen_const c p := + begin induction p, reflexivity end + + definition ap1_gen_compose_const_right + {A B C : Type} (g : B → C) (b : B) {a₁ a₂ : A} (p : a₁ = a₂) : + ap1_gen_compose g (const A b) idp idp idp idp p ⬝ + ap (ap1_gen g idp idp) (ap1_gen_const b p) = + ap1_gen_const (g b) p := + begin induction p, reflexivity end + + definition ap1_pcompose_pconst_left {A B C : Type*} (f : A →* B) : + phsquare (ap1_pcompose (pconst B C) f) + (ap1_pconst A C) + (ap1_phomotopy (pconst_pcompose f)) + (pwhisker_right (Ω→ f) (ap1_pconst B C) ⬝* pconst_pcompose (Ω→ f)) := + 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₀, + refine idp ◾** !trans_refl ⬝ _ ⬝ !refl_trans⁻¹ ⬝ !ap1_phomotopy_refl⁻¹ ◾** idp, + fapply phomotopy_eq, + { exact ap1_gen_compose_const_left c₀ f }, + { reflexivity } + end + + definition ap1_pcompose_pconst_right {A B C : Type*} (g : B →* C) : + phsquare (ap1_pcompose g (pconst A B)) + (ap1_pconst A C) + (ap1_phomotopy (pcompose_pconst g)) + (pwhisker_left (Ω→ g) (ap1_pconst A B) ⬝* pcompose_pconst (Ω→ g)) := + begin + induction A with A a₀, induction B with B b₀, induction C with C c₀, induction g with g g₀, + esimp at *, induction g₀, + refine idp ◾** !trans_refl ⬝ _ ⬝ !refl_trans⁻¹ ⬝ !ap1_phomotopy_refl⁻¹ ◾** idp, + fapply phomotopy_eq, + { exact ap1_gen_compose_const_right g b₀ }, + { reflexivity } + end + + definition pap1_natural_left [constructor] (f : X' →* X) : + psquare (pap1 X Y) (pap1 X' Y) (ppcompose_right f) (ppcompose_right (Ω→ f)) := + begin + fapply phomotopy_mk_ppmap, + { intro g, exact !ap1_pcompose⁻¹* }, + { refine idp ◾** (ap phomotopy_of_eq (!ap1_eq_of_phomotopy ◾ idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ + !phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ (ap phomotopy_of_eq (!pcompose_right_eq_of_phomotopy ◾ + idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ !phomotopy_of_eq_of_phomotopy)⁻¹, + apply symm_trans_eq_of_eq_trans, exact (ap1_pcompose_pconst_left f)⁻¹ } + end + + definition pap1_natural_right [constructor] (f : Y →* Y') : + psquare (pap1 X Y) (pap1 X Y') (ppcompose_left f) (ppcompose_left (Ω→ f)) := + begin + fapply phomotopy_mk_ppmap, + { intro g, exact !ap1_pcompose⁻¹* }, + { refine idp ◾** (ap phomotopy_of_eq (!ap1_eq_of_phomotopy ◾ idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ + !phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ (ap phomotopy_of_eq (!pcompose_left_eq_of_phomotopy ◾ + idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ !phomotopy_of_eq_of_phomotopy)⁻¹, + apply symm_trans_eq_of_eq_trans, exact (ap1_pcompose_pconst_right f)⁻¹ } + end + +namespace susp + + definition susp_functor_pconst_homotopy [unfold 3] {X Y : Type*} (x : psusp X) : + psusp_functor (pconst X Y) x = pt := + begin + induction x, + { reflexivity }, + { exact (merid pt)⁻¹ }, + { apply eq_pathover, refine !elim_merid ⬝ph _ ⬝hp !ap_constant⁻¹, exact square_of_eq !con.right_inv⁻¹ } + end + + definition susp_functor_pconst [constructor] (X Y : Type*) : psusp_functor (pconst X Y) ~* pconst (psusp X) (psusp Y) := + begin + fapply phomotopy.mk, + { exact susp_functor_pconst_homotopy }, + { reflexivity } + end + + definition psusp_pfunctor [constructor] (X Y : Type*) : ppmap X Y →* ppmap (psusp X) (psusp Y) := + pmap.mk psusp_functor (eq_of_phomotopy !susp_functor_pconst) + + definition psusp_pelim [constructor] (X Y : Type*) : ppmap X (Ω Y) →* ppmap (psusp X) Y := + ppcompose_left (loop_psusp_counit Y) ∘* psusp_pfunctor X (Ω Y) + + definition loop_psusp_pintro [constructor] (X Y : Type*) : ppmap (psusp X) Y →* ppmap X (Ω Y) := + ppcompose_right (loop_psusp_unit X) ∘* pap1 (psusp X) Y + + definition loop_psusp_pintro_natural_left (f : X' →* X) : + psquare (loop_psusp_pintro X Y) (loop_psusp_pintro X' Y) + (ppcompose_right (psusp_functor f)) (ppcompose_right f) := + !pap1_natural_left ⬝h* ppcompose_right_psquare (loop_psusp_unit_natural f)⁻¹* + + definition loop_psusp_pintro_natural_right (f : Y →* Y') : + psquare (loop_psusp_pintro X Y) (loop_psusp_pintro X Y') + (ppcompose_left f) (ppcompose_left (Ω→ f)) := + !pap1_natural_right ⬝h* !ppcompose_left_ppcompose_right⁻¹* + + definition is_equiv_loop_psusp_pintro [constructor] (X Y : Type*) : + is_equiv (loop_psusp_pintro X Y) := + begin + fapply adjointify, + { exact psusp_pelim X Y }, + { intro g, apply eq_of_phomotopy, exact psusp_adjoint_loop_right_inv g }, + { intro f, apply eq_of_phomotopy, exact psusp_adjoint_loop_left_inv f } + end + + definition psusp_adjoint_loop' [constructor] (X Y : Type*) : ppmap (psusp X) Y ≃* ppmap X (Ω Y) := + pequiv_of_pmap (loop_psusp_pintro X Y) (is_equiv_loop_psusp_pintro X Y) + + definition psusp_adjoint_loop_natural_right (f : Y →* Y') : + psquare (psusp_adjoint_loop' X Y) (psusp_adjoint_loop' X Y') + (ppcompose_left f) (ppcompose_left (Ω→ f)) := + loop_psusp_pintro_natural_right f + + definition psusp_adjoint_loop_natural_left (f : X' →* X) : + psquare (psusp_adjoint_loop' X Y) (psusp_adjoint_loop' X' Y) + (ppcompose_right (psusp_functor f)) (ppcompose_right f) := + loop_psusp_pintro_natural_left f + +end susp diff --git a/pointed.hlean b/pointed.hlean index 17c867a..e74b29d 100644 --- a/pointed.hlean +++ b/pointed.hlean @@ -10,6 +10,10 @@ open pointed eq equiv function is_equiv unit is_trunc trunc nat algebra group si namespace pointed + definition loop_pequiv_eq_closed [constructor] {A : Type} {a a' : A} (p : a = a') + : pointed.MK (a = a) idp ≃* pointed.MK (a' = a') idp := + pequiv_of_equiv (loop_equiv_eq_closed p) (con.left_inv p) + definition punit_pmap_phomotopy [constructor] {A : Type*} (f : punit →* A) : f ~* pconst punit A := begin fapply phomotopy.mk, @@ -31,16 +35,16 @@ namespace pointed ap010 to_homotopy r a definition ap1_gen_con_left {A B : Type} {a a' : A} {b₀ b₁ b₂ : B} - {f : A → b₀ = b₁} {f' : A → b₁ = b₂} (p : a = a') {q₀ q₁ : b₀ = b₁} {q₀' q₁' : b₁ = b₂} - (r₀ : f a = q₀) (r₁ : f a' = q₁) (r₀' : f' a = q₀') (r₁' : f' a' = q₁') : - ap1_gen (λa, f a ⬝ f' a) p (r₀ ◾ r₀') (r₁ ◾ r₁') = - whisker_right q₀' (ap1_gen f p r₀ r₁) ⬝ whisker_left q₁ (ap1_gen f' p r₀' r₁') := + {f : A → b₀ = b₁} {f' : A → b₁ = b₂} {q₀ q₁ : b₀ = b₁} {q₀' q₁' : b₁ = b₂} + (r₀ : f a = q₀) (r₁ : f a' = q₁) (r₀' : f' a = q₀') (r₁' : f' a' = q₁') (p : a = a') : + ap1_gen (λa, f a ⬝ f' a) (r₀ ◾ r₀') (r₁ ◾ r₁') p = + whisker_right q₀' (ap1_gen f r₀ r₁ p) ⬝ whisker_left q₁ (ap1_gen f' r₀' r₁' p) := begin induction r₀, induction r₁, induction r₀', induction r₁', induction p, reflexivity end definition ap1_gen_con_left_idp {A B : Type} {a : A} {b₀ b₁ b₂ : B} {f : A → b₀ = b₁} {f' : A → b₁ = b₂} {q₀ : b₀ = b₁} {q₁ : b₁ = b₂} (r₀ : f a = q₀) (r₁ : f' a = q₁) : - ap1_gen_con_left idp r₀ r₀ r₁ r₁ = + ap1_gen_con_left r₀ r₀ r₁ r₁ idp = !con.left_inv ⬝ (ap (whisker_right q₁) !con.left_inv ◾ ap (whisker_left _) !con.left_inv)⁻¹ := begin induction r₀, induction r₁, reflexivity end @@ -406,6 +410,22 @@ namespace pointed {r : f ~* h} (s : p ⬝* q = r) : p = r ⬝* q⁻¹* := !trans_refl⁻¹ ⬝ idp ◾** !trans_right_inv⁻¹ ⬝ !trans_assoc⁻¹ ⬝ s ◾** idp + definition eq_trans_of_symm_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} + {r : f ~* h} (s : p⁻¹* ⬝* r = q) : r = p ⬝* q := + !refl_trans⁻¹ ⬝ !trans_right_inv⁻¹ ◾** idp ⬝ !trans_assoc ⬝ idp ◾** s + + definition symm_trans_eq_of_eq_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} + {r : f ~* h} (s : r = p ⬝* q) : p⁻¹* ⬝* r = q := + idp ◾** s ⬝ !trans_assoc⁻¹ ⬝ trans_left_inv p ◾** idp ⬝ !refl_trans + + definition eq_trans_of_trans_symm_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} + {r : f ~* h} (s : r ⬝* q⁻¹* = p) : r = p ⬝* q := + !trans_refl⁻¹ ⬝ idp ◾** !trans_left_inv⁻¹ ⬝ !trans_assoc⁻¹ ⬝ s ◾** idp + + definition trans_symm_eq_of_eq_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} + {r : f ~* h} (s : r = p ⬝* q) : r ⬝* q⁻¹* = p := + s ◾** idp ⬝ !trans_assoc ⬝ idp ◾** trans_right_inv q ⬝ !trans_refl + section phsquare /- Squares of pointed homotopies @@ -425,6 +445,17 @@ namespace pointed definition phsquare_of_eq (p : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂) : phsquare p₁₀ p₁₂ p₀₁ p₂₁ := p definition eq_of_phsquare (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂ := p + definition phsquare.mk (p : Πx, square (p₁₀ x) (p₁₂ x) (p₀₁ x) (p₂₁ x)) + (q : cube (square_of_eq (to_homotopy_pt p₁₀)) (square_of_eq (to_homotopy_pt p₁₂)) + (square_of_eq (to_homotopy_pt p₀₁)) (square_of_eq (to_homotopy_pt p₂₁)) + (p pt) ids) : phsquare p₁₀ p₁₂ p₀₁ p₂₁ := + begin + fapply phomotopy_eq, + { intro x, apply eq_of_square (p x) }, + { generalize p pt, intro r, exact sorry } + end + + definition phhconcat (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (q : phsquare p₃₀ p₃₂ p₂₁ p₄₁) : phsquare (p₁₀ ⬝* p₃₀) (p₁₂ ⬝* p₃₂) p₀₁ p₄₁ := !trans_assoc ⬝ idp ◾** q ⬝ !trans_assoc⁻¹ ⬝ p ◾** idp ⬝ !trans_assoc @@ -565,6 +596,25 @@ namespace pointed exact !pwhisker_right_refl⁻¹ end + definition ap1_phomotopy_refl {X Y : Type*} (f : X →* Y) : + ap1_phomotopy (phomotopy.refl f) = phomotopy.refl (Ω→ f) := + begin + -- induction X with X x₀, induction Y with Y y₀, induction f with f f₀, esimp at *, induction f₀, + -- fapply phomotopy_eq, + -- { intro x, unfold [ap1_phomotopy], }, + -- { } + exact sorry + end + + definition ap1_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) : + ap Ω→ (eq_of_phomotopy p) = eq_of_phomotopy (ap1_phomotopy p) := + begin + induction p using phomotopy_rec_on_idp, + refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _, + exact !ap1_phomotopy_refl⁻¹ + end + + -- duplicate of ap_eq_of_phomotopy definition to_fun_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) (a : A) : ap010 pmap.to_fun (eq_of_phomotopy p) a = p a := begin @@ -726,6 +776,11 @@ namespace pointed (ppcompose_left f₀₁) (ppcompose_left f₂₁) := !ppcompose_left_pcompose⁻¹* ⬝* ppcompose_left_phomotopy p ⬝* !ppcompose_left_pcompose + definition ppcompose_right_psquare {A : Type*} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare (@ppcompose_right _ _ A f₁₂) (ppcompose_right f₁₀) + (ppcompose_right f₂₁) (ppcompose_right f₀₁) := + !ppcompose_right_pcompose⁻¹* ⬝* ppcompose_right_phomotopy p⁻¹* ⬝* !ppcompose_right_pcompose + definition trans_phomotopy_hconcat {f₀₁' f₀₁''} (q₂ : f₀₁'' ~* f₀₁') (q₁ : f₀₁' ~* f₀₁) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : (q₂ ⬝* q₁) ⬝ph* p = q₂ ⬝ph* q₁ ⬝ph* p := @@ -820,22 +875,8 @@ namespace pointed pmap_eq (λx, idpath (f x)) !idp_con⁻¹ = idpath f := ap (λx, eq_of_phomotopy (phomotopy.mk _ x)) !inv_inv ⬝ eq_of_phomotopy_refl f - definition pfunext [constructor] (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) := - begin - fapply pequiv_of_equiv, - { fapply equiv.MK: esimp, - { intro f, fapply pmap_eq, - { intro x, exact f x }, - { exact (respect_pt f)⁻¹ }}, - { intro p, fapply pmap.mk, - { intro x, exact ap010 pmap.to_fun p x }, - { note z := apd respect_pt p, - note z2 := square_of_pathover z, - refine eq_of_hdeg_square z2 ⬝ !ap_constant }}, - { intro p, exact sorry }, - { intro p, exact sorry }}, - { apply pmap_eq_idp} - end + definition pfunext (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) := + (loop_pmap_commute X Y)⁻¹ᵉ* /- Do we want to use a structure of homotopies between pointed homotopies? Or are equalities fine?