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