diff --git a/homotopy/LES_applications.hlean b/homotopy/LES_applications.hlean index 739ae03..e60225f 100644 --- a/homotopy/LES_applications.hlean +++ b/homotopy/LES_applications.hlean @@ -1,6 +1,7 @@ import .LES_of_homotopy_groups homotopy.connectedness homotopy.homotopy_group homotopy.join open eq is_trunc pointed homotopy is_equiv fiber equiv trunc nat chain_complex prod fin algebra group trunc_index function join pushout + namespace nat open sigma sum definition eq_even_or_eq_odd (n : ℕ) : (Σk, 2 * k = n) ⊎ (Σk, 2 * k + 1 = n) := @@ -25,61 +26,6 @@ open nat namespace is_conn - theorem is_contr_HG_fiber_of_is_connected {A B : Type*} (k n : ℕ) (f : A →* B) - [H : is_conn_map n f] (H2 : k ≤ n) : is_contr (π[k] (pfiber f)) := - @(trivial_homotopy_group_of_is_conn (pfiber f) H2) (H pt) - - -- TODO: use this for trivial_homotopy_group_of_is_conn (in homotopy.homotopy_group) - theorem is_conn_of_le (A : Type) {n k : ℕ₋₂} (H : n ≤ k) [is_conn k A] : is_conn n A := - begin - apply is_contr_equiv_closed, - apply trunc_trunc_equiv_left _ n k H - end - - definition zero_le_of_nat (n : ℕ) : 0 ≤[ℕ₋₂] n := - of_nat_le_of_nat (zero_le n) - - local attribute is_conn_map [reducible] --TODO - theorem is_conn_map_of_le {A B : Type} (f : A → B) {n k : ℕ₋₂} (H : n ≤ k) - [is_conn_map k f] : is_conn_map n f := - λb, is_conn_of_le _ H - - definition is_surjective_trunc_functor {A B : Type} (n : ℕ₋₂) (f : A → B) [H : is_surjective f] - : is_surjective (trunc_functor n f) := - begin - cases n with n: intro b, - { exact tr (fiber.mk !center !is_prop.elim)}, - { refine @trunc.rec _ _ _ _ _ b, {intro x, exact is_trunc_of_le _ !minus_one_le_succ}, - clear b, intro b, induction H b with v, induction v with a p, - exact tr (fiber.mk (tr a) (ap tr p))} - end - - definition is_surjective_cancel_right {A B C : Type} (g : B → C) (f : A → B) - [H : is_surjective (g ∘ f)] : is_surjective g := - begin - intro c, - induction H c with v, induction v with a p, - exact tr (fiber.mk (f a) p) - end - - -- Lemma 7.5.14 - theorem is_equiv_trunc_functor_of_is_conn_map {A B : Type} (n : ℕ₋₂) (f : A → B) - [H : is_conn_map n f] : is_equiv (trunc_functor n f) := - begin - fapply adjointify, - { intro b, induction b with b, exact trunc_functor n point (center (trunc n (fiber f b)))}, - { intro b, induction b with b, esimp, generalize center (trunc n (fiber f b)), intro v, - induction v with v, induction v with a p, esimp, exact ap tr p}, - { intro a, induction a with a, esimp, rewrite [center_eq (tr (fiber.mk a idp))]} - end - - theorem trunc_equiv_trunc_of_is_conn_map {A B : Type} (n : ℕ₋₂) (f : A → B) - [H : is_conn_map n f] : trunc n A ≃ trunc n B := - equiv.mk (trunc_functor n f) (is_equiv_trunc_functor_of_is_conn_map n f) - - definition is_equiv_tinverse [constructor] (A : Type*) : is_equiv (@tinverse A) := - by apply @is_equiv_trunc_functor; apply is_equiv_eq_inverse - local attribute comm_group.to_group [coercion] local attribute is_equiv_tinverse [instance] @@ -124,20 +70,20 @@ namespace is_conn [H : is_conn_map n f] : is_surjective (π→[n + 1] f) := begin induction n using rec_on_even_odd with n, - { cases n with n, - { exact sorry}, - { have H3 : is_surjective (π→*[2*(succ n) + 1] f ∘* tinverse), from - @is_surjective_of_trivial _ - (LES_of_homotopy_groups3 f) _ - (is_exact_LES_of_homotopy_groups3 f (succ n, 2)) - (@is_contr_HG_fiber_of_is_connected A B (2 * succ n) (2 * succ n) f H !le.refl), - exact @(is_surjective_cancel_right (pmap.to_fun (π→*[2*(succ n) + 1] f)) tinverse) H3}}, + { have H3 : is_surjective (π→*[2*n + 1] f ∘* tinverse), from + @is_surjective_of_trivial _ + (LES_of_homotopy_groups3 f) _ + (is_exact_LES_of_homotopy_groups3 f (n, 2)) + (@is_contr_HG_fiber_of_is_connected A B (2 * n) (2 * n) f H !le.refl), + exact @(is_surjective_cancel_right (pmap.to_fun (π→*[2*n + 1] f)) tinverse) H3}, { exact @is_surjective_of_trivial _ (LES_of_homotopy_groups3 f) _ (is_exact_LES_of_homotopy_groups3 f (k, 5)) (@is_contr_HG_fiber_of_is_connected A B (2 * k + 1) (2 * k + 1) f H !le.refl)} end + /- joins -/ + definition join_empty_right [constructor] (A : Type) : join A empty ≃ A := begin fapply equiv.MK, @@ -153,8 +99,6 @@ namespace is_conn { exact empty.elim (pr2 v)}} end - /- joins -/ - definition join_functor [unfold 7] {A A' B B' : Type} (f : A → A') (g : B → B') : join A B → join A' B' := begin diff --git a/homotopy/chain_complex.hlean b/homotopy/chain_complex.hlean index 5e68931..e9fb8b1 100644 --- a/homotopy/chain_complex.hlean +++ b/homotopy/chain_complex.hlean @@ -495,7 +495,6 @@ namespace chain_complex pt_mul := one_mul, mul_pt := mul_one, mul_left_inv_pt := mul.left_inv⦄ - end -- the following theorems would also be true of the replace "is_contr" by "is_prop" diff --git a/homotopy/sec86.hlean b/homotopy/sec86.hlean index 56bd096..61f3e83 100644 --- a/homotopy/sec86.hlean +++ b/homotopy/sec86.hlean @@ -1,45 +1,259 @@ +-- TODO: in wedge connectivity and is_conn.elim, unbundle P +import homotopy.wedge types.pi .LES_applications --TODO: remove -import homotopy.wedge types.pi +open eq homotopy is_trunc pointed susp nat pi equiv is_equiv trunc fiber trunc_index -open eq homotopy is_trunc pointed susp nat pi equiv is_equiv trunc - -section freudenthal - -parameters {A : Type*} (n : ℕ) [is_conn n A] - ---set_option pp.notation false - -protected definition my_wedge_extension.ext : Π {A : Type*} {B : Type*} (n m : ℕ) [cA : is_conn n (carrier A)] [cB : is_conn m (carrier B)] -(P : carrier A → carrier B → (m+n)-Type) (f : Π (a : carrier A), trunctype.carrier (P a (Point B))) -(g : Π (b : carrier B), trunctype.carrier (P (Point A) b)), - f (Point A) = g (Point B) → (Π (a : carrier A) (b : carrier B), trunctype.carrier (P a b)) := -sorry - -definition code_fun (a : A) (q : north = north :> susp A) - : trunc (n * 2) (fiber (pmap.to_fun (loop_susp_unit A)) q) → trunc (n * 2) (fiber merid (q ⬝ merid a)) := -begin - intro x, induction x with x, - esimp at *, cases x with a' p, --- apply my_wedge_extension.ext n n, - exact sorry -end - -definition code (y : susp A) : north = y → Type := -susp.rec_on y - (λp, trunc (2*n) (fiber (loop_susp_unit A) p)) - (λq, trunc (2*n) (fiber merid q)) + definition iterated_loop_ptrunc_pequiv_con (n : ℕ₋₂) (k : ℕ) (A : Type*) + (p q : Ω[k](ptrunc (n+k) (Ω A))) : + iterated_loop_ptrunc_pequiv n k (Ω A) (loop_mul trunc_concat p q) = + trunc_functor2 (loop_mul concat) (iterated_loop_ptrunc_pequiv n k (Ω A) p) + (iterated_loop_ptrunc_pequiv n k (Ω A) q) := begin - intros, - apply arrow_pathover_constant_right, - intro q, rewrite [transport_eq_r], - apply ua, - exact sorry + revert n p q, induction k with k IH: intro n p q, + { reflexivity}, + { exact sorry} end -definition freudenthal_suspension : is_conn_map (n*2) (loop_susp_unit A) := -sorry + theorem elim_type_merid_inv {A : Type} (PN : Type) (PS : Type) (Pm : A → PN ≃ PS) + (a : A) : transport (susp.elim_type PN PS Pm) (merid a)⁻¹ = to_inv (Pm a) := + by rewrite [tr_eq_cast_ap_fn,↑susp.elim_type,ap_inv,elim_merid]; apply cast_ua_inv_fn + definition is_conn_trunc (A : Type) (n k : ℕ₋₂) [H : is_conn n A] + : is_conn n (trunc k A) := + begin + apply is_trunc_equiv_closed, apply trunc_trunc_equiv_trunc_trunc + end + section open sphere sphere.ops + definition psphere_succ [unfold_full] (n : ℕ) : S. (n + 1) = psusp (S. n) := idp + end -end freudenthal +namespace freudenthal section + + parameters {A : Type*} {n : ℕ} [is_conn n A] + + --porting from Agda + -- definition Q (x : susp A) : Type := + -- trunc (k) (north = x) + + definition up (a : A) : north = north :> susp A := -- up a = loop_susp_unit A a + merid a ⬝ (merid pt)⁻¹ + + definition code_merid : A → ptrunc (n + n) A → ptrunc (n + n) A := + begin + have is_conn n (ptrunc (n + n) A), from !is_conn_trunc, + refine wedge_extension.ext n n (λ x y, ttrunc (n + n) A) _ _ _, + { exact tr}, + { exact id}, + { reflexivity} + end + + definition code_merid_β_left (a : A) : code_merid a pt = tr a := + by apply wedge_extension.β_left + + definition code_merid_β_right (b : ptrunc (n + n) A) : code_merid pt b = b := + by apply wedge_extension.β_right + + definition code_merid_coh : code_merid_β_left pt = code_merid_β_right pt := + begin + symmetry, apply eq_of_inv_con_eq_idp, apply wedge_extension.coh + end + + definition is_equiv_code_merid (a : A) : is_equiv (code_merid a) := + begin + refine @is_conn.elim (n.-1) _ _ _ _ a, + { intro a, apply is_trunc_of_le, apply minus_one_le_succ}, + { esimp, exact homotopy_closed id (homotopy.symm (code_merid_β_right))} + end + + definition code_merid_equiv [constructor] (a : A) : trunc (n + n) A ≃ trunc (n + n) A := + equiv.mk _ (is_equiv_code_merid a) + + definition code_merid_inv_pt (x : trunc (n + n) A) : (code_merid_equiv pt)⁻¹ x = x := + begin + refine ap010 @(is_equiv.inv _) _ x ⬝ _, + { exact homotopy_closed id (homotopy.symm code_merid_β_right)}, + { apply is_conn.elim_β}, + { reflexivity} + end + + definition code [unfold 4] : susp A → Type := + susp.elim_type (trunc (n + n) A) (trunc (n + n) A) code_merid_equiv + + definition is_trunc_code (x : susp A) : is_trunc (n + n) (code x) := + begin + induction x with a: esimp, + { exact _}, + { exact _}, + { apply is_prop.elimo} + end + local attribute is_trunc_code [instance] + + definition decode_north [unfold 4] : code north → trunc (n + n) (north = north :> susp A) := + trunc_functor (n + n) up + + definition decode_north_pt : decode_north (tr pt) = tr idp := + ap tr !con.right_inv + + definition decode_south [unfold 4] : code south → trunc (n + n) (north = south :> susp A) := + trunc_functor (n + n) merid + + definition encode' {x : susp A} (p : north = x) : code x := + transport code p (tr pt) + + definition encode [unfold 5] {x : susp A} (p : trunc (n + n) (north = x)) : code x := + begin + induction p with p, + exact transport code p (tr pt) + end + + theorem encode_decode_north (c : code north) : encode (decode_north c) = c := + begin + have H : Πc, is_trunc (n + n) (encode (decode_north c) = c), from _, + esimp at *, + induction c with a, + rewrite [↑[encode, decode_north, up, code], con_tr, elim_type_merid, ▸*, + code_merid_β_left, elim_type_merid_inv, ▸*, code_merid_inv_pt] + end + + definition decode_coh_f (a : A) : tr (up pt) =[merid a] decode_south (code_merid a (tr pt)) := + begin + refine _ ⬝op ap decode_south (code_merid_β_left a)⁻¹, + apply trunc_pathover, + apply eq_pathover, + refine !ap_constant ⬝ph _ ⬝hp !ap_id⁻¹, + apply square_of_eq, + exact whisker_right !con.right_inv (merid a) + end + + definition decode_coh_g (a' : A) : tr (up a') =[merid pt] decode_south (code_merid pt (tr a')) := + begin + refine _ ⬝op ap decode_south (code_merid_β_right (tr a'))⁻¹, + apply trunc_pathover, + apply eq_pathover, + refine !ap_constant ⬝ph _ ⬝hp !ap_id⁻¹, + apply square_of_eq, refine !inv_con_cancel_right ⬝ !idp_con⁻¹ + end + + definition decode_coh_equality {A : Type} {a a' : A} (p : a = a') + : whisker_right (con.right_inv p) p = inv_con_cancel_right p p ⬝ (idp_con p)⁻¹ := + by induction p; reflexivity + + theorem decode_coh (a : A) : decode_north =[merid a] decode_south := + begin + apply arrow_pathover_left, intro c, esimp at *, + induction c with a', + rewrite [↑code, elim_type_merid, ▸*], + refine wedge_extension.ext n n _ _ _ _ a a', + { exact _}, + { exact decode_coh_f}, + { exact decode_coh_g}, + { clear a a', unfold [decode_coh_f, decode_coh_g], refine ap011 concato_eq _ _, + { apply ap (λp, trunc_pathover (eq_pathover (_ ⬝ph square_of_eq p ⬝hp _))), + apply decode_coh_equality}, + { apply ap (λp, ap decode_south p⁻¹), apply code_merid_coh}} + end + + definition decode [unfold 4] {x : susp A} (c : code x) : trunc (n + n) (north = x) := + begin + induction x with a, + { exact decode_north c}, + { exact decode_south c}, + { exact decode_coh a} + end + + theorem decode_encode {x : susp A} (p : trunc (n + n) (north = x)) : decode (encode p) = p := + begin + induction p with p, induction p, esimp, apply decode_north_pt + end + + parameters (A n) + definition equiv' : trunc (n + n) A ≃ trunc (n + n) (Ω (psusp A)) := + equiv.MK decode_north encode decode_encode encode_decode_north + + definition pequiv' : ptrunc (n + n) A ≃* ptrunc (n + n) (Ω (psusp A)) := + pequiv_of_equiv equiv' decode_north_pt + + -- can we get this? + -- definition freudenthal_suspension : is_conn_map (n+n) (loop_susp_unit A) := + -- begin + -- intro p, esimp at *, fapply is_contr.mk, + -- { note c := encode (tr p), esimp at *, induction c with a, }, + -- { exact sorry} + -- end + +-- {- Used to prove stability in iterated suspensions -} +-- module FreudenthalIso +-- {i} (n : ℕ₋₂) (k : ℕ) (t : k ≠ O) (kle : ⟨ k ⟩ ≤T S (n +2+ S n)) +-- (X : Ptd i) (cX : is-connected (S (S n)) (fst X)) where + +-- open FreudenthalEquiv n (⟨ k ⟩) kle (fst X) (snd X) cX public + +-- hom : Ω^-Group k t (⊙Trunc ⟨ k ⟩ X) Trunc-level +-- →ᴳ Ω^-Group k t (⊙Trunc ⟨ k ⟩ (⊙Ω (⊙Susp X))) Trunc-level +-- hom = record { +-- f = fst F; +-- pres-comp = ap^-conc^ k t (decodeN , decodeN-pt) } +-- where F = ap^ k (decodeN , decodeN-pt) + +-- iso : Ω^-Group k t (⊙Trunc ⟨ k ⟩ X) Trunc-level +-- ≃ᴳ Ω^-Group k t (⊙Trunc ⟨ k ⟩ (⊙Ω (⊙Susp X))) Trunc-level +-- iso = (hom , is-equiv-ap^ k (decodeN , decodeN-pt) (snd eq)) + +end end freudenthal + +open algebra +definition freudenthal_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n) + : ptrunc k A ≃* ptrunc k (Ω (psusp 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)) := +freudenthal_pequiv A H + +namespace sphere + open ops algebra pointed function + + definition stability_pequiv (k n : ℕ) (H : k + 2 ≤ 2 * n) : π*[k + 1] (S. (n+1)) ≃* π*[k] (S. n) := + begin + have H' : k ≤ 2 * pred n, + begin + rewrite [mul_pred_right], change pred (pred (k + 2)) ≤ pred (pred (2 * n)), + apply pred_le_pred, apply pred_le_pred, exact H + end, + have is_conn (of_nat (pred n)) (S. n), + begin + cases n with n, + { exfalso, exact not_succ_le_zero _ H}, + { esimp, apply is_conn_psphere} + end, + refine pequiv_of_eq (ap (ptrunc 0) (loop_space_succ_eq_in (S. (n+1)) k)) ⬝e* _, + rewrite psphere_succ, + refine !phomotopy_group_pequiv_loop_ptrunc ⬝e* _, + refine loopn_pequiv_loopn k (freudenthal_pequiv _ H')⁻¹ᵉ* ⬝e* _, + exact !phomotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*, + end +print phomotopy_group_pequiv_loop_ptrunc +print iterated_loop_ptrunc_pequiv + definition to_fun_stability_pequiv (k n : ℕ) (H : k + 2 ≤ 2 * n) --(p : π*[k + 1] (S. (n+1))) + : stability_pequiv k n H = _ ∘ _ ∘ cast (ap (ptrunc 0) (loop_space_succ_eq_in (S. (n+1)) k)) := + sorry + + -- definition stability (k n : ℕ) (H : k + 3 ≤ 2 * n) : πg[k+1 +1] (S. (n+1)) = πg[k+1] (S. n) := + -- begin + -- fapply Group_eq, + -- { refine equiv_of_pequiv (stability_pequiv _ _ _), rewrite succ_add, exact H}, + -- { intro g h, esimp, } + -- end + +end sphere + +/- + changes in book: + proof 8.6.15: also mention that we ignore multiplication + proof 8.4.4: respects points + proof 8.4.8: do k=0 separately +-/