From 3367c20f9d36e9335cf89843aead16913c468f4f Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 20 Jul 2017 18:01:22 +0100 Subject: [PATCH] make pointed suspension and spheres the default There is one proof in realprojective which I couldn't quite fix, so for now I left a sorry --- Notes/lessons.md | 10 +++ algebra/arrow_group.hlean | 4 +- algebra/cogroup.hlean | 50 ++++++------- archive/smash_old.hlean | 38 +++++----- cohomology/basic.hlean | 60 ++++++++-------- homology/basic.hlean | 53 +++++++------- homology/sphere.hlean | 18 ++--- homology/torus.hlean | 32 ++++----- homotopy/EM.hlean | 27 +++---- homotopy/degree.hlean | 12 ++-- homotopy/fwedge.hlean | 30 ++++---- homotopy/pushout.hlean | 2 +- homotopy/realprojective.hlean | 28 ++++---- homotopy/smash.hlean | 12 ++-- homotopy/smash_adjoint.hlean | 83 +++++++++++----------- homotopy/spherical_fibrations.hlean | 59 +++++++++------- homotopy/susp.hlean | 105 +++++++++++++--------------- homotopy/wedge.hlean | 31 ++++---- move_to_lib.hlean | 21 ++++-- pointed.hlean | 1 + pointed_pi.hlean | 3 + spectrum/basic.hlean | 2 +- spectrum/smash.hlean | 12 ++-- 23 files changed, 360 insertions(+), 333 deletions(-) diff --git a/Notes/lessons.md b/Notes/lessons.md index e62bc96..b1836ec 100644 --- a/Notes/lessons.md +++ b/Notes/lessons.md @@ -22,3 +22,13 @@ Some of these things still need to be changes, some of them are already changed, - Type class inference for equivalences doesn't really work in Lean, since it recognizes that `f ∘ id` is definitionally `f`, hence it can always apply `is_equiv_compose` and get trapped in a loop. - Coercions should all be defined *immediately* after defining a structure, *before* declaring any instances. This is because the coercion graph is updated after each declared coercion. +- When you have a functor in two arguments (`→`, `×`, `Π`, `Σ`, pointed versions of these, `=`, `∧`, + `∨`, and so on), the functoriality should be stated in both arguments at once, and the special + cases where only one argument changes should be a special case of that one. This makes it easier + to prove properties about the functorial action, because you only have to do work once (although + that work is sometimes twice as much, but sometimes much less). We haven't always done this, + because it's sometimes easier to define a special case first (even though later you probably still + have to define the general case). Note that for `=` this gives square filling as primitive, + instead of concatenation (which can be seen as functoriality in the second argument), and Dan + Licata argued for that as primitive instead of concatenation. On the other hand, the definition + of the more general functor might be more complicated, in which case definitional reduction won't be as nice \ No newline at end of file diff --git a/algebra/arrow_group.hlean b/algebra/arrow_group.hlean index 16d2aa7..f062688 100644 --- a/algebra/arrow_group.hlean +++ b/algebra/arrow_group.hlean @@ -58,8 +58,8 @@ namespace group refine !con.assoc ⬝ whisker_left _ _, apply ap1_gen_con_idp } end - definition loop_psusp_intro_pmap_mul {X Y : Type*} (f g : psusp X →* Ω Y) : - loop_psusp_intro (pmap_mul f g) ~* pmap_mul (loop_psusp_intro f) (loop_psusp_intro g) := + definition loop_susp_intro_pmap_mul {X Y : Type*} (f g : susp X →* Ω Y) : + loop_susp_intro (pmap_mul f g) ~* pmap_mul (loop_susp_intro f) (loop_susp_intro g) := pwhisker_right _ !ap1_pmap_mul ⬝* !pmap_mul_pcompose definition inf_group_pmap [constructor] [instance] (A B : Type*) : inf_group (A →* Ω B) := diff --git a/algebra/cogroup.hlean b/algebra/cogroup.hlean index c1256b6..563167b 100644 --- a/algebra/cogroup.hlean +++ b/algebra/cogroup.hlean @@ -74,28 +74,28 @@ section prod definition wpr2 (A B : Type*) : (A ∨ B) →* B := pmap.mk (wedge.elim (pconst A B) (pid B) idp) idp - definition ppr1_pprod_of_pwedge (A B : Type*) - : ppr1 ∘* pprod_of_pwedge A B ~* wpr1 A B := + definition ppr1_pprod_of_wedge (A B : Type*) + : ppr1 ∘* pprod_of_wedge A B ~* wpr1 A B := begin fconstructor, { intro w, induction w with a b, { reflexivity }, { reflexivity }, { apply eq_pathover, apply hdeg_square, - apply trans (ap_compose ppr1 (pprod_of_pwedge A B) (pushout.glue star)), + apply trans (ap_compose ppr1 (pprod_of_wedge A B) (pushout.glue star)), krewrite pushout.elim_glue, krewrite pushout.elim_glue } }, { reflexivity } end - definition ppr2_pprod_of_pwedge (A B : Type*) - : ppr2 ∘* pprod_of_pwedge A B ~* wpr2 A B := + definition ppr2_pprod_of_wedge (A B : Type*) + : ppr2 ∘* pprod_of_wedge A B ~* wpr2 A B := begin fconstructor, { intro w, induction w with a b, { reflexivity }, { reflexivity }, { apply eq_pathover, apply hdeg_square, - apply trans (ap_compose ppr2 (pprod_of_pwedge A B) (pushout.glue star)), + apply trans (ap_compose ppr2 (pprod_of_wedge A B) (pushout.glue star)), krewrite pushout.elim_glue, krewrite pushout.elim_glue } }, { reflexivity } end @@ -103,7 +103,7 @@ section prod end prod structure co_h_space [class] (A : Type*) := (comul : A →* (A ∨ A)) -(colaw : pprod_of_pwedge A A ∘* comul ~* pdiag A) +(colaw : pprod_of_wedge A A ∘* comul ~* pdiag A) open co_h_space @@ -113,18 +113,18 @@ definition co_h_space_of_counit_laws {A : Type*} : co_h_space A := co_h_space.mk c (pair_phomotopy (calc - ppr1 ∘* pprod_of_pwedge A A ∘* c - ~* (ppr1 ∘* pprod_of_pwedge A A) ∘* c - : (passoc ppr1 (pprod_of_pwedge A A) c)⁻¹* + ppr1 ∘* pprod_of_wedge A A ∘* c + ~* (ppr1 ∘* pprod_of_wedge A A) ∘* c + : (passoc ppr1 (pprod_of_wedge A A) c)⁻¹* ... ~* wpr1 A A ∘* c - : pwhisker_right c (ppr1_pprod_of_pwedge A A) + : pwhisker_right c (ppr1_pprod_of_wedge A A) ... ~* pid A : l) (calc - ppr2 ∘* pprod_of_pwedge A A ∘* c - ~* (ppr2 ∘* pprod_of_pwedge A A) ∘* c - : (passoc ppr2 (pprod_of_pwedge A A) c)⁻¹* + ppr2 ∘* pprod_of_wedge A A ∘* c + ~* (ppr2 ∘* pprod_of_wedge A A) ∘* c + : (passoc ppr2 (pprod_of_wedge A A) c)⁻¹* ... ~* wpr2 A A ∘* c - : pwhisker_right c (ppr2_pprod_of_pwedge A A) + : pwhisker_right c (ppr2_pprod_of_wedge A A) ... ~* pid A : r)) section @@ -134,20 +134,20 @@ section definition counit_left : wpr1 A A ∘* comul A ~* pid A := calc wpr1 A A ∘* comul A - ~* (ppr1 ∘* (pprod_of_pwedge A A)) ∘* comul A - : (pwhisker_right (comul A) (ppr1_pprod_of_pwedge A A))⁻¹* - ... ~* ppr1 ∘* ((pprod_of_pwedge A A) ∘* comul A) - : passoc ppr1 (pprod_of_pwedge A A) (comul A) + ~* (ppr1 ∘* (pprod_of_wedge A A)) ∘* comul A + : (pwhisker_right (comul A) (ppr1_pprod_of_wedge A A))⁻¹* + ... ~* ppr1 ∘* ((pprod_of_wedge A A) ∘* comul A) + : passoc ppr1 (pprod_of_wedge A A) (comul A) ... ~* pid A : pwhisker_left ppr1 (colaw A) definition counit_right : wpr2 A A ∘* comul A ~* pid A := calc wpr2 A A ∘* comul A - ~* (ppr2 ∘* (pprod_of_pwedge A A)) ∘* comul A - : (pwhisker_right (comul A) (ppr2_pprod_of_pwedge A A))⁻¹* - ... ~* ppr2 ∘* ((pprod_of_pwedge A A) ∘* comul A) - : passoc ppr2 (pprod_of_pwedge A A) (comul A) + ~* (ppr2 ∘* (pprod_of_wedge A A)) ∘* comul A + : (pwhisker_right (comul A) (ppr2_pprod_of_wedge A A))⁻¹* + ... ~* ppr2 ∘* ((pprod_of_wedge A A) ∘* comul A) + : passoc ppr2 (pprod_of_wedge A A) (comul A) ... ~* pid A : pwhisker_left ppr2 (colaw A) @@ -169,7 +169,7 @@ end section variable (A : Type*) - definition pinch : ⅀ A →* pwedge (⅀ A) (⅀ A) := + definition pinch : ⅀ A →* wedge (⅀ A) (⅀ A) := begin fapply pmap.mk, { intro sa, induction sa with a, @@ -178,7 +178,7 @@ section { reflexivity } end - definition co_h_space_psusp : co_h_space (⅀ A) := + definition co_h_space_susp : co_h_space (⅀ A) := co_h_space_of_counit_laws (pinch A) begin fapply phomotopy.mk, diff --git a/archive/smash_old.hlean b/archive/smash_old.hlean index fff8b18..c4ed1a0 100644 --- a/archive/smash_old.hlean +++ b/archive/smash_old.hlean @@ -91,7 +91,7 @@ exit open susp - definition psusp_of_smash_pcircle [unfold 2] (x : smash A S¹*) : psusp A := + definition susp_of_smash_pcircle [unfold 2] (x : smash A S¹*) : susp A := begin induction x using smash.elim, { induction b, exact pt, exact merid a ⬝ (merid pt)⁻¹ }, @@ -102,7 +102,7 @@ exit exact !elim_loop ⬝ !con.right_inv } end - definition smash_pcircle_of_psusp [unfold 2] (x : psusp A) : smash A S¹* := + definition smash_pcircle_of_susp [unfold 2] (x : susp A) : smash A S¹* := begin induction x, { exact pt }, @@ -111,13 +111,13 @@ exit end -- the definitions below compile, but take a long time to do so and have sorry's in them - definition smash_pcircle_of_psusp_of_smash_pcircle_pt [unfold 3] (a : A) (x : S¹*) : - smash_pcircle_of_psusp (psusp_of_smash_pcircle (smash.mk a x)) = smash.mk a x := + definition smash_pcircle_of_susp_of_smash_pcircle_pt [unfold 3] (a : A) (x : S¹*) : + smash_pcircle_of_susp (susp_of_smash_pcircle (smash.mk a x)) = smash.mk a x := begin induction x, { exact gluel' pt a }, { exact abstract begin apply eq_pathover, - refine ap_compose smash_pcircle_of_psusp _ _ ⬝ph _, + refine ap_compose smash_pcircle_of_susp _ _ ⬝ph _, refine ap02 _ (elim_loop north (merid a ⬝ (merid pt)⁻¹)) ⬝ph _, refine !ap_con ⬝ (!elim_merid ◾ (!ap_inv ⬝ !elim_merid⁻²)) ⬝ph _, -- make everything below this a lemma defined by path induction? @@ -136,10 +136,10 @@ exit end end } end - -- definition smash_pcircle_of_psusp_of_smash_pcircle_gluer_base (b : S¹*) - -- : square (smash_pcircle_of_psusp_of_smash_pcircle_pt (Point A) b) + -- definition smash_pcircle_of_susp_of_smash_pcircle_gluer_base (b : S¹*) + -- : square (smash_pcircle_of_susp_of_smash_pcircle_pt (Point A) b) -- (gluer pt) - -- (ap smash_pcircle_of_psusp (ap (λ a, psusp_of_smash_pcircle a) (gluer b))) + -- (ap smash_pcircle_of_susp (ap (λ a, susp_of_smash_pcircle a) (gluer b))) -- (gluer b) := -- begin -- refine ap02 _ !elim_gluer ⬝ph _, @@ -149,36 +149,36 @@ exit -- end exit - definition smash_pcircle_pequiv [constructor] (A : Type*) : smash A S¹* ≃* psusp A := + definition smash_pcircle_pequiv [constructor] (A : Type*) : smash A S¹* ≃* susp A := begin fapply pequiv_of_equiv, { fapply equiv.MK, - { exact psusp_of_smash_pcircle }, - { exact smash_pcircle_of_psusp }, + { exact susp_of_smash_pcircle }, + { exact smash_pcircle_of_susp }, { exact abstract begin intro x, induction x, { reflexivity }, { exact merid pt }, { apply eq_pathover_id_right, - refine ap_compose psusp_of_smash_pcircle _ _ ⬝ph _, + refine ap_compose susp_of_smash_pcircle _ _ ⬝ph _, refine ap02 _ !elim_merid ⬝ph _, rewrite [↑gluel', +ap_con, +ap_inv, -ap_compose'], refine (_ ◾ _⁻² ◾ _ ◾ (_ ◾ _⁻²)) ⬝ph _, - rotate 5, do 2 (unfold [psusp_of_smash_pcircle]; apply elim_gluel), - esimp, apply elim_loop, do 2 (unfold [psusp_of_smash_pcircle]; apply elim_gluel), + rotate 5, do 2 (unfold [susp_of_smash_pcircle]; apply elim_gluel), + esimp, apply elim_loop, do 2 (unfold [susp_of_smash_pcircle]; apply elim_gluel), refine idp_con (merid a ⬝ (merid (Point A))⁻¹) ⬝ph _, apply square_of_eq, refine !idp_con ⬝ _⁻¹, apply inv_con_cancel_right } end end }, { intro x, induction x using smash.rec, - { exact smash_pcircle_of_psusp_of_smash_pcircle_pt a b }, + { exact smash_pcircle_of_susp_of_smash_pcircle_pt a b }, { exact gluel pt }, { exact gluer pt }, { apply eq_pathover_id_right, - refine ap_compose smash_pcircle_of_psusp _ _ ⬝ph _, - unfold [psusp_of_smash_pcircle], + refine ap_compose smash_pcircle_of_susp _ _ ⬝ph _, + unfold [susp_of_smash_pcircle], refine ap02 _ !elim_gluel ⬝ph _, esimp, apply whisker_rt, exact vrfl }, { apply eq_pathover_id_right, - refine ap_compose smash_pcircle_of_psusp _ _ ⬝ph _, - unfold [psusp_of_smash_pcircle], + refine ap_compose smash_pcircle_of_susp _ _ ⬝ph _, + unfold [susp_of_smash_pcircle], refine ap02 _ !elim_gluer ⬝ph _, induction b, { apply square_of_eq, exact whisker_right _ !con.right_inv }, diff --git a/cohomology/basic.hlean b/cohomology/basic.hlean index 58bf35b..4c88433 100644 --- a/cohomology/basic.hlean +++ b/cohomology/basic.hlean @@ -180,49 +180,49 @@ parametrized_cohomology_isomorphism_right /- suspension axiom -/ -definition cohomology_psusp_2 (Y : spectrum) (n : ℤ) : +definition cohomology_susp_2 (Y : spectrum) (n : ℤ) : Ω (Ω[2] (Y ((n+1)+2))) ≃* Ω[2] (Y (n+2)) := begin apply loopn_pequiv_loopn 2, exact loop_pequiv_loop (pequiv_of_eq (ap Y (add.right_comm n 1 2))) ⬝e* !equiv_glue⁻¹ᵉ* end -definition cohomology_psusp_1 (X : Type*) (Y : spectrum) (n : ℤ) : - psusp X →* Ω (Ω (Y (n + 1 + 2))) ≃ X →* Ω (Ω (Y (n+2))) := +definition cohomology_susp_1 (X : Type*) (Y : spectrum) (n : ℤ) : + susp X →* Ω (Ω (Y (n + 1 + 2))) ≃ X →* Ω (Ω (Y (n+2))) := calc - psusp X →* Ω[2] (Y (n + 1 + 2)) ≃ X →* Ω (Ω[2] (Y (n + 1 + 2))) : psusp_adjoint_loop_unpointed + susp X →* Ω[2] (Y (n + 1 + 2)) ≃ X →* Ω (Ω[2] (Y (n + 1 + 2))) : susp_adjoint_loop_unpointed ... ≃ X →* Ω[2] (Y (n+2)) : equiv_of_pequiv (pequiv_ppcompose_left - (cohomology_psusp_2 Y n)) + (cohomology_susp_2 Y n)) -definition cohomology_psusp_1_pmap_mul {X : Type*} {Y : spectrum} {n : ℤ} - (f g : psusp X →* Ω (Ω (Y (n + 1 + 2)))) : cohomology_psusp_1 X Y n (pmap_mul f g) ~* - pmap_mul (cohomology_psusp_1 X Y n f) (cohomology_psusp_1 X Y n g) := +definition cohomology_susp_1_pmap_mul {X : Type*} {Y : spectrum} {n : ℤ} + (f g : susp X →* Ω (Ω (Y (n + 1 + 2)))) : cohomology_susp_1 X Y n (pmap_mul f g) ~* + pmap_mul (cohomology_susp_1 X Y n f) (cohomology_susp_1 X Y n g) := begin - unfold [cohomology_psusp_1], - refine pwhisker_left _ !loop_psusp_intro_pmap_mul ⬝* _, + unfold [cohomology_susp_1], + refine pwhisker_left _ !loop_susp_intro_pmap_mul ⬝* _, apply pcompose_pmap_mul end -definition cohomology_psusp_equiv (X : Type*) (Y : spectrum) (n : ℤ) : - H^n+1[psusp X, Y] ≃ H^n[X, Y] := -trunc_equiv_trunc _ (cohomology_psusp_1 X Y n) +definition cohomology_susp_equiv (X : Type*) (Y : spectrum) (n : ℤ) : + H^n+1[susp X, Y] ≃ H^n[X, Y] := +trunc_equiv_trunc _ (cohomology_susp_1 X Y n) -definition cohomology_psusp (X : Type*) (Y : spectrum) (n : ℤ) : - H^n+1[psusp X, Y] ≃g H^n[X, Y] := -isomorphism_of_equiv (cohomology_psusp_equiv X Y n) +definition cohomology_susp (X : Type*) (Y : spectrum) (n : ℤ) : + H^n+1[susp X, Y] ≃g H^n[X, Y] := +isomorphism_of_equiv (cohomology_susp_equiv X Y n) begin intro f₁ f₂, induction f₁ with f₁, induction f₂ with f₂, - apply ap tr, apply eq_of_phomotopy, exact cohomology_psusp_1_pmap_mul f₁ f₂ + apply ap tr, apply eq_of_phomotopy, exact cohomology_susp_1_pmap_mul f₁ f₂ end -definition cohomology_psusp_natural {X X' : Type*} (f : X →* X') (Y : spectrum) (n : ℤ) : - cohomology_psusp X Y n ∘ cohomology_functor (psusp_functor f) Y (n+1) ~ - cohomology_functor f Y n ∘ cohomology_psusp X' Y n := +definition cohomology_susp_natural {X X' : Type*} (f : X →* X') (Y : spectrum) (n : ℤ) : + cohomology_susp X Y n ∘ cohomology_functor (susp_functor f) Y (n+1) ~ + cohomology_functor f Y n ∘ cohomology_susp X' Y n := begin refine (trunc_functor_compose _ _ _)⁻¹ʰᵗʸ ⬝hty _ ⬝hty trunc_functor_compose _ _ _, apply trunc_functor_homotopy, intro g, apply eq_of_phomotopy, refine _ ⬝* !passoc⁻¹*, apply pwhisker_left, - apply loop_psusp_intro_natural + apply loop_susp_intro_natural end /- exactness -/ @@ -284,9 +284,9 @@ structure cohomology_theory.{u} : Type.{u+1} := (Hid : Π(n : ℤ) {X : Type*} (x : HH n X), Hh n (pid X) x = x) (Hcompose : Π(n : ℤ) {X Y Z : Type*} (g : Y →* Z) (f : X →* Y) (z : HH n Z), Hh n (g ∘* f) z = Hh n f (Hh n g z)) - (Hsusp : Π(n : ℤ) (X : Type*), HH (succ n) (psusp X) ≃g HH n X) + (Hsusp : Π(n : ℤ) (X : Type*), HH (succ n) (susp X) ≃g HH n X) (Hsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y), - Hsusp n X ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hsusp n Y) + Hsusp n X ∘ Hh (succ n) (susp_functor f) ~ Hh n f ∘ Hsusp n Y) (Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n (pcod f)) (Hh n f)) (Hadditive : Π(n : ℤ) {I : Type.{u}} (X : I → Type*), has_choice 0 I → is_equiv (Group_pi_intro (λi, Hh n (pinl i)) : HH n (⋁ X) → Πᵍ i, HH n (X i))) @@ -301,19 +301,19 @@ open cohomology_theory definition Hequiv (H : cohomology_theory) (n : ℤ) {X Y : Type*} (f : X ≃* Y) : H n Y ≃ H n X := equiv_of_isomorphism (Hiso H n f) -definition Hsusp_neg (H : cohomology_theory) (n : ℤ) (X : Type*) : H n (psusp X) ≃g H (pred n) X := +definition Hsusp_neg (H : cohomology_theory) (n : ℤ) (X : Type*) : H n (susp X) ≃g H (pred n) X := isomorphism_of_eq (ap (λn, H n _) proof (sub_add_cancel n 1)⁻¹ qed) ⬝g cohomology_theory.Hsusp H (pred n) X definition Hsusp_neg_natural (H : cohomology_theory) (n : ℤ) {X Y : Type*} (f : X →* Y) : - Hsusp_neg H n X ∘ H ^→ n (psusp_functor f) ~ H ^→ (pred n) f ∘ Hsusp_neg H n Y := + Hsusp_neg H n X ∘ H ^→ n (susp_functor f) ~ H ^→ (pred n) f ∘ Hsusp_neg H n Y := sorry definition Hsusp_inv_natural (H : cohomology_theory) (n : ℤ) {X Y : Type*} (f : X →* Y) : - H ^→ (succ n) (psusp_functor f) ∘g (Hsusp H n Y)⁻¹ᵍ ~ (Hsusp H n X)⁻¹ᵍ ∘ H ^→ n f := + H ^→ (succ n) (susp_functor f) ∘g (Hsusp H n Y)⁻¹ᵍ ~ (Hsusp H n X)⁻¹ᵍ ∘ H ^→ n f := sorry definition Hsusp_neg_inv_natural (H : cohomology_theory) (n : ℤ) {X Y : Type*} (f : X →* Y) : - H ^→ n (psusp_functor f) ∘g (Hsusp_neg H n Y)⁻¹ᵍ ~ (Hsusp_neg H n X)⁻¹ᵍ ∘ H ^→ (pred n) f := + H ^→ n (susp_functor f) ∘g (Hsusp_neg H n Y)⁻¹ᵍ ~ (Hsusp_neg H n X)⁻¹ᵍ ∘ H ^→ (pred n) f := sorry definition Hadditive_equiv (H : cohomology_theory) (n : ℤ) {I : Type} (X : I → Type*) (H2 : has_choice 0 I) @@ -346,7 +346,7 @@ end -- definition Hwedge (H : cohomology_theory) (n : ℤ) (A B : Type*) : H n (A ∨ B) ≃g H n A ×ag H n B := -- begin --- refine Hiso H n (pwedge_pequiv_fwedge A B)⁻¹ᵉ* ⬝g _, +-- refine Hiso H n (wedge_pequiv_fwedge A B)⁻¹ᵉ* ⬝g _, -- refine Hadditive_equiv H n _ _ ⬝g _ -- end @@ -360,8 +360,8 @@ cohomology_theory.mk (λn A B f x, cohomology_functor_phomotopy_refl f Y n x) (λn A x, cohomology_functor_pid A Y n x) (λn A B C g f x, cohomology_functor_pcompose g f Y n x) - (λn A, cohomology_psusp A Y n) - (λn A B f, cohomology_psusp_natural f Y n) + (λn A, cohomology_susp A Y n) + (λn A B f, cohomology_susp_natural f Y n) (λn A B f, cohomology_exact f Y n) (λn I A H, spectrum_additive H A Y n) diff --git a/homology/basic.hlean b/homology/basic.hlean index 8d39387..30aff2b 100644 --- a/homology/basic.hlean +++ b/homology/basic.hlean @@ -20,15 +20,15 @@ namespace homology (Hpid : Π(n : ℤ) {X : Type*} (x : HH n X), Hh n (pid X) x = x) (Hpcompose : Π(n : ℤ) {X Y Z : Type*} (f : Y →* Z) (g : X →* Y), Hh n (f ∘* g) ~ Hh n f ∘ Hh n g) - (Hpsusp : Π(n : ℤ) (X : Type*), HH (succ n) (psusp X) ≃g HH n X) - (Hpsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y), - Hpsusp n Y ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hpsusp n X) + (Hsusp : Π(n : ℤ) (X : Type*), HH (succ n) (susp X) ≃g HH n X) + (Hsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y), + Hsusp n Y ∘ Hh (succ n) (susp_functor f) ~ Hh n f ∘ Hsusp n X) (Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n f) (Hh n (pcod f))) (Hadditive : Π(n : ℤ) {I : Set.{u}} (X : I → Type*), is_equiv (dirsum_elim (λi, Hh n (pinl i)) : dirsum (λi, HH n (X i)) → HH n (⋁ X))) structure ordinary_homology_theory.{u} extends homology_theory.{u} : Type.{u+1} := - (Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (HH n (plift (psphere 0)))) + (Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (HH n (plift (sphere 0)))) section universe variable u @@ -37,20 +37,20 @@ namespace homology theorem HH_base_indep (n : ℤ) {A : Type} (a b : A) : HH theory n (pType.mk A a) ≃g HH theory n (pType.mk A b) := - calc HH theory n (pType.mk A a) ≃g HH theory (int.succ n) (psusp A) : by exact (Hpsusp theory n (pType.mk A a)) ⁻¹ᵍ - ... ≃g HH theory n (pType.mk A b) : by exact Hpsusp theory n (pType.mk A b) + calc HH theory n (pType.mk A a) ≃g HH theory (int.succ n) (susp A) : by exact (Hsusp theory n (pType.mk A a)) ⁻¹ᵍ + ... ≃g HH theory n (pType.mk A b) : by exact Hsusp theory n (pType.mk A b) theorem Hh_homotopy' (n : ℤ) {A B : Type*} (f : A → B) (p q : f pt = pt) : Hh theory n (pmap.mk f p) ~ Hh theory n (pmap.mk f q) := λ x, calc Hh theory n (pmap.mk f p) x - = Hh theory n (pmap.mk f p) (Hpsusp theory n A ((Hpsusp theory n A)⁻¹ᵍ x)) - : by exact ap (Hh theory n (pmap.mk f p)) (equiv.to_right_inv (equiv_of_isomorphism (Hpsusp theory n A)) x)⁻¹ - ... = Hpsusp theory n B (Hh theory (succ n) (pmap.mk (susp.functor f) !refl) ((Hpsusp theory n A)⁻¹ x)) - : by exact (Hpsusp_natural theory n (pmap.mk f p) ((Hpsusp theory n A)⁻¹ᵍ x))⁻¹ - ... = Hh theory n (pmap.mk f q) (Hpsusp theory n A ((Hpsusp theory n A)⁻¹ x)) - : by exact Hpsusp_natural theory n (pmap.mk f q) ((Hpsusp theory n A)⁻¹ x) + = Hh theory n (pmap.mk f p) (Hsusp theory n A ((Hsusp theory n A)⁻¹ᵍ x)) + : by exact ap (Hh theory n (pmap.mk f p)) (equiv.to_right_inv (equiv_of_isomorphism (Hsusp theory n A)) x)⁻¹ + ... = Hsusp theory n B (Hh theory (succ n) (pmap.mk (susp_functor' f) !refl) ((Hsusp theory n A)⁻¹ x)) + : by exact (Hsusp_natural theory n (pmap.mk f p) ((Hsusp theory n A)⁻¹ᵍ x))⁻¹ + ... = Hh theory n (pmap.mk f q) (Hsusp theory n A ((Hsusp theory n A)⁻¹ x)) + : by exact Hsusp_natural theory n (pmap.mk f q) ((Hsusp theory n A)⁻¹ x) ... = Hh theory n (pmap.mk f q) x - : by exact ap (Hh theory n (pmap.mk f q)) (equiv.to_right_inv (equiv_of_isomorphism (Hpsusp theory n A)) x) + : by exact ap (Hh theory n (pmap.mk f q)) (equiv.to_right_inv (equiv_of_isomorphism (Hsusp theory n A)) x) theorem Hh_homotopy (n : ℤ) {A B : Type*} (f g : A →* B) (h : f ~ g) : Hh theory n f ~ Hh theory n g := λ x, calc Hh theory n f x @@ -122,8 +122,8 @@ namespace homology definition Hfwedge (n : ℤ) {I : Type} [is_set I] (X : I → Type*): HH theory n (⋁ X) ≃g dirsum (λi, HH theory n (X i)) := (isomorphism.mk _ (Hadditive theory n X))⁻¹ᵍ - definition Hpwedge (n : ℤ) (A B : Type*) : HH theory n (pwedge A B) ≃g HH theory n A ×g HH theory n B := - calc HH theory n (A ∨ B) ≃g HH theory n (⋁ (bool.rec A B)) : by exact HH_isomorphism n (pwedge_pequiv_fwedge A B) + definition Hwedge (n : ℤ) (A B : Type*) : HH theory n (wedge A B) ≃g HH theory n A ×g HH theory n B := + calc HH theory n (A ∨ B) ≃g HH theory n (⋁ (bool.rec A B)) : by exact HH_isomorphism n (wedge_pequiv_fwedge A B) ... ≃g dirsum (λb, HH theory n (bool.rec A B b)) : by exact (Hadditive'_equiv n (bool.rec A B))⁻¹ᵍ ... ≃g dirsum (bool.rec (HH theory n A) (HH theory n B)) : by exact dirsum_isomorphism (bool.rec !isomorphism.refl !isomorphism.refl) ... ≃g HH theory n A ×g HH theory n B : by exact binary_dirsum (HH theory n A) (HH theory n B) @@ -134,13 +134,13 @@ namespace homology parameter (theory : homology_theory.{max u v}) open homology_theory - definition Hplift_psusp (n : ℤ) (A : Type*): HH theory (n + 1) (plift.{u v} (psusp A)) ≃g HH theory n (plift.{u v} A) := - calc HH theory (n + 1) (plift.{u v} (psusp A)) ≃g HH theory (n + 1) (psusp (plift.{u v} A)) : by exact HH_isomorphism theory (n + 1) (plift_psusp _) - ... ≃g HH theory n (plift.{u v} A) : by exact Hpsusp theory n (plift.{u v} A) + definition Hplift_susp (n : ℤ) (A : Type*): HH theory (n + 1) (plift.{u v} (susp A)) ≃g HH theory n (plift.{u v} A) := + calc HH theory (n + 1) (plift.{u v} (susp A)) ≃g HH theory (n + 1) (susp (plift.{u v} A)) : by exact HH_isomorphism theory (n + 1) (plift_susp _) + ... ≃g HH theory n (plift.{u v} A) : by exact Hsusp theory n (plift.{u v} A) - definition Hplift_pwedge (n : ℤ) (A B : Type*): HH theory n (plift.{u v} (A ∨ B)) ≃g HH theory n (plift.{u v} A) ×g HH theory n (plift.{u v} B) := - calc HH theory n (plift.{u v} (A ∨ B)) ≃g HH theory n (plift.{u v} A ∨ plift.{u v} B) : by exact HH_isomorphism theory n (plift_pwedge A B) - ... ≃g HH theory n (plift.{u v} A) ×g HH theory n (plift.{u v} B) : by exact Hpwedge theory n (plift.{u v} A) (plift.{u v} B) + definition Hplift_wedge (n : ℤ) (A B : Type*): HH theory n (plift.{u v} (A ∨ B)) ≃g HH theory n (plift.{u v} A) ×g HH theory n (plift.{u v} B) := + calc HH theory n (plift.{u v} (A ∨ B)) ≃g HH theory n (plift.{u v} A ∨ plift.{u v} B) : by exact HH_isomorphism theory n (plift_wedge A B) + ... ≃g HH theory n (plift.{u v} A) ×g HH theory n (plift.{u v} B) : by exact Hwedge theory n (plift.{u v} A) (plift.{u v} B) definition Hplift_isomorphism (n : ℤ) {A B : Type*} (e : A ≃* B) : HH theory n (plift.{u v} A) ≃g HH theory n (plift.{u v} B) := HH_isomorphism theory n (!pequiv_plift⁻¹ᵉ* ⬝e* e ⬝e* !pequiv_plift) @@ -175,11 +175,12 @@ definition homology_functor [constructor] {X Y : Type*} {E F : prespectrum} (f : (g : E →ₛ F) (n : ℤ) : homology X E n →g homology Y F n := pshomotopy_group_fun n (smash_prespectrum_fun f g) +print is_exact_g +print is_exact definition homology_theory_spectrum_is_exact.{u} (E : spectrum.{u}) (n : ℤ) {X Y : Type*} (f : X →* Y) : - is_exact_g (homology_functor f (sid (gen_spectrum.to_prespectrum E)) n) - (homology_functor (pcod f) (sid (gen_spectrum.to_prespectrum E)) n) := + is_exact_g (homology_functor f (sid E) n) (homology_functor (pcod f) (sid E) n) := begin - esimp[is_exact_g], + esimp [is_exact_g], -- fconstructor, -- { intro a, exact sorry }, -- { intro a, exact sorry } @@ -211,8 +212,8 @@ begin -- (λn A B f x, cohomology_functor_phomotopy_refl f Y n x) -- (λn A x, cohomology_functor_pid A Y n x) -- (λn A B C g f x, cohomology_functor_pcompose g f Y n x) --- (λn A, cohomology_psusp A Y n) --- (λn A B f, cohomology_psusp_natural f Y n) +-- (λn A, cohomology_susp A Y n) +-- (λn A B f, cohomology_susp_natural f Y n) -- (λn A B f, cohomology_exact f Y n) -- (λn I A H, spectrum_additive H A Y n) end diff --git a/homology/sphere.hlean b/homology/sphere.hlean index a22abbe..b0daeb6 100644 --- a/homology/sphere.hlean +++ b/homology/sphere.hlean @@ -17,18 +17,18 @@ section open homology_theory - theorem Hpsphere : Π(n : ℤ)(m : ℕ), HH theory n (plift (psphere m)) ≃g HH theory (n - m) (plift (psphere 0)) := + theorem Hsphere : Π(n : ℤ)(m : ℕ), HH theory n (plift (sphere m)) ≃g HH theory (n - m) (plift (sphere 0)) := begin intros n m, revert n, induction m with m, - { exact λ n, isomorphism_ap (λ n, HH theory n (plift (psphere 0))) (sub_zero n)⁻¹ }, + { exact λ n, isomorphism_ap (λ n, HH theory n (plift (sphere 0))) (sub_zero n)⁻¹ }, { intro n, exact calc - HH theory n (plift (psusp (psphere m))) - ≃g HH theory (succ (pred n)) (plift (psusp (psphere m))) - : by exact isomorphism_ap (λ n, HH theory n (plift (psusp (psphere m)))) (succ_pred n)⁻¹ - ... ≃g HH theory (pred n) (plift (psphere m)) : by exact Hplift_psusp theory (pred n) (psphere m) - ... ≃g HH theory (pred n - m) (plift (psphere 0)) : by exact v_0 (pred n) - ... ≃g HH theory (n - succ m) (plift (psphere 0)) - : by exact isomorphism_ap (λ n, HH theory n (plift (psphere 0))) (sub_sub n 1 m ⬝ ap (λ m, n - m) (add.comm 1 m)) + HH theory n (plift (susp (sphere m))) + ≃g HH theory (succ (pred n)) (plift (susp (sphere m))) + : by exact isomorphism_ap (λ n, HH theory n (plift (susp (sphere m)))) (succ_pred n)⁻¹ + ... ≃g HH theory (pred n) (plift (sphere m)) : by exact Hplift_susp theory (pred n) (sphere m) + ... ≃g HH theory (pred n - m) (plift (sphere 0)) : by exact v_0 (pred n) + ... ≃g HH theory (n - succ m) (plift (sphere 0)) + : by exact isomorphism_ap (λ n, HH theory n (plift (sphere 0))) (sub_sub n 1 m ⬝ ap (λ m, n - m) (add.comm 1 m)) } end end diff --git a/homology/torus.hlean b/homology/torus.hlean index 4525ad8..3158cff 100644 --- a/homology/torus.hlean +++ b/homology/torus.hlean @@ -17,23 +17,23 @@ section open ordinary_homology_theory - theorem Hptorus : Π(n : ℤ)(m : ℕ), HH theory n (plift (psphere m ×* psphere m)) ≃g - HH theory n (plift (psphere m)) ×g (HH theory n (plift (psphere m)) ×g HH theory n (plift (psphere (m + m)))) := λ n m, - calc HH theory n (plift (psphere m ×* psphere m)) - ≃g HH theory (n + 1) (plift (⅀ (psphere m ×* psphere m))) : by exact (Hplift_psusp theory n (psphere m ×* psphere m))⁻¹ᵍ - ... ≃g HH theory (n + 1) (plift (⅀ (psphere m) ∨ (⅀ (psphere m) ∨ ⅀ (psphere m ∧ psphere m)))) - : by exact Hplift_isomorphism theory (n + 1) (susp_product (psphere m) (psphere m)) - ... ≃g HH theory (n + 1) (plift (⅀ (psphere m))) ×g HH theory (n + 1) (plift (⅀ (psphere m) ∨ (⅀ (psphere m ∧ psphere m)))) - : by exact Hplift_pwedge theory (n + 1) (⅀ (psphere m)) (⅀ (psphere m) ∨ (⅀ (psphere m ∧ psphere m))) - ... ≃g HH theory n (plift (psphere m)) ×g (HH theory n (plift (psphere m)) ×g HH theory n (plift (psphere (m + m)))) - : by exact product_isomorphism (Hplift_psusp theory n (psphere m)) + theorem Hptorus : Π(n : ℤ)(m : ℕ), HH theory n (plift (sphere m ×* sphere m)) ≃g + HH theory n (plift (sphere m)) ×g (HH theory n (plift (sphere m)) ×g HH theory n (plift (sphere (m + m)))) := λ n m, + calc HH theory n (plift (sphere m ×* sphere m)) + ≃g HH theory (n + 1) (plift (⅀ (sphere m ×* sphere m))) : by exact (Hplift_susp theory n (sphere m ×* sphere m))⁻¹ᵍ + ... ≃g HH theory (n + 1) (plift (⅀ (sphere m) ∨ (⅀ (sphere m) ∨ ⅀ (sphere m ∧ sphere m)))) + : by exact Hplift_isomorphism theory (n + 1) (susp_product (sphere m) (sphere m)) + ... ≃g HH theory (n + 1) (plift (⅀ (sphere m))) ×g HH theory (n + 1) (plift (⅀ (sphere m) ∨ (⅀ (sphere m ∧ sphere m)))) + : by exact Hplift_wedge theory (n + 1) (⅀ (sphere m)) (⅀ (sphere m) ∨ (⅀ (sphere m ∧ sphere m))) + ... ≃g HH theory n (plift (sphere m)) ×g (HH theory n (plift (sphere m)) ×g HH theory n (plift (sphere (m + m)))) + : by exact product_isomorphism (Hplift_susp theory n (sphere m)) (calc - HH theory (n + 1) (plift (⅀ (psphere m) ∨ (⅀ (psphere m ∧ psphere m)))) - ≃g HH theory (n + 1) (plift (⅀ (psphere m))) ×g HH theory (n + 1) (plift (⅀ (psphere m ∧ psphere m))) - : by exact Hplift_pwedge theory (n + 1) (⅀ (psphere m)) (⅀ (psphere m ∧ psphere m)) - ... ≃g HH theory n (plift (psphere m)) ×g HH theory n (plift (psphere (m + m))) - : by exact product_isomorphism (Hplift_psusp theory n (psphere m)) - (Hplift_psusp theory n (psphere m ∧ psphere m) ⬝g Hplift_isomorphism theory n (sphere_smash_sphere m m))) + HH theory (n + 1) (plift (⅀ (sphere m) ∨ (⅀ (sphere m ∧ sphere m)))) + ≃g HH theory (n + 1) (plift (⅀ (sphere m))) ×g HH theory (n + 1) (plift (⅀ (sphere m ∧ sphere m))) + : by exact Hplift_wedge theory (n + 1) (⅀ (sphere m)) (⅀ (sphere m ∧ sphere m)) + ... ≃g HH theory n (plift (sphere m)) ×g HH theory n (plift (sphere (m + m))) + : by exact product_isomorphism (Hplift_susp theory n (sphere m)) + (Hplift_susp theory n (sphere m ∧ sphere m) ⬝g Hplift_isomorphism theory n (sphere_smash_sphere m m))) end diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean index 9bdf616..1ac553b 100644 --- a/homotopy/EM.hlean +++ b/homotopy/EM.hlean @@ -1,7 +1,7 @@ -- Authors: Floris van Doorn import homotopy.EM algebra.category.functor.equivalence types.pointed2 ..pointed_pi ..pointed - ..move_to_lib .susp + ..move_to_lib .susp ..algebra.quotient_group open eq equiv is_equiv algebra group nat pointed EM.ops is_trunc trunc susp function is_conn @@ -10,7 +10,7 @@ open eq equiv is_equiv algebra group nat pointed EM.ops is_trunc trunc susp func namespace EM definition EMadd1_functor_succ [unfold_full] {G H : AbGroup} (φ : G →g H) (n : ℕ) : - EMadd1_functor φ (succ n) ~* ptrunc_functor (n+2) (psusp_functor (EMadd1_functor φ n)) := + EMadd1_functor φ (succ n) ~* ptrunc_functor (n+2) (susp_functor (EMadd1_functor φ n)) := by reflexivity definition EM1_functor_gid (G : Group) : EM1_functor (gid G) ~* !pid := @@ -28,7 +28,7 @@ namespace EM induction n with n p, { apply EM1_functor_gid }, { refine !EMadd1_functor_succ ⬝* _, - refine ptrunc_functor_phomotopy _ (psusp_functor_phomotopy p ⬝* !psusp_functor_pid) ⬝* _, + refine ptrunc_functor_phomotopy _ (susp_functor_phomotopy p ⬝* !susp_functor_pid) ⬝* _, apply ptrunc_functor_pid } end @@ -58,7 +58,7 @@ namespace EM induction n with n p, { apply EM1_functor_gcompose }, { refine !EMadd1_functor_succ ⬝* _, - refine ptrunc_functor_phomotopy _ (psusp_functor_phomotopy p ⬝* !psusp_functor_pcompose) ⬝* _, + refine ptrunc_functor_phomotopy _ (susp_functor_phomotopy p ⬝* !susp_functor_pcompose) ⬝* _, apply ptrunc_functor_pcompose } end @@ -87,7 +87,7 @@ namespace EM begin induction n with n q, { exact EM1_functor_phomotopy p }, - { exact ptrunc_functor_phomotopy _ (psusp_functor_phomotopy q) } + { exact ptrunc_functor_phomotopy _ (susp_functor_phomotopy q) } end definition EM_functor_phomotopy {G H : AbGroup} {φ ψ : G →g H} (p : φ ~ ψ) (n : ℕ) : @@ -154,7 +154,7 @@ namespace EM -- is_trunc_EMadd1 G n definition loop_EMadd1_succ (G : AbGroup) (n : ℕ) : - loop_EMadd1 G (n+1) ~* (loop_ptrunc_pequiv (n+1+1) (psusp (EMadd1 G (n+1))))⁻¹ᵉ* ∘* + loop_EMadd1 G (n+1) ~* (loop_ptrunc_pequiv (n+1+1) (susp (EMadd1 G (n+1))))⁻¹ᵉ* ∘* freudenthal_pequiv (EMadd1 G (n+1)) (add_mul_le_mul_add n 1 1) ∘* (ptrunc_pequiv (n+1+1) (EMadd1 G (n+1)))⁻¹ᵉ* := by reflexivity @@ -166,7 +166,7 @@ namespace EM induction n with n IH, { refine pwhisker_left _ !hopf.to_pmap_delooping_pinv ⬝* _ ⬝* pwhisker_right _ !hopf.to_pmap_delooping_pinv⁻¹*, - refine !loop_psusp_unit_natural⁻¹* ⬝h* _, + refine !loop_susp_unit_natural⁻¹* ⬝h* _, apply ap1_psquare, apply ptr_natural }, { refine pwhisker_left _ !loop_EMadd1_succ ⬝* _ ⬝* pwhisker_right _ !loop_EMadd1_succ⁻¹*, @@ -175,7 +175,7 @@ namespace EM refine pwhisker_left _ !to_pmap_freudenthal_pequiv ⬝* _ ⬝* pwhisker_right _ !to_pmap_freudenthal_pequiv⁻¹*, apply ptrunc_functor_psquare, - exact !loop_psusp_unit_natural⁻¹* } + exact !loop_susp_unit_natural⁻¹* } end definition apn_EMadd1_pequiv_EM1_natural {G H : AbGroup} (φ : G →g H) (n : ℕ) : @@ -264,10 +264,10 @@ namespace EM refine (ptrunc_elim_pcompose ((succ n).+1) _ _)⁻¹* ⬝* _ ⬝* (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 _ ⬝* !susp_elim_susp_functor⁻¹*, + refine _ ⬝* susp_elim_phomotopy (IH _ _ _ _ _ (is_homomorphism_EM_up eX rX) _ (@is_conn_loop _ _ H1) (@is_trunc_loop _ _ H2) _ _ (EM_up_natural φ f eX eY p)), - apply psusp_elim_natural } + apply susp_elim_natural } end definition EMadd1_pequiv'_natural {G H : AbGroup} {X Y : Type*} (f : X →* Y) (n : ℕ) (eX : Ω[succ n] X ≃* G) @@ -374,7 +374,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_mul_hom_EM_up e r) _ _)), + -- (susp.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) := @@ -550,7 +550,7 @@ namespace EM begin induction n with n IH, { exact is_contr_EM1 H }, - { have is_contr (ptrunc (n+2) (psusp (EMadd1 G n))), from _, + { have is_contr (ptrunc (n+2) (susp (EMadd1 G n))), from _, exact this } end @@ -640,6 +640,7 @@ namespace EM -- end + open group algebra definition homotopy_group_fiber_EM1_functor {G H : Group} (φ : G →g H) : π₁ (pfiber (EM1_functor φ)) ≃g kernel φ := sorry diff --git a/homotopy/degree.hlean b/homotopy/degree.hlean index 404feb6..bc8635b 100644 --- a/homotopy/degree.hlean +++ b/homotopy/degree.hlean @@ -86,14 +86,14 @@ namespace sphere { unfold [πnSn], exact sorry} end - definition deg {n : ℕ} [H : is_succ n] (f : S* n →* S* n) : ℤ := + definition deg {n : ℕ} [H : is_succ n] (f : S n →* S n) : ℤ := by induction H with n; exact πnSn n (π→g[n+1] f (tr surf)) - definition deg_id (n : ℕ) [H : is_succ n] : deg (pid (S* n)) = (1 : ℤ) := + definition deg_id (n : ℕ) [H : is_succ n] : deg (pid (S n)) = (1 : ℤ) := by induction H with n; - exact ap (πnSn n) (homotopy_group_functor_pid (succ n) (S* (succ n)) (tr surf)) ⬝ πnSn_surf n + exact ap (πnSn n) (homotopy_group_functor_pid (succ n) (S (succ n)) (tr surf)) ⬝ πnSn_surf n - definition deg_phomotopy {n : ℕ} [H : is_succ n] {f g : S* n →* S* n} (p : f ~* g) : + definition deg_phomotopy {n : ℕ} [H : is_succ n] {f g : S n →* S n} (p : f ~* g) : deg f = deg g := begin induction H with n, @@ -115,7 +115,7 @@ namespace sphere { symmetry, exact to_right_inv (equiv_of_isomorphism e) n} end - definition deg_compose {n : ℕ} [H : is_succ n] (f g : S* n →* S* n) : + definition deg_compose {n : ℕ} [H : is_succ n] (f g : S n →* S n) : deg (g ∘* f) = deg g *[ℤ] deg f := begin induction H with n, @@ -123,7 +123,7 @@ namespace sphere apply endomorphism_equiv_Z !πnSn !πnSn_surf (π→g[n+1] g) end - definition deg_equiv {n : ℕ} [H : is_succ n] (f : S* n ≃* S* n) : + definition deg_equiv {n : ℕ} [H : is_succ n] (f : S n ≃* S n) : deg f = 1 ⊎ deg f = -1 := begin induction H with n, diff --git a/homotopy/fwedge.hlean b/homotopy/fwedge.hlean index 26cf5eb..387e389 100644 --- a/homotopy/fwedge.hlean +++ b/homotopy/fwedge.hlean @@ -48,7 +48,7 @@ attribute fwedge.il fwedge.inl [constructor] namespace fwedge - definition fwedge_of_pwedge [unfold 3] {A B : Type*} (x : A ∨ B) : ⋁(bool.rec A B) := + definition fwedge_of_wedge [unfold 3] {A B : Type*} (x : A ∨ B) : ⋁(bool.rec A B) := begin induction x with a b, { exact inl ff a }, @@ -56,7 +56,7 @@ namespace fwedge { exact glue ff ⬝ (glue tt)⁻¹ } end - definition pwedge_of_fwedge [unfold 3] {A B : Type*} (x : ⋁(bool.rec A B)) : A ∨ B := + definition wedge_of_fwedge [unfold 3] {A B : Type*} (x : ⋁(bool.rec A B)) : A ∨ B := begin induction x with b x b, { induction b, exact pushout.inl x, exact pushout.inr x }, @@ -64,24 +64,24 @@ namespace fwedge { induction b, exact pushout.glue ⋆, reflexivity } end - definition pwedge_pequiv_fwedge [constructor] (A B : Type*) : A ∨ B ≃* ⋁(bool.rec A B) := + definition wedge_pequiv_fwedge [constructor] (A B : Type*) : A ∨ B ≃* ⋁(bool.rec A B) := begin fapply pequiv_of_equiv, { fapply equiv.MK, - { exact fwedge_of_pwedge }, - { exact pwedge_of_fwedge }, + { exact fwedge_of_wedge }, + { exact wedge_of_fwedge }, { exact abstract begin intro x, induction x with b x b, { induction b: reflexivity }, { exact glue tt }, { apply eq_pathover_id_right, - refine ap_compose fwedge_of_pwedge _ _ ⬝ ap02 _ !elim_glue ⬝ph _, + refine ap_compose fwedge_of_wedge _ _ ⬝ ap02 _ !elim_glue ⬝ph _, induction b, exact !elim_glue ⬝ph whisker_bl _ hrfl, apply square_of_eq idp } end end }, { exact abstract begin intro x, induction x with a b, { reflexivity }, { reflexivity }, { apply eq_pathover_id_right, - refine ap_compose pwedge_of_fwedge _ _ ⬝ ap02 _ !elim_glue ⬝ !ap_con ⬝ + refine ap_compose wedge_of_fwedge _ _ ⬝ ap02 _ !elim_glue ⬝ !ap_con ⬝ !elim_glue ◾ (!ap_inv ⬝ !elim_glue⁻²) ⬝ph _, exact hrfl } end end}}, { exact glue ff } end @@ -104,7 +104,7 @@ namespace fwedge { reflexivity } end - definition pwedge_pmap [constructor] {A B : Type*} {X : Type*} (f : A →* X) (g : B →* X) : (A ∨ B) →* X := + definition wedge_pmap [constructor] {A B : Type*} {X : Type*} (f : A →* X) (g : B →* X) : (A ∨ B) →* X := begin fapply pmap.mk, { intro x, induction x, exact (f a), exact (g a), exact (respect_pt (f) ⬝ (respect_pt g)⁻¹) }, @@ -149,9 +149,9 @@ namespace fwedge { intro g, apply eq_of_phomotopy, exact fwedge_pmap_eta g } end - definition pwedge_pmap_equiv [constructor] (A B X : Type*) : + definition wedge_pmap_equiv [constructor] (A B X : Type*) : ((A ∨ B) →* X) ≃ ((A →* X) × (B →* X)) := - calc (A ∨ B) →* X ≃ ⋁(bool.rec A B) →* X : by exact pequiv_ppcompose_right (pwedge_pequiv_fwedge A B)⁻¹ᵉ* + calc (A ∨ B) →* X ≃ ⋁(bool.rec A B) →* X : by exact pequiv_ppcompose_right (wedge_pequiv_fwedge A B)⁻¹ᵉ* ... ≃ Πi, (bool.rec A B) i →* X : by exact fwedge_pmap_equiv (bool.rec A B) X ... ≃ (A →* X) × (B →* X) : by exact pi_bool_left (λ i, bool.rec A B i →* X) @@ -211,16 +211,16 @@ namespace fwedge end -- hsquare 3: - definition fwedge_to_pwedge_nat_square {A B X Y : Type*} (f : X →* Y) : - hsquare (pequiv_ppcompose_right (pwedge_pequiv_fwedge A B)) (pequiv_ppcompose_right (pwedge_pequiv_fwedge A B)) (pcompose f) (pcompose f) := + definition fwedge_to_wedge_nat_square {A B X Y : Type*} (f : X →* Y) : + hsquare (pequiv_ppcompose_right (wedge_pequiv_fwedge A B)) (pequiv_ppcompose_right (wedge_pequiv_fwedge A B)) (pcompose f) (pcompose f) := begin exact sorry end - definition pwedge_pmap_nat₂ (A B X Y : Type*) (f : X →* Y) (h : A →* X) (k : B →* X) : Π (w : A ∨ B), - (f ∘* (pwedge_pmap h k)) w = pwedge_pmap (f ∘* h )(f ∘* k) w := + definition wedge_pmap_nat₂ (A B X Y : Type*) (f : X →* Y) (h : A →* X) (k : B →* X) : Π (w : A ∨ B), + (f ∘* (wedge_pmap h k)) w = wedge_pmap (f ∘* h )(f ∘* k) w := have H : _, from - (@prod_to_pi_bool_nat_square A B X Y f) ⬝htyh (fwedge_pmap_nat_square f) ⬝htyh (fwedge_to_pwedge_nat_square f), + (@prod_to_pi_bool_nat_square A B X Y f) ⬝htyh (fwedge_pmap_nat_square f) ⬝htyh (fwedge_to_wedge_nat_square f), sorry -- SA to here 7/5 diff --git a/homotopy/pushout.hlean b/homotopy/pushout.hlean index 38f7a8f..8ea2578 100644 --- a/homotopy/pushout.hlean +++ b/homotopy/pushout.hlean @@ -501,7 +501,7 @@ namespace pushout /- cofiber of pcod is suspension -/ - definition pcofiber_pcod {A B : Type*} (f : A →* B) : pcofiber (pcod f) ≃* psusp A := + definition pcofiber_pcod {A B : Type*} (f : A →* B) : pcofiber (pcod f) ≃* susp A := begin fapply pequiv_of_equiv, { refine !pushout.symm ⬝e _, diff --git a/homotopy/realprojective.hlean b/homotopy/realprojective.hlean index 6930671..1a8596d 100644 --- a/homotopy/realprojective.hlean +++ b/homotopy/realprojective.hlean @@ -4,7 +4,7 @@ import homotopy.join open eq nat susp pointed pmap sigma is_equiv equiv fiber is_trunc trunc - trunc_index is_conn sphere_index bool unit join pushout + trunc_index is_conn bool unit join pushout definition of_is_contr (A : Type) : is_contr A → A := @center A @@ -23,7 +23,7 @@ definition sigma_eq_equiv' {A : Type} (B : A → Type) : (⟨a₁, b₁⟩ = ⟨a₂, b₂⟩) ≃ (Σ(p : a₁ = a₂), p ▸ b₁ = b₂) := calc (⟨a₁, b₁⟩ = ⟨a₂, b₂⟩) ≃ Σ(p : a₁ = a₂), b₁ =[p] b₂ : sigma_eq_equiv -... ≃ Σ(p : a₁ = a₂), p ▸ b₁ = b₂ +... ≃ Σ(p : a₁ = a₂), p ▸ b₁ = b₂ : by apply sigma_equiv_sigma_right; intro e; apply pathover_equiv_tr_eq definition dec_eq_is_prop [instance] (A : Type) : is_prop (decidable_eq A) := @@ -88,7 +88,7 @@ calc (A = B) ... ≃ (BoolType.carrier A = BoolType.carrier B) : begin induction A with A p, induction B with B q, - symmetry, esimp, apply equiv_subtype + symmetry, esimp, apply equiv_subtype end ... ≃ (A ≃ B) : eq_equiv_equiv A B @@ -134,7 +134,7 @@ begin induction f with f, induction f, induction x, { apply is_contr.mk ⟨ equiv_bnot, idp ⟩, intro w, induction w with e p, symmetry, - apply to_inv (lemma_II_4 tt ff e equiv_bnot p idp), + apply to_inv (lemma_II_4 tt ff e equiv_bnot p idp), fapply sigma.mk, { intro b, induction b, { exact theorem_II_2_lemma_2 e p }, @@ -220,19 +220,19 @@ begin { intro w, apply is_prop.elimo } } end -definition realprojective_two_cover : ℕ₋₁ → two_cover := -sphere_index.rec empty_two_cover (λ x, two_cover_step) +definition realprojective_two_cover : ℕ → two_cover := +nat.rec (two_cover_step empty_two_cover) (λ x, two_cover_step) -definition realprojective : ℕ₋₁ → Type₀ := +definition realprojective : ℕ → Type₀ := λ n, carrier (realprojective_two_cover n) -definition realprojective_cov [reducible] (n : ℕ₋₁) +definition realprojective_cov [reducible] (n : ℕ) : realprojective n → BoolType := λ x, BoolType.mk (cov (realprojective_two_cover n) x) (cov_eq (realprojective_two_cover n) x) -definition theorem_III_3_u [reducible] (n : ℕ₋₁) +definition theorem_III_3_u [reducible] (n : ℕ) : (Σ (w : Σ x, realprojective_cov n x), realprojective_cov n w.1) ≃ (Σ x, realprojective_cov n x) × bool := calc (Σ (w : Σ x, realprojective_cov n x), realprojective_cov n w.1) @@ -245,14 +245,14 @@ calc (Σ (w : Σ x, realprojective_cov n x), realprojective_cov n w.1) ... ≃ (Σ x, realprojective_cov n x) × bool : equiv_prod -definition theorem_III_3 (n : ℕ₋₁) +definition theorem_III_3 (n : ℕ) : sphere n ≃ sigma (realprojective_cov n) := begin induction n with n IH, - { symmetry, apply sigma_empty_left }, - { apply equiv.trans (join.bool (sphere n))⁻¹ᵉ, - apply equiv.trans (join.equiv_closed erfl IH), - symmetry, refine equiv.trans _ !join.symm, + { symmetry, apply sorry /-sigma_empty_left-/ }, + { apply equiv.trans (join_bool (sphere n))⁻¹ᵉ, + apply equiv.trans (join_equiv_join erfl IH), + symmetry, refine equiv.trans _ !join_symm, apply equiv.trans !pushout.flattening, esimp, fapply pushout.equiv, { unfold function.compose, exact theorem_III_3_u n}, diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean index 4757257..04d0fd4 100644 --- a/homotopy/smash.hlean +++ b/homotopy/smash.hlean @@ -752,9 +752,9 @@ namespace smash definition smash_pequiv_right [constructor] (A : Type*) (g : B ≃* D) : A ∧ B ≃* A ∧ D := smash_pequiv pequiv.rfl g - /- A ∧ B ≃* pcofiber (pprod_of_pwedge A B) -/ + /- A ∧ B ≃* pcofiber (pprod_of_wedge A B) -/ - definition prod_of_wedge [unfold 3] (v : pwedge A B) : A × B := + definition prod_of_wedge [unfold 3] (v : wedge A B) : A × B := begin induction v with a b , { exact (a, pt) }, @@ -762,7 +762,7 @@ namespace smash { reflexivity } end - definition wedge_of_sum [unfold 3] (v : A + B) : pwedge A B := + definition wedge_of_sum [unfold 3] (v : A + B) : wedge A B := begin induction v with a b, { exact pushout.inl a }, @@ -780,7 +780,7 @@ end smash open smash namespace pushout - definition eq_inl_pushout_wedge_of_sum [unfold 3] (v : pwedge A B) : + 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, @@ -856,14 +856,14 @@ namespace smash refine !con.right_inv ⬝pv _, exact square_of_eq idp }, end - definition pprod_of_pwedge [constructor] : pwedge A B →* A ×* B := + definition pprod_of_wedge [constructor] : wedge A B →* A ×* B := begin fconstructor, { exact prod_of_wedge }, { reflexivity } end - definition smash_pequiv_pcofiber [constructor] : smash A B ≃* pcofiber (pprod_of_pwedge A B) := + definition smash_pequiv_pcofiber [constructor] : smash A B ≃* pcofiber (pprod_of_wedge A B) := begin apply pequiv_of_equiv (smash_equiv_cofiber A B), exact cofiber.glue pt diff --git a/homotopy/smash_adjoint.hlean b/homotopy/smash_adjoint.hlean index 93121bc..10cc21d 100644 --- a/homotopy/smash_adjoint.hlean +++ b/homotopy/smash_adjoint.hlean @@ -506,77 +506,78 @@ namespace smash 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 := + definition smash_susp_elim_equiv (A B X : Type*) : + ppmap (A ∧ susp B) X ≃* ppmap (susp (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 (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) : smash_adjoint_pmap A B (Ω X) - ... ≃* ppmap (psusp (A ∧ B)) X : psusp_adjoint_loop' (A ∧ B) X + ... ≃* ppmap (susp (A ∧ B)) X : susp_adjoint_loop' (A ∧ B) X - definition smash_psusp_elim_natural_right (A B : Type*) (f : X →* X') : - psquare (smash_psusp_elim_equiv A B X) (smash_psusp_elim_equiv 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') (ppcompose_left f) (ppcompose_left f) := smash_adjoint_pmap_natural_right f ⬝h* - psusp_adjoint_loop_natural_right (ppcompose_left f) ⬝h* + susp_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)⁻¹ʰ* + (susp_adjoint_loop_natural_right f)⁻¹ʰ* - definition smash_psusp_elim_natural_left (X : Type*) (f : A' →* A) (g : B' →* B) : - psquare (smash_psusp_elim_equiv A B X) (smash_psusp_elim_equiv A' B' X) - (ppcompose_right (f ∧→ psusp_functor g)) (ppcompose_right (psusp_functor (f ∧→ g))) := + 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))) := begin - refine smash_adjoint_pmap_natural_lm X f (psusp_functor g) ⬝h* + refine smash_adjoint_pmap_natural_lm X f (susp_functor g) ⬝h* _ ⬝h* _ ⬝h* (smash_adjoint_pmap_natural_lm (Ω X) f g)⁻¹ʰ* ⬝h* - (psusp_adjoint_loop_natural_left (f ∧→ g))⁻¹ʰ*, + (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 psusp_adjoint_loop_natural_left g ⬝v* psusp_adjoint_loop_natural_right (ppcompose_right f) + exact susp_adjoint_loop_natural_left g ⬝v* susp_adjoint_loop_natural_right (ppcompose_right f) end - definition smash_psusp (A B : Type*) : A ∧ ⅀ B ≃* ⅀(A ∧ B) := + definition smash_susp (A B : Type*) : A ∧ ⅀ B ≃* ⅀(A ∧ B) := begin fapply pequiv.MK, - { exact !smash_psusp_elim_equiv⁻¹ᵉ* !pid }, - { exact !smash_psusp_elim_equiv !pid }, - { refine phomotopy_of_eq (!smash_psusp_elim_natural_right⁻¹ʰ* _) ⬝* _, - refine pap !smash_psusp_elim_equiv⁻¹ᵉ* !pcompose_pid ⬝* _, - apply phomotopy_of_eq, apply to_left_inv !smash_psusp_elim_equiv }, - { refine phomotopy_of_eq (!smash_psusp_elim_natural_right _) ⬝* _, - refine pap !smash_psusp_elim_equiv !pcompose_pid ⬝* _, - apply phomotopy_of_eq, apply to_right_inv !smash_psusp_elim_equiv } + { 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 } end - definition smash_psusp_natural (f : A →* A') (g : B →* B') : - psquare (smash_psusp A B) (smash_psusp A' B') (f ∧→ (psusp_functor g)) (psusp_functor (f ∧→ g)) := + 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_psusp_elim_natural_right⁻¹ʰ* _) ⬝* _, - refine pap !smash_psusp_elim_equiv⁻¹ᵉ* (!pcompose_pid ⬝* !pid_pcompose⁻¹*) ⬝* _, - rexact phomotopy_of_eq ((smash_psusp_elim_natural_left _ f g)⁻¹ʰ* !pid)⁻¹ + 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 smash_iterate_psusp (n : ℕ) (A B : Type*) : A ∧ iterate_psusp n B ≃* iterate_psusp n (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 induction n with n e, { reflexivity }, - { exact smash_psusp A (iterate_psusp n B) ⬝e* psusp_pequiv e } + { exact smash_susp A (iterate_susp n B) ⬝e* susp_pequiv e } end - definition smash_sphere (A : Type*) (n : ℕ) : A ∧ psphere n ≃* iterate_psusp n A := - smash_pequiv pequiv.rfl (psphere_pequiv_iterate_psusp n) ⬝e* - smash_iterate_psusp n A pbool ⬝e* - iterate_psusp_pequiv n (smash_pbool_pequiv A) + definition smash_sphere (A : Type*) (n : ℕ) : A ∧ sphere n ≃* iterate_susp n A := + smash_pequiv 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 ≃* psusp A := + definition smash_pcircle (A : Type*) : A ∧ pcircle ≃* susp A := smash_sphere A 1 - definition sphere_smash_sphere (n m : ℕ) : psphere n ∧ psphere m ≃* psphere (n+m) := - smash_sphere (psphere n) m ⬝e* - iterate_psusp_pequiv m (psphere_pequiv_iterate_psusp n) ⬝e* - iterate_psusp_iterate_psusp_rev m n pbool ⬝e* - (psphere_pequiv_iterate_psusp (n + m))⁻¹ᵉ* + definition sphere_smash_sphere (n m : ℕ) : sphere n ∧ sphere m ≃* sphere (n+m) := + smash_sphere (sphere n) m ⬝e* + iterate_susp_pequiv m (sphere_pequiv_iterate_susp n) ⬝e* + iterate_susp_iterate_susp_rev m n pbool ⬝e* + (sphere_pequiv_iterate_susp (n + m))⁻¹ᵉ* end smash diff --git a/homotopy/spherical_fibrations.hlean b/homotopy/spherical_fibrations.hlean index 6c81560..8bbb8f0 100644 --- a/homotopy/spherical_fibrations.hlean +++ b/homotopy/spherical_fibrations.hlean @@ -1,29 +1,29 @@ -import homotopy.join homotopy.smash +import homotopy.join homotopy.smash types.nat.hott -open eq equiv trunc function bool join sphere sphere_index sphere.ops prod -open pointed sigma smash is_trunc +open eq equiv trunc function bool join sphere sphere.ops prod +open pointed sigma smash is_trunc nat namespace spherical_fibrations /- classifying type of spherical fibrations -/ - definition BG (n : ℕ) : Type₁ := - Σ(X : Type₀), ∥ X ≃ S n..-1 ∥ + definition BG (n : ℕ) [is_succ n] : Type₁ := + Σ(X : Type₀), ∥ X ≃ S (pred n) ∥ - definition pointed_BG [instance] [constructor] (n : ℕ) : pointed (BG n) := - pointed.mk ⟨ S n..-1 , tr erfl ⟩ + definition pointed_BG [instance] [constructor] (n : ℕ) [is_succ n] : pointed (BG n) := + pointed.mk ⟨ S (pred n) , tr erfl ⟩ - definition pBG [constructor] (n : ℕ) : Type* := pointed.mk' (BG n) + definition pBG [constructor] (n : ℕ) [is_succ n] : Type* := pointed.mk' (BG n) - definition G (n : ℕ) : Type₁ := + definition G (n : ℕ) [is_succ n] : Type₁ := pt = pt :> BG n - definition G_char (n : ℕ) : G n ≃ (S n..-1 ≃ S n..-1) := + definition G_char (n : ℕ) [is_succ n] : G n ≃ (S (pred n) ≃ S (pred n)) := calc - G n ≃ Σ(p : S n..-1 = S n..-1), _ : sigma_eq_equiv - ... ≃ (S n..-1 = S n..-1) : sigma_equiv_of_is_contr_right - ... ≃ (S n..-1 ≃ S n..-1) : eq_equiv_equiv + G n ≃ Σ(p : pType.carrier (S (pred n)) = pType.carrier (S (pred n))), _ : sigma_eq_equiv + ... ≃ (pType.carrier (S (pred n)) = pType.carrier (S (pred n))) : sigma_equiv_of_is_contr_right + ... ≃ (S (pred n) ≃ S (pred n)) : eq_equiv_equiv - definition mirror (n : ℕ) : S n..-1 → G n := + definition mirror (n : ℕ) [is_succ n] : S (pred n) → G n := begin intro v, apply to_inv (G_char n), exact sorry @@ -35,35 +35,38 @@ namespace spherical_fibrations Yes, let eval : BG (n+1) → S n be the evaluation map -/ + definition is_succ_1 [instance] : is_succ 1 := is_succ.mk 0 definition S_of_BG (n : ℕ) : Ω(pBG (n+1)) → S n := - λ f, f..1 ▸ base + λ f, f..1 ▸ pt - definition BG_succ (n : ℕ) : BG n → BG (n+1) := + definition BG_succ (n : ℕ) [H : is_succ n] : BG n → BG (n+1) := begin + induction H with n, intro X, cases X with X p, - apply sigma.mk (susp X), induction p with f, apply tr, - apply susp.equiv f + refine sigma.mk (susp X) _, induction p with f, apply tr, + exact susp.equiv f end /- classifying type of pointed spherical fibrations -/ definition BF (n : ℕ) : Type₁ := - Σ(X : Type*), ∥ X ≃* S* n ∥ + Σ(X : Type*), ∥ X ≃* S n ∥ definition pointed_BF [instance] [constructor] (n : ℕ) : pointed (BF n) := - pointed.mk ⟨ S* n , tr pequiv.rfl ⟩ + pointed.mk ⟨ S n , tr pequiv.rfl ⟩ definition pBF [constructor] (n : ℕ) : Type* := pointed.mk' (BF n) definition BF_succ (n : ℕ) : BF n → BF (n+1) := begin intro X, cases X with X p, - apply sigma.mk (psusp X), induction p with f, apply tr, - apply susp.psusp_pequiv f + apply sigma.mk (susp X), induction p with f, apply tr, + apply susp.susp_pequiv f end - definition BF_of_BG {n : ℕ} : BG n → BF n := + definition BF_of_BG {n : ℕ} [H : is_succ n] : BG n → BF n := begin + induction H with n, intro X, cases X with X p, apply sigma.mk (pointed.MK (susp X) susp.north), induction p with f, apply tr, @@ -78,13 +81,15 @@ namespace spherical_fibrations apply tr, exact fX end - definition BG_mul {n m : ℕ} (X : BG n) (Y : BG m) : BG (n + m) := + definition BG_mul {n m : ℕ} [Hn : is_succ n] [Hm : is_succ m] (X : BG n) (Y : BG m) : + BG (n + m) := begin + induction Hn with n, induction Hm with m, cases X with X pX, cases Y with Y pY, apply sigma.mk (join X Y), induction pX with fX, induction pY with fY, - apply tr, rewrite add_sub_one, - exact (join.equiv_closed fX fY) ⬝e (join.spheres n..-1 m..-1) + apply tr, rewrite [succ_add], + exact join_equiv_join fX fY ⬝e join_sphere n m end definition BF_mul {n m : ℕ} (X : BF n) (Y : BF m) : BF (n + m) := @@ -95,7 +100,7 @@ namespace spherical_fibrations exact sorry -- needs smash.spheres : psmash (S. n) (S. m) ≃ S. (n + m) end - definition BF_of_BG_mul (n m : ℕ) (X : BG n) (Y : BG m) + definition BF_of_BG_mul (n m : ℕ) [is_succ n] [is_succ m] (X : BG n) (Y : BG m) : BF_of_BG (BG_mul X Y) = BF_mul (BF_of_BG X) (BF_of_BG Y) := sorry diff --git a/homotopy/susp.hlean b/homotopy/susp.hlean index 62675b2..4157da6 100644 --- a/homotopy/susp.hlean +++ b/homotopy/susp.hlean @@ -5,13 +5,8 @@ open susp eq pointed function is_equiv lift equiv is_trunc nat namespace susp variables {X X' Y Y' Z : Type*} - /- TODO: remove susp and rename psusp to susp -/ - definition psuspn : ℕ → Type* → Type* - | psuspn 0 X := X - | psuspn (succ n) X := psusp (psuspn n X) - - definition susp_functor_pconst_homotopy [unfold 3] {X Y : Type*} (x : psusp X) : - psusp_functor (pconst X Y) x = pt := + definition susp_functor_pconst_homotopy [unfold 3] {X Y : Type*} (x : susp X) : + susp_functor (pconst X Y) x = pt := begin induction x, { reflexivity }, @@ -19,81 +14,81 @@ namespace susp { 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) := + definition susp_functor_pconst [constructor] (X Y : Type*) : susp_functor (pconst X Y) ~* pconst (susp X) (susp 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 susp_pfunctor [constructor] (X Y : Type*) : ppmap X Y →* ppmap (susp X) (susp Y) := + pmap.mk susp_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 susp_pelim [constructor] (X Y : Type*) : ppmap X (Ω Y) →* ppmap (susp X) Y := + ppcompose_left (loop_susp_counit Y) ∘* susp_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_susp_pintro [constructor] (X Y : Type*) : ppmap (susp X) Y →* ppmap X (Ω Y) := + ppcompose_right (loop_susp_unit X) ∘* pap1 (susp 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_susp_pintro_natural_left (f : X' →* X) : + psquare (loop_susp_pintro X Y) (loop_susp_pintro X' Y) + (ppcompose_right (susp_functor f)) (ppcompose_right f) := + !pap1_natural_left ⬝h* ppcompose_right_psquare (loop_susp_unit_natural f)⁻¹* - definition loop_psusp_pintro_natural_right (f : Y →* Y') : - psquare (loop_psusp_pintro X Y) (loop_psusp_pintro X Y') + definition loop_susp_pintro_natural_right (f : Y →* Y') : + psquare (loop_susp_pintro X Y) (loop_susp_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) := + definition is_equiv_loop_susp_pintro [constructor] (X Y : Type*) : + is_equiv (loop_susp_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 } + { exact susp_pelim X Y }, + { intro g, apply eq_of_phomotopy, exact susp_adjoint_loop_right_inv g }, + { intro f, apply eq_of_phomotopy, exact susp_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 susp_adjoint_loop' [constructor] (X Y : Type*) : ppmap (susp X) Y ≃* ppmap X (Ω Y) := + pequiv_of_pmap (loop_susp_pintro X Y) (is_equiv_loop_susp_pintro X Y) - definition psusp_adjoint_loop_natural_right (f : Y →* Y') : - psquare (psusp_adjoint_loop' X Y) (psusp_adjoint_loop' X Y') + definition susp_adjoint_loop_natural_right (f : Y →* Y') : + psquare (susp_adjoint_loop' X Y) (susp_adjoint_loop' X Y') (ppcompose_left f) (ppcompose_left (Ω→ f)) := - loop_psusp_pintro_natural_right f + loop_susp_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 + definition susp_adjoint_loop_natural_left (f : X' →* X) : + psquare (susp_adjoint_loop' X Y) (susp_adjoint_loop' X' Y) + (ppcompose_right (susp_functor f)) (ppcompose_right f) := + loop_susp_pintro_natural_left f - definition iterate_psusp_iterate_psusp_rev (n m : ℕ) (A : Type*) : - iterate_psusp n (iterate_psusp m A) ≃* iterate_psusp (m + n) A := + definition iterate_susp_iterate_susp_rev (n m : ℕ) (A : Type*) : + iterate_susp n (iterate_susp m A) ≃* iterate_susp (m + n) A := begin induction n with n e, { reflexivity }, - { exact psusp_pequiv e } + { exact susp_pequiv e } end - definition iterate_psusp_pequiv [constructor] (n : ℕ) {X Y : Type*} (f : X ≃* Y) : - iterate_psusp n X ≃* iterate_psusp n Y := + definition iterate_susp_pequiv [constructor] (n : ℕ) {X Y : Type*} (f : X ≃* Y) : + iterate_susp n X ≃* iterate_susp n Y := begin induction n with n e, { exact f }, - { exact psusp_pequiv e } + { exact susp_pequiv e } end open algebra nat - definition iterate_psusp_iterate_psusp (n m : ℕ) (A : Type*) : - iterate_psusp n (iterate_psusp m A) ≃* iterate_psusp (n + m) A := - iterate_psusp_iterate_psusp_rev n m A ⬝e* pequiv_of_eq (ap (λk, iterate_psusp k A) (add.comm m n)) + definition iterate_susp_iterate_susp (n m : ℕ) (A : Type*) : + iterate_susp n (iterate_susp m A) ≃* iterate_susp (n + m) A := + iterate_susp_iterate_susp_rev n m A ⬝e* pequiv_of_eq (ap (λk, iterate_susp k A) (add.comm m n)) - definition plift_psusp.{u v} : Π(A : Type*), plift.{u v} (psusp A) ≃* psusp (plift.{u v} A) := + definition plift_susp.{u v} : Π(A : Type*), plift.{u v} (susp A) ≃* susp (plift.{u v} A) := begin intro A, calc - plift.{u v} (psusp A) ≃* psusp A : by exact (pequiv_plift (psusp A))⁻¹ᵉ* - ... ≃* psusp (plift.{u v} A) : by exact psusp_pequiv (pequiv_plift.{u v} A) + plift.{u v} (susp A) ≃* susp A : by exact (pequiv_plift (susp A))⁻¹ᵉ* + ... ≃* susp (plift.{u v} A) : by exact susp_pequiv (pequiv_plift.{u v} A) end definition is_contr_susp [instance] (A : Type) [H : is_contr A] : is_contr (susp A) := @@ -106,32 +101,30 @@ namespace susp exact whisker_left idp (ap merid !eq_of_is_contr) end - definition is_contr_psusp [instance] (A : Type) [H : is_contr A] : is_contr (psusp A) := - is_contr_susp A - -definition psusp_pelim2 {X Y : Type*} {f g : ⅀ X →* Y} (p : f ~* g) : ((loop_psusp_pintro X Y) f) ~* ((loop_psusp_pintro X Y) g) := -pwhisker_right (loop_psusp_unit X) (Ω⇒ p) + definition loop_susp_pintro_phomotopy {X Y : Type*} {f g : ⅀ X →* Y} (p : f ~* g) : + loop_susp_pintro X Y f ~* loop_susp_pintro X Y g := + pwhisker_right (loop_susp_unit X) (Ω⇒ p) variables {A₀₀ A₂₀ A₀₂ A₂₂ : Type*} {f₁₀ : A₀₀ →* A₂₀} {f₁₂ : A₀₂ →* A₂₂} {f₀₁ : A₀₀ →* A₀₂} {f₂₁ : A₂₀ →* A₂₂} - -- rename: psusp_functor_psquare + -- rename: susp_functor_psquare definition suspend_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : psquare (⅀→ f₁₀) (⅀→ f₁₂) (⅀→ f₀₁) (⅀→ f₂₁) := sorry - definition susp_to_loop_psquare (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : psusp A₀₀ →* A₀₂) (f₂₁ : psusp A₂₀ →* A₂₂) : (psquare (⅀→ f₁₀) f₁₂ f₀₁ f₂₁) → (psquare f₁₀ (Ω→ f₁₂) ((loop_psusp_pintro A₀₀ A₀₂) f₀₁) ((loop_psusp_pintro A₂₀ A₂₂) f₂₁)) := + definition susp_to_loop_psquare (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : susp A₀₀ →* A₀₂) (f₂₁ : susp A₂₀ →* A₂₂) : (psquare (⅀→ f₁₀) f₁₂ f₀₁ f₂₁) → (psquare f₁₀ (Ω→ f₁₂) ((loop_susp_pintro A₀₀ A₀₂) f₀₁) ((loop_susp_pintro A₂₀ A₂₂) f₂₁)) := begin intro p, refine pvconcat _ (ap1_psquare p), - exact loop_psusp_unit_natural f₁₀ + exact loop_susp_unit_natural f₁₀ end - definition loop_to_susp_square (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : A₀₀ →* Ω A₀₂) (f₂₁ : A₂₀ →* Ω A₂₂) : (psquare f₁₀ (Ω→ f₁₂) f₀₁ f₂₁) → (psquare (⅀→ f₁₀) f₁₂ ((psusp_pelim A₀₀ A₀₂) f₀₁) ((psusp_pelim A₂₀ A₂₂) f₂₁)) := + definition loop_to_susp_square (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : A₀₀ →* Ω A₀₂) (f₂₁ : A₂₀ →* Ω A₂₂) : (psquare f₁₀ (Ω→ f₁₂) f₀₁ f₂₁) → (psquare (⅀→ f₁₀) f₁₂ ((susp_pelim A₀₀ A₀₂) f₀₁) ((susp_pelim A₂₀ A₂₂) f₂₁)) := begin intro p, refine pvconcat (suspend_psquare p) _, - exact psquare_transpose (loop_psusp_counit_natural f₁₂) + exact psquare_transpose (loop_susp_counit_natural f₁₂) end end susp diff --git a/homotopy/wedge.hlean b/homotopy/wedge.hlean index e60afe7..45e2531 100644 --- a/homotopy/wedge.hlean +++ b/homotopy/wedge.hlean @@ -6,7 +6,7 @@ open wedge pushout eq prod sum pointed equiv is_equiv unit lift namespace wedge - definition wedge_flip [unfold 3] {A B : Type*} (x : A ∨ B) : B ∨ A := + definition wedge_flip' [unfold 3] {A B : Type*} (x : A ∨ B) : B ∨ A := begin induction x, { exact inr a }, @@ -15,26 +15,29 @@ namespace wedge end -- TODO: fix precedences - definition pwedge_flip [constructor] (A B : Type*) : (A ∨ B) →* (B ∨ A) := - pmap.mk wedge_flip (glue ⋆)⁻¹ + definition wedge_flip [constructor] (A B : Type*) : A ∨ B →* B ∨ A := + pmap.mk wedge_flip' (glue ⋆)⁻¹ - definition wedge_flip_wedge_flip {A B : Type*} (x : A ∨ B) : wedge_flip (wedge_flip x) = x := + definition wedge_flip'_wedge_flip' [unfold 3] {A B : Type*} (x : A ∨ B) : wedge_flip' (wedge_flip' x) = x := begin induction x, { reflexivity }, { reflexivity }, { apply eq_pathover_id_right, apply hdeg_square, - exact ap_compose wedge_flip _ _ ⬝ ap02 _ !elim_glue ⬝ !ap_inv ⬝ !elim_glue⁻² ⬝ !inv_inv } + exact ap_compose wedge_flip' _ _ ⬝ ap02 _ !elim_glue ⬝ !ap_inv ⬝ !elim_glue⁻² ⬝ !inv_inv } end - definition pwedge_comm [constructor] (A B : Type*) : A ∨ B ≃* B ∨ A := + definition wedge_flip_wedge_flip (A B : Type*) : wedge_flip B A ∘* wedge_flip A B ~* pid (A ∨ B) := + phomotopy.mk wedge_flip'_wedge_flip' (whisker_right _ (!ap_inv ⬝ !wedge.elim_glue⁻²) ⬝ !con.left_inv)⁻¹ + + definition wedge_comm [constructor] (A B : Type*) : A ∨ B ≃* B ∨ A := begin - fapply pequiv.MK', - { exact pwedge_flip A B }, - { exact wedge_flip }, - { exact wedge_flip_wedge_flip }, - { exact wedge_flip_wedge_flip } + fapply pequiv.MK, + { exact wedge_flip A B }, + { exact wedge_flip B A }, + { exact wedge_flip_wedge_flip A B }, + { exact wedge_flip_wedge_flip B A } end -- TODO: wedge is associative @@ -53,15 +56,15 @@ namespace wedge end - definition pwedge_pequiv [constructor] {A A' B B' : Type*} (a : A ≃* A') (b : B ≃* B') : A ∨ B ≃* A' ∨ B' := + definition wedge_pequiv [constructor] {A A' B B' : Type*} (a : A ≃* A') (b : B ≃* B') : A ∨ B ≃* A' ∨ B' := begin fapply pequiv_of_equiv, exact pushout.equiv !pconst !pconst !pconst !pconst !pequiv.refl a b (λdummy, respect_pt a) (λdummy, respect_pt b), exact ap pushout.inl (respect_pt a) end - definition plift_pwedge.{u v} (A B : Type*) : plift.{u v} (A ∨ B) ≃* plift.{u v} A ∨ plift.{u v} B := + definition plift_wedge.{u v} (A B : Type*) : plift.{u v} (A ∨ B) ≃* plift.{u v} A ∨ plift.{u v} B := calc plift.{u v} (A ∨ B) ≃* A ∨ B : by exact !pequiv_plift⁻¹ᵉ* - ... ≃* plift.{u v} A ∨ plift.{u v} B : by exact pwedge_pequiv !pequiv_plift !pequiv_plift + ... ≃* plift.{u v} A ∨ plift.{u v} B : by exact wedge_pequiv !pequiv_plift !pequiv_plift end wedge diff --git a/move_to_lib.hlean b/move_to_lib.hlean index dfa5ddc..8413d76 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -174,6 +174,10 @@ namespace eq phomotopy_rec_on_idp phomotopy.rfl H = H := !phomotopy_rec_on_eq_phomotopy_of_eq + definition eq_tr_of_pathover_con_tr_eq_of_pathover {A : Type} {B : A → Type} + {a₁ a₂ : A} (p : a₁ = a₂) {b₁ : B a₁} {b₂ : B a₂} (q : b₁ =[p] b₂) : + eq_tr_of_pathover q ⬝ tr_eq_of_pathover q⁻¹ᵒ = idp := + by induction q; reflexivity end eq open eq @@ -477,6 +481,11 @@ namespace is_trunc end is_trunc namespace sigma + open sigma.ops + + definition sigma_eq_equiv_of_is_prop_right [constructor] {A : Type} {B : A → Type} (u v : Σa, B a) + [H : Π a, is_prop (B a)] : u = v ≃ u.1 = v.1 := + !sigma_eq_equiv ⬝e !sigma_equiv_of_is_contr_right definition ap_sigma_pr1 {A B : Type} {C : B → Type} {a₁ a₂ : A} (f : A → B) (g : Πa, C (f a)) (p : a₁ = a₂) : (ap (λa, ⟨f a, g a⟩) p)..1 = ap f p := @@ -903,13 +912,13 @@ end category namespace sphere - -- definition constant_sphere_map_sphere {n m : ℕ} (H : n < m) (f : S* n →* S* m) : - -- f ~* pconst (S* n) (S* m) := + -- definition constant_sphere_map_sphere {n m : ℕ} (H : n < m) (f : S n →* S m) : + -- f ~* pconst (S n) (S m) := -- begin - -- assert H : is_contr (Ω[n] (S* m)), + -- assert H : is_contr (Ω[n] (S m)), -- { apply homotopy_group_sphere_le, }, -- apply phomotopy_of_eq, - -- apply eq_of_fn_eq_fn !psphere_pmap_pequiv, + -- apply eq_of_fn_eq_fn !sphere_pmap_pequiv, -- apply @is_prop.elim -- end @@ -948,8 +957,8 @@ end injective_surjective -- Yuri Sulyma's code from HoTT MRC -notation `⅀→`:(max+5) := psusp_functor -notation `⅀⇒`:(max+5) := psusp_functor_phomotopy +notation `⅀→`:(max+5) := susp_functor +notation `⅀⇒`:(max+5) := susp_functor_phomotopy notation `Ω⇒`:(max+5) := ap1_phomotopy definition ap1_phomotopy_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : (Ω⇒ p)⁻¹* = Ω⇒ (p⁻¹*) := diff --git a/pointed.hlean b/pointed.hlean index 3591af6..bb50a18 100644 --- a/pointed.hlean +++ b/pointed.hlean @@ -37,6 +37,7 @@ 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 + /- 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)⁻¹ᵉ* diff --git a/pointed_pi.hlean b/pointed_pi.hlean index c6b58b1..9eb5e47 100644 --- a/pointed_pi.hlean +++ b/pointed_pi.hlean @@ -1014,6 +1014,8 @@ namespace pointed ppmap A₊ B ≃* A →ᵘ* B := pequiv_of_equiv (pmap_equiv_left A B) idp + /- There are some lemma's needed to prove the naturality of the equivalence + Ω (Π*a, B a) ≃* Π*(a : A), Ω (B a) -/ definition ppi_eq_equiv_natural_gen_lem {B C : A → Type} {b₀ : B pt} {c₀ : C pt} {f : Π(a : A), B a → C a} {f₀ : f pt b₀ = c₀} {k : ppi_gen B b₀} {k' : ppi_gen C c₀} (p : pmap_compose_ppi_gen f f₀ k ~~* k') : @@ -1086,6 +1088,7 @@ namespace pointed { exact !ppi_eq_equiv_natural_gen_refl ◾ (!idp_con ⬝ !ppi_eq_refl) } end + /- below is an alternate proof strategy for the naturality of loop_pppi_pequiv_natural, where we define loop_pppi_pequiv as composite of pointed equivalences, and proved the naturality individually. That turned out to be harder. diff --git a/spectrum/basic.hlean b/spectrum/basic.hlean index 8224ceb..7c96370 100644 --- a/spectrum/basic.hlean +++ b/spectrum/basic.hlean @@ -779,7 +779,7 @@ namespace spectrum -- Suspension prespectra are one that's naturally indexed on the natural numbers definition psp_susp (X : Type*) : gen_prespectrum +ℕ := - gen_prespectrum.mk (λn, psuspn n X) (λn, loop_psusp_unit (psuspn n X)) + gen_prespectrum.mk (λn, iterate_susp n X) (λn, loop_susp_unit (iterate_susp n X)) -- The sphere prespectrum definition psp_sphere : gen_prespectrum +ℕ := diff --git a/spectrum/smash.hlean b/spectrum/smash.hlean index 5b78779..1d9ab4a 100644 --- a/spectrum/smash.hlean +++ b/spectrum/smash.hlean @@ -7,10 +7,10 @@ namespace spectrum definition smash_prespectrum (X : Type*) (Y : prespectrum) : prespectrum := prespectrum.mk (λ z, X ∧ Y z) begin - intro n, refine loop_psusp_pintro (X ∧ Y n) (X ∧ Y (n + 1)) _, - refine _ ∘* (smash_psusp X (Y n))⁻¹ᵉ*, + intro n, refine loop_susp_pintro (X ∧ Y n) (X ∧ Y (n + 1)) _, + refine _ ∘* (smash_susp X (Y n))⁻¹ᵉ*, refine smash_functor !pid _, - refine psusp_pelim (Y n) (Y (n + 1)) _, + refine susp_pelim (Y n) (Y (n + 1)) _, exact !glue end @@ -18,11 +18,11 @@ definition smash_prespectrum_fun {X X' : Type*} {Y Y' : prespectrum} (f : X →* smap.mk (λn, smash_functor f (g n)) begin intro n, refine susp_to_loop_psquare _ _ _ _ _, - refine pvconcat (psquare_transpose (phinverse (smash_psusp_natural f (g n)))) _, + refine pvconcat (psquare_transpose (phinverse (smash_susp_natural f (g n)))) _, refine vconcat_phomotopy _ (smash_functor_split f (g (S n))), - refine phomotopy_vconcat (smash_functor_split f (psusp_functor (g n))) _, + refine phomotopy_vconcat (smash_functor_split f (susp_functor (g n))) _, refine phconcat _ _, - let glue_adjoint := psusp_pelim (Y n) (Y (S n)) (glue Y n), + let glue_adjoint := susp_pelim (Y n) (Y (S n)) (glue Y n), exact pid X' ∧→ glue_adjoint, exact smash_functor_psquare (pvrefl f) (phrefl glue_adjoint), refine smash_functor_psquare (phrefl (pid X')) _,