From 4f1db25e169c9adaafe794375592dad1b207d2e4 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 17 Nov 2016 16:21:40 -0500 Subject: [PATCH] Work on the uniqueness of Eilenberg-Maclane spaces --- homotopy/EM.hlean | 54 +++- homotopy/EMnew.hlean | 518 ++++++++++++++++++++++++++++++++++++++ homotopy/cohomology.hlean | 7 +- homotopy/degree.hlean | 4 +- homotopy/smash.hlean | 4 +- move_to_lib.hlean | 401 ++++++++++++++++++++++++++--- 6 files changed, 933 insertions(+), 55 deletions(-) create mode 100644 homotopy/EMnew.hlean diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean index e7e5de8..a4d8113 100644 --- a/homotopy/EM.hlean +++ b/homotopy/EM.hlean @@ -153,7 +153,7 @@ namespace EM [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n →* X := pmap.mk (EMadd1_map e r) begin cases n with n: reflexivity end - definition loop_pEMadd1_pmap {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G) + definition loopn_pEMadd1_pmap {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G) (r : Π(p q : Ω[succ n] X), e (@concat (Ω[n] X) pt pt pt p q) = e p * e q) [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : Ω→[succ n](pEMadd1_pmap e r) ~ e⁻¹ᵉ ∘ loopn_EMadd1 G n := @@ -185,7 +185,7 @@ namespace EM do 2 exact trivial_homotopy_group_of_is_conn _ (le_of_lt_succ H)}, { cases H, esimp, apply is_equiv_trunc_functor, esimp, apply is_equiv.homotopy_closed, rotate 1, - { symmetry, exact loop_pEMadd1_pmap _ _}, + { symmetry, exact loopn_pEMadd1_pmap _ _}, apply is_equiv_compose, apply pequiv.to_is_equiv}, { apply @is_equiv_of_is_contr, do 2 exact trivial_homotopy_group_of_is_trunc _ H} @@ -206,18 +206,15 @@ namespace EM definition EM_pequiv_zero {G : CommGroup} {X : Type*} (e : X ≃* pType_of_Group G) : EM G 0 ≃* X := proof e⁻¹ᵉ* qed - definition EM_spectrum /-[constructor]-/ (G : CommGroup) : spectrum := - spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*) - /- uniqueness of K(G,n), method 2: -/ -- 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] (psusp A) ≃* π[k] A := -- calc --- π*[k + 1] (psusp A) ≃* π*[k] (Ω (psusp A)) : pequiv_of_eq (homotopy_group_succ_in (psusp A) k) +-- π[k + 1] (psusp A) ≃* π[k] (Ω (psusp A)) : homotopy_group_succ_in -- ... ≃* Ω[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] A : (homotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ* definition iterate_psusp_succ_pequiv (n : ℕ) (A : Type*) : iterate_psusp (succ n) A ≃* iterate_psusp n (psusp A) := @@ -273,6 +270,47 @@ namespace EM symmetry, apply loopn_succ_in} end + /- new method of uniqueness, define K(G,n+1) as the truncation of the suspension of K(G,n) -/ + + definition EMadd2 (G : CommGroup) (n : ℕ) : Type* := ptrunc (n.+2) (psusp (EMadd1 G n)) + + definition EMadd2_map [constructor] {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[n+2] X ≃ G) + (r : Π(p q : Ω[n+2] X), e (@concat (Ω[n+1] X) pt pt pt p q) = e p * e q) + [H1 : is_conn (n.+1) X] [H2 : is_trunc (n.+2) X] : EMadd2 G n → X := + begin + intro x, induction x with x, induction x with x, + { exact pt }, + { exact pt }, + { refine EMadd1_map ((loopn_succ_in _ (n+1))⁻¹ᵉ ⬝e e) _ x, + exact abstract begin + intro p q, refine _ ⬝ !r, apply ap e, esimp, + refine @inv_eq_of_eq _ _ (pequiv.to_equiv (loopn_succ_in X (n + 1))) _ _ _ _, + refine _⁻¹ ⬝ !loopn_succ_in_con⁻¹, + exact to_right_inv (loopn_succ_in X (succ n)) p ◾ to_right_inv (loopn_succ_in X (succ n)) q + end end } + end + + -- -- general case + -- definition EMadd1_map [unfold 8] {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G) + -- (r : Π(p q : Ω (Ω[n] X)), e (p ⬝ q) = e p * e q) + -- [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n → X := + -- begin + -- revert X e r H1 H2, induction n with n f: intro X e r H1 H2, + -- { change trunc 1 (EM1 G) → X, intro x, induction x with x, exact EM1_map e r x}, + -- change trunc (n.+2) (susp (iterate_psusp n (pEM1 G))) → X, intro x, + -- induction x with x, induction x with x, + -- { exact pt}, + -- { exact pt}, + -- change carrier (Ω X), refine f _ _ _ _ _ (tr x), + -- { refine _⁻¹ᵉ ⬝e e, apply equiv_of_pequiv, apply loopn_succ_in}, + -- exact abstract begin + -- intro p q, refine _ ⬝ !r, apply ap e, esimp, + -- apply inv_eq_of_eq, + -- refine _⁻¹ ⬝ !loopn_succ_in_con⁻¹, + -- exact to_right_inv (loopn_succ_in X (succ n)) p ◾ to_right_inv (loopn_succ_in X (succ n)) q + -- end end + -- end + end EM -- cohomology ∥ X → K(G,n) ∥ -- reduced cohomology ∥ X →* K(G,n) ∥ diff --git a/homotopy/EMnew.hlean b/homotopy/EMnew.hlean new file mode 100644 index 0000000..a768547 --- /dev/null +++ b/homotopy/EMnew.hlean @@ -0,0 +1,518 @@ +/- +Copyright (c) 2016 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Floris van Doorn + +Eilenberg MacLane spaces + +This file replaces the file in the HoTT library +-/ + +import hit.groupoid_quotient homotopy.hopf homotopy.freudenthal homotopy.homotopy_group + ..move_to_lib +open algebra pointed nat eq category group is_trunc iso unit trunc equiv is_conn function is_equiv + trunc_index + +local attribute pType_of_Group [coercion] + +namespace EMnew + open groupoid_quotient + + variables {G : Group} + definition EM1' (G : Group) : Type := + groupoid_quotient (Groupoid_of_Group G) + definition EM1 [constructor] (G : Group) : Type* := + pointed.MK (EM1' G) (elt star) + + definition base : EM1' G := elt star + definition pth : G → base = base := pth + definition resp_mul (g h : G) : pth (g * h) = pth g ⬝ pth h := resp_comp h g + definition resp_one : pth (1 : G) = idp := + resp_id star + + definition resp_inv (g : G) : pth (g⁻¹) = (pth g)⁻¹ := + resp_inv g + + local attribute pointed.MK pointed.carrier EM1 EM1' [reducible] + protected definition rec {P : EM1' G → Type} [H : Π(x : EM1' G), is_trunc 1 (P x)] + (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb) + (Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h) (x : EM1' G) : P x := + begin + induction x, + { induction g, exact Pb}, + { induction a, induction b, exact Pp f}, + { induction a, induction b, induction c, exact Pmul f g} + end + + protected definition rec_on {P : EM1' G → Type} [H : Π(x : EM1' G), is_trunc 1 (P x)] + (x : EM1' G) (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb) + (Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h) : P x := + EMnew.rec Pb Pp Pmul x + + protected definition set_rec {P : EM1' G → Type} [H : Π(x : EM1' G), is_set (P x)] + (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb) (x : EM1' G) : P x := + EMnew.rec Pb Pp !center x + + protected definition prop_rec {P : EM1' G → Type} [H : Π(x : EM1' G), is_prop (P x)] + (Pb : P base) (x : EM1' G) : P x := + EMnew.rec Pb !center !center x + + definition rec_pth {P : EM1' G → Type} [H : Π(x : EM1' G), is_trunc 1 (P x)] + {Pb : P base} {Pp : Π(g : G), Pb =[pth g] Pb} + (Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h) + (g : G) : apd (EMnew.rec Pb Pp Pmul) (pth g) = Pp g := + proof !rec_pth qed + + protected definition elim {P : Type} [is_trunc 1 P] (Pb : P) (Pp : Π(g : G), Pb = Pb) + (Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) (x : EM1' G) : P := + begin + induction x, + { exact Pb}, + { exact Pp f}, + { exact Pmul f g} + end + + protected definition elim_on [reducible] {P : Type} [is_trunc 1 P] (x : EM1' G) + (Pb : P) (Pp : G → Pb = Pb) (Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) : P := + EMnew.elim Pb Pp Pmul x + + protected definition set_elim [reducible] {P : Type} [is_set P] (Pb : P) (Pp : G → Pb = Pb) + (x : EM1' G) : P := + EMnew.elim Pb Pp !center x + + protected definition prop_elim [reducible] {P : Type} [is_prop P] (Pb : P) (x : EM1' G) : P := + EMnew.elim Pb !center !center x + + definition elim_pth {P : Type} [is_trunc 1 P] {Pb : P} {Pp : G → Pb = Pb} + (Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) (g : G) : ap (EMnew.elim Pb Pp Pmul) (pth g) = Pp g := + proof !elim_pth qed + + protected definition elim_set.{u} (Pb : Set.{u}) (Pp : Π(g : G), Pb ≃ Pb) + (Pmul : Π(g h : G) (x : Pb), Pp (g * h) x = Pp h (Pp g x)) (x : EM1' G) : Set.{u} := + groupoid_quotient.elim_set (λu, Pb) (λu v, Pp) (λu v w g h, proof Pmul h g qed) x + + theorem elim_set_pth {Pb : Set} {Pp : Π(g : G), Pb ≃ Pb} + (Pmul : Π(g h : G) (x : Pb), Pp (g * h) x = Pp h (Pp g x)) (g : G) : + transport (EMnew.elim_set Pb Pp Pmul) (pth g) = Pp g := + !elim_set_pth + +end EMnew + +attribute EMnew.base [constructor] +attribute EMnew.rec EMnew.elim [unfold 7] [recursor 7] +attribute EMnew.rec_on EMnew.elim_on [unfold 4] +attribute EMnew.set_rec EMnew.set_elim [unfold 6] +attribute EMnew.prop_rec EMnew.prop_elim EMnew.elim_set [unfold 5] + +namespace EMnew + open groupoid_quotient + + variables (G : Group) + definition base_eq_base_equiv : (base = base :> EM1 G) ≃ G := + !elt_eq_elt_equiv + + definition fundamental_group_EM1 : π₁ (EM1 G) ≃g G := + begin + fapply isomorphism_of_equiv, + { exact trunc_equiv_trunc 0 !base_eq_base_equiv ⬝e trunc_equiv 0 G}, + { intros g h, induction g with p, induction h with q, + exact encode_con p q} + end + + proposition is_trunc_EM1 [instance] : is_trunc 1 (EM1 G) := + !is_trunc_groupoid_quotient + + proposition is_trunc_EM1' [instance] : is_trunc 1 (EM1' G) := + !is_trunc_groupoid_quotient + + proposition is_conn_EM1' [instance] : is_conn 0 (EM1' G) := + by apply @is_conn_groupoid_quotient; esimp; exact _ + + proposition is_conn_EM1 [instance] : is_conn 0 (EM1 G) := + is_conn_EM1' G + + variable {G} + definition EM1_map [unfold 7] {X : Type*} (e : G → Ω X) + (r : Πg h, e (g * h) = e g ⬝ e h) [is_conn 0 X] [is_trunc 1 X] : EM1 G → X := + begin + intro x, induction x using EMnew.elim, + { exact Point X }, + { exact e g }, + { exact r g h } + end + + /- Uniqueness of K(G, 1) -/ + + definition EM1_pmap [constructor] {X : Type*} (e : G → Ω X) + (r : Πg h, e (g * h) = e g ⬝ e h) [is_conn 0 X] [is_trunc 1 X] : EM1 G →* X := + pmap.mk (EM1_map e r) idp + + variable (G) + definition loop_EM1 [constructor] : G ≃* Ω (EM1 G) := + (pequiv_of_equiv (base_eq_base_equiv G) idp)⁻¹ᵉ* + + variable {G} + definition loop_EM1_pmap {X : Type*} (e : G →* Ω X) + (r : Πg h, e (g * h) = e g ⬝ e h) [is_conn 0 X] [is_trunc 1 X] : + Ω→(EM1_pmap e r) ∘* loop_EM1 G ~* e := + begin + fapply phomotopy.mk, + { intro g, refine !idp_con ⬝ elim_pth r g }, + { apply is_set.elim } + end + + definition EM1_pequiv'.{u} {G : Group.{u}} {X : pType.{u}} (e : G ≃* Ω X) + (r : Πg h, e (g * h) = e g ⬝ e h) [is_conn 0 X] [is_trunc 1 X] : EM1 G ≃* X := + begin + apply pequiv_of_pmap (EM1_pmap e r), + apply whitehead_principle_pointed 1, + intro k, cases k with k, + { apply @is_equiv_of_is_contr, + all_goals (esimp; exact _)}, + { cases k with k, + { apply is_equiv_trunc_functor, esimp, + apply is_equiv.homotopy_closed, rotate 1, + { symmetry, exact phomotopy_pinv_right_of_phomotopy (loop_EM1_pmap _ _) }, + apply is_equiv_compose e }, + { apply @is_equiv_of_is_contr, + do 2 exact trivial_homotopy_group_of_is_trunc _ (succ_lt_succ !zero_lt_succ)}} + end + + definition EM1_pequiv.{u} {G : Group.{u}} {X : pType.{u}} (e : G ≃g π₁ X) + [is_conn 0 X] [is_trunc 1 X] : EM1 G ≃* X := + begin + apply EM1_pequiv' (pequiv_of_isomorphism e ⬝e* ptrunc_pequiv _ _ _), + refine is_equiv.preserve_binary_of_inv_preserve _ mul concat _, + intro p q, + exact to_respect_mul e⁻¹ᵍ (tr p) (tr q) + end + + definition EM1_pequiv_type (X : Type*) [is_conn 0 X] [is_trunc 1 X] : EM1 (π₁ X) ≃* X := + EM1_pequiv !isomorphism.refl + +end EMnew + +open hopf new_susp susp +namespace EMnew + /- EM1 G is an h-space if G is an abelian group. This allows us to construct K(G,n) for n ≥ 2 -/ + variables {G : CommGroup} (n : ℕ) + + definition EM1_mul [unfold 2 3] (x x' : EM1' G) : EM1' G := + begin + induction x, + { exact x'}, + { induction x' using EMnew.set_rec, + { exact pth g}, + { exact abstract begin apply loop_pathover, apply square_of_eq, + refine !resp_mul⁻¹ ⬝ _ ⬝ !resp_mul, + exact ap pth !mul.comm end end}}, + { refine EMnew.prop_rec _ x', apply resp_mul } + end + + variable (G) + definition EM1_mul_one (x : EM1' G) : EM1_mul x base = x := + begin + induction x using EMnew.set_rec, + { reflexivity}, + { apply eq_pathover_id_right, apply hdeg_square, refine EMnew.elim_pth _ g} + end + + definition h_space_EM1 [constructor] [instance] : h_space (EM1' G) := + begin + fapply h_space.mk, + { exact EM1_mul}, + { exact base}, + { intro x', reflexivity}, + { apply EM1_mul_one} + end + + /- K(G, n+1) -/ + definition EMadd1 : ℕ → Type* + | 0 := EM1 G + | (n+1) := ptrunc (n+2) (psusp (EMadd1 n)) + + definition EMadd1_succ [unfold_full] (n : ℕ) : + EMadd1 G (succ n) = ptrunc (n.+2) (psusp (EMadd1 G n)) := + idp + + definition loop_EM2 : Ω[1] (EMadd1 G 1) ≃* EM1 G := + hopf.delooping (EM1' G) idp + + definition is_conn_EMadd1 [instance] (n : ℕ) : is_conn n (EMadd1 G n) := + begin + induction n with n IH, + { apply is_conn_EM1 }, + { rewrite EMadd1_succ, esimp, exact _ } + end + + definition is_trunc_EMadd1 [instance] (n : ℕ) : is_trunc (n+1) (EMadd1 G n) := + begin + cases n with n, + { apply is_trunc_EM1 }, + { apply is_trunc_trunc } + end + + /- loops of an EM-space -/ + definition loop_EMadd1 (n : ℕ) : EMadd1 G n ≃* Ω (EMadd1 G (succ n)) := + begin + cases n with n, + { exact !loop_EM2⁻¹ᵉ* }, + { rewrite [EMadd1_succ G (succ n)], + refine (ptrunc_pequiv (succ n + 1) _ _)⁻¹ᵉ* ⬝e* _ ⬝e* (loop_ptrunc_pequiv _ _)⁻¹ᵉ*, + have succ n + 1 ≤ 2 * succ n, from add_mul_le_mul_add n 1 1, + refine freudenthal_pequiv _ this } + end + + definition loopn_EMadd1_pequiv_EM1 (G : CommGroup) (n : ℕ) : EM1 G ≃* Ω[n] (EMadd1 G n) := + begin + induction n with n e, + { reflexivity }, + { refine _ ⬝e* !loopn_succ_in⁻¹ᵉ*, + refine _ ⬝e* loopn_pequiv_loopn n !loop_EMadd1, + exact e } + end + + -- use loopn_EMadd1_pequiv_EM1 in this definition? + definition loopn_EMadd1 (G : CommGroup) (n : ℕ) : G ≃* Ω[succ n] (EMadd1 G n) := + begin + induction n with n e, + { apply loop_EM1 }, + { refine _ ⬝e* !loopn_succ_in⁻¹ᵉ*, + refine _ ⬝e* loopn_pequiv_loopn (succ n) !loop_EMadd1, + exact e } + end + + definition loopn_EMadd1_succ [unfold_full] (G : CommGroup) (n : ℕ) : loopn_EMadd1 G (succ n) ~* + !loopn_succ_in⁻¹ᵉ* ∘* apn (succ n) !loop_EMadd1 ∘* loopn_EMadd1 G n := + by reflexivity + + definition EM_up {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ (succ n)] X ≃* G) + : Ω[succ n] (Ω X) ≃* G := + !loopn_succ_in⁻¹ᵉ* ⬝e* e + + definition is_homomorphism_EM_up {G : CommGroup} {X : Type*} {n : ℕ} + (e : Ω[succ (succ n)] X ≃* G) + (r : Π(p q : Ω[succ (succ n)] X), e (p ⬝ q) = e p * e q) + (p q : Ω[succ n] (Ω X)) : EM_up e (p ⬝ q) = EM_up e p * EM_up e q := + begin + refine _ ⬝ !r, apply ap e, esimp, apply apn_con + end + + definition EMadd1_pmap [unfold 8] {G : CommGroup} {X : Type*} (n : ℕ) + (e : Ω[succ n] X ≃* G) + (r : Πp q, e (p ⬝ q) = e p * e q) + [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n →* X := + begin + revert X e r H1 H2, induction n with n f: intro X e r H1 H2, + { 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) _ _)), + end + + definition EMadd1_pmap_succ {G : CommGroup} {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))) := + by reflexivity + + definition loop_EMadd1_pmap {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ (succ n)] X ≃* G) + (r : Πp q, e (p ⬝ q) = e p * e q) + [H1 : is_conn (succ n) X] [H2 : is_trunc ((succ n).+1) X] : + Ω→(EMadd1_pmap (succ n) e r) ∘* loop_EMadd1 G n ~* + EMadd1_pmap n (EM_up e) (is_homomorphism_EM_up e r) := + begin + cases n with n, + { apply hopf_delooping_elim }, + { refine !passoc⁻¹* ⬝* _, + rewrite [EMadd1_pmap_succ (succ n)], + refine pwhisker_right _ !ap1_ptrunc_elim ⬝* _, + refine !passoc⁻¹* ⬝* _, + refine pwhisker_right _ (ptrunc_elim_freudenthal_pequiv + (succ n) (succ (succ n)) (add_mul_le_mul_add n 1 1) _) ⬝* _, + reflexivity } + end + + definition loopn_EMadd1_pmap' {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃* G) + (r : Πp q, e (p ⬝ q) = e p * e q) + [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : + Ω→[succ n](EMadd1_pmap n e r) ∘* loopn_EMadd1 G n ~* e⁻¹ᵉ* := + begin + revert X e r H1 H2, induction n with n IH: intro X e r H1 H2, + { apply loop_EM1_pmap }, + refine pwhisker_left _ !loopn_EMadd1_succ ⬝* _, + refine !passoc⁻¹* ⬝* _, + refine pwhisker_right _ !loopn_succ_in_inv_natural ⬝* _, + refine !passoc ⬝* _, + refine pwhisker_left _ (!passoc⁻¹* ⬝* + pwhisker_right _ (!apn_pcompose⁻¹* ⬝* apn_phomotopy _ !loop_EMadd1_pmap) ⬝* + !IH ⬝* !pinv_trans_pinv_left) ⬝* _, + apply pinv_pcompose_cancel_left + end + + definition EMadd1_pequiv' {G : CommGroup} {X : Type*} (n : ℕ) (e : Ω[succ n] X ≃* G) + (r : Π(p q : Ω[succ n] X), e (p ⬝ q) = e p * e q) + [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X := + begin + apply pequiv_of_pmap (EMadd1_pmap n e r), + have is_conn 0 (EMadd1 G n), from is_conn_of_le _ (zero_le_of_nat n), + have is_trunc (n.+1) (EMadd1 G n), from !is_trunc_EMadd1, + refine whitehead_principle_pointed (n.+1) _ _, + intro k, apply @nat.lt_by_cases k (succ n): intro H, + { apply @is_equiv_of_is_contr, + do 2 exact trivial_homotopy_group_of_is_conn _ (le_of_lt_succ H)}, + { cases H, esimp, apply is_equiv_trunc_functor, esimp, + apply is_equiv.homotopy_closed, rotate 1, + { symmetry, exact phomotopy_pinv_right_of_phomotopy (loopn_EMadd1_pmap' _ _) }, + apply is_equiv_compose (e⁻¹ᵉ*)}, + { apply @is_equiv_of_is_contr, + do 2 exact trivial_homotopy_group_of_is_trunc _ H} + end + + definition EMadd1_pequiv {G : CommGroup} {X : Type*} (n : ℕ) (e : πg[n+1] X ≃g G) + [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X := + begin + have is_set (Ω[succ n] X), from !is_set_loopn, + apply EMadd1_pequiv' n ((ptrunc_pequiv _ _ _)⁻¹ᵉ* ⬝e* pequiv_of_isomorphism e), + intro p q, esimp, exact to_respect_mul e (tr p) (tr q) + end + + definition EMadd1_pequiv_succ {G : CommGroup} {X : Type*} (n : ℕ) (e : πag[n+2] X ≃g G) + [H1 : is_conn (n.+1) X] [H2 : is_trunc (n.+2) X] : EMadd1 G (succ n) ≃* X := + EMadd1_pequiv (succ n) e + + definition ghomotopy_group_EMadd1 (n : ℕ) : πg[n+1] (EMadd1 G n) ≃g G := + begin + change π₁ (Ω[n] (EMadd1 G n)) ≃g G, + refine homotopy_group_isomorphism_of_pequiv 0 (loopn_EMadd1_pequiv_EM1 G n)⁻¹ᵉ* ⬝g _, + apply fundamental_group_EM1, + end + + definition EMadd1_pequiv_type (X : Type*) (n : ℕ) [is_conn (n+1) X] [is_trunc (n+1+1) X] + : EMadd1 (πag[n+2] X) (succ n) ≃* X := + EMadd1_pequiv_succ n !isomorphism.refl + + /- K(G, n) -/ + definition EM (G : CommGroup) : ℕ → Type* + | 0 := G + | (k+1) := EMadd1 G k + + namespace ops + abbreviation K := @EM + end ops + open ops + + definition homotopy_group_EM (n : ℕ) : π[n] (EM G n) ≃* G := + begin + cases n with n, + { rexact ptrunc_pequiv 0 (G) _}, + { exact pequiv_of_isomorphism (ghomotopy_group_EMadd1 G n)} + end + + definition ghomotopy_group_EM (n : ℕ) : πg[n+1] (EM G (n+1)) ≃g G := + ghomotopy_group_EMadd1 G n + + definition is_conn_EM [instance] (n : ℕ) : is_conn (n.-1) (EM G n) := + begin + cases n with n, + { apply is_conn_minus_one, apply tr, unfold [EM], exact 1}, + { apply is_conn_EMadd1} + end + + definition is_conn_EM_succ [instance] (n : ℕ) : is_conn n (EM G (succ n)) := + is_conn_EM G (succ n) + + definition is_trunc_EM [instance] (n : ℕ) : is_trunc n (EM G n) := + begin + cases n with n, + { unfold [EM], apply semigroup.is_set_carrier}, + { apply is_trunc_EMadd1} + end + + definition loop_EM (n : ℕ) : Ω (K G (succ n)) ≃* K G n := + begin + cases n with n, + { refine _ ⬝e* pequiv_of_isomorphism (fundamental_group_EM1 G), + symmetry, apply ptrunc_pequiv, exact _}, + { exact !loop_EMadd1⁻¹ᵉ* } + end + + open circle int + definition EM_pequiv_circle : K agℤ 1 ≃* S¹* := + EM1_pequiv fundamental_group_of_circle⁻¹ᵍ + + /- Functorial action of Eilenberg-Maclane spaces -/ + + definition EM1_functor [constructor] {G H : Group} (φ : G →g H) : EM1 G →* EM1 H := + begin + fconstructor, + { intro g, induction g, + { exact base }, + { exact pth (φ g) }, + { exact ap pth (to_respect_mul φ g h) ⬝ resp_mul (φ g) (φ h) }}, + { reflexivity } + end + + definition EMadd1_functor [constructor] {G H : CommGroup} (φ : G →g H) (n : ℕ) : + EMadd1 G n →* EMadd1 H n := + begin + induction n with n ψ, + { exact EM1_functor φ }, + { apply ptrunc_functor, apply psusp_functor, exact ψ } + end + + definition EM_functor [unfold 4] {G H : CommGroup} (φ : G →g H) (n : ℕ) : + K G n →* K H n := + begin + cases n with n, + { exact pmap_of_homomorphism φ }, + { exact EMadd1_functor φ n } + end + + -- TODO: (K G n →* K H n) ≃ (G →g H) + + /- Equivalence of Groups and pointed connected 1-truncated types -/ + + definition ptruncconntype10_pequiv (X Y : 1-Type*[0]) (e : π₁ X ≃g π₁ Y) : X ≃* Y := + (EM1_pequiv !isomorphism.refl)⁻¹ᵉ* ⬝e* EM1_pequiv e + + definition EM1_pequiv_ptruncconntype10 (X : 1-Type*[0]) : EM1 (π₁ X) ≃* X := + EM1_pequiv_type X + + definition Group_equiv_ptruncconntype10 [constructor] : Group ≃ 1-Type*[0] := + equiv.MK (λG, ptruncconntype.mk (EM1 G) _ pt !is_conn_EM1) + (λX, π₁ X) + begin intro X, apply ptruncconntype_eq, esimp, exact EM1_pequiv_type X end + begin intro G, apply eq_of_isomorphism, apply fundamental_group_EM1 end + + /- Equivalence of CommGroups and pointed n-connected (n+1)-truncated types (n ≥ 1) -/ + + open trunc_index + definition ptruncconntype_pequiv : Π(n : ℕ) (X Y : (n.+1)-Type*[n]) + (e : πg[n+1] X ≃g πg[n+1] Y), X ≃* Y + | 0 X Y e := ptruncconntype10_pequiv X Y e + | (succ n) X Y e := + begin + refine (EMadd1_pequiv_succ n _)⁻¹ᵉ* ⬝e* EMadd1_pequiv_succ n !isomorphism.refl, + exact e + end + + definition EM1_pequiv_ptruncconntype (n : ℕ) (X : (n+1+1)-Type*[n+1]) : + EMadd1 (πag[n+2] X) (succ n) ≃* X := + EMadd1_pequiv_type X n + + definition CommGroup_equiv_ptruncconntype' [constructor] (n : ℕ) : + CommGroup ≃ (n + 1 + 1)-Type*[n+1] := + equiv.MK + (λG, ptruncconntype.mk (EMadd1 G (n+1)) _ pt _) + (λX, πag[n+2] X) + begin intro X, apply ptruncconntype_eq, apply EMadd1_pequiv_type end + begin intro G, apply CommGroup_eq_of_isomorphism, exact ghomotopy_group_EMadd1 G (n+1) end + + definition CommGroup_equiv_ptruncconntype [constructor] (n : ℕ) : + CommGroup ≃ (n.+2)-Type*[n.+1] := + CommGroup_equiv_ptruncconntype' n + + print axioms CommGroup_equiv_ptruncconntype + +end EMnew diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean index c8fce49..1c15223 100644 --- a/homotopy/cohomology.hlean +++ b/homotopy/cohomology.hlean @@ -6,9 +6,12 @@ Authors: Floris van Doorn Reduced cohomology -/ -import .EM algebra.arrow_group +import .EM algebra.arrow_group .spectrum -open eq spectrum int trunc pointed EM group algebra circle sphere nat +open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops + +definition EM_spectrum /-[constructor]-/ (G : CommGroup) : spectrum := +spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*) definition cohomology (X : Type*) (Y : spectrum) (n : ℤ) : CommGroup := CommGroup_pmap X (πag[2] (Y (2+n))) diff --git a/homotopy/degree.hlean b/homotopy/degree.hlean index 5d3d2e2..249b88c 100644 --- a/homotopy/degree.hlean +++ b/homotopy/degree.hlean @@ -51,7 +51,7 @@ namespace sphere end 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)) + 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 : ℤ) := by induction H with n; @@ -94,7 +94,7 @@ namespace sphere apply eq_one_or_eq_neg_one_of_mul_eq_one (deg f⁻¹ᵉ*), refine !deg_compose⁻¹ ⬝ _, refine deg_phomotopy (pright_inv f) ⬝ _, - apply deg_id, + apply deg_id end end sphere diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean index 85e5285..2bf7e8f 100644 --- a/homotopy/smash.hlean +++ b/homotopy/smash.hlean @@ -244,8 +244,8 @@ namespace smash begin induction x with x x, { refine (pushout.glue pt)⁻¹ }, - { }, - { } + { exact sorry }, + { exact sorry } end definition smash_of_pcofiber_of_smash (x : smash A B) : diff --git a/move_to_lib.hlean b/move_to_lib.hlean index c978b6d..718a77e 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -14,6 +14,23 @@ attribute isomorphism._trans_of_to_hom [unfold 3] attribute homomorphism.struct [unfold 3] attribute pequiv.trans pequiv.symm [constructor] +namespace equiv + + variables {A B : Type} (f : A ≃ B) {a : A} {b : B} + definition to_eq_of_eq_inv (p : a = f⁻¹ b) : f a = b := + ap f p ⬝ right_inv f b + + definition to_eq_of_inv_eq (p : f⁻¹ b = a) : b = f a := + (eq_of_eq_inv p⁻¹)⁻¹ + + definition to_inv_eq_of_eq (p : b = f a) : f⁻¹ b = a := + ap f⁻¹ p ⬝ left_inv f a + + definition to_eq_inv_of_eq (p : f a = b) : a = f⁻¹ b := + (inv_eq_of_eq p⁻¹)⁻¹ + +end equiv open equiv + namespace sigma definition sigma_equiv_sigma_left' [constructor] {A A' : Type} {B : A' → Type} (Hf : A ≃ A') : (Σa, B (Hf a)) ≃ (Σa', B a') := @@ -77,8 +94,124 @@ namespace group abbreviation gid [constructor] := @homomorphism_id + definition comm_group.to_has_mul {A : Type} (H : comm_group A) : has_mul A := _ + local attribute comm_group.to_has_mul [coercion] + + definition comm_group_eq {A : Type} {G H : comm_group A} + (same_mul : Π(g h : A), @mul A G g h = @mul A H g h) + : G = H := + begin + have g_eq : @comm_group.to_group A G = @comm_group.to_group A H, from group_eq same_mul, + cases G with Gm Gs Gh1 G1 Gh2 Gh3 Gi Gh4 Gh5, + cases H with Hm Hs Hh1 H1 Hh2 Hh3 Hi Hh4 Hh5, + have pm : Gm = Hm, from ap (@mul _ ∘ _) g_eq, + have pi : Gi = Hi, from ap (@inv _ ∘ _) g_eq, + have p1 : G1 = H1, from ap (@one _ ∘ _) g_eq, + induction pm, induction pi, induction p1, + have ps : Gs = Hs, from !is_prop.elim, + have ph1 : Gh1 = Hh1, from !is_prop.elim, + have ph2 : Gh2 = Hh2, from !is_prop.elim, + have ph3 : Gh3 = Hh3, from !is_prop.elim, + have ph4 : Gh4 = Hh4, from !is_prop.elim, + have ph5 : Gh5 = Hh5, from !is_prop.elim, + induction ps, induction ph1, induction ph2, induction ph3, induction ph4, induction ph5, + reflexivity + end + + definition comm_group_pathover {A B : Type} {G : comm_group A} {H : comm_group B} {p : A = B} + (resp_mul : Π(g h : A), cast p (g * h) = cast p g * cast p h) : G =[p] H := + begin + induction p, + apply pathover_idp_of_eq, exact comm_group_eq (resp_mul) + end + + definition CommGroup_eq_of_isomorphism {G₁ G₂ : CommGroup} (φ : G₁ ≃g G₂) : G₁ = G₂ := + begin + induction G₁, induction G₂, + apply apd011 CommGroup.mk (ua (equiv_of_isomorphism φ)), + apply comm_group_pathover, + intro g h, exact !cast_ua ⬝ respect_mul φ g h ⬝ ap011 mul !cast_ua⁻¹ !cast_ua⁻¹ + end + end group open group +namespace trunc + + -- TODO: make argument in ptrunc_pequiv implicit + + definition ptr [constructor] (n : ℕ₋₂) (A : Type*) : A →* ptrunc n A := + pmap.mk tr idp + + definition puntrunc [constructor] (n : ℕ₋₂) (A : Type*) [is_trunc n A] : ptrunc n A →* A := + pmap.mk untrunc_of_is_trunc idp + + definition ptrunc.elim [constructor] (n : ℕ₋₂) {X Y : Type*} [is_trunc n Y] (f : X →* Y) : + ptrunc n X →* Y := + pmap.mk (trunc.elim f) (respect_pt f) + + definition ptrunc_elim_ptr [constructor] (n : ℕ₋₂) {X Y : Type*} [is_trunc n Y] (f : X →* Y) : + ptrunc.elim n f ∘* ptr n X ~* f := + begin + fapply phomotopy.mk, + { reflexivity }, + { reflexivity } + end + + definition ptrunc_elim_phomotopy (n : ℕ₋₂) {X Y : Type*} [is_trunc n Y] {f g : X →* Y} + (H : f ~* g) : ptrunc.elim n f ~* ptrunc.elim n g := + begin + fapply phomotopy.mk, + { intro x, induction x with x, exact H x }, + { exact to_homotopy_pt H } + end + + definition ap1_ptrunc_functor (n : ℕ₋₂) {A B : Type*} (f : A →* B) : + Ω→ (ptrunc_functor (n.+1) f) ∘* (loop_ptrunc_pequiv n A)⁻¹ᵉ* ~* + (loop_ptrunc_pequiv n B)⁻¹ᵉ* ∘* ptrunc_functor n (Ω→ f) := + begin + fapply phomotopy.mk, + { intro p, induction p with p, + refine (!ap_inv⁻¹ ◾ !ap_compose⁻¹ ◾ idp) ⬝ _ ⬝ !ap_con⁻¹, + apply whisker_right, refine _ ⬝ !ap_con⁻¹, exact whisker_left _ !ap_compose }, + { induction B with B b, induction f with f p, esimp at f, esimp at p, induction p, reflexivity } + end + + definition ap1_ptrunc_elim (n : ℕ₋₂) {A B : Type*} (f : A →* B) [is_trunc (n.+1) B] : + Ω→ (ptrunc.elim (n.+1) f) ∘* (loop_ptrunc_pequiv n A)⁻¹ᵉ* ~* + ptrunc.elim n (Ω→ f) := + begin + fapply phomotopy.mk, + { intro p, induction p with p, exact idp ◾ !ap_compose⁻¹ ◾ idp }, + { reflexivity } + end + + definition ap1_ptr (n : ℕ₋₂) (A : Type*) : + Ω→ (ptr (n.+1) A) ~* (loop_ptrunc_pequiv n A)⁻¹ᵉ* ∘* ptr n (Ω A) := + begin + fapply phomotopy.mk, + { intro p, apply idp_con }, + { reflexivity } + end + + -- definition ap1_ptr' (n : ℕ₋₂) (A : Type*) : + -- loop_ptrunc_pequiv n A ∘* Ω→ (ptr (n.+1) A) ~* ptr n (Ω A) := + -- begin + -- fapply phomotopy.mk, + -- { intro p, refine ap trunc.encode !idp_con ⬝ _, esimp, }, + -- { reflexivity } + -- end + + definition ptrunc_elim_ptrunc_functor (n : ℕ₋₂) {A B C : Type*} (g : B →* C) (f : A →* B) + [is_trunc n C] : + ptrunc.elim n g ∘* ptrunc_functor n f ~* ptrunc.elim n (g ∘* f) := + begin + fapply phomotopy.mk, + { intro x, induction x with a, reflexivity }, + { esimp, exact !idp_con ⬝ whisker_right !ap_compose _ }, + end + +end trunc open trunc + namespace pi -- move to types.arrow definition pmap_eq_idp {X Y : Type*} (f : X →* Y) : @@ -218,6 +351,73 @@ namespace pointed infixr ` ∘*ᵉ `:60 := pequiv_compose + definition pcompose2 {A B C : Type*} {g g' : B →* C} {f f' : A →* B} (p : f ~* f') (q : g ~* g') : + g ∘* f ~* g' ∘* f' := + pwhisker_right f q ⬝* pwhisker_left g' p + + infixr ` ◾* `:80 := pcompose2 + + definition phomotopy_pinv_of_phomotopy_pid {A B : Type*} {f : A →* B} {g : B ≃* A} + (p : g ∘* f ~* pid A) : f ~* g⁻¹ᵉ* := + phomotopy_pinv_left_of_phomotopy p ⬝* !pcompose_pid + + definition phomotopy_pinv_of_phomotopy_pid' {A B : Type*} {f : A →* B} {g : B ≃* A} + (p : f ∘* g ~* pid B) : f ~* g⁻¹ᵉ* := + phomotopy_pinv_right_of_phomotopy p ⬝* !pid_pcompose + + definition pinv_phomotopy_of_pid_phomotopy {A B : Type*} {f : A →* B} {g : B ≃* A} + (p : pid A ~* g ∘* f) : g⁻¹ᵉ* ~* f := + (phomotopy_pinv_of_phomotopy_pid p⁻¹*)⁻¹* + + definition pinv_phomotopy_of_pid_phomotopy' {A B : Type*} {f : A →* B} {g : B ≃* A} + (p : pid B ~* f ∘* g) : g⁻¹ᵉ* ~* f := + (phomotopy_pinv_of_phomotopy_pid' p⁻¹*)⁻¹* + + definition pinv_pinv {A B : Type*} (f : A ≃* B) : (f⁻¹ᵉ*)⁻¹ᵉ* ~* f := + (phomotopy_pinv_of_phomotopy_pid (pleft_inv f))⁻¹* + + definition pinv2 {A B : Type*} {f f' : A ≃* B} (p : f ~* f') : f⁻¹ᵉ* ~* f'⁻¹ᵉ* := + phomotopy_pinv_of_phomotopy_pid (pinv_right_phomotopy_of_phomotopy (!pid_pcompose ⬝* p)⁻¹*) + + postfix [parsing_only] `⁻²*`:(max+10) := pinv2 + + definition trans_pinv {A B C : Type*} (f : A ≃* B) (g : B ≃* C) : + (f ⬝e* g)⁻¹ᵉ* ~* f⁻¹ᵉ* ∘* g⁻¹ᵉ* := + begin + refine (phomotopy_pinv_of_phomotopy_pid _)⁻¹*, + refine !passoc ⬝* _, + refine pwhisker_left _ (!passoc⁻¹* ⬝* pwhisker_right _ !pright_inv ⬝* !pid_pcompose) ⬝* _, + apply pright_inv + end + + definition pinv_trans_pinv_left {A B C : Type*} (f : B ≃* A) (g : B ≃* C) : + (f⁻¹ᵉ* ⬝e* g)⁻¹ᵉ* ~* f ∘* g⁻¹ᵉ* := + !trans_pinv ⬝* pwhisker_right _ !pinv_pinv + + definition pinv_trans_pinv_right {A B C : Type*} (f : A ≃* B) (g : C ≃* B) : + (f ⬝e* g⁻¹ᵉ*)⁻¹ᵉ* ~* f⁻¹ᵉ* ∘* g := + !trans_pinv ⬝* pwhisker_left _ !pinv_pinv + + definition pinv_trans_pinv_pinv {A B C : Type*} (f : B ≃* A) (g : C ≃* B) : + (f⁻¹ᵉ* ⬝e* g⁻¹ᵉ*)⁻¹ᵉ* ~* f ∘* g := + !trans_pinv ⬝* !pinv_pinv ◾* !pinv_pinv + + definition pinv_pcompose_cancel_left {A B C : Type*} (g : B ≃* C) (f : A →* B) : + g⁻¹ᵉ* ∘* (g ∘* f) ~* f := + !passoc⁻¹* ⬝* pwhisker_right f !pleft_inv ⬝* !pid_pcompose + + definition pcompose_pinv_cancel_left {A B C : Type*} (g : C ≃* B) (f : A →* B) : + g ∘* (g⁻¹ᵉ* ∘* f) ~* f := + !passoc⁻¹* ⬝* pwhisker_right f !pright_inv ⬝* !pid_pcompose + + definition pinv_pcompose_cancel_right {A B C : Type*} (g : B →* C) (f : B ≃* A) : + (g ∘* f⁻¹ᵉ*) ∘* f ~* g := + !passoc ⬝* pwhisker_left g !pleft_inv ⬝* !pcompose_pid + + definition pcompose_pinv_cancel_right {A B C : Type*} (g : B →* C) (f : A ≃* B) : + (g ∘* f) ∘* f⁻¹ᵉ* ~* g := + !passoc ⬝* pwhisker_left g !pright_inv ⬝* !pcompose_pid + definition pmap.sigma_char [constructor] {A B : Type*} : (A →* B) ≃ Σ(f : A → B), f pt = pt := begin fapply equiv.MK : intros f, @@ -270,31 +470,6 @@ namespace pointed ... -/ ≃ (A →* Ω B) : pmap.sigma_char) (by reflexivity) - -- definition ppcompose_left {A B C : Type*} (g : B →* C) : ppmap A B →* ppmap A C := - -- pmap.mk (pcompose g) (eq_of_phomotopy (phomotopy.mk (λa, resp_pt g) (idp_con _)⁻¹)) - - -- definition is_equiv_ppcompose_left [instance] {A B C : Type*} (g : B →* C) [H : is_equiv g] : is_equiv (@ppcompose_left A B C g) := - -- begin - -- fapply is_equiv.adjointify, - -- { exact (ppcompose_left (pequiv_of_pmap g H)⁻¹ᵉ*) }, - -- all_goals (intros f; esimp; apply eq_of_phomotopy), - -- { exact calc g ∘* ((pequiv_of_pmap g H)⁻¹ᵉ* ∘* f) ~* (g ∘* (pequiv_of_pmap g H)⁻¹ᵉ*) ∘* f : passoc - -- ... ~* pid _ ∘* f : pwhisker_right f (pright_inv (pequiv_of_pmap g H)) - -- ... ~* f : pid_pcompose f }, - -- { exact calc (pequiv_of_pmap g H)⁻¹ᵉ* ∘* (g ∘* f) ~* ((pequiv_of_pmap g H)⁻¹ᵉ* ∘* g) ∘* f : passoc - -- ... ~* pid _ ∘* f : pwhisker_right f (pleft_inv (pequiv_of_pmap g H)) - -- ... ~* f : pid_pcompose f } - -- end - - -- definition pequiv_ppcompose_left {A B C : Type*} (g : B ≃* C) : ppmap A B ≃* ppmap A C := - -- pequiv_of_pmap (ppcompose_left g) _ - - -- definition pcompose_pconst {A B C : Type*} (f : B →* C) : f ∘* pconst A B ~* pconst A C := - -- phomotopy.mk (λa, respect_pt f) (idp_con _)⁻¹ - - -- definition pconst_pcompose {A B C : Type*} (f : A →* B) : pconst B C ∘* f ~* pconst A C := - -- phomotopy.mk (λa, rfl) (ap_constant _ _)⁻¹ - definition ap1_pconst (A B : Type*) : Ω→(pconst A B) ~* pconst (Ω A) (Ω B) := phomotopy.mk (λp, idp_con _ ⬝ ap_constant p pt) rfl @@ -470,6 +645,18 @@ namespace susp { exact psusp_functor g } end + definition iterate_psusp_succ_in (n : ℕ) (A : Type*) : + iterate_psusp (succ n) A ≃* iterate_psusp n (psusp A) := + begin + induction n with n IH, + { reflexivity}, + { exact psusp_equiv IH} + end + + 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 + end susp namespace is_conn -- homotopy.connectedness @@ -674,26 +861,46 @@ namespace new_susp { reflexivity } end + definition psusp.elim [constructor] {X Y : Type*} (f : X →* Ω Y) : psusp X →* Y := + loop_psusp_counit Y ∘* psusp_functor f + + definition loop_psusp_intro [constructor] {X Y : Type*} (f : psusp X →* Y) : X →* Ω Y := + ap1 f ∘* loop_psusp_unit X + + definition psusp_adjoint_loop_right_inv {X Y : Type*} (g : X →* Ω Y) : + loop_psusp_intro (psusp.elim g) ~* g := + begin + refine !pwhisker_right !ap1_pcompose ⬝* _, + refine !passoc ⬝* _, + refine !pwhisker_left !loop_psusp_unit_natural⁻¹* ⬝* _, + refine !passoc⁻¹* ⬝* _, + refine !pwhisker_right !loop_psusp_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 := + begin + refine !pwhisker_left !psusp_functor_compose ⬝* _, + refine !passoc⁻¹* ⬝* _, + refine !pwhisker_right !loop_psusp_counit_natural⁻¹* ⬝* _, + refine !passoc ⬝* _, + refine !pwhisker_left !loop_psusp_unit_counit ⬝* _, + apply pcompose_pid + 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 + -- TODO: rename to psusp_adjoint_loop (also in above lemmas) definition psusp_adjoint_loop_unpointed [constructor] (X Y : Type*) : psusp X →* Y ≃ X →* Ω Y := begin fapply equiv.MK, - { intro f, exact ap1 f ∘* loop_psusp_unit X }, - { intro g, exact loop_psusp_counit Y ∘* psusp_functor g }, - { intro g, apply eq_of_phomotopy, esimp, - refine !pwhisker_right !ap1_pcompose ⬝* _, - refine !passoc ⬝* _, - refine !pwhisker_left !loop_psusp_unit_natural⁻¹* ⬝* _, - refine !passoc⁻¹* ⬝* _, - refine !pwhisker_right !loop_psusp_counit_unit ⬝* _, - apply pid_pcompose }, - { intro f, apply eq_of_phomotopy, esimp, - refine !pwhisker_left !psusp_functor_compose ⬝* _, - refine !passoc⁻¹* ⬝* _, - refine !pwhisker_right !loop_psusp_counit_natural⁻¹* ⬝* _, - refine !passoc ⬝* _, - refine !pwhisker_left !loop_psusp_unit_counit ⬝* _, - apply pcompose_pid }, + { 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 } end definition psusp_adjoint_loop_pconst (X Y : Type*) : @@ -710,8 +917,120 @@ namespace new_susp apply psusp_adjoint_loop_pconst end + -- in freudenthal + open trunc + local attribute ptrunc_pequiv_ptrunc_of_le [constructor] + 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) := + begin + fapply phomotopy.mk, + { intro x, induction x with a, reflexivity }, + { refine !idp_con ⬝ _, refine _ ⬝ ap02 _ !idp_con⁻¹, refine _ ⬝ !ap_compose, apply ap_compose } + 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 := + begin + refine pwhisker_left _ !to_pmap_freudenthal_pequiv ⬝* _, + refine !ptrunc_elim_ptrunc_functor ⬝* _, + exact ptrunc_elim_phomotopy k !ap1_psusp_elim, + end + + open susp + 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)) := + begin + revert A n k HA H, induction m with m IH: intro A n k HA H, + { 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)} + end + + definition iterate_psusp_adjoint_loopn [constructor] (X Y : Type*) (n : ℕ) : + ppmap (iterate_psusp 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, + symmetry, apply loopn_succ_in } + end + end new_susp open new_susp +namespace hopf + + definition my_transport_codes_merid.{u} (A : Type.{u}) [T : is_trunc 1 A] [K : is_conn 0 A] + [H : h_space A] (a a' : A) : transport (hopf A) (merid a) a' = a * a' :> A := + ap10 (elim_type_merid _ _ _ a) a' + + definition my_transport_codes_merid_one_inv.{u} (A : Type.{u}) [T : is_trunc 1 A] + [K : is_conn 0 A] [H : h_space A] (a : A) : transport (hopf A) (merid 1)⁻¹ a = a := + ap10 (elim_type_merid_inv _ _ _ 1) a ⬝ + begin apply to_inv_eq_of_eq, esimp, refine !one_mul⁻¹ end + + definition my_encode_decode' (A : Type) [T : is_trunc 1 A] [K : is_conn 0 A] + [H : h_space A] (a : A) : encode A (decode' A a) = a := + begin + esimp [encode, decode', encode₀], +-- refine ap (λp, transport (hopf A) p a) _ ⬝ _ + refine !con_tr ⬝ _, + refine (ap (transport _ _) !my_transport_codes_merid ⬝ !my_transport_codes_merid_one_inv) ⬝ _, + apply mul_one + end + + definition to_pmap_main_lemma_point_pinv (A : Type) [T : is_trunc 1 A] [K : is_conn 0 A] + [H : h_space A] (coh : one_mul 1 = mul_one 1 :> (1 * 1 = 1 :> A)) + : (main_lemma_point A coh)⁻¹ᵉ* ~* !ptr ∘* loop_psusp_unit (pointed.MK A 1) := + begin + apply pinv_phomotopy_of_pid_phomotopy, + fapply phomotopy.mk, + { intro a, exact (my_encode_decode' A a)⁻¹ }, + { esimp [main_lemma_point, main_lemma, encode], + apply inv_con_eq_of_eq_con, + refine !ap_compose'⁻¹ ⬝ _, esimp, + esimp [my_encode_decode'], + unfold [encode₀], + exact sorry + -- assert p : Π(A : Type) (a a' : A) (p : a = a') (B : A → Type) (b : B a), + -- ap (λ p, p ▸ b) (con.right_inv p) = con_tr p p⁻¹ b ⬝ (ap (transport B p⁻¹) + -- (transport_codes_merid A b b ⬝ mul_one 1) ⬝ transport_codes_merid_one_inv A 1), + + } + end + + definition to_pmap_delooping_pinv (A : Type) [T : is_trunc 1 A] [K : is_conn 0 A] [H : h_space A] + (coh : one_mul 1 = mul_one 1 :> (1 * 1 = 1 :> A)) + : (hopf.delooping A coh)⁻¹ᵉ* ~* Ω→ !ptr ∘* loop_psusp_unit (pointed.MK A 1) := + begin + refine !trans_pinv ⬝* _, + refine pwhisker_left _ !to_pmap_main_lemma_point_pinv ⬝* _, + refine !passoc⁻¹* ⬝* _, + refine pwhisker_right _ !ap1_ptr⁻¹*, + end + + definition hopf_delooping_elim {A : Type} {B : Type*} [T : is_trunc 1 A] [K : is_conn 0 A] + [H : h_space A] (coh : one_mul 1 = mul_one 1 :> (1 * 1 = 1 :> A)) (f : pointed.MK A 1 →* Ω B) + /-[H1 : is_conn 1 B]-/ [H2 : is_trunc 2 B] : + Ω→(ptrunc.elim 2 (psusp.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 + end + +end hopf -- this should replace corresponding definitions in homotopy.sphere namespace new_sphere