diff --git a/algebra/serre.hlean b/algebra/serre.hlean index a81ce06..fceeb39 100644 --- a/algebra/serre.hlean +++ b/algebra/serre.hlean @@ -6,6 +6,10 @@ import .module_exact_couple namespace left_module + /- The Atiyah-Hirzebruch spectral sequence (with local coefficents) -/ + + /- The Serre Spectral Sequence -/ + end left_module diff --git a/choice.hlean b/choice.hlean index c720f33..79c6f9f 100644 --- a/choice.hlean +++ b/choice.hlean @@ -54,7 +54,7 @@ begin { intro f, induction f, apply eq_of_homotopy, intro x, esimp, induction x with a b: reflexivity } end -/- currently we prove it using univalence -/ +/- currently we prove it using univalence, which means we cannot apply it to lift. TODO: change -/ definition has_choice_equiv_closed.{u} (n : ℕ₋₂) {A B : Type.{u}} (f : A ≃ B) (hA : has_choice n B) : has_choice n A := begin diff --git a/homotopy/3x3.hlean b/homotopy/3x3.hlean index d30d718..646421b 100644 --- a/homotopy/3x3.hlean +++ b/homotopy/3x3.hlean @@ -1,4 +1,4 @@ - +-- WIP import ..move_to_lib open function eq diff --git a/homotopy/fwedge.hlean b/homotopy/fwedge.hlean index 9409062..a6ecdb4 100644 --- a/homotopy/fwedge.hlean +++ b/homotopy/fwedge.hlean @@ -1,7 +1,7 @@ /- Copyright (c) 2016 Jakob von Raumer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jakob von Raumer, Ulrik Buchholtz +Authors: Floris van Doorn The Wedge Sum of a family of Pointed Types -/ diff --git a/homotopy/susp.hlean b/homotopy/susp.hlean index a481e46..f8c7786 100644 --- a/homotopy/susp.hlean +++ b/homotopy/susp.hlean @@ -1,82 +1,9 @@ import ..pointed open susp eq pointed function is_equiv - variables {X X' Y Y' Z : Type*} - --- move - definition pap1 [constructor] (X Y : Type*) : ppmap X Y →* ppmap (Ω X) (Ω Y) := - pmap.mk ap1 (eq_of_phomotopy !ap1_pconst) - - definition ap1_gen_const {A B : Type} {a₁ a₂ : A} (b : B) (p : a₁ = a₂) : - ap1_gen (const A b) idp idp p = idp := - ap1_gen_idp_left (const A b) p ⬝ ap_constant p b - - definition ap1_gen_compose_const_left - {A B C : Type} (c : C) (f : A → B) {a₁ a₂ : A} (p : a₁ = a₂) : - ap1_gen_compose (const B c) f idp idp idp idp p ⬝ - ap1_gen_const c (ap1_gen f idp idp p) = - ap1_gen_const c p := - begin induction p, reflexivity end - - definition ap1_gen_compose_const_right - {A B C : Type} (g : B → C) (b : B) {a₁ a₂ : A} (p : a₁ = a₂) : - ap1_gen_compose g (const A b) idp idp idp idp p ⬝ - ap (ap1_gen g idp idp) (ap1_gen_const b p) = - ap1_gen_const (g b) p := - begin induction p, reflexivity end - - definition ap1_pcompose_pconst_left {A B C : Type*} (f : A →* B) : - phsquare (ap1_pcompose (pconst B C) f) - (ap1_pconst A C) - (ap1_phomotopy (pconst_pcompose f)) - (pwhisker_right (Ω→ f) (ap1_pconst B C) ⬝* pconst_pcompose (Ω→ f)) := - begin - induction A with A a₀, induction B with B b₀, induction C with C c₀, induction f with f f₀, - esimp at *, induction f₀, - refine idp ◾** !trans_refl ⬝ _ ⬝ !refl_trans⁻¹ ⬝ !ap1_phomotopy_refl⁻¹ ◾** idp, - fapply phomotopy_eq, - { exact ap1_gen_compose_const_left c₀ f }, - { reflexivity } - end - - definition ap1_pcompose_pconst_right {A B C : Type*} (g : B →* C) : - phsquare (ap1_pcompose g (pconst A B)) - (ap1_pconst A C) - (ap1_phomotopy (pcompose_pconst g)) - (pwhisker_left (Ω→ g) (ap1_pconst A B) ⬝* pcompose_pconst (Ω→ g)) := - begin - induction A with A a₀, induction B with B b₀, induction C with C c₀, induction g with g g₀, - esimp at *, induction g₀, - refine idp ◾** !trans_refl ⬝ _ ⬝ !refl_trans⁻¹ ⬝ !ap1_phomotopy_refl⁻¹ ◾** idp, - fapply phomotopy_eq, - { exact ap1_gen_compose_const_right g b₀ }, - { reflexivity } - end - - definition pap1_natural_left [constructor] (f : X' →* X) : - psquare (pap1 X Y) (pap1 X' Y) (ppcompose_right f) (ppcompose_right (Ω→ f)) := - begin - fapply phomotopy_mk_ppmap, - { intro g, exact !ap1_pcompose⁻¹* }, - { refine idp ◾** (ap phomotopy_of_eq (!ap1_eq_of_phomotopy ◾ idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ - !phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ (ap phomotopy_of_eq (!pcompose_right_eq_of_phomotopy ◾ - idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ !phomotopy_of_eq_of_phomotopy)⁻¹, - apply symm_trans_eq_of_eq_trans, exact (ap1_pcompose_pconst_left f)⁻¹ } - end - - definition pap1_natural_right [constructor] (f : Y →* Y') : - psquare (pap1 X Y) (pap1 X Y') (ppcompose_left f) (ppcompose_left (Ω→ f)) := - begin - fapply phomotopy_mk_ppmap, - { intro g, exact !ap1_pcompose⁻¹* }, - { refine idp ◾** (ap phomotopy_of_eq (!ap1_eq_of_phomotopy ◾ idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ - !phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ (ap phomotopy_of_eq (!pcompose_left_eq_of_phomotopy ◾ - idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ !phomotopy_of_eq_of_phomotopy)⁻¹, - apply symm_trans_eq_of_eq_trans, exact (ap1_pcompose_pconst_right f)⁻¹ } - end namespace susp - + variables {X X' Y Y' Z : Type*} definition susp_functor_pconst_homotopy [unfold 3] {X Y : Type*} (x : psusp X) : psusp_functor (pconst X Y) x = pt := begin diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 2e9ca17..bb13e71 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -899,7 +899,41 @@ namespace function is_surjective f' := is_surjective_homotopy_closed p⁻¹ʰᵗʸ H -end function + definition is_equiv_ap1_gen_of_is_embedding {A B : Type} (f : A → B) [is_embedding f] + {a a' : A} {b b' : B} (q : f a = b) (q' : f a' = b') : is_equiv (ap1_gen f q q') := + begin + induction q, induction q', + exact is_equiv.homotopy_closed _ (ap1_gen_idp_left f)⁻¹ʰᵗʸ, + end + + definition is_equiv_ap1_of_is_embedding {A B : Type*} (f : A →* B) [is_embedding f] : + is_equiv (Ω→ f) := + is_equiv_ap1_gen_of_is_embedding f (respect_pt f) (respect_pt f) + + definition loop_pequiv_loop_of_is_embedding [constructor] {A B : Type*} (f : A →* B) + [is_embedding f] : Ω A ≃* Ω B := + pequiv_of_pmap (Ω→ f) (is_equiv_ap1_of_is_embedding f) + + definition loopn_pequiv_loopn_of_is_embedding [constructor] (n : ℕ) [H : is_succ n] + {A B : Type*} (f : A →* B) [is_embedding f] : Ω[n] A ≃* Ω[n] B := + begin + induction H with n, + exact !loopn_succ_in ⬝e* + loopn_pequiv_loopn n (loop_pequiv_loop_of_is_embedding f) ⬝e* + !loopn_succ_in⁻¹ᵉ* + end + + definition homotopy_group_isomorphism_of_is_embedding (n : ℕ) [H : is_succ n] {A B : Type*} + (f : A →* B) [H2 : is_embedding f] : πg[n] A ≃g πg[n] B := + begin + apply isomorphism.mk (homotopy_group_homomorphism n f), + induction H with n, + apply is_equiv_of_equiv_of_homotopy + (ptrunc_pequiv_ptrunc 0 (loopn_pequiv_loopn_of_is_embedding (n+1) f)), + exact sorry + end + +end function open function namespace fiber open pointed @@ -1201,6 +1235,9 @@ namespace is_conn definition component_incl [constructor] (A : Type*) : component A →* A := pmap.mk pr1 idp + definition is_embedding_component_incl [instance] (A : Type*) : is_embedding (component_incl A) := + is_embedding_pr1 _ + definition component_intro [constructor] {A B : Type*} (f : A →* B) (H : merely_constant f) : A →* component B := begin @@ -1220,17 +1257,7 @@ namespace is_conn -- exact subtype_eq !respect_pt -- end - /- move!-/ - lemma is_equiv_ap1_of_is_embedding {A B : Type*} (f : A →* B) [is_embedding f] : - is_equiv (Ω→ f) := - sorry - - definition loop_pequiv_loop_of_is_embedding [constructor] {A B : Type*} (f : A →* B) [is_embedding f] : - Ω A ≃* Ω B := - pequiv_of_pmap (Ω→ f) (is_equiv_ap1_of_is_embedding f) - definition loop_component (A : Type*) : Ω (component A) ≃* Ω A := - have is_embedding (component_incl A), from is_embedding_pr1 _, loop_pequiv_loop_of_is_embedding (component_incl A) lemma loopn_component (n : ℕ) (A : Type*) : Ω[n+1] (component A) ≃* Ω[n+1] A := @@ -1240,9 +1267,10 @@ namespace is_conn -- isomorphism_of_equiv (trunc_equiv_trunc 0 (loop_component A)) _ lemma homotopy_group_component (n : ℕ) (A : Type*) : πg[n+1] (component A) ≃g πg[n+1] A := - sorry + homotopy_group_isomorphism_of_is_embedding (n+1) (component_incl A) - definition is_trunc_component [instance] (n : ℕ₋₂) (A : Type*) [is_trunc n A] : is_trunc n (component A) := + definition is_trunc_component [instance] (n : ℕ₋₂) (A : Type*) [is_trunc n A] : + is_trunc n (component A) := begin apply @is_trunc_sigma, intro a, cases n with n, { apply is_contr_of_inhabited_prop, exact tr !is_prop.elim }, @@ -1262,7 +1290,8 @@ namespace is_conn { exact sorry } end - definition ptrunc_component (n : ℕ₋₂) (A : Type*) : ptrunc n (component A) ≃* component (ptrunc n A) := + definition ptrunc_component (n : ℕ₋₂) (A : Type*) : + ptrunc n (component A) ≃* component (ptrunc n A) := begin cases n with n, exact sorry, cases n with n, exact sorry, diff --git a/pointed.hlean b/pointed.hlean index c749a82..ac5858b 100644 --- a/pointed.hlean +++ b/pointed.hlean @@ -1004,4 +1004,76 @@ namespace pointed -- definition phomotopy_eq_equiv_phomotopy2 : p = q ≃ p ~*2 q := -- sorry + variables {X X' Y Y' Z : Type*} + definition pap1 [constructor] (X Y : Type*) : ppmap X Y →* ppmap (Ω X) (Ω Y) := + pmap.mk ap1 (eq_of_phomotopy !ap1_pconst) + + definition ap1_gen_const {A B : Type} {a₁ a₂ : A} (b : B) (p : a₁ = a₂) : + ap1_gen (const A b) idp idp p = idp := + ap1_gen_idp_left (const A b) p ⬝ ap_constant p b + + definition ap1_gen_compose_const_left + {A B C : Type} (c : C) (f : A → B) {a₁ a₂ : A} (p : a₁ = a₂) : + ap1_gen_compose (const B c) f idp idp idp idp p ⬝ + ap1_gen_const c (ap1_gen f idp idp p) = + ap1_gen_const c p := + begin induction p, reflexivity end + + definition ap1_gen_compose_const_right + {A B C : Type} (g : B → C) (b : B) {a₁ a₂ : A} (p : a₁ = a₂) : + ap1_gen_compose g (const A b) idp idp idp idp p ⬝ + ap (ap1_gen g idp idp) (ap1_gen_const b p) = + ap1_gen_const (g b) p := + begin induction p, reflexivity end + + definition ap1_pcompose_pconst_left {A B C : Type*} (f : A →* B) : + phsquare (ap1_pcompose (pconst B C) f) + (ap1_pconst A C) + (ap1_phomotopy (pconst_pcompose f)) + (pwhisker_right (Ω→ f) (ap1_pconst B C) ⬝* pconst_pcompose (Ω→ f)) := + begin + induction A with A a₀, induction B with B b₀, induction C with C c₀, induction f with f f₀, + esimp at *, induction f₀, + refine idp ◾** !trans_refl ⬝ _ ⬝ !refl_trans⁻¹ ⬝ !ap1_phomotopy_refl⁻¹ ◾** idp, + fapply phomotopy_eq, + { exact ap1_gen_compose_const_left c₀ f }, + { reflexivity } + end + + definition ap1_pcompose_pconst_right {A B C : Type*} (g : B →* C) : + phsquare (ap1_pcompose g (pconst A B)) + (ap1_pconst A C) + (ap1_phomotopy (pcompose_pconst g)) + (pwhisker_left (Ω→ g) (ap1_pconst A B) ⬝* pcompose_pconst (Ω→ g)) := + begin + induction A with A a₀, induction B with B b₀, induction C with C c₀, induction g with g g₀, + esimp at *, induction g₀, + refine idp ◾** !trans_refl ⬝ _ ⬝ !refl_trans⁻¹ ⬝ !ap1_phomotopy_refl⁻¹ ◾** idp, + fapply phomotopy_eq, + { exact ap1_gen_compose_const_right g b₀ }, + { reflexivity } + end + + definition pap1_natural_left [constructor] (f : X' →* X) : + psquare (pap1 X Y) (pap1 X' Y) (ppcompose_right f) (ppcompose_right (Ω→ f)) := + begin + fapply phomotopy_mk_ppmap, + { intro g, exact !ap1_pcompose⁻¹* }, + { refine idp ◾** (ap phomotopy_of_eq (!ap1_eq_of_phomotopy ◾ idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ + !phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ (ap phomotopy_of_eq (!pcompose_right_eq_of_phomotopy ◾ + idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ !phomotopy_of_eq_of_phomotopy)⁻¹, + apply symm_trans_eq_of_eq_trans, exact (ap1_pcompose_pconst_left f)⁻¹ } + end + + definition pap1_natural_right [constructor] (f : Y →* Y') : + psquare (pap1 X Y) (pap1 X Y') (ppcompose_left f) (ppcompose_left (Ω→ f)) := + begin + fapply phomotopy_mk_ppmap, + { intro g, exact !ap1_pcompose⁻¹* }, + { refine idp ◾** (ap phomotopy_of_eq (!ap1_eq_of_phomotopy ◾ idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ + !phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ (ap phomotopy_of_eq (!pcompose_left_eq_of_phomotopy ◾ + idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ !phomotopy_of_eq_of_phomotopy)⁻¹, + apply symm_trans_eq_of_eq_trans, exact (ap1_pcompose_pconst_right f)⁻¹ } + end + end pointed