From a76e4fce0893e692bcda5ab6f1bc75b93ae2bee9 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 3 Mar 2016 12:48:31 -0500 Subject: [PATCH 01/11] prove that the join of two spheres is a sphere --- homotopy/LES_applications.hlean | 96 +++++++++++++++++++++++++++++++-- 1 file changed, 93 insertions(+), 3 deletions(-) diff --git a/homotopy/LES_applications.hlean b/homotopy/LES_applications.hlean index d1e892f..739ae03 100644 --- a/homotopy/LES_applications.hlean +++ b/homotopy/LES_applications.hlean @@ -1,6 +1,6 @@ -import .LES_of_homotopy_groups homotopy.connectedness homotopy.homotopy_group +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 + 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) := @@ -66,9 +66,17 @@ namespace is_conn 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 - exact sorry + 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 @@ -130,4 +138,86 @@ namespace is_conn (@is_contr_HG_fiber_of_is_connected A B (2 * k + 1) (2 * k + 1) f H !le.refl)} end + definition join_empty_right [constructor] (A : Type) : join A empty ≃ A := + begin + fapply equiv.MK, + { intro x, induction x with a o v, + { exact a}, + { exact empty.elim o}, + { exact empty.elim (pr2 v)}}, + { exact pushout.inl}, + { intro a, reflexivity}, + { intro x, induction x with a o v, + { reflexivity}, + { exact empty.elim o}, + { 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 + intro x, induction x with a b v, + { exact inl (f a)}, + { exact inr (g b)}, + { exact glue (f (pr1 v), g (pr2 v))} + end + + theorem join_functor_glue {A A' B B' : Type} (f : A → A') (g : B → B') + (v : A × B) : ap (join_functor f g) (glue v) = glue (f (pr1 v), g (pr2 v)) := + !elim_glue + + definition natural_square2 {A B X : Type} {f : A → X} {g : B → X} (h : Πa b, f a = g b) + {a a' : A} {b b' : B} (p : a = a') (q : b = b') + : square (ap f p) (ap g q) (h a b) (h a' b') := + by induction p; induction q; exact hrfl + + definition join_equiv_join {A A' B B' : Type} (f : A ≃ A') (g : B ≃ B') : + join A B ≃ join A' B' := + begin + fapply equiv.MK, + { apply join_functor f g}, + { apply join_functor f⁻¹ g⁻¹}, + { intro x', induction x' with a' b' v', + { esimp, exact ap inl (right_inv f a')}, + { esimp, exact ap inr (right_inv g b')}, + { cases v' with a' b', apply eq_pathover, + rewrite [▸*, ap_id, ap_compose' (join_functor _ _), ▸*], + xrewrite [+join_functor_glue, ▸*], + exact natural_square2 jglue (right_inv f a') (right_inv g b')}}, + { intro x, induction x with a b v, + { esimp, exact ap inl (left_inv f a)}, + { esimp, exact ap inr (left_inv g b)}, + { cases v with a b, apply eq_pathover, + rewrite [▸*, ap_id, ap_compose' (join_functor _ _), ▸*], + xrewrite [+join_functor_glue, ▸*], + exact natural_square2 jglue (left_inv f a) (left_inv g b)}} + end + + section + open sphere sphere_index + + 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_join_sphere (n m : ℕ₋₁) : join (sphere n) (sphere m) ≃ sphere (n +1+ m) := + begin + revert n, induction m with m IH: intro n, + { apply join_empty_right}, + { rewrite [sphere_succ m], + refine join_equiv_join erfl !join.bool⁻¹ᵉ ⬝e _, + refine !join.assoc⁻¹ᵉ ⬝e _, + refine join_equiv_join !join.symm erfl ⬝e _, + refine join_equiv_join !join.bool erfl ⬝e _, + rewrite [-sphere_succ n], + refine !IH ⬝e _, + rewrite [add_plus_one_succ, succ_add_plus_one]} + end + end + end is_conn From 0483966328211d573c2d0b35f83725c13769fe54 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 3 Mar 2016 17:24:34 -0500 Subject: [PATCH 02/11] prove the Freudenthal Suspension Theorem --- homotopy/LES_applications.hlean | 74 +-------- homotopy/chain_complex.hlean | 1 - homotopy/sec86.hlean | 286 ++++++++++++++++++++++++++++---- 3 files changed, 259 insertions(+), 102 deletions(-) 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 +-/ From 97d7d0c108ebce6a3c8a35e8a593d117f3a8eb79 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sun, 6 Mar 2016 11:26:15 -0500 Subject: [PATCH 03/11] updates after changes in the HoTT library --- homotopy/LES_applications.hlean | 8 ++--- homotopy/sample.hlean | 32 +++++++++--------- homotopy/sec83.hlean | 44 ------------------------ homotopy/sec86.hlean | 59 +++++++++++++++++++++------------ 4 files changed, 58 insertions(+), 85 deletions(-) delete mode 100644 homotopy/sec83.hlean diff --git a/homotopy/LES_applications.hlean b/homotopy/LES_applications.hlean index e60225f..d4e1fdf 100644 --- a/homotopy/LES_applications.hlean +++ b/homotopy/LES_applications.hlean @@ -30,12 +30,12 @@ namespace is_conn local attribute is_equiv_tinverse [instance] theorem is_equiv_π_of_is_connected.{u} {A B : pType.{u}} (n k : ℕ) (f : A →* B) - [H : is_conn_map n f] (H2 : k ≤ n) : is_equiv (π→[k] f) := + [H : is_conn_fun n f] (H2 : k ≤ n) : is_equiv (π→[k] f) := begin induction k using rec_on_even_odd with k: cases k with k, { /- k = 0 -/ - change (is_equiv (trunc_functor 0 f)), apply is_equiv_trunc_functor_of_is_conn_map, - refine is_conn_map_of_le f (zero_le_of_nat n)}, + change (is_equiv (trunc_functor 0 f)), apply is_equiv_trunc_functor_of_is_conn_fun, + refine is_conn_fun_of_le f (zero_le_of_nat n)}, { /- k > 0 even -/ have H2' : 2 * k + 1 ≤ n, from le.trans !self_le_succ H2, exact @@ -67,7 +67,7 @@ namespace is_conn end theorem is_surjective_π_of_is_connected.{u} {A B : pType.{u}} (n : ℕ) (f : A →* B) - [H : is_conn_map n f] : is_surjective (π→[n + 1] f) := + [H : is_conn_fun n f] : is_surjective (π→[n + 1] f) := begin induction n using rec_on_even_odd with n, { have H3 : is_surjective (π→*[2*n + 1] f ∘* tinverse), from diff --git a/homotopy/sample.hlean b/homotopy/sample.hlean index 6eccc8c..b53cc0d 100644 --- a/homotopy/sample.hlean +++ b/homotopy/sample.hlean @@ -21,13 +21,13 @@ namespace homotopy assumption end - definition is_conn_map (n : trunc_index) {A B : Type} (f : A → B) : Type := + definition is_conn_fun (n : trunc_index) {A B : Type} (f : A → B) : Type := Πb : B, is_conn n (fiber f b) - namespace is_conn_map + namespace is_conn_fun section parameters {n : trunc_index} {A B : Type} {h : A → B} - (H : is_conn_map n h) (P : B → n -Type) + (H : is_conn_fun n h) (P : B → n -Type) private definition helper : (Πa : A, P (h a)) → Πb : B, trunc n (fiber h b) → P b := λt b, trunc.rec (λx, point_eq x ▸ t (point x)) @@ -67,7 +67,7 @@ namespace homotopy include sec -- the other half of Lemma 7.5.7 - definition intro : is_conn_map n h := + definition intro : is_conn_fun n h := begin intro b, apply is_contr.mk (@is_retraction.sect _ _ _ s (λa, tr (fiber.mk a idp)) b), @@ -79,22 +79,22 @@ namespace homotopy exact apd10 (@right_inverse _ _ _ s (λa, tr (fiber.mk a idp))) a end end - end is_conn_map + end is_conn_fun -- Connectedness is related to maps to and from the unit type, first to section parameters (n : trunc_index) (A : Type) definition is_conn_of_map_to_unit - : is_conn_map n (λx : A, unit.star) → is_conn n A := + : is_conn_fun n (λx : A, unit.star) → is_conn n A := begin - intro H, unfold is_conn_map at H, + intro H, unfold is_conn_fun at H, rewrite [-(ua (fiber.fiber_star_equiv A))], exact (H unit.star) end -- now maps from unit - definition is_conn_of_map_from_unit (a₀ : A) (H : is_conn_map n (const unit a₀)) + definition is_conn_of_map_from_unit (a₀ : A) (H : is_conn_fun n (const unit a₀)) : is_conn n .+1 A := is_contr.mk (tr a₀) begin @@ -103,8 +103,8 @@ namespace homotopy (@center _ (H a)) end - definition is_conn_map_from_unit (a₀ : A) [H : is_conn n .+1 A] - : is_conn_map n (const unit a₀) := + definition is_conn_fun_from_unit (a₀ : A) [H : is_conn n .+1 A] + : is_conn_fun n (const unit a₀) := begin intro a, apply is_conn_equiv_closed n (equiv.symm (fiber_const_equiv A a₀ a)), @@ -115,14 +115,14 @@ namespace homotopy -- Lemma 7.5.2 definition minus_one_conn_of_surjective {A B : Type} (f : A → B) - : is_surjective f → is_conn_map -1 f := + : is_surjective f → is_conn_fun -1 f := begin intro H, intro b, exact @is_contr_of_inhabited_prop (∥fiber f b∥) (is_trunc_trunc -1 (fiber f b)) (H b), end definition is_surjection_of_minus_one_conn {A B : Type} (f : A → B) - : is_conn_map -1 f → is_surjective f := + : is_conn_fun -1 f → is_surjective f := begin intro H, intro b, exact @center (∥fiber f b∥) (H b), @@ -141,7 +141,7 @@ namespace homotopy -- Lemma 7.5.4 definition retract_of_conn_is_conn [instance] (r : arrow_hom f g) [H : is_retraction r] - (n : trunc_index) [K : is_conn_map n f] : is_conn_map n g := + (n : trunc_index) [K : is_conn_fun n f] : is_conn_fun n g := begin intro b, unfold is_conn, apply is_contr_retract (trunc_functor n (retraction_on_fiber r b)), @@ -152,7 +152,7 @@ namespace homotopy -- Corollary 7.5.5 definition is_conn_homotopy (n : trunc_index) {A B : Type} {f g : A → B} - (p : f ~ g) (H : is_conn_map n f) : is_conn_map n g := + (p : f ~ g) (H : is_conn_fun n f) : is_conn_fun n g := @retract_of_conn_is_conn _ _ (arrow.arrow_hom_of_homotopy p) (arrow.is_retraction_arrow_hom_of_homotopy p) n H -- all types are -2-connected @@ -181,8 +181,8 @@ namespace homotopy { intros H, change ap (@tr n .+2 (susp A)) (merid a) = ap tr (merid a'), generalize a', - apply is_conn_map.elim - (is_conn_map_from_unit n A a) + apply is_conn_fun.elim + (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), diff --git a/homotopy/sec83.hlean b/homotopy/sec83.hlean deleted file mode 100644 index 8c5a634..0000000 --- a/homotopy/sec83.hlean +++ /dev/null @@ -1,44 +0,0 @@ --- Section 8.3 - -import types.trunc types.pointed homotopy.connectedness homotopy.sphere homotopy.circle algebra.group algebra.homotopy_group - -open eq is_trunc is_equiv nat equiv trunc function circle algebra pointed trunc_index homotopy - - --- Lemma 8.3.1 - -theorem trivial_homotopy_group_of_is_trunc (A : Type*) (n k : ℕ) [is_trunc n A] (H : n ≤ k) - : is_contr (πg[k+1] A) := -begin - apply is_trunc_trunc_of_is_trunc, - apply is_contr_loop_of_is_trunc, - apply @is_trunc_of_le A n _, - exact of_nat_le_of_nat H -end - --- Lemma 8.3.2 -theorem trivial_homotopy_group_of_is_conn (A : Type*) {k n : ℕ} (H : k ≤ n) [is_conn n A] - : is_contr (π[k] A) := -begin - have H2 : of_nat k ≤ of_nat n, from of_nat_le_of_nat H, - have H3 : is_contr (ptrunc k A), - begin - fapply is_contr_equiv_closed, - { apply trunc_trunc_equiv_left _ k n H2} - end, - have H4 : is_contr (Ω[k](ptrunc k A)), - from !is_trunc_loop_of_is_trunc, - apply is_trunc_equiv_closed_rev, - { apply equiv_of_pequiv (phomotopy_group_pequiv_loop_ptrunc k A)} -end - --- Corollary 8.3.3 -open sphere.ops sphere_index -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), - rewrite [-trunc_index.of_sphere_index_of_nat, -trunc_index.succ_sub_one], apply is_conn_sphere} -end diff --git a/homotopy/sec86.hlean b/homotopy/sec86.hlean index 61f3e83..a97edd9 100644 --- a/homotopy/sec86.hlean +++ b/homotopy/sec86.hlean @@ -4,15 +4,33 @@ import homotopy.wedge types.pi .LES_applications --TODO: remove open eq homotopy is_trunc pointed susp nat pi equiv is_equiv trunc fiber trunc_index + -- 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 + -- revert n p q, induction k with k IH: intro n p q, + -- { reflexivity}, + -- { exact sorry} + -- end + + -- example : ((@add.{0} trunc_index has_add_trunc_index n + -- (trunc_index.of_nat + -- (@add.{0} nat nat._trans_of_decidable_linear_ordered_semiring_17 nat.zero + -- (@one.{0} nat nat._trans_of_decidable_linear_ordered_semiring_21))))) = (0 : ℕ₋₂) := proof idp qed + 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) := + (p q : Ω[k + 1](ptrunc (n+k+1) A)) : + iterated_loop_ptrunc_pequiv n (k+1) A (p ⬝ q) = + trunc_concat (iterated_loop_ptrunc_pequiv n (k+1) A p) + (iterated_loop_ptrunc_pequiv n (k+1) A q) := begin - revert n p q, induction k with k IH: intro n p q, - { reflexivity}, - { exact sorry} + exact sorry + -- induction k with k IH, + -- { replace (nat.zero + 1) with (nat.succ nat.zero), esimp [iterated_loop_ptrunc_pequiv], + -- exact sorry}, + -- { exact sorry} end theorem elim_type_merid_inv {A : Type} (PN : Type) (PS : Type) (Pm : A → PN ≃ PS) @@ -62,8 +80,9 @@ namespace freudenthal section 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}, + have Πa, is_trunc n.-2.+1 (is_equiv (code_merid a)), + from λa, is_trunc_of_le _ !minus_one_le_succ, + refine is_conn.elim (n.-1) _ _ a, { esimp, exact homotopy_closed id (homotopy.symm (code_merid_β_right))} end @@ -121,8 +140,7 @@ namespace freudenthal section begin refine _ ⬝op ap decode_south (code_merid_β_left a)⁻¹, apply trunc_pathover, - apply eq_pathover, - refine !ap_constant ⬝ph _ ⬝hp !ap_id⁻¹, + apply eq_pathover_constant_left_id_right, apply square_of_eq, exact whisker_right !con.right_inv (merid a) end @@ -131,12 +149,11 @@ namespace freudenthal section 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 eq_pathover_constant_left_id_right, apply square_of_eq, refine !inv_con_cancel_right ⬝ !idp_con⁻¹ end - definition decode_coh_equality {A : Type} {a a' : A} (p : a = a') + definition decode_coh_lem {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 @@ -146,12 +163,11 @@ namespace freudenthal section 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}, + { refine ap (λp, trunc_pathover (eq_pathover_constant_left_id_right (square_of_eq p))) _, + apply decode_coh_lem}, { apply ap (λp, ap decode_south p⁻¹), apply code_merid_coh}} end @@ -176,7 +192,7 @@ namespace freudenthal section pequiv_of_equiv equiv' decode_north_pt -- can we get this? - -- definition freudenthal_suspension : is_conn_map (n+n) (loop_susp_unit A) := + -- definition freudenthal_suspension : is_conn_fun (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, }, @@ -236,11 +252,12 @@ namespace sphere 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 to_fun_stability_pequiv (k n : ℕ) (H : k + 3 ≤ 2 * n) --(p : π*[k + 1] (S. (n+1))) + -- : stability_pequiv (k+1) n H = _ ∘ _ ∘ cast (ap (ptrunc 0) (loop_space_succ_eq_in (S. (n+1)) (k+1))) := + -- sorry -- definition stability (k n : ℕ) (H : k + 3 ≤ 2 * n) : πg[k+1 +1] (S. (n+1)) = πg[k+1] (S. n) := -- begin From 00978587e5f601ab3b3337f6ff20eb3cc1bc97ec Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sun, 6 Mar 2016 13:23:30 -0500 Subject: [PATCH 04/11] update README --- README.md | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/README.md b/README.md index e1732ce..9e4c302 100644 --- a/README.md +++ b/README.md @@ -1,8 +1,8 @@ # Spectral Sequences -Formalization project of the CMU HoTT group towards formalizing the Serre spectral sequence. +Formalization project of the CMU HoTT group towards formalizing the Serre spectral sequence. -#### Participants +#### Participants Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, Egbert Rijke, Mike Shulman. ## Resources @@ -20,7 +20,7 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, - some basic theory: product, tensor, hom, projective, - categories of algebras, [abelian categories](http://ncatlab.org/nlab/show/abelian+category), - exact sequences, short and long -- [snake lemma](http://ncatlab.org/nlab/show/snake+lemma) +- [snake lemma](http://ncatlab.org/nlab/show/snake+lemma) - [5-lemma](http://ncatlab.org/nlab/show/five+lemma) - [chain complexes](http://ncatlab.org/nlab/show/chain+complex) and [homology](http://ncatlab.org/nlab/show/homology) - [exact couples](http://ncatlab.org/nlab/show/exact+couple), probably just of Z-graded objects, and derived exact couples @@ -28,8 +28,8 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, - [convergence of spectral sequences](http://ncatlab.org/nlab/show/spectral+sequence#ConvergenceOfSpectralSequences) ### Topology To Do: -- HoTT Book chapter 8 -- fiber and cofiber sequences (is this in the library already?) +- HoTT Book sections 8.7, 8.8. +- cofiber sequences - [prespectra](http://ncatlab.org/nlab/show/spectrum+object) and [spectra](http://ncatlab.org/nlab/show/spectrum), suspension - [spectrification](http://ncatlab.org/nlab/show/higher+inductive+type#spectrification) - [parametrized spectra](http://ncatlab.org/nlab/show/parametrized+spectrum), parametrized smash and hom between types and spectra @@ -40,6 +40,7 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, - exact couple of a tower of spectra ### Already Done: -- pointed types -- definition of algebraic structures such as groups, rings, fields, -- some algebra: quotient, product, free. +- Most things in the HoTT Book up to Section 8.6 (see [this file](https://github.com/leanprover/lean/blob/master/hott/book.md)) +- pointed types, maps, homotopies and equivalences +- definition of algebraic structures such as groups, rings, fields +- some algebra: quotient, product, free groups. \ No newline at end of file From 9ca4a3fbb19e8a5df20043dc994e78afd2e0d8a7 Mon Sep 17 00:00:00 2001 From: Ulrik Buchholtz Date: Thu, 10 Mar 2016 19:50:49 -0500 Subject: [PATCH 05/11] start spherical fibrations (NB post #1021 lean) --- homotopy/spherical_fibrations.hlean | 110 ++++++++++++++++++++++++++++ 1 file changed, 110 insertions(+) create mode 100644 homotopy/spherical_fibrations.hlean diff --git a/homotopy/spherical_fibrations.hlean b/homotopy/spherical_fibrations.hlean new file mode 100644 index 0000000..354317f --- /dev/null +++ b/homotopy/spherical_fibrations.hlean @@ -0,0 +1,110 @@ +import homotopy.join homotopy.smash + +open eq equiv trunc function bool join sphere sphere_index sphere.ops prod +open pointed sigma smash + +namespace spherical_fibrations + + /- classifying type of spherical fibrations -/ + definition BG (n : ℕ) : Type₁ := + Σ(X : Type₀), ∥ X ≃ S n..-1 ∥ + + definition pointed_BG [instance] [constructor] (n : ℕ) : pointed (BG n) := + pointed.mk ⟨ S n..-1 , tr erfl ⟩ + + definition pBG [constructor] (n : ℕ) : Type* := pointed.mk' (BG n) + + definition BG_succ (n : ℕ) : BG n → BG (n+1) := + begin + intro X, cases X with X p, + apply sigma.mk (susp X), induction p with f, apply tr, + apply susp.equiv f + end + + /- classifying type of pointed spherical fibrations -/ + definition BF (n : ℕ) : Type₁ := + Σ(X : Type*), ∥ X ≃* S. n ∥ + + definition pointed_BF [instance] [constructor] (n : ℕ) : pointed (BF n) := + pointed.mk ⟨ S. n , tr pequiv.rfl ⟩ + + definition pBF [constructor] (n : ℕ) : Type* := pointed.mk' (BF n) + + definition BF_succ (n : ℕ) : BF n → BF (n+1) := + begin + intro X, cases X with X p, + apply sigma.mk (psusp X), induction p with f, apply tr, + apply susp.psusp_equiv f + end + + definition BF_of_BG {n : ℕ} : BG n → BF n := + begin + intro X, cases X with X p, + apply sigma.mk (pointed.MK (susp X) susp.north), + induction p with f, apply tr, + apply pequiv_of_equiv (susp.equiv f), + reflexivity + end + + definition BG_of_BF {n : ℕ} : BF n → BG (n + 1) := + begin + intro X, cases X with X hX, + apply sigma.mk (carrier X), induction hX with fX, + apply tr, exact fX + end + + definition BG_mul {n m : ℕ} (X : BG n) (Y : BG m) : BG (n + m) := + begin + cases X with X pX, cases Y with Y pY, + apply sigma.mk (join X Y), + induction pX with fX, induction pY with fY, + apply tr, rewrite add_sub_one, + exact (join.equiv_closed fX fY) ⬝e (join.spheres n..-1 m..-1) + end + + definition BF_mul {n m : ℕ} (X : BF n) (Y : BF m) : BF (n + m) := + begin + cases X with X hX, cases Y with Y hY, + apply sigma.mk (psmash X Y), + induction hX with fX, induction hY with fY, apply tr, + exact sorry -- needs smash.spheres : psmash (S. n) (S. m) ≃ S. (n + m) + end + + definition BF_of_BG_mul (n m : ℕ) (X : BG n) (Y : BG m) + : BF_of_BG (BG_mul X Y) = BF_mul (BF_of_BG X) (BF_of_BG Y) := + sorry + + -- Thom spaces + namespace thom + variables {X : Type} {n : ℕ} (α : X → BF n) + + -- the canonical section of an F-object + protected definition sec (x : X) : carrier (sigma.pr1 (α x)) := + Point _ + + open pushout sigma + + definition thom_space : Type := + pushout (λx : X, ⟨x , thom.sec α x⟩) (const X unit.star) + end thom + +/- + Things to do: + - Orientability and orientations + * Thom class u ∈ ~Hⁿ(Tξ) + * eventually prove Thom-Isomorphism (Rudyak IV.5.7) + - define BG∞ and BF∞ as colimits of BG n and BF n + - Ω(BF n) = ΩⁿSⁿ₁ + ΩⁿSⁿ₋₁ (self-maps of degree ±1) + - succ_BF n is (n - 2) connected (from Freudenthal) + - pfiber (BG_of_BF n) ≃ S. n + - π₁(BF n)=π₁(BG n)=ℤ/2ℤ + - double covers BSG and BSF + - O : BF n → BG 1 = Σ(A : Type), ∥ A = bool ∥ + - BSG n = sigma O + - π₁(BSG n)=π₁(BSF n)=O + - BSO(n), BSTop(n) + - find BF' n : Type₀ with BF' n ≃ BF n etc. + - canonical bundle γₙ : ℝP(n) → ℝP∞=BO(1) → Type₀ + prove T(γₙ) = ℝP(n+1) +-/ +end spherical_fibrations From 652ca1da842128eece977ce1f7181a211575e866 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 10 Mar 2016 22:51:32 -0500 Subject: [PATCH 06/11] working on the join theorem --- homotopy/join_theorem.hlean | 83 +++++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) create mode 100644 homotopy/join_theorem.hlean diff --git a/homotopy/join_theorem.hlean b/homotopy/join_theorem.hlean new file mode 100644 index 0000000..fba4afc --- /dev/null +++ b/homotopy/join_theorem.hlean @@ -0,0 +1,83 @@ +/-- Authors: Clive, Egbert --/ + +import homotopy.connectedness homotopy.join + +open eq sigma pi function join homotopy is_trunc equiv is_equiv + +namespace retraction + variables {A B C : Type} (r2 : B → C) (r1 : A → B) + + + definition is_retraction_compose + [Hr2 : is_retraction r2] [Hr1 : is_retraction r1] : + is_retraction (r2 ∘ r1) := + begin + cases Hr2 with s2 s2_is_right_inverse, + cases Hr1 with s1 s1_is_right_inverse, + fapply is_retraction.mk, + { exact s1 ∘ s2}, + { intro b, esimp, + calc + r2 (r1 (s1 (s2 (b)))) = r2 (s2 (b)) : ap r2 (s1_is_right_inverse (s2 b)) + ... = b : s2_is_right_inverse b + + }, /-- QED --/ + end + + definition is_retraction_compose_equiv_left [Hr2 : is_equiv r2] [Hr1 : is_retraction r1] : is_retraction (r2 ∘ r1) := + begin + apply is_retraction_compose, + end + + definition is_retraction_compose_equiv_right [Hr2 : is_retraction r2] [Hr1 : is_equiv r1] : is_retraction (r2 ∘ r1) := + begin + apply is_retraction_compose, + end + +end retraction + +namespace is_conn +section + + open retraction + + universe variable u + parameters (n : ℕ₋₂) {A : Type.{u}} + parameter sec : ΠV : trunctype.{u} n, + is_retraction (const A : V → (A → V)) + + include sec + + protected definition intro : is_conn n A := + begin + apply is_conn_of_map_to_unit, + apply is_conn_fun.intro, + intro P, + refine is_retraction_compose_equiv_right (const A) (pi_unit_left P), + end +end +end is_conn + +section Join_Theorem + +variables (X Y : Type) + (m n : ℕ₋₂) + [HXm : is_conn m X] + [HYn : is_conn n Y] + +include HXm HYn + +theorem is_conn_join : is_conn (m +2+ n) (join X Y) := +begin + apply is_conn.intro, + intro V, + apply is_retraction_of_is_equiv, + apply is_equiv_of_is_contr_fun, + intro f, + refine is_contr_equiv_closed _, + {exact unit}, + symmetry, + exact sorry +end + +end Join_Theorem From 5a23744094015a34eb00f9b0ad43c5f84b3a312f Mon Sep 17 00:00:00 2001 From: Ulrik Buchholtz Date: Mon, 21 Mar 2016 14:44:57 -0400 Subject: [PATCH 07/11] update README to reflect recent discussion --- README.md | 19 ++++++++++- homotopy/spherical_fibrations.hlean | 52 +++++++++++++++++++++++++++-- 2 files changed, 68 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 9e4c302..d796019 100644 --- a/README.md +++ b/README.md @@ -29,18 +29,35 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, ### Topology To Do: - HoTT Book sections 8.7, 8.8. +- fiber sequence + + already have the LES + + need shift isomorphism + + Hom'ing into a fiber sequence gives another fiber sequence. - cofiber sequences + + Hom'ing out gives a fiber sequence: if `A → B → coker f` cofiber + sequences, then `X^A → X^B → X^(coker f)` is a fiber sequence. - [prespectra](http://ncatlab.org/nlab/show/spectrum+object) and [spectra](http://ncatlab.org/nlab/show/spectrum), suspension + + try indexing on arbitrary successor structure + + think about equivariant spectra indexed by representations of `G` - [spectrification](http://ncatlab.org/nlab/show/higher+inductive+type#spectrification) + + adjoint to forgetful + + as sequential colimit, prove induction principle (if useful) + + connective spectrum: `is_conn n.-2 Eₙ` - [parametrized spectra](http://ncatlab.org/nlab/show/parametrized+spectrum), parametrized smash and hom between types and spectra - fiber and cofiber sequences of spectra, stability + + limits are levelwise + + colimits need to be spectrified - long exact sequences from (co)fiber sequences of spectra + + indexed on ℤ, need to splice together LES's - [Eilenberg-MacLane spaces](http://ncatlab.org/nlab/show/Eilenberg-Mac+Lane+space) and spectra - Postnikov towers of spectra + + basic definition already there + + fibers of Postnikov sequence unstably and stably - exact couple of a tower of spectra + + need to splice together LES's ### Already Done: - Most things in the HoTT Book up to Section 8.6 (see [this file](https://github.com/leanprover/lean/blob/master/hott/book.md)) - pointed types, maps, homotopies and equivalences - definition of algebraic structures such as groups, rings, fields -- some algebra: quotient, product, free groups. \ No newline at end of file +- some algebra: quotient, product, free groups. diff --git a/homotopy/spherical_fibrations.hlean b/homotopy/spherical_fibrations.hlean index 354317f..506e3c0 100644 --- a/homotopy/spherical_fibrations.hlean +++ b/homotopy/spherical_fibrations.hlean @@ -14,6 +14,28 @@ namespace spherical_fibrations definition pBG [constructor] (n : ℕ) : Type* := pointed.mk' (BG n) + definition G (n : ℕ) : Type₁ := + pt = pt :> BG n + + definition G_char (n : ℕ) : G n ≃ (S n..-1 ≃ S n..-1) := + sorry + + definition mirror (n : ℕ) : S n..-1 → G n := + begin + intro v, apply to_inv (G_char n), + exact sorry + end + +/- + Can we give a fibration P : S n → Type, P base = F n = Ω(BF n) = (S. n ≃* S. n) + and total space sigma P ≃ G (n+1) = Ω(BG (n+1)) = (S n.+1 ≃ S .n+1) + + Yes, let eval : BG (n+1) → S n be the evaluation map +-/ + + definition S_of_BG (n : ℕ) : Ω(pBG (n+1)) → S n := + λ f, f..1 ▸ base + definition BG_succ (n : ℕ) : BG n → BG (n+1) := begin intro X, cases X with X p, @@ -96,15 +118,41 @@ namespace spherical_fibrations - define BG∞ and BF∞ as colimits of BG n and BF n - Ω(BF n) = ΩⁿSⁿ₁ + ΩⁿSⁿ₋₁ (self-maps of degree ±1) - succ_BF n is (n - 2) connected (from Freudenthal) - - pfiber (BG_of_BF n) ≃ S. n + - pfiber (BG_of_BF n) ≃* S. n - π₁(BF n)=π₁(BG n)=ℤ/2ℤ - double covers BSG and BSF - O : BF n → BG 1 = Σ(A : Type), ∥ A = bool ∥ - BSG n = sigma O - π₁(BSG n)=π₁(BSF n)=O - - BSO(n), BSTop(n) + - BSO(n), - find BF' n : Type₀ with BF' n ≃ BF n etc. - canonical bundle γₙ : ℝP(n) → ℝP∞=BO(1) → Type₀ prove T(γₙ) = ℝP(n+1) + - BG∞ = BF∞ (in fact = BGL₁(S), the group of units of the sphere spectrum) + - clutching construction: + any f : S n → SG(n) gives S n.+1 → BSG(n) (mut.mut. for O(n),SO(n),etc.) + - all bundles on S 3 are trivial, incl. tangent bundle + - Adams' result on vector fields on spheres: + there are maximally ρ(n)-1 indep.sections of the tangent bundle of S (n-1) + where ρ(n) is the n'th Radon-Hurwitz number.→ -/ + +-- tangent bundle on S 2: + + namespace two_sphere + + definition tau : S 2 → BG 2 := + begin + intro v, induction v with x, do 2 exact pt, + fapply sigma_eq, + { apply ua, fapply equiv.MK, + { }, + { }, + { }, + { } }, + { } + end + + end two_sphere + end spherical_fibrations From 680788383080c9e7fe5fe77e92465db029f7ec61 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 24 Mar 2016 13:41:03 -0400 Subject: [PATCH 08/11] port module from the standard library --- module.hlean | 73 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 73 insertions(+) create mode 100644 module.hlean diff --git a/module.hlean b/module.hlean new file mode 100644 index 0000000..2279517 --- /dev/null +++ b/module.hlean @@ -0,0 +1,73 @@ +/- +Copyright (c) 2015 Nathaniel Thomas. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Nathaniel Thomas, Jeremy Avigad + +Modules prod vector spaces over a ring. + +(We use "left_module," which is more precise, because "module" is a keyword.) +-/ +import algebra.field +open algebra + +structure has_scalar [class] (F V : Type) := +(smul : F → V → V) + +infixl ` • `:73 := has_scalar.smul + +/- modules over a ring -/ + +structure left_module [class] (R M : Type) [ringR : ring R] + extends has_scalar R M, add_comm_group M := +(smul_left_distrib : Π (r : R) (x y : M), smul r (add x y) = (add (smul r x) (smul r y))) +(smul_right_distrib : Π (r s : R) (x : M), smul (ring.add r s) x = (add (smul r x) (smul s x))) +(mul_smul : Π r s x, smul (mul r s) x = smul r (smul s x)) +(one_smul : Π x, smul one x = x) + +section left_module + variables {R M : Type} + variable [ringR : ring R] + variable [moduleRM : left_module R M] + include ringR moduleRM + + -- Note: the anonymous include does not work in the propositions below. + + proposition smul_left_distrib (a : R) (u v : M) : a • (u + v) = a • u + a • v := + !left_module.smul_left_distrib + + proposition smul_right_distrib (a b : R) (u : M) : (a + b) • u = a • u + b • u := + !left_module.smul_right_distrib + + proposition mul_smul (a : R) (b : R) (u : M) : (a * b) • u = a • (b • u) := + !left_module.mul_smul + + proposition one_smul (u : M) : (1 : R) • u = u := !left_module.one_smul + + proposition zero_smul (u : M) : (0 : R) • u = 0 := + have (0 : R) • u + 0 • u = 0 • u + 0, by rewrite [-smul_right_distrib, *add_zero], + !add.left_cancel this + + proposition smul_zero (a : R) : a • (0 : M) = 0 := + have a • (0:M) + a • 0 = a • 0 + 0, by rewrite [-smul_left_distrib, *add_zero], + !add.left_cancel this + + proposition neg_smul (a : R) (u : M) : (-a) • u = - (a • u) := + eq_neg_of_add_eq_zero (by rewrite [-smul_right_distrib, add.left_inv, zero_smul]) + + proposition neg_one_smul (u : M) : -(1 : R) • u = -u := + by rewrite [neg_smul, one_smul] + + proposition smul_neg (a : R) (u : M) : a • (-u) = -(a • u) := + by rewrite [-neg_one_smul, -mul_smul, mul_neg_one_eq_neg, neg_smul] + + proposition smul_sub_left_distrib (a : R) (u v : M) : a • (u - v) = a • u - a • v := + by rewrite [sub_eq_add_neg, smul_left_distrib, smul_neg] + + proposition sub_smul_right_distrib (a b : R) (v : M) : (a - b) • v = a • v - b • v := + by rewrite [sub_eq_add_neg, smul_right_distrib, neg_smul] +end left_module + +/- vector spaces -/ + +structure vector_space [class] (F V : Type) [fieldF : field F] + extends left_module F V From 0b1fbbe3e169f9fcc2dba96824dddd8fb3ab2c21 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 24 Mar 2016 14:19:06 -0400 Subject: [PATCH 09/11] initiating algebra folder --- module.hlean => algebra/module.hlean | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename module.hlean => algebra/module.hlean (100%) diff --git a/module.hlean b/algebra/module.hlean similarity index 100% rename from module.hlean rename to algebra/module.hlean From 960e7075bd0d288ba82858a05f28e4d76f0910a0 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 24 Mar 2016 14:24:47 -0400 Subject: [PATCH 10/11] initiating graded.hlean --- algebra/graded.hlean | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 algebra/graded.hlean diff --git a/algebra/graded.hlean b/algebra/graded.hlean new file mode 100644 index 0000000..36f84cf --- /dev/null +++ b/algebra/graded.hlean @@ -0,0 +1,7 @@ +/- +Copyright (c) 2016 Egbert Rijke. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Egbert Rijke + +Graded modules and rings. +-/ From 288e0d71b230cc87de7048425ab205dd7aedc0bb Mon Sep 17 00:00:00 2001 From: Ulrik Buchholtz Date: Thu, 24 Mar 2016 16:14:44 -0400 Subject: [PATCH 11/11] make everything compile on lean post 6f74f6522... --- homotopy/LES_applications.hlean | 68 ++++----------------------- homotopy/LES_of_homotopy_groups.hlean | 7 +-- homotopy/chain_complex.hlean | 4 +- homotopy/join_theorem.hlean | 2 +- homotopy/sec86.hlean | 6 +-- homotopy/spherical_fibrations.hlean | 8 +--- 6 files changed, 21 insertions(+), 74 deletions(-) diff --git a/homotopy/LES_applications.hlean b/homotopy/LES_applications.hlean index d4e1fdf..99b628d 100644 --- a/homotopy/LES_applications.hlean +++ b/homotopy/LES_applications.hlean @@ -1,5 +1,5 @@ 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 +open eq is_trunc pointed is_conn is_equiv fiber equiv trunc nat chain_complex prod fin algebra group trunc_index function join pushout namespace nat @@ -87,58 +87,23 @@ namespace is_conn definition join_empty_right [constructor] (A : Type) : join A empty ≃ A := begin fapply equiv.MK, - { intro x, induction x with a o v, - { exact a}, - { exact empty.elim o}, - { exact empty.elim (pr2 v)}}, - { exact pushout.inl}, + { intro x, induction x with a o a o, + { exact a }, + { exact empty.elim o }, + { exact empty.elim o } }, + { exact pushout.inl }, { intro a, reflexivity}, - { intro x, induction x with a o v, - { reflexivity}, - { exact empty.elim o}, - { exact empty.elim (pr2 v)}} + { intro x, induction x with a o a o, + { reflexivity }, + { exact empty.elim o }, + { exact empty.elim o } } end - definition join_functor [unfold 7] {A A' B B' : Type} (f : A → A') (g : B → B') : - join A B → join A' B' := - begin - intro x, induction x with a b v, - { exact inl (f a)}, - { exact inr (g b)}, - { exact glue (f (pr1 v), g (pr2 v))} - end - - theorem join_functor_glue {A A' B B' : Type} (f : A → A') (g : B → B') - (v : A × B) : ap (join_functor f g) (glue v) = glue (f (pr1 v), g (pr2 v)) := - !elim_glue - definition natural_square2 {A B X : Type} {f : A → X} {g : B → X} (h : Πa b, f a = g b) {a a' : A} {b b' : B} (p : a = a') (q : b = b') : square (ap f p) (ap g q) (h a b) (h a' b') := by induction p; induction q; exact hrfl - definition join_equiv_join {A A' B B' : Type} (f : A ≃ A') (g : B ≃ B') : - join A B ≃ join A' B' := - begin - fapply equiv.MK, - { apply join_functor f g}, - { apply join_functor f⁻¹ g⁻¹}, - { intro x', induction x' with a' b' v', - { esimp, exact ap inl (right_inv f a')}, - { esimp, exact ap inr (right_inv g b')}, - { cases v' with a' b', apply eq_pathover, - rewrite [▸*, ap_id, ap_compose' (join_functor _ _), ▸*], - xrewrite [+join_functor_glue, ▸*], - exact natural_square2 jglue (right_inv f a') (right_inv g b')}}, - { intro x, induction x with a b v, - { esimp, exact ap inl (left_inv f a)}, - { esimp, exact ap inr (left_inv g b)}, - { cases v with a b, apply eq_pathover, - rewrite [▸*, ap_id, ap_compose' (join_functor _ _), ▸*], - xrewrite [+join_functor_glue, ▸*], - exact natural_square2 jglue (left_inv f a) (left_inv g b)}} - end - section open sphere sphere_index @@ -149,19 +114,6 @@ namespace is_conn 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_join_sphere (n m : ℕ₋₁) : join (sphere n) (sphere m) ≃ sphere (n +1+ m) := - begin - revert n, induction m with m IH: intro n, - { apply join_empty_right}, - { rewrite [sphere_succ m], - refine join_equiv_join erfl !join.bool⁻¹ᵉ ⬝e _, - refine !join.assoc⁻¹ᵉ ⬝e _, - refine join_equiv_join !join.symm erfl ⬝e _, - refine join_equiv_join !join.bool erfl ⬝e _, - rewrite [-sphere_succ n], - refine !IH ⬝e _, - rewrite [add_plus_one_succ, succ_add_plus_one]} - end end end is_conn diff --git a/homotopy/LES_of_homotopy_groups.hlean b/homotopy/LES_of_homotopy_groups.hlean index 0c34b19..b84dd10 100644 --- a/homotopy/LES_of_homotopy_groups.hlean +++ b/homotopy/LES_of_homotopy_groups.hlean @@ -208,9 +208,10 @@ namespace chain_complex theorem fiber_sequence_fun_eq : Π(x : fiber_sequence_carrier f (n + 4)), fiber_sequence_carrier_pequiv f n (fiber_sequence_fun f (n + 3) x) = ap1 (fiber_sequence_fun f n) (fiber_sequence_carrier_pequiv f (n + 1) x)⁻¹ := - homotopy_of_inv_homotopy - (pequiv.to_equiv (fiber_sequence_carrier_pequiv f (n + 1))) - (fiber_sequence_fun_eq_helper f n) + begin + apply homotopy_of_inv_homotopy_pre (fiber_sequence_carrier_pequiv f (n + 1)), + apply fiber_sequence_fun_eq_helper f n + end theorem fiber_sequence_fun_phomotopy : fiber_sequence_carrier_pequiv f n ∘* diff --git a/homotopy/chain_complex.hlean b/homotopy/chain_complex.hlean index e9fb8b1..db104b1 100644 --- a/homotopy/chain_complex.hlean +++ b/homotopy/chain_complex.hlean @@ -209,8 +209,8 @@ namespace chain_complex have H2 : tcc_to_fn X (f m) ((equiv_of_eq (ap (λx, X x) (c m)))⁻¹ᵉ (e⁻¹ y)) = pt, begin refine _ ⬝ ap e⁻¹ᵉ* q ⬝ (respect_pt (e⁻¹ᵉ*)), apply eq_inv_of_eq, clear q, revert y, - refine inv_homotopy_of_homotopy (pequiv.to_equiv e) _, - apply inv_homotopy_of_homotopy, apply p + apply inv_homotopy_of_homotopy_pre e, + apply inv_homotopy_of_homotopy_pre, apply p end, induction (H _ H2) with x r, refine fiber.mk (e (cast (ap (λx, X x) (c (S m))) (cast (ap (λx, X (S x)) (c m)) x))) _, diff --git a/homotopy/join_theorem.hlean b/homotopy/join_theorem.hlean index fba4afc..6185190 100644 --- a/homotopy/join_theorem.hlean +++ b/homotopy/join_theorem.hlean @@ -2,7 +2,7 @@ import homotopy.connectedness homotopy.join -open eq sigma pi function join homotopy is_trunc equiv is_equiv +open eq sigma pi function join is_conn is_trunc equiv is_equiv namespace retraction variables {A B C : Type} (r2 : B → C) (r1 : A → B) diff --git a/homotopy/sec86.hlean b/homotopy/sec86.hlean index a97edd9..117ff81 100644 --- a/homotopy/sec86.hlean +++ b/homotopy/sec86.hlean @@ -2,7 +2,7 @@ import homotopy.wedge types.pi .LES_applications --TODO: remove -open eq homotopy is_trunc pointed susp nat pi equiv is_equiv trunc fiber trunc_index +open eq is_conn is_trunc pointed susp nat pi equiv is_equiv trunc fiber trunc_index -- definition iterated_loop_ptrunc_pequiv_con' (n : ℕ₋₂) (k : ℕ) (A : Type*) -- (p q : Ω[k](ptrunc (n+k) (Ω A))) : @@ -253,8 +253,8 @@ namespace sphere exact !phomotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*, end -print phomotopy_group_pequiv_loop_ptrunc -print iterated_loop_ptrunc_pequiv +--print phomotopy_group_pequiv_loop_ptrunc +--print iterated_loop_ptrunc_pequiv -- definition to_fun_stability_pequiv (k n : ℕ) (H : k + 3 ≤ 2 * n) --(p : π*[k + 1] (S. (n+1))) -- : stability_pequiv (k+1) n H = _ ∘ _ ∘ cast (ap (ptrunc 0) (loop_space_succ_eq_in (S. (n+1)) (k+1))) := -- sorry diff --git a/homotopy/spherical_fibrations.hlean b/homotopy/spherical_fibrations.hlean index 506e3c0..2dab9b5 100644 --- a/homotopy/spherical_fibrations.hlean +++ b/homotopy/spherical_fibrations.hlean @@ -144,13 +144,7 @@ namespace spherical_fibrations definition tau : S 2 → BG 2 := begin intro v, induction v with x, do 2 exact pt, - fapply sigma_eq, - { apply ua, fapply equiv.MK, - { }, - { }, - { }, - { } }, - { } + exact sorry end end two_sphere