From ddef24223bd72d52a0332cb6bf280a13977f1cf0 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 20 Jul 2017 15:01:40 +0100 Subject: [PATCH] make pointed suspensions, wedges and spheres the default (in contrast to the unpointed ones), remove sphere_index All HITs which automatically have a point are pointed without a 'p' in front. HITs which do not automatically have a point do still have a p (e.g. pushout/ppushout). There were a lot of annoyances with spheres being indexed by N_{-1} with almost no extra generality. We now index the spheres by nat, making sphere 0 = pbool. --- hott/homotopy/EM.hlean | 12 +- hott/homotopy/cellcomplex.hlean | 2 +- hott/homotopy/circle.hlean | 17 +- hott/homotopy/cofiber.hlean | 2 +- hott/homotopy/complex_hopf.hlean | 23 +- hott/homotopy/connectedness.hlean | 3 + hott/homotopy/freudenthal.hlean | 100 ++++---- hott/homotopy/homotopy_group.hlean | 6 +- hott/homotopy/hopf.hlean | 16 +- hott/homotopy/imaginaroid.hlean | 2 +- hott/homotopy/interval.hlean | 2 +- hott/homotopy/join.hlean | 74 +++--- hott/homotopy/quaternionic_hopf.hlean | 32 +-- hott/homotopy/sphere.hlean | 343 +++----------------------- hott/homotopy/sphere2.hlean | 67 ++--- hott/homotopy/susp.hlean | 255 +++++++++---------- hott/homotopy/wedge.hlean | 19 +- 17 files changed, 334 insertions(+), 641 deletions(-) diff --git a/hott/homotopy/EM.hlean b/hott/homotopy/EM.hlean index 43dfa982a..adc51424a 100644 --- a/hott/homotopy/EM.hlean +++ b/hott/homotopy/EM.hlean @@ -226,10 +226,10 @@ namespace EM /- K(G, n+1) -/ definition EMadd1 : ℕ → Type* | 0 := EM1 G - | (n+1) := ptrunc (n+2) (psusp (EMadd1 n)) + | (n+1) := ptrunc (n+2) (susp (EMadd1 n)) definition EMadd1_succ [unfold_full] (n : ℕ) : - EMadd1 G (succ n) = ptrunc (n.+2) (psusp (EMadd1 G n)) := + EMadd1 G (succ n) = ptrunc (n.+2) (susp (EMadd1 G n)) := idp definition loop_EM2 : Ω[1] (EMadd1 G 1) ≃* EM1 G := @@ -239,7 +239,7 @@ namespace EM begin induction n with n IH, { apply is_conn_EM1 }, - { rewrite EMadd1_succ, esimp, exact _ } + { rewrite EMadd1_succ, exact _ } end definition is_trunc_EMadd1 [instance] (n : ℕ) : is_trunc (n+1) (EMadd1 G n) := @@ -304,12 +304,12 @@ 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) _ _)), + (susp_elim (f _ (EM_up e) (is_homomorphism_EM_up e r) _ _)), end definition EMadd1_pmap_succ {G : AbGroup} {X : Type*} (n : ℕ) (e : Ω[succ (succ n)] X ≃* G) r [H1 : is_conn (succ n) X] [H2 : is_trunc ((succ n).+1) X] : EMadd1_pmap (succ n) e r = - ptrunc.elim ((succ n).+1) (psusp.elim (EMadd1_pmap n (EM_up e) (is_homomorphism_EM_up e r))) := + ptrunc.elim ((succ n).+1) (susp_elim (EMadd1_pmap n (EM_up e) (is_homomorphism_EM_up e r))) := by reflexivity definition loop_EMadd1_pmap {G : AbGroup} {X : Type*} {n : ℕ} (e : Ω[succ (succ n)] X ≃* G) @@ -454,7 +454,7 @@ namespace EM begin induction n with n ψ, { exact EM1_functor φ }, - { apply ptrunc_functor, apply psusp_functor, exact ψ } + { apply ptrunc_functor, apply susp_functor, exact ψ } end definition EM_functor [unfold 4] {G H : AbGroup} (φ : G →g H) (n : ℕ) : diff --git a/hott/homotopy/cellcomplex.hlean b/hott/homotopy/cellcomplex.hlean index cd7f8771f..5ef55d238 100644 --- a/hott/homotopy/cellcomplex.hlean +++ b/hott/homotopy/cellcomplex.hlean @@ -5,7 +5,7 @@ Authors: Ulrik Buchholtz -/ import types.trunc homotopy.sphere hit.pushout -open eq is_trunc is_equiv nat equiv trunc prod pushout sigma sphere_index unit +open eq is_trunc is_equiv nat equiv trunc prod pushout sigma unit pointed -- where should this be? definition family : Type := ΣX, X → Type diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean index e75092eba..4166fabbd 100644 --- a/hott/homotopy/circle.hlean +++ b/hott/homotopy/circle.hlean @@ -10,7 +10,7 @@ import .sphere import types.int.hott import algebra.homotopy_group .connectedness -open eq susp bool sphere_index is_equiv equiv is_trunc is_conn pi algebra pointed +open eq susp bool is_equiv equiv is_trunc is_conn pi algebra pointed definition circle : Type₀ := sphere 1 @@ -18,8 +18,8 @@ namespace circle notation `S¹` := circle definition base1 : S¹ := !north definition base2 : S¹ := !south - definition seg1 : base1 = base2 := merid !north - definition seg2 : base1 = base2 := merid !south + definition seg1 : base1 = base2 := merid ff + definition seg2 : base1 = base2 := merid tt definition base : S¹ := base1 definition loop : base = base := seg2 ⬝ seg1⁻¹ @@ -28,12 +28,11 @@ namespace circle (Ps1 : Pb1 =[seg1] Pb2) (Ps2 : Pb1 =[seg2] Pb2) (x : S¹) : P x := begin induction x with b, - { exact Pb1}, - { exact Pb2}, + { exact Pb1 }, + { exact Pb2 }, { esimp at *, induction b with y, - { exact Ps1}, - { exact Ps2}, - { cases y}}, + { exact Ps1 }, + { exact Ps2 }}, end definition rec2_on [reducible] {P : S¹ → Type} (x : S¹) (Pb1 : P base1) (Pb2 : P base2) @@ -335,7 +334,7 @@ namespace circle end proposition is_conn_circle [instance] : is_conn 0 S¹ := - sphere.is_conn_sphere -1.+2 + sphere.is_conn_sphere 1 definition is_conn_pcircle [instance] : is_conn 0 S¹* := !is_conn_circle definition is_trunc_pcircle [instance] : is_trunc 1 S¹* := !is_trunc_circle diff --git a/hott/homotopy/cofiber.hlean b/hott/homotopy/cofiber.hlean index 36e20800c..adba6a1d3 100644 --- a/hott/homotopy/cofiber.hlean +++ b/hott/homotopy/cofiber.hlean @@ -92,7 +92,7 @@ namespace cofiber { exact !con_inv_cancel_left⁻¹ ⬝ idp ◾ (!ap_inv⁻¹ ◾ idp) } end - definition pcofiber_punit (A : Type*) : pcofiber (pconst A punit) ≃* psusp A := + definition pcofiber_punit (A : Type*) : pcofiber (pconst A punit) ≃* susp A := begin fapply pequiv_of_pmap, { fconstructor, intro x, induction x, exact north, exact south, exact merid x, diff --git a/hott/homotopy/complex_hopf.hlean b/hott/homotopy/complex_hopf.hlean index 4d91ba633..a425af5a1 100644 --- a/hott/homotopy/complex_hopf.hlean +++ b/hott/homotopy/complex_hopf.hlean @@ -10,6 +10,7 @@ The H-space structure on S¹ and the complex Hopf fibration import .hopf .circle types.fin open eq equiv is_equiv circle is_conn trunc is_trunc sphere susp pointed fiber sphere.ops function + join namespace hopf @@ -25,29 +26,27 @@ namespace hopf { exact natural_square (λa : S¹, ap (λb : S¹, b * z) (circle_mul_base a)) loop }, - { apply is_prop.elimo, apply is_trunc_square } } + { apply is_prop.elimo, apply is_trunc_square }} end - open sphere_index - - definition complex_hopf : S 3 → S 2 := + definition complex_hopf' : S 3 → S 2 := begin intro x, apply @sigma.pr1 (susp S¹) (hopf S¹), - apply inv (hopf.total S¹), apply inv (join.spheres 1 1), exact x + apply inv (hopf.total S¹), exact (join_sphere 1 1)⁻¹ᵉ x end - definition complex_phopf [constructor] : S* 3 →* S* 2 := - proof pmap.mk complex_hopf idp qed + definition complex_hopf [constructor] : S 3 →* S 2 := + proof pmap.mk complex_hopf' idp qed - definition pfiber_complex_phopf : pfiber complex_phopf ≃* S* 1 := + definition pfiber_complex_hopf : pfiber complex_hopf ≃* S 1 := begin fapply pequiv_of_equiv, - { esimp, unfold [complex_hopf], + { esimp, unfold [complex_hopf'], refine fiber.equiv_precompose (sigma.pr1 ∘ (hopf.total S¹)⁻¹ᵉ) - (join.spheres (of_nat 1) (of_nat 1))⁻¹ᵉ _ ⬝e _, + (join_sphere 1 1)⁻¹ᵉ _ ⬝e _, refine fiber.equiv_precompose _ (hopf.total S¹)⁻¹ᵉ _ ⬝e _, - apply fiber_pr1}, - { reflexivity} + apply fiber_pr1 }, + { reflexivity } end end hopf diff --git a/hott/homotopy/connectedness.hlean b/hott/homotopy/connectedness.hlean index 00e4fdabb..3fff7d6ef 100644 --- a/hott/homotopy/connectedness.hlean +++ b/hott/homotopy/connectedness.hlean @@ -269,6 +269,9 @@ namespace is_conn definition is_conn_minus_one (A : Type) (a : ∥ A ∥) : is_conn -1 A := is_contr.mk a (is_prop.elim _) + definition is_conn_minus_one_pointed [instance] (A : Type*) : is_conn -1 A := + is_conn_minus_one A (tr pt) + definition is_conn_trunc [instance] (A : Type) (n k : ℕ₋₂) [H : is_conn n A] : is_conn n (trunc k A) := begin diff --git a/hott/homotopy/freudenthal.hlean b/hott/homotopy/freudenthal.hlean index 07329ef14..5505fd669 100644 --- a/hott/homotopy/freudenthal.hlean +++ b/hott/homotopy/freudenthal.hlean @@ -17,12 +17,12 @@ namespace freudenthal section /- This proof is ported from Agda This is the 95% version of the Freudenthal Suspension Theorem, which means that we don't - prove that loop_psusp_unit : A →* Ω(psusp A) is 2n-connected (if A is n-connected), + prove that loop_susp_unit : A →* Ω(susp A) is 2n-connected (if A is n-connected), but instead we only prove that it induces an equivalence on the first 2n homotopy groups. -/ private definition up (a : A) : north = north :> susp A := - loop_psusp_unit A a + loop_susp_unit A a definition code_merid : A → ptrunc (n + n) A → ptrunc (n + n) A := begin @@ -127,7 +127,7 @@ namespace freudenthal section theorem decode_coh (a : A) : decode_north =[merid a] decode_south := begin - apply arrow_pathover_left, intro c, esimp at *, + apply arrow_pathover_left, intro c, induction c with a', rewrite [↑code, elim_type_merid], refine @wedge_extension.ext _ _ n n _ _ (λ a a', tr (up a') =[merid a] decode_south @@ -155,38 +155,38 @@ namespace freudenthal section end parameters (A n) - definition equiv' : trunc (n + n) A ≃ trunc (n + n) (Ω (psusp A)) := + definition equiv' : trunc (n + n) A ≃ trunc (n + n) (Ω (susp A)) := equiv.MK decode_north encode decode_encode encode_decode_north - definition pequiv' : ptrunc (n + n) A ≃* ptrunc (n + n) (Ω (psusp A)) := + definition pequiv' : ptrunc (n + n) A ≃* ptrunc (n + n) (Ω (susp A)) := pequiv_of_equiv equiv' decode_north_pt -- We don't prove this: - -- theorem freudenthal_suspension : is_conn_fun (n+n) (loop_psusp_unit A) := sorry + -- theorem freudenthal_suspension : is_conn_fun (n+n) (loop_susp_unit A) := sorry end end freudenthal open algebra group definition freudenthal_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n) - : ptrunc k A ≃* ptrunc k (Ω (psusp A)) := + : ptrunc k A ≃* ptrunc k (Ω (susp A)) := have H' : k ≤[ℕ₋₂] n + n, by rewrite [mul.comm at H, -algebra.zero_add n at {1}]; exact of_nat_le_of_nat H, ptrunc_pequiv_ptrunc_of_le H' (freudenthal.pequiv' A n) definition freudenthal_equiv {A : Type*} {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n) - : trunc k A ≃ trunc k (Ω (psusp A)) := + : trunc k A ≃ trunc k (Ω (susp A)) := freudenthal_pequiv A H definition freudenthal_homotopy_group_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n) - : π[k + 1] (psusp A) ≃* π[k] A := + : π[k + 1] (susp A) ≃* π[k] A := calc - π[k + 1] (psusp A) ≃* π[k] (Ω (psusp A)) : homotopy_group_succ_in (psusp A) k - ... ≃* Ω[k] (ptrunc k (Ω (psusp A))) : homotopy_group_pequiv_loop_ptrunc k (Ω (psusp A)) - ... ≃* Ω[k] (ptrunc k A) : loopn_pequiv_loopn k (freudenthal_pequiv A H) - ... ≃* π[k] A : (homotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ* + π[k + 1] (susp A) ≃* π[k] (Ω (susp A)) : homotopy_group_succ_in (susp A) k + ... ≃* Ω[k] (ptrunc k (Ω (susp A))) : homotopy_group_pequiv_loop_ptrunc k (Ω (susp A)) + ... ≃* Ω[k] (ptrunc k A) : loopn_pequiv_loopn k (freudenthal_pequiv A H) + ... ≃* π[k] A : (homotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ* definition freudenthal_homotopy_group_isomorphism (A : Type*) {n k : ℕ} [is_conn n A] - (H : k + 1 ≤ 2 * n) : πg[k+2] (psusp A) ≃g πg[k + 1] A := + (H : k + 1 ≤ 2 * n) : πg[k+2] (susp A) ≃g πg[k + 1] A := begin fapply isomorphism_of_equiv, { exact equiv_of_pequiv (freudenthal_homotopy_group_pequiv A H)}, @@ -199,7 +199,7 @@ begin end definition to_pmap_freudenthal_pequiv {A : Type*} (n k : ℕ) [is_conn n A] (H : k ≤ 2 * n) - : freudenthal_pequiv A H ~* ptrunc_functor k (loop_psusp_unit A) := + : freudenthal_pequiv A H ~* ptrunc_functor k (loop_susp_unit A) := begin fapply phomotopy.mk, { intro x, induction x with a, reflexivity }, @@ -208,24 +208,24 @@ end definition ptrunc_elim_freudenthal_pequiv {A B : Type*} (n k : ℕ) [is_conn n A] (H : k ≤ 2 * n) (f : A →* Ω B) [is_trunc (k.+1) (B)] : - ptrunc.elim k (Ω→ (psusp.elim f)) ∘* freudenthal_pequiv A H ~* ptrunc.elim k f := + ptrunc.elim k (Ω→ (susp_elim f)) ∘* freudenthal_pequiv A H ~* ptrunc.elim k f := begin refine pwhisker_left _ !to_pmap_freudenthal_pequiv ⬝* _, refine !ptrunc_elim_ptrunc_functor ⬝* _, - exact ptrunc_elim_phomotopy k !ap1_psusp_elim, + exact ptrunc_elim_phomotopy k !ap1_susp_elim, end namespace susp - definition iterate_psusp_stability_pequiv (A : Type*) {k n : ℕ} [is_conn 0 A] - (H : k ≤ 2 * n) : π[k + 1] (iterate_psusp (n + 1) A) ≃* π[k] (iterate_psusp n A) := - have is_conn n (iterate_psusp n A), by rewrite [-zero_add n]; exact _, - freudenthal_homotopy_group_pequiv (iterate_psusp n A) H + definition iterate_susp_stability_pequiv_of_is_conn_0 (A : Type*) {k n : ℕ} [is_conn 0 A] + (H : k ≤ 2 * n) : π[k + 1] (iterate_susp (n + 1) A) ≃* π[k] (iterate_susp n A) := + have is_conn n (iterate_susp n A), by rewrite [-zero_add n]; exact _, + freudenthal_homotopy_group_pequiv (iterate_susp n A) H - definition iterate_psusp_stability_isomorphism (A : Type*) {k n : ℕ} [is_conn 0 A] - (H : k + 1 ≤ 2 * n) : πg[k+2] (iterate_psusp (n + 1) A) ≃g πg[k+1] (iterate_psusp n A) := - have is_conn n (iterate_psusp n A), by rewrite [-zero_add n]; exact _, - freudenthal_homotopy_group_isomorphism (iterate_psusp n A) H + definition iterate_susp_stability_isomorphism_of_is_conn_0 (A : Type*) {k n : ℕ} [is_conn 0 A] + (H : k + 1 ≤ 2 * n) : πg[k+2] (iterate_susp (n + 1) A) ≃g πg[k+1] (iterate_susp n A) := + have is_conn n (iterate_susp n A), by rewrite [-zero_add n]; exact _, + freudenthal_homotopy_group_isomorphism (iterate_susp n A) H definition stability_helper1 {k n : ℕ} (H : k + 2 ≤ 2 * n) : k ≤ 2 * pred n := begin @@ -233,49 +233,43 @@ namespace susp apply pred_le_pred, apply pred_le_pred, exact H end - definition stability_helper2 (A : Type) {k n : ℕ} (H : k + 2 ≤ 2 * n) : - is_conn (pred n) (iterate_susp (n + 1) A) := - have Π(n : ℕ), n = -2 + (succ n + 1), + definition stability_helper2 (A : Type*) {k n : ℕ} (H : k + 2 ≤ 2 * n) : + is_conn (pred n) (iterate_susp n A) := + have Π(n : ℕ), n = -1 + (n + 1), begin intro n, induction n with n IH, reflexivity, exact ap succ IH end, begin cases n with n, - { exfalso, exact not_succ_le_zero _ H}, - { esimp, rewrite [this n], apply is_conn_iterate_susp} + { exfalso, exact not_succ_le_zero _ H }, + { esimp, rewrite [this n], exact is_conn_iterate_susp -1 _ A } end - definition iterate_susp_stability_pequiv (A : Type) {k n : ℕ} - (H : k + 2 ≤ 2 * n) : π[k + 1] (pointed.MK (iterate_susp (n + 2) A) !north) ≃* - π[k ] (pointed.MK (iterate_susp (n + 1) A) !north) := - have is_conn (pred n) (carrier (pointed.MK (iterate_susp (n + 1) A) !north)), from - stability_helper2 A H, - freudenthal_homotopy_group_pequiv (pointed.MK (iterate_susp (n + 1) A) !north) - (stability_helper1 H) + definition iterate_susp_stability_pequiv (A : Type*) {k n : ℕ} + (H : k + 2 ≤ 2 * n) : π[k + 1] (iterate_susp (n + 1) A) ≃* π[k] (iterate_susp n A) := + have is_conn (pred n) (iterate_susp n A), from stability_helper2 A H, + freudenthal_homotopy_group_pequiv (iterate_susp n A) (stability_helper1 H) - definition iterate_susp_stability_isomorphism (A : Type) {k n : ℕ} - (H : k + 3 ≤ 2 * n) : πg[k+1 +1] (pointed.MK (iterate_susp (n + 2) A) !north) ≃g - πg[k+1] (pointed.MK (iterate_susp (n + 1) A) !north) := - have is_conn (pred n) (carrier (pointed.MK (iterate_susp (n + 1) A) !north)), from - @stability_helper2 A (k+1) n H, - freudenthal_homotopy_group_isomorphism (pointed.MK (iterate_susp (n + 1) A) !north) - (stability_helper1 H) + definition iterate_susp_stability_isomorphism (A : Type*) {k n : ℕ} + (H : k + 3 ≤ 2 * n) : πg[k+2] (iterate_susp (n + 1) A) ≃g πg[k+1] (iterate_susp n A) := + have is_conn (pred n) (iterate_susp n A), from @stability_helper2 A (k+1) n H, + freudenthal_homotopy_group_isomorphism (iterate_susp n A) (stability_helper1 H) definition iterated_freudenthal_pequiv (A : Type*) {n k m : ℕ} [HA : is_conn n A] (H : k ≤ 2 * n) - : ptrunc k A ≃* ptrunc k (Ω[m] (iterate_psusp m A)) := + : ptrunc k A ≃* ptrunc k (Ω[m] (iterate_susp m A)) := begin revert A n k HA H, induction m with m IH: intro A n k HA H, - { reflexivity}, + { reflexivity }, { have H2 : succ k ≤ 2 * succ n, from calc succ k ≤ succ (2 * n) : succ_le_succ H ... ≤ 2 * succ n : self_le_succ, exact calc - ptrunc k A ≃* ptrunc k (Ω (psusp A)) : freudenthal_pequiv A H - ... ≃* Ω (ptrunc (succ k) (psusp A)) : loop_ptrunc_pequiv - ... ≃* Ω (ptrunc (succ k) (Ω[m] (iterate_psusp m (psusp A)))) : - loop_pequiv_loop (IH (psusp A) (succ n) (succ k) _ H2) - ... ≃* ptrunc k (Ω[succ m] (iterate_psusp m (psusp A))) : loop_ptrunc_pequiv - ... ≃* ptrunc k (Ω[succ m] (iterate_psusp (succ m) A)) : - ptrunc_pequiv_ptrunc _ (loopn_pequiv_loopn _ !iterate_psusp_succ_in)} + ptrunc k A ≃* ptrunc k (Ω (susp A)) : freudenthal_pequiv A H + ... ≃* Ω (ptrunc (succ k) (susp A)) : loop_ptrunc_pequiv + ... ≃* Ω (ptrunc (succ k) (Ω[m] (iterate_susp m (susp A)))) : + loop_pequiv_loop (IH (susp A) (succ n) (succ k) _ H2) + ... ≃* ptrunc k (Ω[succ m] (iterate_susp m (susp A))) : loop_ptrunc_pequiv + ... ≃* ptrunc k (Ω[succ m] (iterate_susp (succ m) A)) : + ptrunc_pequiv_ptrunc _ (loopn_pequiv_loopn _ !iterate_susp_succ_in)} end end susp diff --git a/hott/homotopy/homotopy_group.hlean b/hott/homotopy/homotopy_group.hlean index 3c56158d2..448c8f404 100644 --- a/hott/homotopy/homotopy_group.hlean +++ b/hott/homotopy/homotopy_group.hlean @@ -38,16 +38,14 @@ namespace is_trunc end -- Corollary 8.3.3 - section - open sphere sphere.ops sphere_index - theorem homotopy_group_sphere_le (n k : ℕ) (H : k < n) : is_contr (π[k] (S* n)) := + open sphere sphere.ops + theorem homotopy_group_sphere_le (n k : ℕ) (H : k < n) : is_contr (π[k] (S n)) := begin cases n with n, { exfalso, apply not_lt_zero, exact H}, { have H2 : k ≤ n, from le_of_lt_succ H, apply @(trivial_homotopy_group_of_is_conn _ H2) } end - end theorem is_contr_HG_fiber_of_is_connected {A B : Type*} (k n : ℕ) (f : A →* B) [H : is_conn_fun n f] (H2 : k ≤ n) : is_contr (π[k] (pfiber f)) := diff --git a/hott/homotopy/hopf.hlean b/hott/homotopy/hopf.hlean index bfd8894c2..f3ef47af8 100644 --- a/hott/homotopy/hopf.hlean +++ b/hott/homotopy/hopf.hlean @@ -8,7 +8,7 @@ H-spaces and the Hopf construction import types.equiv .wedge .join -open eq eq.ops equiv is_equiv is_conn is_trunc trunc susp join +open eq eq.ops equiv is_equiv is_conn is_trunc trunc susp join pointed namespace hopf @@ -186,15 +186,15 @@ section (equiv.MK decode' encode decode_encode encode_decode')⁻¹ᵉ definition main_lemma_point - : ptrunc 1 (Ω(psusp A)) ≃* pointed.MK A 1 := + : ptrunc 1 (Ω(susp A)) ≃* pointed.MK A 1 := pointed.pequiv_of_equiv main_lemma idp - protected definition delooping : Ω (ptrunc 2 (psusp A)) ≃* pointed.MK A 1 := - loop_ptrunc_pequiv 1 (psusp A) ⬝e* main_lemma_point + protected definition delooping : Ω (ptrunc 2 (susp A)) ≃* pointed.MK A 1 := + loop_ptrunc_pequiv 1 (susp A) ⬝e* main_lemma_point /- characterization of the underlying pointed maps -/ definition to_pmap_main_lemma_point_pinv - : main_lemma_point⁻¹ᵉ* ~* !ptr ∘* loop_psusp_unit (pointed.MK A 1) := + : main_lemma_point⁻¹ᵉ* ~* !ptr ∘* loop_susp_unit (pointed.MK A 1) := begin fapply phomotopy.mk, { intro a, reflexivity }, @@ -202,7 +202,7 @@ section end definition to_pmap_delooping_pinv : - delooping⁻¹ᵉ* ~* Ω→ !ptr ∘* loop_psusp_unit (pointed.MK A 1) := + delooping⁻¹ᵉ* ~* Ω→ !ptr ∘* loop_susp_unit (pointed.MK A 1) := begin refine !trans_pinv ⬝* _, refine pwhisker_left _ !to_pmap_main_lemma_point_pinv ⬝* _, @@ -211,12 +211,12 @@ section end definition hopf_delooping_elim {B : Type*} (f : pointed.MK A 1 →* Ω B) [H2 : is_trunc 2 B] : - Ω→(ptrunc.elim 2 (psusp.elim f)) ∘* (hopf.delooping A coh)⁻¹ᵉ* ~* f := + Ω→(ptrunc.elim 2 (susp_elim f)) ∘* (hopf.delooping A coh)⁻¹ᵉ* ~* f := begin refine pwhisker_left _ !to_pmap_delooping_pinv ⬝* _, refine !passoc⁻¹* ⬝* _, refine pwhisker_right _ (!ap1_pcompose⁻¹* ⬝* ap1_phomotopy !ptrunc_elim_ptr) ⬝* _, - apply ap1_psusp_elim + apply ap1_susp_elim end end diff --git a/hott/homotopy/imaginaroid.hlean b/hott/homotopy/imaginaroid.hlean index 29e9de7a1..9f545e921 100644 --- a/hott/homotopy/imaginaroid.hlean +++ b/hott/homotopy/imaginaroid.hlean @@ -8,7 +8,7 @@ Cayley-Dickson construction via imaginaroids import algebra.group cubical.square types.pi .hopf -open eq eq.ops equiv susp hopf +open eq eq.ops equiv susp hopf pointed open [notation] sum namespace imaginaroid diff --git a/hott/homotopy/interval.hlean b/hott/homotopy/interval.hlean index 35a20d679..d8df97ae0 100644 --- a/hott/homotopy/interval.hlean +++ b/hott/homotopy/interval.hlean @@ -7,7 +7,7 @@ Declaration of the interval -/ import .susp types.eq types.prod cubical.square -open eq susp unit equiv is_trunc nat prod +open eq susp unit equiv is_trunc nat prod pointed definition interval : Type₀ := susp unit diff --git a/hott/homotopy/join.hlean b/hott/homotopy/join.hlean index 79d042cdb..b7afd445b 100644 --- a/hott/homotopy/join.hlean +++ b/hott/homotopy/join.hlean @@ -57,11 +57,11 @@ namespace join protected definition hsquare {a a' : A} {b b' : B} (p : a = a') (q : b = b') : square (ap inl p) (ap inr q) (glue a b) (glue a' b') := - eq.rec_on p (eq.rec_on q hrfl) + by induction p; induction q; exact hrfl protected definition vsquare {a a' : A} {b b' : B} (p : a = a') (q : b = b') : square (glue a b) (glue a' b') (ap inl p) (ap inr q) := - eq.rec_on p (eq.rec_on q vrfl) + by induction p; induction q; exact vrfl end @@ -120,7 +120,7 @@ end join namespace join variables {A₁ A₂ B₁ B₂ : Type} - protected definition functor [reducible] + definition join_functor [reducible] (f : A₁ → A₂) (g : B₁ → B₂) : join A₁ B₁ → join A₂ B₂ := begin intro x, induction x with a b a b, @@ -132,12 +132,12 @@ namespace join : join.diamond a a' b b' → join.diamond (f a) (f a') (g b) (g b') := begin unfold join.diamond, intro s, - note s' := aps (join.functor f g) s, + note s' := aps (join_functor f g) s, do 2 rewrite eq.ap_inv at s', do 4 rewrite join.elim_glue at s', exact s' end - protected definition equiv_closed + definition join_equiv_join : A₁ ≃ A₂ → B₁ ≃ B₂ → join A₁ B₁ ≃ join A₂ B₂ := begin intros H K, @@ -170,7 +170,7 @@ namespace join cases p, apply pathover_idp_of_eq, apply join.symm_diamond end - protected definition empty (A : Type) : join empty A ≃ A := + definition join_empty (A : Type) : join empty A ≃ A := begin fapply equiv.MK, { intro x, induction x with z a z a, @@ -185,7 +185,7 @@ namespace join { induction z } } end - protected definition bool (A : Type) : join bool A ≃ susp A := + definition join_bool (A : Type) : join bool A ≃ susp A := begin fapply equiv.MK, { intro ba, induction ba with [b, a, b, a], @@ -229,7 +229,7 @@ end join namespace join variables (A B C : Type) - protected definition is_contr [HA : is_contr A] : + definition is_contr_join [HA : is_contr A] : is_contr (join A B) := begin fapply is_contr.mk, exact inl (center A), @@ -239,24 +239,24 @@ namespace join generalize center_eq a, intro p, cases p, apply idp_con, end - protected definition swap : join A B → join B A := + definition join_swap : join A B → join B A := begin intro x, induction x with a b a b, exact inr a, exact inl b, apply !glue⁻¹ end - protected definition swap_involutive (x : join A B) : - join.swap B A (join.swap A B x) = x := + definition join_swap_involutive (x : join A B) : + join_swap B A (join_swap A B x) = x := begin induction x with a b a b, do 2 reflexivity, apply eq_pathover, rewrite ap_id, - apply hdeg_square, esimp[join.swap], + apply hdeg_square, apply concat, apply ap_compose' (join.elim _ _ _), krewrite [join.elim_glue, ap_inv, join.elim_glue], apply inv_inv, end - protected definition symm : join A B ≃ join B A := - by fapply equiv.MK; do 2 apply join.swap; do 2 apply join.swap_involutive + definition join_symm : join A B ≃ join B A := + by fapply equiv.MK; do 2 apply join_swap; do 2 apply join_swap_involutive end join @@ -482,49 +482,49 @@ section join_switch end join_switch - protected definition switch_equiv (A B C : Type) : join (join A B) C ≃ join (join C B) A := + definition join_switch_equiv (A B C : Type) : join (join A B) C ≃ join (join C B) A := by apply equiv.MK; do 2 apply join.switch_involutive - protected definition assoc (A B C : Type) : join (join A B) C ≃ join A (join B C) := - calc join (join A B) C ≃ join (join C B) A : join.switch_equiv - ... ≃ join A (join C B) : join.symm - ... ≃ join A (join B C) : join.equiv_closed erfl (join.symm C B) + definition join_assoc (A B C : Type) : join (join A B) C ≃ join A (join B C) := + calc join (join A B) C ≃ join (join C B) A : join_switch_equiv + ... ≃ join A (join C B) : join_symm + ... ≃ join A (join B C) : join_equiv_join erfl (join_symm C B) - protected definition ap_assoc_inv_glue_inl {A B : Type} (C : Type) (a : A) (b : B) - : ap (to_inv (join.assoc A B C)) (glue a (inl b)) = ap inl (glue a b) := + definition ap_join_assoc_inv_glue_inl {A B : Type} (C : Type) (a : A) (b : B) + : ap (to_inv (join_assoc A B C)) (glue a (inl b)) = ap inl (glue a b) := begin - unfold join.assoc, rewrite ap_compose, krewrite join.elim_glue, + unfold join_assoc, rewrite ap_compose, krewrite join.elim_glue, rewrite ap_compose, krewrite join.elim_glue, rewrite ap_inv, krewrite join.elim_glue, - unfold switch_coh, unfold join.symm, unfold join.swap, esimp, rewrite eq.inv_inv + unfold switch_coh, unfold join_symm, unfold join_swap, esimp, rewrite inv_inv end protected definition ap_assoc_inv_glue_inr {A C : Type} (B : Type) (a : A) (c : C) - : ap (to_inv (join.assoc A B C)) (glue a (inr c)) = glue (inl a) c := + : ap (to_inv (join_assoc A B C)) (glue a (inr c)) = glue (inl a) c := begin - unfold join.assoc, rewrite ap_compose, krewrite join.elim_glue, + unfold join_assoc, rewrite ap_compose, krewrite join.elim_glue, rewrite ap_compose, krewrite join.elim_glue, rewrite ap_inv, krewrite join.elim_glue, - unfold switch_coh, unfold join.symm, unfold join.swap, esimp, rewrite eq.inv_inv + unfold switch_coh, unfold join_symm, unfold join_swap, esimp, rewrite inv_inv end end join namespace join - open sphere sphere_index sphere.ops - protected definition spheres (n m : ℕ₋₁) : join (S n) (S m) ≃ S (n+1+m) := + open sphere sphere.ops + definition join_sphere (n m : ℕ) : join (S n) (S m) ≃ S (n+m+1) := begin - apply equiv.trans (join.symm (S n) (S m)), + refine join_symm (S n) (S m) ⬝e _, induction m with m IH, - { exact join.empty (S n) }, - { calc join (S m.+1) (S n) + { exact join_bool (S n) }, + { calc join (S (m+1)) (S n) ≃ join (join bool (S m)) (S n) - : join.equiv_closed (equiv.symm (join.bool (S m))) erfl + : join_equiv_join (join_bool (S m))⁻¹ᵉ erfl ... ≃ join bool (join (S m) (S n)) - : join.assoc - ... ≃ join bool (S (n+1+m)) - : join.equiv_closed erfl IH - ... ≃ sphere (n+1+m.+1) - : join.bool (S (n+1+m)) } + : join_assoc + ... ≃ join bool (S (n+m+1)) + : join_equiv_join erfl IH + ... ≃ sphere (n+m+2) + : join_bool (S (n+m+1)) } end end join diff --git a/hott/homotopy/quaternionic_hopf.hlean b/hott/homotopy/quaternionic_hopf.hlean index 6919d2268..3f3172024 100644 --- a/hott/homotopy/quaternionic_hopf.hlean +++ b/hott/homotopy/quaternionic_hopf.hlean @@ -9,19 +9,18 @@ The H-space structure on S³ and the quaternionic Hopf fibration import .complex_hopf .imaginaroid -open eq equiv is_equiv circle is_conn trunc is_trunc sphere_index sphere susp -open imaginaroid +open eq equiv is_equiv circle is_conn trunc is_trunc sphere susp imaginaroid pointed bool join namespace hopf - definition involutive_neg_empty [instance] : involutive_neg empty := - ⦃ involutive_neg, neg := empty.elim, neg_neg := by intro a; induction a ⦄ + definition involutive_neg_bool [instance] : involutive_neg bool := + ⦃ involutive_neg, neg := bnot, neg_neg := by intro a; induction a: reflexivity ⦄ definition involutive_neg_circle [instance] : involutive_neg circle := - by change involutive_neg (susp (susp empty)); exact _ + by change involutive_neg (susp bool); exact _ definition has_star_circle [instance] : has_star circle := - by change has_star (susp (susp empty)); exact _ + by change has_star (susp bool); exact _ -- this is the "natural" conjugation defined using the base-loop recursor definition circle_star [reducible] : S¹ → S¹ := @@ -52,7 +51,7 @@ namespace hopf (ap (λw, w ⬝ (tr_constant seg1 base)⁻¹) (con.right_inv seg2)⁻¹), apply con.assoc }, { apply eq_pathover, krewrite elim_merid, rewrite elim_seg2, - apply square_of_eq, rewrite [↑loop,con_inv,inv_inv,idp_con], + apply square_of_eq, rewrite [↑circle.loop,con_inv,inv_inv,idp_con], apply con.assoc } end @@ -85,10 +84,11 @@ namespace hopf { apply is_prop.elimo } } end + open sphere.ops + definition imaginaroid_sphere_zero [instance] - : imaginaroid (sphere (-1.+1)) := - ⦃ imaginaroid, - neg_neg := susp_neg_neg, + : imaginaroid (S 0) := + ⦃ imaginaroid, involutive_neg_bool, mul := circle_mul, one_mul := circle_base_mul, mul_one := circle_mul_base, @@ -96,12 +96,9 @@ namespace hopf norm := circle_norm, star_mul := circle_star_mul ⦄ - local attribute sphere [reducible] - open sphere.ops - definition sphere_three_h_space [instance] : h_space (S 3) := @h_space_equiv_closed (join S¹ S¹) - (cd_h_space (S -1.+1) circle_assoc) (S 3) (join.spheres 1 1) + (cd_h_space (S 0) circle_assoc) (S 3) (join_sphere 1 1) definition is_conn_sphere_three : is_conn 0 (S 3) := begin @@ -115,10 +112,13 @@ namespace hopf local attribute is_conn_sphere_three [instance] - definition quaternionic_hopf : S 7 → S 4 := + definition quaternionic_hopf' : S 7 → S 4 := begin intro x, apply @sigma.pr1 (susp (S 3)) (hopf (S 3)), - apply inv (hopf.total (S 3)), apply inv (join.spheres 3 3), exact x + apply inv (hopf.total (S 3)), apply inv (join_sphere 3 3), exact x end + definition quaternionic_hopf [constructor] : S 7 →* S 4 := + pmap.mk quaternionic_hopf' idp + end hopf diff --git a/hott/homotopy/sphere.hlean b/hott/homotopy/sphere.hlean index 391a5ad21..9f8551aa9 100644 --- a/hott/homotopy/sphere.hlean +++ b/hott/homotopy/sphere.hlean @@ -8,7 +8,7 @@ Declaration of the n-spheres import .susp types.trunc -open eq nat susp bool is_trunc unit pointed algebra +open eq nat susp bool is_trunc unit pointed algebra equiv /- We can define spheres with the following possible indices: @@ -16,310 +16,49 @@ open eq nat susp bool is_trunc unit pointed algebra - nat (forgetting that S^-1 = empty) - nat, but counting wrong (S^0 = empty, S^1 = bool, ...) - some new type "integers >= -1" - We choose the last option here. + We choose the second option here. -/ - /- Sphere levels -/ - -inductive sphere_index : Type₀ := -| minus_one : sphere_index -| succ : sphere_index → sphere_index - -notation `ℕ₋₁` := sphere_index - -namespace trunc_index - definition sub_one [reducible] (n : ℕ₋₁) : ℕ₋₂ := - sphere_index.rec_on n -2 (λ n k, k.+1) - postfix `..-1`:(max+1) := sub_one - - definition of_sphere_index [reducible] (n : ℕ₋₁) : ℕ₋₂ := - n..-1.+1 - - -- we use a double dot to distinguish with the notation .-1 in trunc_index (of type ℕ → ℕ₋₂) -end trunc_index - -namespace sphere_index - /- - notation for sphere_index is -1, 0, 1, ... - from 0 and up this comes from a coercion from num to sphere_index (via nat) - -/ - - postfix `.+1`:(max+1) := sphere_index.succ - postfix `.+2`:(max+1) := λ(n : sphere_index), (n .+1 .+1) - notation `-1` := minus_one - - definition has_zero_sphere_index [instance] : has_zero ℕ₋₁ := - has_zero.mk (succ minus_one) - - definition has_one_sphere_index [instance] : has_one ℕ₋₁ := - has_one.mk (succ (succ minus_one)) - - definition add_plus_one (n m : ℕ₋₁) : ℕ₋₁ := - sphere_index.rec_on m n (λ k l, l .+1) - - -- addition of sphere_indices, where (-1 + -1) is defined to be -1. - protected definition add (n m : ℕ₋₁) : ℕ₋₁ := - sphere_index.cases_on m - (sphere_index.cases_on n -1 id) - (sphere_index.rec n (λn' r, succ r)) - - inductive le (a : ℕ₋₁) : ℕ₋₁ → Type := - | sp_refl : le a a - | step : Π {b}, le a b → le a (b.+1) - - infix ` +1+ `:65 := sphere_index.add_plus_one - - definition has_add_sphere_index [instance] [priority 2000] [reducible] : has_add ℕ₋₁ := - has_add.mk sphere_index.add - - definition has_le_sphere_index [instance] : has_le ℕ₋₁ := - has_le.mk sphere_index.le - - definition sub_one [reducible] (n : ℕ) : ℕ₋₁ := - nat.rec_on n -1 (λ n k, k.+1) - - postfix `..-1`:(max+1) := sub_one - - definition of_nat [coercion] [reducible] (n : ℕ) : ℕ₋₁ := - n..-1.+1 - - -- we use a double dot to distinguish with the notation .-1 in trunc_index (of type ℕ → ℕ₋₂) - - definition add_one [reducible] (n : ℕ₋₁) : ℕ := - sphere_index.rec_on n 0 (λ n k, nat.succ k) - - definition add_plus_one_of_nat (n m : ℕ) : (n +1+ m) = sphere_index.of_nat (n + m + 1) := - begin - induction m with m IH, - { reflexivity }, - { exact ap succ IH} - end - - definition succ_sub_one (n : ℕ) : (nat.succ n)..-1 = n :> ℕ₋₁ := - idp - - definition add_sub_one (n m : ℕ) : (n + m)..-1 = n..-1 +1+ m..-1 :> ℕ₋₁ := - begin - induction m with m IH, - { reflexivity }, - { exact ap succ IH } - end - - definition succ_le_succ {n m : ℕ₋₁} (H : n ≤ m) : n.+1 ≤[ℕ₋₁] m.+1 := - by induction H with m H IH; apply le.sp_refl; exact le.step IH - - definition minus_one_le (n : ℕ₋₁) : -1 ≤[ℕ₋₁] n := - by induction n with n IH; apply le.sp_refl; exact le.step IH - - open decidable - protected definition has_decidable_eq [instance] : Π(n m : ℕ₋₁), decidable (n = m) - | has_decidable_eq -1 -1 := inl rfl - | has_decidable_eq (n.+1) -1 := inr (by contradiction) - | has_decidable_eq -1 (m.+1) := inr (by contradiction) - | has_decidable_eq (n.+1) (m.+1) := - match has_decidable_eq n m with - | inl xeqy := inl (by rewrite xeqy) - | inr xney := inr (λ h : succ n = succ m, by injection h with xeqy; exact absurd xeqy xney) - end - - definition not_succ_le_minus_two {n : sphere_index} (H : n .+1 ≤[ℕ₋₁] -1) : empty := - by cases H - - protected definition le_trans {n m k : ℕ₋₁} (H1 : n ≤[ℕ₋₁] m) (H2 : m ≤[ℕ₋₁] k) : n ≤[ℕ₋₁] k := - begin - induction H2 with k H2 IH, - { exact H1}, - { exact le.step IH} - end - - definition le_of_succ_le_succ {n m : ℕ₋₁} (H : n.+1 ≤[ℕ₋₁] m.+1) : n ≤[ℕ₋₁] m := - begin - cases H with m H', - { apply le.sp_refl}, - { exact sphere_index.le_trans (le.step !le.sp_refl) H'} - end - - theorem not_succ_le_self {n : ℕ₋₁} : ¬n.+1 ≤[ℕ₋₁] n := - begin - induction n with n IH: intro H, - { exact not_succ_le_minus_two H}, - { exact IH (le_of_succ_le_succ H)} - end - - protected definition le_antisymm {n m : ℕ₋₁} (H1 : n ≤[ℕ₋₁] m) (H2 : m ≤[ℕ₋₁] n) : n = m := - begin - induction H2 with n H2 IH, - { reflexivity}, - { exfalso, apply @not_succ_le_self n, exact sphere_index.le_trans H1 H2} - end - - protected definition le_succ {n m : ℕ₋₁} (H1 : n ≤[ℕ₋₁] m): n ≤[ℕ₋₁] m.+1 := - le.step H1 - - definition add_plus_one_minus_one (n : ℕ₋₁) : n +1+ -1 = n := idp - definition add_plus_one_succ (n m : ℕ₋₁) : n +1+ (m.+1) = (n +1+ m).+1 := idp - definition minus_one_add_plus_one (n : ℕ₋₁) : -1 +1+ n = n := - begin induction n with n IH, reflexivity, exact ap succ IH end - definition succ_add_plus_one (n m : ℕ₋₁) : (n.+1) +1+ m = (n +1+ m).+1 := - begin induction m with m IH, reflexivity, exact ap succ IH end - - definition sphere_index_of_nat_add_one (n : ℕ₋₁) : sphere_index.of_nat (add_one n) = n.+1 := - begin induction n with n IH, reflexivity, exact ap succ IH end - - definition add_one_succ (n : ℕ₋₁) : add_one (n.+1) = succ (add_one n) := - by reflexivity - - definition add_one_sub_one (n : ℕ) : add_one (n..-1) = n := - begin induction n with n IH, reflexivity, exact ap nat.succ IH end - - definition add_one_of_nat (n : ℕ) : add_one n = nat.succ n := - ap nat.succ (add_one_sub_one n) - - definition sphere_index.of_nat_succ (n : ℕ) - : sphere_index.of_nat (nat.succ n) = (sphere_index.of_nat n).+1 := - begin induction n with n IH, reflexivity, exact ap succ IH end - - /- - warning: if this coercion is available, the coercion ℕ → ℕ₋₂ is the composition of the coercions - ℕ → ℕ₋₁ → ℕ₋₂. We don't want this composition as coercion, because it has worse computational - properties. You can rewrite it with trans_to_of_sphere_index_eq defined below. - -/ - attribute trunc_index.of_sphere_index [coercion] - -end sphere_index open sphere_index - -definition weak_order_sphere_index [trans_instance] [reducible] : weak_order sphere_index := -weak_order.mk le sphere_index.le.sp_refl @sphere_index.le_trans @sphere_index.le_antisymm - -namespace trunc_index - definition sub_two_eq_sub_one_sub_one (n : ℕ) : n.-2 = n..-1..-1 := - begin - induction n with n IH, - { reflexivity}, - { exact ap trunc_index.succ IH} - end - - definition of_nat_sub_one (n : ℕ) - : (sphere_index.of_nat n)..-1 = (trunc_index.sub_two n).+1 := - begin - induction n with n IH, - { reflexivity}, - { exact ap trunc_index.succ IH} - end - - definition sub_one_of_sphere_index (n : ℕ) - : of_sphere_index n..-1 = (trunc_index.sub_two n).+1 := - begin - induction n with n IH, - { reflexivity}, - { exact ap trunc_index.succ IH} - end - - definition succ_sub_one (n : ℕ₋₁) : n.+1..-1 = n :> ℕ₋₂ := - idp - - definition of_sphere_index_of_nat (n : ℕ) - : of_sphere_index (sphere_index.of_nat n) = of_nat n :> ℕ₋₂ := - begin - induction n with n IH, - { reflexivity}, - { exact ap trunc_index.succ IH} - end - - definition trans_to_of_sphere_index_eq (n : ℕ) - : trunc_index._trans_to_of_sphere_index n = of_nat n :> ℕ₋₂ := - of_sphere_index_of_nat n - - definition trunc_index_of_nat_add_one (n : ℕ₋₁) - : trunc_index.of_nat (add_one n) = (of_sphere_index n).+1 := - begin induction n with n IH, reflexivity, exact ap succ IH end - - definition of_sphere_index_succ (n : ℕ₋₁) : of_sphere_index (n.+1) = (of_sphere_index n).+1 := - begin induction n with n IH, reflexivity, exact ap succ IH end - -end trunc_index - -open sphere_index equiv - -definition sphere (n : ℕ₋₁) : Type₀ := iterate_susp (add_one n) empty +definition sphere (n : ℕ) : Type* := iterate_susp n pbool namespace sphere - export [notation] sphere_index - - definition base {n : ℕ} : sphere n := north - definition pointed_sphere [instance] [constructor] (n : ℕ) : pointed (sphere n) := - pointed.mk base - definition psphere [constructor] (n : ℕ) : Type* := pointed.mk' (sphere n) - - namespace ops abbreviation S := sphere - notation `S*` := psphere end ops open sphere.ops - definition sphere_minus_one : S -1 = empty := idp - definition sphere_succ [unfold_full] (n : ℕ₋₁) : S n.+1 = susp (S n) := idp - definition psphere_succ [unfold_full] (n : ℕ) : S* (n + 1) = psusp (S* n) := idp - definition psphere_eq_iterate_susp (n : ℕ) - : S* n = pointed.MK (iterate_susp (succ n) empty) !north := - begin - esimp, - apply ap (λx, pointed.MK (susp x) (@north x)); apply ap (λx, iterate_susp x empty), - apply add_one_sub_one - end + definition sphere_succ [unfold_full] (n : ℕ) : S (n+1) = susp (S n) := idp + definition sphere_eq_iterate_susp (n : ℕ) : S n = iterate_susp n pbool := idp - definition equator [constructor] (n : ℕ) : S* n →* Ω (S* (succ n)) := - loop_psusp_unit (S* n) + definition equator [constructor] (n : ℕ) : S n →* Ω (S (succ n)) := + loop_susp_unit (S n) - definition surf {n : ℕ} : Ω[n] (S* n) := + definition surf {n : ℕ} : Ω[n] (S n) := begin induction n with n s, - { exact south }, - { exact (loopn_succ_in (S* (succ n)) n)⁻¹ᵉ* (apn n (equator n) s) } + { exact tt }, + { exact (loopn_succ_in (S (succ n)) n)⁻¹ᵉ* (apn n (equator n) s) } end - definition bool_of_sphere [unfold 1] : S 0 → bool := - proof susp.rec ff tt (λx, empty.elim x) qed + definition sphere_equiv_bool [constructor] : S 0 ≃ bool := by reflexivity - definition sphere_of_bool [unfold 1] : bool → S 0 - | ff := proof north qed - | tt := proof south qed + definition sphere_pequiv_pbool [constructor] : S 0 ≃* pbool := by reflexivity - definition sphere_equiv_bool [constructor] : S 0 ≃ bool := - equiv.MK bool_of_sphere - sphere_of_bool - (λb, match b with | tt := idp | ff := idp end) - (λx, proof susp.rec_on x idp idp (empty.rec _) qed) + definition sphere_pequiv_iterate_susp (n : ℕ) : sphere n ≃* iterate_susp n pbool := + by reflexivity - definition psphere_pequiv_pbool [constructor] : S* 0 ≃* pbool := - pequiv_of_equiv sphere_equiv_bool idp - - definition sphere_eq_bool : S 0 = bool := - ua sphere_equiv_bool - - definition sphere_eq_pbool : S* 0 = pbool := - pType_eq sphere_equiv_bool idp - - definition psphere_pequiv_iterate_psusp (n : ℕ) : psphere n ≃* iterate_psusp n pbool := - begin - induction n with n e, - { exact psphere_pequiv_pbool }, - { exact psusp_pequiv e } - end - - definition psphere_pmap_pequiv' (A : Type*) (n : ℕ) : ppmap (S* n) A ≃* Ω[n] A := + definition sphere_pmap_pequiv' (A : Type*) (n : ℕ) : ppmap (S n) A ≃* Ω[n] A := begin revert A, induction n with n IH: intro A, - { refine _ ⬝e* !ppmap_pbool_pequiv, exact pequiv_ppcompose_right psphere_pequiv_pbool⁻¹ᵉ* }, - { refine psusp_adjoint_loop (S* n) A ⬝e* IH (Ω A) ⬝e* !loopn_succ_in⁻¹ᵉ* } + { refine !ppmap_pbool_pequiv }, + { refine susp_adjoint_loop (S n) A ⬝e* IH (Ω A) ⬝e* !loopn_succ_in⁻¹ᵉ* } end - definition psphere_pmap_pequiv (A : Type*) (n : ℕ) : ppmap (S* n) A ≃* Ω[n] A := + definition sphere_pmap_pequiv (A : Type*) (n : ℕ) : ppmap (S n) A ≃* Ω[n] A := begin fapply pequiv_change_fun, - { exact psphere_pmap_pequiv' A n }, + { exact sphere_pmap_pequiv' A n }, { exact papn_fun A surf }, { revert A, induction n with n IH: intro A, { reflexivity }, @@ -327,33 +66,29 @@ namespace sphere exact !loopn_succ_in_inv_natural⁻¹* _ }} end - protected definition elim {n : ℕ} {P : Type*} (p : Ω[n] P) : S* n →* P := - !psphere_pmap_pequiv⁻¹ᵉ* p + protected definition elim {n : ℕ} {P : Type*} (p : Ω[n] P) : S n →* P := + !sphere_pmap_pequiv⁻¹ᵉ* p -- definition elim_surf {n : ℕ} {P : Type*} (p : Ω[n] P) : apn n (sphere.elim p) surf = p := -- begin -- induction n with n IH, - -- { esimp [apn,surf,sphere.elim,psphere_pmap_equiv], apply sorry}, + -- { esimp [apn,surf,sphere.elim,sphere_pmap_equiv], apply sorry}, -- { apply sorry} -- end end sphere namespace sphere - open is_conn trunc_index sphere_index sphere.ops + open is_conn trunc_index sphere.ops -- Corollary 8.2.2 - theorem is_conn_sphere [instance] (n : ℕ₋₁) : is_conn (n..-1) (S n) := + theorem is_conn_sphere [instance] (n : ℕ) : is_conn (n.-1) (S n) := begin induction n with n IH, - { apply is_conn_minus_two }, - { rewrite [trunc_index.succ_sub_one n, sphere.sphere_succ], - apply is_conn_susp } + { apply is_conn_minus_one_pointed }, + { apply is_conn_susp, exact IH } end - theorem is_conn_psphere [instance] (n : ℕ) : is_conn (n.-1) (S* n) := - transport (λx, is_conn x (sphere n)) (of_nat_sub_one n) (is_conn_sphere n) - end sphere open sphere sphere.ops @@ -361,12 +96,12 @@ open sphere sphere.ops namespace is_trunc open trunc_index variables {n : ℕ} {A : Type} - definition is_trunc_of_psphere_pmap_equiv_constant - (H : Π(a : A) (f : S* n →* pointed.Mk a) (x : S n), f x = f base) : is_trunc (n.-2.+1) A := + definition is_trunc_of_sphere_pmap_equiv_constant + (H : Π(a : A) (f : S n →* pointed.Mk a) (x : S n), f x = f pt) : is_trunc (n.-2.+1) A := begin apply iff.elim_right !is_trunc_iff_is_contr_loop, intro a, - apply is_trunc_equiv_closed, exact !psphere_pmap_pequiv, + apply is_trunc_equiv_closed, exact !sphere_pmap_pequiv, fapply is_contr.mk, { exact pmap.mk (λx, a) idp}, { intro f, fapply pmap_eq, @@ -375,30 +110,30 @@ namespace is_trunc end definition is_trunc_iff_map_sphere_constant - (H : Π(f : S n → A) (x : S n), f x = f base) : is_trunc (n.-2.+1) A := + (H : Π(f : S n → A) (x : S n), f x = f pt) : is_trunc (n.-2.+1) A := begin - apply is_trunc_of_psphere_pmap_equiv_constant, + apply is_trunc_of_sphere_pmap_equiv_constant, intros, cases f with f p, esimp at *, apply H end - definition psphere_pmap_equiv_constant_of_is_trunc' [H : is_trunc (n.-2.+1) A] - (a : A) (f : S* n →* pointed.Mk a) (x : S n) : f x = f base := + definition sphere_pmap_equiv_constant_of_is_trunc' [H : is_trunc (n.-2.+1) A] + (a : A) (f : S n →* pointed.Mk a) (x : S n) : f x = f pt := begin let H' := iff.elim_left (is_trunc_iff_is_contr_loop n A) H a, - note H'' := @is_trunc_equiv_closed_rev _ _ _ !psphere_pmap_pequiv H', + note H'' := @is_trunc_equiv_closed_rev _ _ _ !sphere_pmap_pequiv H', esimp at H'', - have p : f = pmap.mk (λx, f base) (respect_pt f), + have p : f = pmap.mk (λx, f pt) (respect_pt f), by apply is_prop.elim, exact ap10 (ap pmap.to_fun p) x end - definition psphere_pmap_equiv_constant_of_is_trunc [H : is_trunc (n.-2.+1) A] - (a : A) (f : S* n →* pointed.Mk a) (x y : S n) : f x = f y := - let H := psphere_pmap_equiv_constant_of_is_trunc' a f in !H ⬝ !H⁻¹ + definition sphere_pmap_equiv_constant_of_is_trunc [H : is_trunc (n.-2.+1) A] + (a : A) (f : S n →* pointed.Mk a) (x y : S n) : f x = f y := + let H := sphere_pmap_equiv_constant_of_is_trunc' a f in !H ⬝ !H⁻¹ definition map_sphere_constant_of_is_trunc [H : is_trunc (n.-2.+1) A] (f : S n → A) (x y : S n) : f x = f y := - psphere_pmap_equiv_constant_of_is_trunc (f base) (pmap.mk f idp) x y + sphere_pmap_equiv_constant_of_is_trunc (f pt) (pmap.mk f idp) x y definition map_sphere_constant_of_is_trunc_self [H : is_trunc (n.-2.+1) A] (f : S n → A) (x : S n) : map_sphere_constant_of_is_trunc f x x = idp := diff --git a/hott/homotopy/sphere2.hlean b/hott/homotopy/sphere2.hlean index 94a8f9051..04569477e 100644 --- a/hott/homotopy/sphere2.hlean +++ b/hott/homotopy/sphere2.hlean @@ -14,93 +14,76 @@ In this file we calculate import .homotopy_group .freudenthal open eq group algebra is_equiv equiv fin prod chain_complex pointed fiber nat is_trunc trunc_index - sphere.ops trunc is_conn susp + sphere.ops trunc is_conn susp bool namespace sphere /- Corollaries of the complex hopf fibration combined with the LES of homotopy groups -/ open sphere sphere.ops int circle hopf - definition π2S2 : πg[1+1] (S* 2) ≃g gℤ := + definition π2S2 : πg[1+1] (S 2) ≃g gℤ := begin refine _ ⬝g fundamental_group_of_circle, - refine _ ⬝g homotopy_group_isomorphism_of_pequiv _ pfiber_complex_phopf, + refine _ ⬝g homotopy_group_isomorphism_of_pequiv _ pfiber_complex_hopf, fapply isomorphism_of_equiv, { fapply equiv.mk, - { exact cc_to_fn (LES_of_homotopy_groups complex_phopf) (1, 2)}, - { refine LES_is_equiv_of_trivial complex_phopf 1 2 _ _, + { exact cc_to_fn (LES_of_homotopy_groups complex_hopf) (1, 2)}, + { refine LES_is_equiv_of_trivial complex_hopf 1 2 _ _, { have H : 1 ≤[ℕ] 2, from !one_le_succ, - apply trivial_homotopy_group_of_is_conn, exact H, rexact is_conn_psphere 3 }, + apply trivial_homotopy_group_of_is_conn, exact H, rexact is_conn_sphere 3 }, { refine tr_rev (λx, is_contr (ptrunctype._trans_of_to_pType x)) - (LES_of_homotopy_groups_1 complex_phopf 2) _, - apply trivial_homotopy_group_of_is_conn, apply le.refl, rexact is_conn_psphere 3 }}}, + (LES_of_homotopy_groups_1 complex_hopf 2) _, + apply trivial_homotopy_group_of_is_conn, apply le.refl, rexact is_conn_sphere 3 }}}, { exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (0, 2))} end open circle - definition πnS3_eq_πnS2 (n : ℕ) : πg[n+2 +1] (S* 3) ≃g πg[n+2 +1] (S* 2) := + definition πnS3_eq_πnS2 (n : ℕ) : πg[n+2 +1] (S 3) ≃g πg[n+2 +1] (S 2) := begin fapply isomorphism_of_equiv, { fapply equiv.mk, - { exact cc_to_fn (LES_of_homotopy_groups complex_phopf) (n+3, 0)}, - { have H : is_trunc 1 (pfiber complex_phopf), - from @(is_trunc_equiv_closed_rev _ pfiber_complex_phopf) is_trunc_circle, - refine LES_is_equiv_of_trivial complex_phopf (n+3) 0 _ _, + { exact cc_to_fn (LES_of_homotopy_groups complex_hopf) (n+3, 0)}, + { have H : is_trunc 1 (pfiber complex_hopf), + from @(is_trunc_equiv_closed_rev _ pfiber_complex_hopf) is_trunc_circle, + refine LES_is_equiv_of_trivial complex_hopf (n+3) 0 _ _, { have H2 : 1 ≤[ℕ] n + 1, from !one_le_succ, exact @trivial_ghomotopy_group_of_is_trunc _ _ _ H H2 }, { refine tr_rev (λx, is_contr (ptrunctype._trans_of_to_pType x)) - (LES_of_homotopy_groups_2 complex_phopf _) _, + (LES_of_homotopy_groups_2 complex_hopf _) _, have H2 : 1 ≤[ℕ] n + 2, from !one_le_succ, apply trivial_ghomotopy_group_of_is_trunc _ _ _ H2 }}}, { exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (n+2, 0))} end definition sphere_stability_pequiv (k n : ℕ) (H : k + 2 ≤ 2 * n) : - π[k + 1] (S* (n+1)) ≃* π[k] (S* n) := - begin rewrite [+ psphere_eq_iterate_susp], exact iterate_susp_stability_pequiv empty H end + π[k + 1] (S (n+1)) ≃* π[k] (S n) := + iterate_susp_stability_pequiv pbool H definition stability_isomorphism (k n : ℕ) (H : k + 3 ≤ 2 * n) - : πg[k+1 +1] (S* (n+1)) ≃g πg[k+1] (S* n) := - begin rewrite [+ psphere_eq_iterate_susp], exact iterate_susp_stability_isomorphism empty H end + : πg[k+1 +1] (S (n+1)) ≃g πg[k+1] (S n) := + iterate_susp_stability_isomorphism pbool H open int circle hopf - definition πnSn (n : ℕ) : πg[n+1] (S* (succ n)) ≃g gℤ := + definition πnSn (n : ℕ) : πg[n+1] (S (n+1)) ≃g gℤ := begin cases n with n IH, - { exact fundamental_group_of_circle}, + { exact fundamental_group_of_circle }, { induction n with n IH, - { exact π2S2}, + { exact π2S2 }, { refine _ ⬝g IH, apply stability_isomorphism, - rexact add_mul_le_mul_add n 1 2}} + rexact add_mul_le_mul_add n 1 2 }} end - theorem not_is_trunc_sphere (n : ℕ) : ¬is_trunc n (S* (succ n)) := + theorem not_is_trunc_sphere (n : ℕ) : ¬is_trunc n (S (n+1)) := begin intro H, - note H2 := trivial_ghomotopy_group_of_is_trunc (S* (succ n)) n n !le.refl, + note H2 := trivial_ghomotopy_group_of_is_trunc (S (n+1)) n n !le.refl, have H3 : is_contr ℤ, from is_trunc_equiv_closed _ (equiv_of_isomorphism (πnSn n)), have H4 : (0 : ℤ) ≠ (1 : ℤ), from dec_star, apply H4, apply is_prop.elim, end - section - open sphere_index - - definition not_is_trunc_sphere' (n : ℕ₋₁) : ¬is_trunc n (S (n.+1)) := - begin - cases n with n, - { esimp [sphere.ops.S, sphere], intro H, - have H2 : is_prop bool, from @(is_trunc_equiv_closed -1 sphere_equiv_bool) H, - have H3 : bool.tt ≠ bool.ff, from dec_star, apply H3, apply is_prop.elim}, - { intro H, apply not_is_trunc_sphere (add_one n), - rewrite [▸*, trunc_index_of_nat_add_one, -add_one_succ, - sphere_index_of_nat_add_one], - exact H} - end - - end - - definition π3S2 : πg[2+1] (S* 2) ≃g gℤ := + definition π3S2 : πg[2+1] (S 2) ≃g gℤ := (πnS3_eq_πnS2 0)⁻¹ᵍ ⬝g πnSn 2 end sphere diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean index 5f25b4168..af7ff9d9f 100644 --- a/hott/homotopy/susp.hlean +++ b/hott/homotopy/susp.hlean @@ -8,15 +8,31 @@ Declaration of suspension import hit.pushout types.pointed2 cubical.square .connectedness -open pushout unit eq equiv +open pushout unit eq equiv pointed -definition susp (A : Type) : Type := pushout (λ(a : A), star) (λ(a : A), star) +definition susp' (A : Type) : Type := pushout (λ(a : A), star) (λ(a : A), star) + +namespace susp + + definition north' {A : Type} : susp' A := + inl star + + definition pointed_susp [instance] [constructor] (X : Type) + : pointed (susp' X) := + pointed.mk north' + +end susp open susp + +definition susp [constructor] (X : Type) : Type* := +pointed.MK (susp' X) north' + +notation `⅀` := susp namespace susp variable {A : Type} definition north {A : Type} : susp A := - inl star + north' definition south {A : Type} : susp A := inr star @@ -25,7 +41,7 @@ namespace susp glue a protected definition rec {P : susp A → Type} (PN : P north) (PS : P south) - (Pm : Π(a : A), PN =[merid a] PS) (x : susp A) : P x := + (Pm : Π(a : A), PN =[merid a] PS) (x : susp' A) : P x := begin induction x with u u, { cases u, exact PN}, @@ -33,7 +49,7 @@ namespace susp { apply Pm}, end - protected definition rec_on [reducible] {P : susp A → Type} (y : susp A) + protected definition rec_on [reducible] {P : susp A → Type} (y : susp' A) (PN : P north) (PS : P south) (Pm : Π(a : A), PN =[merid a] PS) : P y := susp.rec PN PS Pm y @@ -43,10 +59,10 @@ namespace susp !rec_glue protected definition elim {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS) - (x : susp A) : P := + (x : susp' A) : P := susp.rec PN PS (λa, pathover_of_eq _ (Pm a)) x - protected definition elim_on [reducible] {P : Type} (x : susp A) + protected definition elim_on [reducible] {P : Type} (x : susp' A) (PN : P) (PS : P) (Pm : A → PN = PS) : P := susp.elim PN PS Pm x @@ -58,10 +74,10 @@ namespace susp end protected definition elim_type (PN : Type) (PS : Type) (Pm : A → PN ≃ PS) - (x : susp A) : Type := + (x : susp' A) : Type := pushout.elim_type (λx, PN) (λx, PS) Pm x - protected definition elim_type_on [reducible] (x : susp A) + protected definition elim_type_on [reducible] (x : susp' A) (PN : Type) (PS : Type) (Pm : A → PN ≃ PS) : Type := susp.elim_type PN PS Pm x @@ -79,7 +95,7 @@ namespace susp end susp -attribute susp.north susp.south [constructor] +attribute susp.north' susp.north susp.south [constructor] attribute susp.rec susp.elim [unfold 6] [recursor 6] attribute susp.elim_type [unfold 5] attribute susp.rec_on susp.elim_on [unfold 3] @@ -94,28 +110,23 @@ namespace susp [H : is_conn n A] : is_conn (n .+1) (susp A) := is_contr.mk (tr north) begin - apply trunc.rec, - fapply susp.rec, + intro x, induction x with x, induction x, { reflexivity }, { exact (trunc.rec (λa, ap tr (merid a)) (center (trunc n A))) }, - { intro a, - generalize (center (trunc n A)), - apply trunc.rec, - intro a', + { generalize (center (trunc n A)), + intro x, induction x with a', apply pathover_of_tr_eq, rewrite [eq_transport_Fr,idp_con], - revert H, induction n with [n, IH], - { intro H, apply is_prop.elim }, - { intros H, - change ap (@tr n .+2 (susp A)) (merid a) = ap tr (merid a'), + revert H, induction n with n IH: intro H, + { apply is_prop.elim }, + { change ap (@tr n .+2 (susp A)) (merid a) = ap tr (merid a'), generalize a', apply is_conn_fun.elim n (is_conn_fun_from_unit n A a) (λx : A, trunctype.mk' n (ap (@tr n .+2 (susp A)) (merid a) = ap tr (merid x))), intros, change ap (@tr n .+2 (susp A)) (merid a) = ap tr (merid a), - reflexivity - } + reflexivity } } end @@ -152,7 +163,7 @@ namespace susp variables {A B : Type} (f : A → B) include f - protected definition functor [unfold 4] : susp A → susp B := + definition susp_functor' [unfold 4] : susp A → susp B := begin intro x, induction x with a, { exact north }, @@ -164,19 +175,19 @@ namespace susp include Hf open is_equiv - protected definition is_equiv_functor [instance] [constructor] : is_equiv (susp.functor f) := - adjointify (susp.functor f) (susp.functor f⁻¹) + protected definition is_equiv_functor [instance] [constructor] : is_equiv (susp_functor' f) := + adjointify (susp_functor' f) (susp_functor' f⁻¹) abstract begin intro sb, induction sb with b, do 2 reflexivity, apply eq_pathover, - rewrite [ap_id,ap_compose' (susp.functor f) (susp.functor f⁻¹)], + rewrite [ap_id,ap_compose' (susp_functor' f) (susp_functor' f⁻¹)], krewrite [susp.elim_merid,susp.elim_merid], apply transpose, apply susp.merid_square (right_inv f b) end end abstract begin intro sa, induction sa with a, do 2 reflexivity, apply eq_pathover, - rewrite [ap_id,ap_compose' (susp.functor f⁻¹) (susp.functor f)], + rewrite [ap_id,ap_compose' (susp_functor' f⁻¹) (susp_functor' f)], krewrite [susp.elim_merid,susp.elim_merid], apply transpose, apply susp.merid_square (left_inv f a) end end @@ -188,59 +199,42 @@ namespace susp variables {A B : Type} (f : A ≃ B) protected definition equiv : susp A ≃ susp B := - equiv.mk (susp.functor f) _ + equiv.mk (susp_functor' f) _ end susp -namespace susp - open pointed - definition pointed_susp [instance] [constructor] (X : Type) - : pointed (susp X) := - pointed.mk north -end susp - -open susp -definition psusp [constructor] (X : Type) : Type* := -pointed.mk' (susp X) - -notation `⅀` := psusp - namespace susp open pointed is_trunc variables {X Y Z : Type*} - definition is_conn_psusp [instance] (n : trunc_index) (A : Type*) - [H : is_conn n A] : is_conn (n .+1) (psusp A) := - is_conn_susp n A - - definition psusp_functor [constructor] (f : X →* Y) : psusp X →* psusp Y := + definition susp_functor [constructor] (f : X →* Y) : susp X →* susp Y := begin fconstructor, - { exact susp.functor f }, + { exact susp_functor' f }, { reflexivity } end - definition is_equiv_psusp_functor [constructor] (f : X →* Y) [Hf : is_equiv f] - : is_equiv (psusp_functor f) := + definition is_equiv_susp_functor [constructor] (f : X →* Y) [Hf : is_equiv f] + : is_equiv (susp_functor f) := susp.is_equiv_functor f - definition psusp_pequiv [constructor] (f : X ≃* Y) : psusp X ≃* psusp Y := + definition susp_pequiv [constructor] (f : X ≃* Y) : susp X ≃* susp Y := pequiv_of_equiv (susp.equiv f) idp - definition psusp_functor_pcompose (g : Y →* Z) (f : X →* Y) : - psusp_functor (g ∘* f) ~* psusp_functor g ∘* psusp_functor f := + definition susp_functor_pcompose (g : Y →* Z) (f : X →* Y) : + susp_functor (g ∘* f) ~* susp_functor g ∘* susp_functor f := begin fapply phomotopy.mk, { intro x, induction x, { reflexivity }, { reflexivity }, - { apply eq_pathover, apply hdeg_square, esimp, - refine !elim_merid ⬝ _ ⬝ (ap_compose (psusp_functor g) _ _)⁻¹ᵖ, + { apply eq_pathover, apply hdeg_square, + refine !elim_merid ⬝ _ ⬝ (ap_compose (susp_functor g) _ _)⁻¹ᵖ, refine _ ⬝ ap02 _ !elim_merid⁻¹, exact !elim_merid⁻¹ }}, { reflexivity }, end - definition psusp_functor_phomotopy {f g : X →* Y} (p : f ~* g) : - psusp_functor f ~* psusp_functor g := + definition susp_functor_phomotopy {f g : X →* Y} (p : f ~* g) : + susp_functor f ~* susp_functor g := begin fapply phomotopy.mk, { intro x, induction x, @@ -251,7 +245,7 @@ namespace susp { reflexivity }, end - definition psusp_functor_pid (A : Type*) : psusp_functor (pid A) ~* pid (psusp A) := + definition susp_functor_pid (A : Type*) : susp_functor (pid A) ~* pid (susp A) := begin fapply phomotopy.mk, { intro x, induction x, @@ -264,15 +258,15 @@ namespace susp /- adjunction originally ported from Coq-HoTT, but we proved some additional naturality conditions -/ - definition loop_psusp_unit [constructor] (X : Type*) : X →* Ω(psusp X) := + definition loop_susp_unit [constructor] (X : Type*) : X →* Ω(susp X) := begin fconstructor, { intro x, exact merid x ⬝ (merid pt)⁻¹ }, { apply con.right_inv }, end - definition loop_psusp_unit_natural (f : X →* Y) - : loop_psusp_unit Y ∘* f ~* Ω→ (psusp_functor f) ∘* loop_psusp_unit X := + definition loop_susp_unit_natural (f : X →* Y) + : loop_susp_unit Y ∘* f ~* Ω→ (susp_functor f) ∘* loop_susp_unit X := begin induction X with X x, induction Y with Y y, induction f with f pf, esimp at *, induction pf, fapply phomotopy.mk, @@ -292,15 +286,15 @@ namespace susp rewrite [-ap_compose (concat idp)] }, end - definition loop_psusp_counit [constructor] (X : Type*) : psusp (Ω X) →* X := + definition loop_susp_counit [constructor] (X : Type*) : susp (Ω X) →* X := begin fconstructor, { intro x, induction x, exact pt, exact pt, exact a }, { reflexivity }, end - definition loop_psusp_counit_natural (f : X →* Y) - : f ∘* loop_psusp_counit X ~* loop_psusp_counit Y ∘* (psusp_functor (ap1 f)) := + definition loop_susp_counit_natural (f : X →* Y) + : f ∘* loop_susp_counit X ~* loop_susp_counit Y ∘* (susp_functor (ap1 f)) := begin induction X with X x, induction Y with Y y, induction f with f pf, esimp at *, induction pf, fconstructor, @@ -313,8 +307,8 @@ namespace susp { reflexivity } end - definition loop_psusp_counit_unit (X : Type*) - : ap1 (loop_psusp_counit X) ∘* loop_psusp_unit (Ω X) ~* pid (Ω X) := + definition loop_susp_counit_unit (X : Type*) + : ap1 (loop_susp_counit X) ∘* loop_susp_unit (Ω X) ~* pid (Ω X) := begin induction X with X x, fconstructor, { intro p, esimp, @@ -328,8 +322,8 @@ namespace susp -ap_compose] } end - definition loop_psusp_unit_counit (X : Type*) - : loop_psusp_counit (psusp X) ∘* psusp_functor (loop_psusp_unit X) ~* pid (psusp X) := + definition loop_susp_unit_counit (X : Type*) + : loop_susp_counit (susp X) ∘* susp_functor (loop_susp_unit X) ~* pid (susp X) := begin induction X with X x, fconstructor, { intro x', induction x', @@ -341,152 +335,141 @@ namespace susp { reflexivity } end - definition psusp.elim [constructor] {X Y : Type*} (f : X →* Ω Y) : psusp X →* Y := - loop_psusp_counit Y ∘* psusp_functor f + definition susp_elim [constructor] {X Y : Type*} (f : X →* Ω Y) : susp X →* Y := + loop_susp_counit Y ∘* susp_functor f - definition loop_psusp_intro [constructor] {X Y : Type*} (f : psusp X →* Y) : X →* Ω Y := - ap1 f ∘* loop_psusp_unit X + definition loop_susp_intro [constructor] {X Y : Type*} (f : susp X →* Y) : X →* Ω Y := + ap1 f ∘* loop_susp_unit X - definition psusp_elim_psusp_functor {A B C : Type*} (g : B →* Ω C) (f : A →* B) : - psusp.elim g ∘* psusp_functor f ~* psusp.elim (g ∘* f) := + definition susp_elim_susp_functor {A B C : Type*} (g : B →* Ω C) (f : A →* B) : + susp_elim g ∘* susp_functor f ~* susp_elim (g ∘* f) := begin - refine !passoc ⬝* _, exact pwhisker_left _ !psusp_functor_pcompose⁻¹* + refine !passoc ⬝* _, exact pwhisker_left _ !susp_functor_pcompose⁻¹* end - definition psusp_elim_phomotopy {A B : Type*} {f g : A →* Ω B} (p : f ~* g) : psusp.elim f ~* psusp.elim g := - pwhisker_left _ (psusp_functor_phomotopy p) + definition susp_elim_phomotopy {A B : Type*} {f g : A →* Ω B} (p : f ~* g) : susp_elim f ~* susp_elim g := + pwhisker_left _ (susp_functor_phomotopy p) - definition psusp_elim_natural {X Y Z : Type*} (g : Y →* Z) (f : X →* Ω Y) - : g ∘* psusp.elim f ~* psusp.elim (Ω→ g ∘* f) := + definition susp_elim_natural {X Y Z : Type*} (g : Y →* Z) (f : X →* Ω Y) + : g ∘* susp_elim f ~* susp_elim (Ω→ g ∘* f) := begin - refine _ ⬝* pwhisker_left _ !psusp_functor_pcompose⁻¹*, + refine _ ⬝* pwhisker_left _ !susp_functor_pcompose⁻¹*, refine !passoc⁻¹* ⬝* _ ⬝* !passoc, - exact pwhisker_right _ !loop_psusp_counit_natural + exact pwhisker_right _ !loop_susp_counit_natural end - definition loop_psusp_intro_natural {X Y Z : Type*} (g : psusp Y →* Z) (f : X →* Y) : - loop_psusp_intro (g ∘* psusp_functor f) ~* loop_psusp_intro g ∘* f := - pwhisker_right _ !ap1_pcompose ⬝* !passoc ⬝* pwhisker_left _ !loop_psusp_unit_natural⁻¹* ⬝* + definition loop_susp_intro_natural {X Y Z : Type*} (g : susp Y →* Z) (f : X →* Y) : + loop_susp_intro (g ∘* susp_functor f) ~* loop_susp_intro g ∘* f := + pwhisker_right _ !ap1_pcompose ⬝* !passoc ⬝* pwhisker_left _ !loop_susp_unit_natural⁻¹* ⬝* !passoc⁻¹* - definition psusp_adjoint_loop_right_inv {X Y : Type*} (g : X →* Ω Y) : - loop_psusp_intro (psusp.elim g) ~* g := + definition susp_adjoint_loop_right_inv {X Y : Type*} (g : X →* Ω Y) : + loop_susp_intro (susp_elim g) ~* g := begin refine !pwhisker_right !ap1_pcompose ⬝* _, refine !passoc ⬝* _, - refine !pwhisker_left !loop_psusp_unit_natural⁻¹* ⬝* _, + refine !pwhisker_left !loop_susp_unit_natural⁻¹* ⬝* _, refine !passoc⁻¹* ⬝* _, - refine !pwhisker_right !loop_psusp_counit_unit ⬝* _, + refine !pwhisker_right !loop_susp_counit_unit ⬝* _, apply pid_pcompose end - definition psusp_adjoint_loop_left_inv {X Y : Type*} (f : psusp X →* Y) : - psusp.elim (loop_psusp_intro f) ~* f := + definition susp_adjoint_loop_left_inv {X Y : Type*} (f : susp X →* Y) : + susp_elim (loop_susp_intro f) ~* f := begin - refine !pwhisker_left !psusp_functor_pcompose ⬝* _, + refine !pwhisker_left !susp_functor_pcompose ⬝* _, refine !passoc⁻¹* ⬝* _, - refine !pwhisker_right !loop_psusp_counit_natural⁻¹* ⬝* _, + refine !pwhisker_right !loop_susp_counit_natural⁻¹* ⬝* _, refine !passoc ⬝* _, - refine !pwhisker_left !loop_psusp_unit_counit ⬝* _, + refine !pwhisker_left !loop_susp_unit_counit ⬝* _, apply pcompose_pid end - definition psusp_adjoint_loop_unpointed [constructor] (X Y : Type*) : psusp X →* Y ≃ X →* Ω Y := + definition susp_adjoint_loop_unpointed [constructor] (X Y : Type*) : susp X →* Y ≃ X →* Ω Y := begin fapply equiv.MK, - { exact loop_psusp_intro }, - { exact psusp.elim }, - { 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 loop_susp_intro }, + { exact susp_elim }, + { 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_pconst (X Y : Type*) : - psusp_adjoint_loop_unpointed X Y (pconst (psusp X) Y) ~* pconst X (Ω Y) := + definition susp_adjoint_loop_pconst (X Y : Type*) : + susp_adjoint_loop_unpointed X Y (pconst (susp X) Y) ~* pconst X (Ω Y) := begin refine pwhisker_right _ !ap1_pconst ⬝* _, apply pconst_pcompose end - definition psusp_adjoint_loop [constructor] (X Y : Type*) : ppmap (psusp X) Y ≃* ppmap X (Ω Y) := + definition susp_adjoint_loop [constructor] (X Y : Type*) : ppmap (susp X) Y ≃* ppmap X (Ω Y) := begin - apply pequiv_of_equiv (psusp_adjoint_loop_unpointed X Y), + apply pequiv_of_equiv (susp_adjoint_loop_unpointed X Y), apply eq_of_phomotopy, - apply psusp_adjoint_loop_pconst + apply susp_adjoint_loop_pconst end - definition ap1_psusp_elim {A : Type*} {X : Type*} (p : A →* Ω X) : - Ω→(psusp.elim p) ∘* loop_psusp_unit A ~* p := - psusp_adjoint_loop_right_inv p + definition ap1_susp_elim {A : Type*} {X : Type*} (p : A →* Ω X) : + Ω→(susp_elim p) ∘* loop_susp_unit A ~* p := + susp_adjoint_loop_right_inv p - definition psusp_adjoint_loop_nat_right (f : psusp X →* Y) (g : Y →* Z) - : psusp_adjoint_loop X Z (g ∘* f) ~* ap1 g ∘* psusp_adjoint_loop X Y f := + definition susp_adjoint_loop_nat_right (f : susp X →* Y) (g : Y →* Z) + : susp_adjoint_loop X Z (g ∘* f) ~* ap1 g ∘* susp_adjoint_loop X Y f := begin - esimp [psusp_adjoint_loop], + esimp [susp_adjoint_loop], refine _ ⬝* !passoc, apply pwhisker_right, apply ap1_pcompose end - definition psusp_adjoint_loop_nat_left (f : Y →* Ω Z) (g : X →* Y) - : (psusp_adjoint_loop X Z)⁻¹ᵉ (f ∘* g) ~* (psusp_adjoint_loop Y Z)⁻¹ᵉ f ∘* psusp_functor g := + definition susp_adjoint_loop_nat_left (f : Y →* Ω Z) (g : X →* Y) + : (susp_adjoint_loop X Z)⁻¹ᵉ (f ∘* g) ~* (susp_adjoint_loop Y Z)⁻¹ᵉ f ∘* susp_functor g := begin - esimp [psusp_adjoint_loop], + esimp [susp_adjoint_loop], refine _ ⬝* !passoc⁻¹*, apply pwhisker_left, - apply psusp_functor_pcompose + apply susp_functor_pcompose end /- iterated suspension -/ - definition iterate_susp (n : ℕ) (A : Type) : Type := iterate susp n A - definition iterate_psusp (n : ℕ) (A : Type*) : Type* := iterate (λX, psusp X) n A + definition iterate_susp (n : ℕ) (A : Type*) : Type* := iterate (λX, susp X) n A open is_conn trunc_index nat - definition iterate_susp_succ (n : ℕ) (A : Type) : + definition iterate_susp_succ (n : ℕ) (A : Type*) : iterate_susp (succ n) A = susp (iterate_susp n A) := idp - definition is_conn_iterate_susp [instance] (n : ℕ₋₂) (m : ℕ) (A : Type) + definition is_conn_iterate_susp [instance] (n : ℕ₋₂) (m : ℕ) (A : Type*) [H : is_conn n A] : is_conn (n + m) (iterate_susp m A) := begin induction m with m IH, exact H, exact @is_conn_susp _ _ IH end - definition is_conn_iterate_psusp [instance] (n : ℕ₋₂) (m : ℕ) (A : Type*) - [H : is_conn n A] : is_conn (n + m) (iterate_psusp m A) := - begin induction m with m IH, exact H, exact @is_conn_susp _ _ IH end - -- Separate cases for n = 0, which comes up often - definition is_conn_iterate_susp_zero [instance] (m : ℕ) (A : Type) + definition is_conn_iterate_susp_zero [instance] (m : ℕ) (A : Type*) [H : is_conn 0 A] : is_conn m (iterate_susp m A) := begin induction m with m IH, exact H, exact @is_conn_susp _ _ IH end - definition is_conn_iterate_psusp_zero [instance] (m : ℕ) (A : Type*) - [H : is_conn 0 A] : is_conn m (iterate_psusp m A) := - begin induction m with m IH, exact H, exact @is_conn_susp _ _ IH end - - definition iterate_psusp_functor (n : ℕ) {A B : Type*} (f : A →* B) : - iterate_psusp n A →* iterate_psusp n B := + definition iterate_susp_functor (n : ℕ) {A B : Type*} (f : A →* B) : + iterate_susp n A →* iterate_susp n B := begin induction n with n g, { exact f }, - { exact psusp_functor g } + { exact susp_functor g } end - definition iterate_psusp_succ_in (n : ℕ) (A : Type*) : - iterate_psusp (succ n) A ≃* iterate_psusp n (psusp A) := + definition iterate_susp_succ_in (n : ℕ) (A : Type*) : + iterate_susp (succ n) A ≃* iterate_susp n (susp A) := begin induction n with n IH, { reflexivity}, - { exact psusp_pequiv IH} + { exact susp_pequiv IH} end - definition iterate_psusp_adjoint_loopn [constructor] (X Y : Type*) (n : ℕ) : - ppmap (iterate_psusp n X) Y ≃* ppmap X (Ω[n] Y) := + definition iterate_susp_adjoint_loopn [constructor] (X Y : Type*) (n : ℕ) : + ppmap (iterate_susp n X) Y ≃* ppmap X (Ω[n] Y) := begin revert X Y, induction n with n IH: intro X Y, { reflexivity }, - { refine !psusp_adjoint_loop ⬝e* !IH ⬝e* _, apply pequiv_ppcompose_left, + { refine !susp_adjoint_loop ⬝e* !IH ⬝e* _, apply pequiv_ppcompose_left, symmetry, apply loopn_succ_in } end - - end susp diff --git a/hott/homotopy/wedge.hlean b/hott/homotopy/wedge.hlean index aecdfd7db..808637fdf 100644 --- a/hott/homotopy/wedge.hlean +++ b/hott/homotopy/wedge.hlean @@ -9,10 +9,10 @@ import hit.pushout .connectedness types.unit open eq pushout pointed unit trunc_index -definition wedge (A B : Type*) : Type := ppushout (pconst punit A) (pconst punit B) -local attribute wedge [reducible] -definition pwedge [constructor] (A B : Type*) : Type* := pointed.mk' (wedge A B) -infixr ` ∨ ` := pwedge +definition wedge' (A B : Type*) : Type := ppushout (pconst punit A) (pconst punit B) +local attribute wedge' [reducible] +definition wedge [constructor] (A B : Type*) : Type* := pointed.mk' (wedge' A B) +infixr ` ∨ ` := wedge namespace wedge @@ -21,11 +21,11 @@ namespace wedge protected definition rec {A B : Type*} {P : wedge A B → Type} (Pinl : Π(x : A), P (inl x)) (Pinr : Π(x : B), P (inr x)) (Pglue : pathover P (Pinl pt) wedge.glue (Pinr pt)) - (y : wedge A B) : P y := + (y : wedge' A B) : P y := by induction y; apply Pinl; apply Pinr; induction x; exact Pglue protected definition elim {A B : Type*} {P : Type} (Pinl : A → P) - (Pinr : B → P) (Pglue : Pinl pt = Pinr pt) (y : wedge A B) : P := + (Pinr : B → P) (Pglue : Pinl pt = Pinr pt) (y : wedge' A B) : P := by induction y with a b x; exact Pinl a; exact Pinr b; induction x; exact Pglue protected definition rec_glue {A B : Type*} {P : wedge A B → Type} (Pinl : Π(x : A), P (inl x)) @@ -33,11 +33,10 @@ namespace wedge apd (wedge.rec Pinl Pinr Pglue) wedge.glue = Pglue := !pushout.rec_glue - protected definition elim_glue {A B : Type*} {P : Type} (Pinl : A → P) - (Pinr : B → P) (Pglue : Pinl pt = Pinr pt) : ap (wedge.elim Pinl Pinr Pglue) wedge.glue = Pglue := + protected definition elim_glue {A B : Type*} {P : Type} (Pinl : A → P) (Pinr : B → P) + (Pglue : Pinl pt = Pinr pt) : ap (wedge.elim Pinl Pinr Pglue) wedge.glue = Pglue := !pushout.elim_glue - end wedge attribute wedge.rec wedge.elim [recursor 7] [unfold 7] @@ -45,7 +44,7 @@ attribute wedge.rec wedge.elim [recursor 7] [unfold 7] namespace wedge -- TODO maybe find a cleaner proof - protected definition unit (A : Type*) : A ≃* pwedge punit A := + protected definition unit (A : Type*) : A ≃* wedge punit A := begin fapply pequiv_of_pmap, { fapply pmap.mk, intro a, apply pinr a, apply respect_pt },