From 6be1b46d5ee2da5cacd5ab407fb24feb4932bbcb Mon Sep 17 00:00:00 2001 From: Steve Awodey Date: Thu, 17 Nov 2016 16:25:14 -0500 Subject: [PATCH 1/5] WIP first group isomorphism them --- algebra/quotient_group.hlean | 48 ++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean index d98f5da..82bc746 100644 --- a/algebra/quotient_group.hlean +++ b/algebra/quotient_group.hlean @@ -254,6 +254,54 @@ definition comm_group_first_iso_thm (A B : CommGroup) (f : A →g B) : quotient_ -- show that the above map is injective and surjective. end +definition comm_group_kernel_factor {A B C: CommGroup} (f : A →g B)(g : A →g C){i : C →g B}(H : f = i ∘g g ) + : Π a:A , kernel_subgroup(g)(a) → kernel_subgroup(f)(a) := + begin + intro a, + intro p, + exact calc + f a = i (g a) : homotopy_of_eq (ap group_fun H) a + ... = i 1 : ap i p + ... = 1 : respect_one i + end + +definition comm_group_kernel_equivalent {A B : CommGroup} (C : CommGroup) (f : A →g B)(g : A →g C)(i : C →g B)(H : f = i ∘g g )(K : is_embedding i) + : Π a:A , kernel_subgroup(g)(a) ↔ kernel_subgroup(f)(a) := +begin + intro a, + fapply iff.intro, + exact comm_group_kernel_factor f g H a, + intro p, + apply @is_injective_of_is_embedding _ _ i _ (g a) 1, + exact calc + i (g a) = f a : (homotopy_of_eq (ap group_fun H) a)⁻¹ + ... = 1 : p + ... = i 1 : (respect_one i)⁻¹ +end + +definition comm_group_kernel_image_lift (A B : CommGroup) (f : A →g B) + : Π a : A, kernel_subgroup(image_lift(f))(a) ↔ kernel_subgroup(f)(a) := + begin + fapply comm_group_kernel_equivalent (comm_image f) (f) (image_lift(f)) (image_incl(f)), + exact image_factor f, + exact is_embedding_of_is_injective (image_incl_injective(f)), + end + +definition comm_group_kernel_quotient_to_image {A B : CommGroup} (f : A →g B) + : quotient_comm_group (kernel_subgroup f) →g comm_image (f) := +begin +fapply quotient_group_elim (image_lift f), intro a, intro p, +apply iff.mpr (comm_group_kernel_image_lift _ _ f a) p +end + +definition is_surjective_kernel_quotient_to_image {A B : CommGroup} (f : A →g B) + : is_surjective (comm_group_kernel_quotient_to_image f) := + begin + intro b, exact sorry + -- have H : is_surjective (image_lift f) + end + +print iff.mpr /- set generating normal subgroup -/ section From c96f3d18f2971bc830acf11fa1f55d350d3d42f5 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 14 Nov 2016 18:04:41 -0500 Subject: [PATCH 2/5] Work on the smash product --- homotopy/smash.hlean | 81 ++++++++++++++++++++++++++++++++++---------- 1 file changed, 64 insertions(+), 17 deletions(-) diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean index 5667b40..85e5285 100644 --- a/homotopy/smash.hlean +++ b/homotopy/smash.hlean @@ -26,8 +26,10 @@ namespace smash definition smash' (A B : Type*) : Type := pushout (@prod_of_sum A B) (@bool_of_sum A B) protected definition mk (a : A) (b : B) : smash' A B := inl (a, b) + definition pointed_smash' [instance] [constructor] (A B : Type*) : pointed (smash' A B) := + pointed.mk (smash.mk pt pt) definition smash [constructor] (A B : Type*) : Type* := - pointed.MK (smash' A B) (smash.mk pt pt) + pointed.mk' (smash' A B) definition auxl : smash A B := inr ff definition auxr : smash A B := inr tt @@ -183,7 +185,7 @@ namespace smash /- smash A B ≃ pcofiber (pprod_of_pwedge A B) -/ - definition prod_of_pwedge [unfold 3] (v : pwedge' A B) : A × B := + definition prod_of_wedge [unfold 3] (v : pwedge' A B) : A × B := begin induction v with a b , { exact (a, pt) }, @@ -191,18 +193,17 @@ namespace smash { reflexivity } end + variables (A B) definition pprod_of_pwedge [constructor] : pwedge' A B →* A ×* B := begin fconstructor, - { intro v, induction v with a b , - { exact (a, pt) }, - { exact (pt, b) }, - { reflexivity }}, + { exact prod_of_wedge }, { reflexivity } end + variables {A B} attribute pcofiber [constructor] - definition pcofiber_of_smash (x : smash A B) : pcofiber' (@pprod_of_pwedge A B) := + definition pcofiber_of_smash [unfold 3] (x : smash A B) : pcofiber' (@pprod_of_pwedge A B) := begin induction x, { exact pushout.inr (a, b) }, @@ -212,26 +213,72 @@ namespace smash { symmetry, exact pushout.glue (pushout.inr b) } end + -- move definition ap_eq_ap011 {A B C X : Type} (f : A → B → C) (g : X → A) (h : X → B) {x x' : X} (p : x = x') : ap (λx, f (g x) (h x)) p = ap011 f (ap g p) (ap h p) := by induction p; reflexivity - definition smash_of_pcofiber (x : pcofiber' (@pprod_of_pwedge A B)) : smash A B := + definition smash_of_pcofiber_glue [unfold 3] (x : pwedge' A B) : + Point (smash A B) = smash.mk (prod_of_wedge x).1 (prod_of_wedge x).2 := + begin + induction x with a b: esimp, + { apply gluel' }, + { apply gluer' }, + { apply eq_pathover_constant_left, refine _ ⬝hp (ap_eq_ap011 smash.mk _ _ _)⁻¹, + rewrite [ap_compose' prod.pr1, ap_compose' prod.pr2], + -- TODO: define elim_glue for wedges and remove k in krewrite + krewrite [pushout.elim_glue], esimp, apply vdeg_square, + exact !con.right_inv ⬝ !con.right_inv⁻¹ } + end + + definition smash_of_pcofiber [unfold 3] (x : pcofiber' (pprod_of_pwedge A B)) : smash A B := begin induction x with x x, { exact smash.mk pt pt }, { exact smash.mk x.1 x.2 }, - { induction x with a b: esimp, - { apply gluel' }, - { apply gluer' }, - { apply eq_pathover_constant_left, refine _ ⬝hp (ap_eq_ap011 smash.mk _ _ _)⁻¹, - unfold [wedge.elim], - rewrite [ap_compose' prod.pr1, ap_compose' prod.pr2], - -- TODO: define elim_glue for wedges and remove krewrite - krewrite [pushout.elim_glue], esimp, apply vdeg_square, - exact !con.right_inv ⬝ !con.right_inv⁻¹ }} + { exact smash_of_pcofiber_glue x } end + definition pcofiber_of_smash_of_pcofiber (x : pcofiber' (pprod_of_pwedge A B)) : + pcofiber_of_smash (smash_of_pcofiber x) = x := + begin + induction x with x x, + { refine (pushout.glue pt)⁻¹ }, + { }, + { } + end + + definition smash_of_pcofiber_of_smash (x : smash A B) : + smash_of_pcofiber (pcofiber_of_smash x) = x := + begin + induction x, + { reflexivity }, + { apply gluel }, + { apply gluer }, + { apply eq_pathover_id_right, refine ap_compose smash_of_pcofiber _ _ ⬝ph _, + refine ap02 _ !elim_gluel ⬝ph _, refine !ap_inv ⬝ph _, refine !pushout.elim_glue⁻² ⬝ph _, + esimp, apply square_of_eq, refine !idp_con ⬝ _ ⬝ whisker_right !inv_con_inv_right⁻¹ _, + exact !inv_con_cancel_right⁻¹ }, + { apply eq_pathover_id_right, refine ap_compose smash_of_pcofiber _ _ ⬝ph _, + refine ap02 _ !elim_gluer ⬝ph _, refine !ap_inv ⬝ph _, refine !pushout.elim_glue⁻² ⬝ph _, + esimp, apply square_of_eq, refine !idp_con ⬝ _ ⬝ whisker_right !inv_con_inv_right⁻¹ _, + exact !inv_con_cancel_right⁻¹ }, + end + + variables (A B) + definition smash_pequiv_pcofiber : smash A B ≃* pcofiber' (pprod_of_pwedge A B) := + begin + fapply pequiv_of_equiv, + { fapply equiv.MK, + { apply pcofiber_of_smash }, + { apply smash_of_pcofiber }, + { exact pcofiber_of_smash_of_pcofiber }, + { exact smash_of_pcofiber_of_smash }}, + { esimp, symmetry, apply pushout.glue pt } + end + + variables {A B} + /- smash A S¹ = susp A -/ open susp From 8e366e08c37684e6787742e20027fa7ee804fbc3 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 18 Nov 2016 15:20:22 -0500 Subject: [PATCH 3/5] Finish the universal property of the direct sum --- algebra/direct_sum.hlean | 26 +++++++++++--------- algebra/free_commutative_group.hlean | 23 +++++++++++------- algebra/quotient_group.hlean | 36 ++++++++++++++++------------ 3 files changed, 51 insertions(+), 34 deletions(-) diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean index 3577240..46ea343 100644 --- a/algebra/direct_sum.hlean +++ b/algebra/direct_sum.hlean @@ -23,7 +23,7 @@ namespace group variables {A' : CommGroup} definition dirsum_carrier : CommGroup := free_comm_group (trunctype.mk (Σi, Y i) _) - local abbreviation ι := @free_comm_group_inclusion + local abbreviation ι [constructor] := @free_comm_group_inclusion inductive dirsum_rel : dirsum_carrier → Type := | rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ * ι ⟨i, y₂⟩ * (ι ⟨i, y₁ * y₂⟩)⁻¹) @@ -35,26 +35,30 @@ namespace group homomorphism.mk (λy, class_of (ι ⟨i, y⟩)) begin intro g h, symmetry, apply gqg_eq_of_rel, apply tr, apply dirsum_rel.rmk end - definition dirsum_elim [constructor] (f : Πi, Y i →g A') : dirsum →g A' := + definition dirsum_elim_resp_quotient (f : Πi, Y i →g A') (g : dirsum_carrier) + (r : ∥dirsum_rel g∥) : free_comm_group_elim (λv, f v.1 v.2) g = 1 := begin - refine homomorphism.mk (gqg_elim _ (free_comm_group_elim (λv, f v.1 v.2)) _) _, - { intro g r, induction r with r, induction r, - rewrite [to_respect_mul, to_respect_inv], apply mul_inv_eq_of_eq_mul, - rewrite [one_mul], apply ap (free_comm_group_elim (λ v, group_fun (f v.1) v.2)), - exact sorry - }, - { exact sorry } + induction r with r, induction r, + rewrite [to_respect_mul, to_respect_inv], apply mul_inv_eq_of_eq_mul, + rewrite [one_mul, to_respect_mul, ▸*, ↑foldl, +one_mul, to_respect_mul] end + definition dirsum_elim [constructor] (f : Πi, Y i →g A') : dirsum →g A' := + gqg_elim _ (free_comm_group_elim (λv, f v.1 v.2)) (dirsum_elim_resp_quotient f) + definition dirsum_elim_compute (f : Πi, Y i →g A') (i : I) : dirsum_elim f ∘g dirsum_incl i ~ f i := begin - intro g, exact sorry + intro g, apply one_mul end definition dirsum_elim_unique (f : Πi, Y i →g A') (k : dirsum →g A') (H : Πi, k ∘g dirsum_incl i ~ f i) : k ~ dirsum_elim f := - sorry + begin + apply gqg_elim_unique, + apply free_comm_group_elim_unique, + intro x, induction x with i y, exact H i y + end end diff --git a/algebra/free_commutative_group.hlean b/algebra/free_commutative_group.hlean index c9ca0c7..26d9af7 100644 --- a/algebra/free_commutative_group.hlean +++ b/algebra/free_commutative_group.hlean @@ -174,20 +174,27 @@ namespace group definition fn_of_free_comm_group_elim [unfold_full] (φ : free_comm_group X →g A) : X → A := φ ∘ free_comm_group_inclusion + definition free_comm_group_elim_unique [constructor] (f : X → A) (k : free_comm_group X →g A) + (H : k ∘ free_comm_group_inclusion ~ f) : k ~ free_comm_group_elim f := + begin + refine set_quotient.rec_prop _, intro l, esimp, + induction l with s l IH, + { esimp [foldl], exact to_respect_one k}, + { rewrite [foldl_cons, fgh_helper_mul], + refine to_respect_mul k (class_of [s]) (class_of l) ⬝ _, + rewrite [IH], apply ap (λx, x * _), induction s: rewrite [▸*, one_mul, -H a], + apply to_respect_inv } + end + variables (X A) - definition free_comm_group_elim_equiv_fn : (free_comm_group X →g A) ≃ (X → A) := + definition free_comm_group_elim_equiv_fn [constructor] : (free_comm_group X →g A) ≃ (X → A) := begin fapply equiv.MK, { exact fn_of_free_comm_group_elim}, { exact free_comm_group_elim}, { intro f, apply eq_of_homotopy, intro x, esimp, unfold [foldl], apply one_mul}, - { intro φ, apply homomorphism_eq, refine set_quotient.rec_prop _, intro l, esimp, - induction l with s l IH, - { esimp [foldl], symmetry, exact to_respect_one φ}, - { rewrite [foldl_cons, fgh_helper_mul], - refine _ ⬝ (to_respect_mul φ (class_of [s]) (class_of l))⁻¹, - rewrite [▸*,IH], induction s: rewrite [▸*, one_mul], apply ap (λx, x * _), - exact !to_respect_inv⁻¹}} + { intro k, symmetry, apply homomorphism_eq, apply free_comm_group_elim_unique, + reflexivity } end end group diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean index 82bc746..314ba15 100644 --- a/algebra/quotient_group.hlean +++ b/algebra/quotient_group.hlean @@ -37,7 +37,7 @@ namespace group have H2 : (g * h⁻¹) * (h * k⁻¹) = g * k⁻¹, from calc (g * h⁻¹) * (h * k⁻¹) = ((g * h⁻¹) * h) * k⁻¹ : by rewrite [mul.assoc (g * h⁻¹)] ... = g * k⁻¹ : by rewrite inv_mul_cancel_right, - show N (g * k⁻¹), from H2 ▸ H1 + show N (g * k⁻¹), by rewrite [-H2]; exact H1 theorem is_equivalence_quotient_rel : is_equivalence (quotient_rel N) := is_equivalence.mk quotient_rel_refl @@ -53,7 +53,7 @@ namespace group g⁻¹ * (h * g⁻¹) * g = g⁻¹ * h * g⁻¹ * g : by rewrite -mul.assoc ... = g⁻¹ * h : inv_mul_cancel_right ... = g⁻¹ * h⁻¹⁻¹ : by rewrite algebra.inv_inv, - show N (g⁻¹ * h⁻¹⁻¹), from H2 ▸ H1 + show N (g⁻¹ * h⁻¹⁻¹), by rewrite [-H2]; exact H1 theorem quotient_rel_resp_mul (r : quotient_rel N g h) (r' : quotient_rel N g' h') : quotient_rel N (g * g') (h * h') := @@ -187,26 +187,33 @@ namespace group apply rel_of_eq _ H end - definition quotient_group_elim (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group N →g G' := + definition quotient_group_elim_fun [unfold 6] (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) + (g : quotient_group N) : G' := + begin + refine set_quotient.elim f _ g, + intro g h K, + apply eq_of_mul_inv_eq_one, + have e : f (g * h⁻¹) = f g * (f h)⁻¹, + from calc + f (g * h⁻¹) = f g * (f h⁻¹) : to_respect_mul + ... = f g * (f h)⁻¹ : to_respect_inv, + rewrite (inverse e), + apply H, exact K + end + + definition quotient_group_elim [constructor] (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group N →g G' := begin fapply homomorphism.mk, -- define function - { apply set_quotient.elim f, - intro g h K, - apply eq_of_mul_inv_eq_one, - have e : f (g * h⁻¹) = f g * (f h)⁻¹, - from calc - f (g * h⁻¹) = f g * (f h⁻¹) : to_respect_mul - ... = f g * (f h)⁻¹ : to_respect_inv, - rewrite (inverse e), - apply H, exact K}, + { exact quotient_group_elim_fun f H }, { intro g h, induction g using set_quotient.rec_prop with g, induction h using set_quotient.rec_prop with h, krewrite (inverse (to_respect_mul (qg_map N) g h)), unfold qg_map, esimp, exact to_respect_mul f g h } end - definition quotient_group_compute (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group_elim f H ∘g qg_map N ~ f := + definition quotient_group_compute (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : + quotient_group_elim f H ∘g qg_map N ~ f := begin intro g, reflexivity end @@ -215,7 +222,6 @@ namespace group : ( k ∘g qg_map N ~ f ) → k ~ quotient_group_elim f H := begin intro K cg, induction cg using set_quotient.rec_prop with g, - krewrite (quotient_group_compute f), exact K g end @@ -340,7 +346,7 @@ print iff.mpr definition gqg_eq_of_rel {g h : A₁} (H : S (g * h⁻¹)) : gqg_map g = gqg_map h := eq_of_rel (tr (rincl H)) - definition gqg_elim (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1) + definition gqg_elim [constructor] (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1) : quotient_comm_group_gen →g A₂ := begin apply quotient_group_elim f, From 4f1db25e169c9adaafe794375592dad1b207d2e4 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 17 Nov 2016 16:21:40 -0500 Subject: [PATCH 4/5] Work on the uniqueness of Eilenberg-Maclane spaces --- homotopy/EM.hlean | 54 +++- homotopy/EMnew.hlean | 518 ++++++++++++++++++++++++++++++++++++++ homotopy/cohomology.hlean | 7 +- homotopy/degree.hlean | 4 +- homotopy/smash.hlean | 4 +- move_to_lib.hlean | 401 ++++++++++++++++++++++++++--- 6 files changed, 933 insertions(+), 55 deletions(-) create mode 100644 homotopy/EMnew.hlean diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean index e7e5de8..a4d8113 100644 --- a/homotopy/EM.hlean +++ b/homotopy/EM.hlean @@ -153,7 +153,7 @@ namespace EM [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n →* X := pmap.mk (EMadd1_map e r) begin cases n with n: reflexivity end - definition loop_pEMadd1_pmap {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G) + definition loopn_pEMadd1_pmap {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G) (r : Π(p q : Ω[succ n] X), e (@concat (Ω[n] X) pt pt pt p q) = e p * e q) [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : Ω→[succ n](pEMadd1_pmap e r) ~ e⁻¹ᵉ ∘ loopn_EMadd1 G n := @@ -185,7 +185,7 @@ namespace EM do 2 exact trivial_homotopy_group_of_is_conn _ (le_of_lt_succ H)}, { cases H, esimp, apply is_equiv_trunc_functor, esimp, apply is_equiv.homotopy_closed, rotate 1, - { symmetry, exact loop_pEMadd1_pmap _ _}, + { symmetry, exact loopn_pEMadd1_pmap _ _}, apply is_equiv_compose, apply pequiv.to_is_equiv}, { apply @is_equiv_of_is_contr, do 2 exact trivial_homotopy_group_of_is_trunc _ H} @@ -206,18 +206,15 @@ namespace EM definition EM_pequiv_zero {G : CommGroup} {X : Type*} (e : X ≃* pType_of_Group G) : EM G 0 ≃* X := proof e⁻¹ᵉ* qed - definition EM_spectrum /-[constructor]-/ (G : CommGroup) : spectrum := - spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*) - /- uniqueness of K(G,n), method 2: -/ -- definition freudenthal_homotopy_group_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n) --- : π*[k + 1] (psusp A) ≃* π*[k] A := +-- : π[k + 1] (psusp A) ≃* π[k] A := -- calc --- π*[k + 1] (psusp A) ≃* π*[k] (Ω (psusp A)) : pequiv_of_eq (homotopy_group_succ_in (psusp A) k) +-- π[k + 1] (psusp A) ≃* π[k] (Ω (psusp A)) : homotopy_group_succ_in -- ... ≃* Ω[k] (ptrunc k (Ω (psusp A))) : homotopy_group_pequiv_loop_ptrunc k (Ω (psusp A)) -- ... ≃* Ω[k] (ptrunc k A) : loopn_pequiv_loopn k (freudenthal_pequiv A H) --- ... ≃* π*[k] A : (homotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ* +-- ... ≃* π[k] A : (homotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ* definition iterate_psusp_succ_pequiv (n : ℕ) (A : Type*) : iterate_psusp (succ n) A ≃* iterate_psusp n (psusp A) := @@ -273,6 +270,47 @@ namespace EM symmetry, apply loopn_succ_in} end + /- new method of uniqueness, define K(G,n+1) as the truncation of the suspension of K(G,n) -/ + + definition EMadd2 (G : CommGroup) (n : ℕ) : Type* := ptrunc (n.+2) (psusp (EMadd1 G n)) + + definition EMadd2_map [constructor] {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[n+2] X ≃ G) + (r : Π(p q : Ω[n+2] X), e (@concat (Ω[n+1] X) pt pt pt p q) = e p * e q) + [H1 : is_conn (n.+1) X] [H2 : is_trunc (n.+2) X] : EMadd2 G n → X := + begin + intro x, induction x with x, induction x with x, + { exact pt }, + { exact pt }, + { refine EMadd1_map ((loopn_succ_in _ (n+1))⁻¹ᵉ ⬝e e) _ x, + exact abstract begin + intro p q, refine _ ⬝ !r, apply ap e, esimp, + refine @inv_eq_of_eq _ _ (pequiv.to_equiv (loopn_succ_in X (n + 1))) _ _ _ _, + refine _⁻¹ ⬝ !loopn_succ_in_con⁻¹, + exact to_right_inv (loopn_succ_in X (succ n)) p ◾ to_right_inv (loopn_succ_in X (succ n)) q + end end } + end + + -- -- general case + -- definition EMadd1_map [unfold 8] {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G) + -- (r : Π(p q : Ω (Ω[n] X)), e (p ⬝ q) = e p * e q) + -- [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n → X := + -- begin + -- revert X e r H1 H2, induction n with n f: intro X e r H1 H2, + -- { change trunc 1 (EM1 G) → X, intro x, induction x with x, exact EM1_map e r x}, + -- change trunc (n.+2) (susp (iterate_psusp n (pEM1 G))) → X, intro x, + -- induction x with x, induction x with x, + -- { exact pt}, + -- { exact pt}, + -- change carrier (Ω X), refine f _ _ _ _ _ (tr x), + -- { refine _⁻¹ᵉ ⬝e e, apply equiv_of_pequiv, apply loopn_succ_in}, + -- exact abstract begin + -- intro p q, refine _ ⬝ !r, apply ap e, esimp, + -- apply inv_eq_of_eq, + -- refine _⁻¹ ⬝ !loopn_succ_in_con⁻¹, + -- exact to_right_inv (loopn_succ_in X (succ n)) p ◾ to_right_inv (loopn_succ_in X (succ n)) q + -- end end + -- end + end EM -- cohomology ∥ X → K(G,n) ∥ -- reduced cohomology ∥ X →* K(G,n) ∥ diff --git a/homotopy/EMnew.hlean b/homotopy/EMnew.hlean new file mode 100644 index 0000000..a768547 --- /dev/null +++ b/homotopy/EMnew.hlean @@ -0,0 +1,518 @@ +/- +Copyright (c) 2016 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Floris van Doorn + +Eilenberg MacLane spaces + +This file replaces the file in the HoTT library +-/ + +import hit.groupoid_quotient homotopy.hopf homotopy.freudenthal homotopy.homotopy_group + ..move_to_lib +open algebra pointed nat eq category group is_trunc iso unit trunc equiv is_conn function is_equiv + trunc_index + +local attribute pType_of_Group [coercion] + +namespace EMnew + open groupoid_quotient + + variables {G : Group} + definition EM1' (G : Group) : Type := + groupoid_quotient (Groupoid_of_Group G) + definition EM1 [constructor] (G : Group) : Type* := + pointed.MK (EM1' G) (elt star) + + definition base : EM1' G := elt star + definition pth : G → base = base := pth + definition resp_mul (g h : G) : pth (g * h) = pth g ⬝ pth h := resp_comp h g + definition resp_one : pth (1 : G) = idp := + resp_id star + + definition resp_inv (g : G) : pth (g⁻¹) = (pth g)⁻¹ := + resp_inv g + + local attribute pointed.MK pointed.carrier EM1 EM1' [reducible] + protected definition rec {P : EM1' G → Type} [H : Π(x : EM1' G), is_trunc 1 (P x)] + (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb) + (Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h) (x : EM1' G) : P x := + begin + induction x, + { induction g, exact Pb}, + { induction a, induction b, exact Pp f}, + { induction a, induction b, induction c, exact Pmul f g} + end + + protected definition rec_on {P : EM1' G → Type} [H : Π(x : EM1' G), is_trunc 1 (P x)] + (x : EM1' G) (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb) + (Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h) : P x := + EMnew.rec Pb Pp Pmul x + + protected definition set_rec {P : EM1' G → Type} [H : Π(x : EM1' G), is_set (P x)] + (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb) (x : EM1' G) : P x := + EMnew.rec Pb Pp !center x + + protected definition prop_rec {P : EM1' G → Type} [H : Π(x : EM1' G), is_prop (P x)] + (Pb : P base) (x : EM1' G) : P x := + EMnew.rec Pb !center !center x + + definition rec_pth {P : EM1' G → Type} [H : Π(x : EM1' G), is_trunc 1 (P x)] + {Pb : P base} {Pp : Π(g : G), Pb =[pth g] Pb} + (Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h) + (g : G) : apd (EMnew.rec Pb Pp Pmul) (pth g) = Pp g := + proof !rec_pth qed + + protected definition elim {P : Type} [is_trunc 1 P] (Pb : P) (Pp : Π(g : G), Pb = Pb) + (Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) (x : EM1' G) : P := + begin + induction x, + { exact Pb}, + { exact Pp f}, + { exact Pmul f g} + end + + protected definition elim_on [reducible] {P : Type} [is_trunc 1 P] (x : EM1' G) + (Pb : P) (Pp : G → Pb = Pb) (Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) : P := + EMnew.elim Pb Pp Pmul x + + protected definition set_elim [reducible] {P : Type} [is_set P] (Pb : P) (Pp : G → Pb = Pb) + (x : EM1' G) : P := + EMnew.elim Pb Pp !center x + + protected definition prop_elim [reducible] {P : Type} [is_prop P] (Pb : P) (x : EM1' G) : P := + EMnew.elim Pb !center !center x + + definition elim_pth {P : Type} [is_trunc 1 P] {Pb : P} {Pp : G → Pb = Pb} + (Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) (g : G) : ap (EMnew.elim Pb Pp Pmul) (pth g) = Pp g := + proof !elim_pth qed + + protected definition elim_set.{u} (Pb : Set.{u}) (Pp : Π(g : G), Pb ≃ Pb) + (Pmul : Π(g h : G) (x : Pb), Pp (g * h) x = Pp h (Pp g x)) (x : EM1' G) : Set.{u} := + groupoid_quotient.elim_set (λu, Pb) (λu v, Pp) (λu v w g h, proof Pmul h g qed) x + + theorem elim_set_pth {Pb : Set} {Pp : Π(g : G), Pb ≃ Pb} + (Pmul : Π(g h : G) (x : Pb), Pp (g * h) x = Pp h (Pp g x)) (g : G) : + transport (EMnew.elim_set Pb Pp Pmul) (pth g) = Pp g := + !elim_set_pth + +end EMnew + +attribute EMnew.base [constructor] +attribute EMnew.rec EMnew.elim [unfold 7] [recursor 7] +attribute EMnew.rec_on EMnew.elim_on [unfold 4] +attribute EMnew.set_rec EMnew.set_elim [unfold 6] +attribute EMnew.prop_rec EMnew.prop_elim EMnew.elim_set [unfold 5] + +namespace EMnew + open groupoid_quotient + + variables (G : Group) + definition base_eq_base_equiv : (base = base :> EM1 G) ≃ G := + !elt_eq_elt_equiv + + definition fundamental_group_EM1 : π₁ (EM1 G) ≃g G := + begin + fapply isomorphism_of_equiv, + { exact trunc_equiv_trunc 0 !base_eq_base_equiv ⬝e trunc_equiv 0 G}, + { intros g h, induction g with p, induction h with q, + exact encode_con p q} + end + + proposition is_trunc_EM1 [instance] : is_trunc 1 (EM1 G) := + !is_trunc_groupoid_quotient + + proposition is_trunc_EM1' [instance] : is_trunc 1 (EM1' G) := + !is_trunc_groupoid_quotient + + proposition is_conn_EM1' [instance] : is_conn 0 (EM1' G) := + by apply @is_conn_groupoid_quotient; esimp; exact _ + + proposition is_conn_EM1 [instance] : is_conn 0 (EM1 G) := + is_conn_EM1' G + + variable {G} + definition EM1_map [unfold 7] {X : Type*} (e : G → Ω X) + (r : Πg h, e (g * h) = e g ⬝ e h) [is_conn 0 X] [is_trunc 1 X] : EM1 G → X := + begin + intro x, induction x using EMnew.elim, + { exact Point X }, + { exact e g }, + { exact r g h } + end + + /- Uniqueness of K(G, 1) -/ + + definition EM1_pmap [constructor] {X : Type*} (e : G → Ω X) + (r : Πg h, e (g * h) = e g ⬝ e h) [is_conn 0 X] [is_trunc 1 X] : EM1 G →* X := + pmap.mk (EM1_map e r) idp + + variable (G) + definition loop_EM1 [constructor] : G ≃* Ω (EM1 G) := + (pequiv_of_equiv (base_eq_base_equiv G) idp)⁻¹ᵉ* + + variable {G} + definition loop_EM1_pmap {X : Type*} (e : G →* Ω X) + (r : Πg h, e (g * h) = e g ⬝ e h) [is_conn 0 X] [is_trunc 1 X] : + Ω→(EM1_pmap e r) ∘* loop_EM1 G ~* e := + begin + fapply phomotopy.mk, + { intro g, refine !idp_con ⬝ elim_pth r g }, + { apply is_set.elim } + end + + definition EM1_pequiv'.{u} {G : Group.{u}} {X : pType.{u}} (e : G ≃* Ω X) + (r : Πg h, e (g * h) = e g ⬝ e h) [is_conn 0 X] [is_trunc 1 X] : EM1 G ≃* X := + begin + apply pequiv_of_pmap (EM1_pmap e r), + apply whitehead_principle_pointed 1, + intro k, cases k with k, + { apply @is_equiv_of_is_contr, + all_goals (esimp; exact _)}, + { cases k with k, + { apply is_equiv_trunc_functor, esimp, + apply is_equiv.homotopy_closed, rotate 1, + { symmetry, exact phomotopy_pinv_right_of_phomotopy (loop_EM1_pmap _ _) }, + apply is_equiv_compose e }, + { apply @is_equiv_of_is_contr, + do 2 exact trivial_homotopy_group_of_is_trunc _ (succ_lt_succ !zero_lt_succ)}} + end + + definition EM1_pequiv.{u} {G : Group.{u}} {X : pType.{u}} (e : G ≃g π₁ X) + [is_conn 0 X] [is_trunc 1 X] : EM1 G ≃* X := + begin + apply EM1_pequiv' (pequiv_of_isomorphism e ⬝e* ptrunc_pequiv _ _ _), + refine is_equiv.preserve_binary_of_inv_preserve _ mul concat _, + intro p q, + exact to_respect_mul e⁻¹ᵍ (tr p) (tr q) + end + + definition EM1_pequiv_type (X : Type*) [is_conn 0 X] [is_trunc 1 X] : EM1 (π₁ X) ≃* X := + EM1_pequiv !isomorphism.refl + +end EMnew + +open hopf new_susp susp +namespace EMnew + /- EM1 G is an h-space if G is an abelian group. This allows us to construct K(G,n) for n ≥ 2 -/ + variables {G : CommGroup} (n : ℕ) + + definition EM1_mul [unfold 2 3] (x x' : EM1' G) : EM1' G := + begin + induction x, + { exact x'}, + { induction x' using EMnew.set_rec, + { exact pth g}, + { exact abstract begin apply loop_pathover, apply square_of_eq, + refine !resp_mul⁻¹ ⬝ _ ⬝ !resp_mul, + exact ap pth !mul.comm end end}}, + { refine EMnew.prop_rec _ x', apply resp_mul } + end + + variable (G) + definition EM1_mul_one (x : EM1' G) : EM1_mul x base = x := + begin + induction x using EMnew.set_rec, + { reflexivity}, + { apply eq_pathover_id_right, apply hdeg_square, refine EMnew.elim_pth _ g} + end + + definition h_space_EM1 [constructor] [instance] : h_space (EM1' G) := + begin + fapply h_space.mk, + { exact EM1_mul}, + { exact base}, + { intro x', reflexivity}, + { apply EM1_mul_one} + end + + /- K(G, n+1) -/ + definition EMadd1 : ℕ → Type* + | 0 := EM1 G + | (n+1) := ptrunc (n+2) (psusp (EMadd1 n)) + + definition EMadd1_succ [unfold_full] (n : ℕ) : + EMadd1 G (succ n) = ptrunc (n.+2) (psusp (EMadd1 G n)) := + idp + + definition loop_EM2 : Ω[1] (EMadd1 G 1) ≃* EM1 G := + hopf.delooping (EM1' G) idp + + definition is_conn_EMadd1 [instance] (n : ℕ) : is_conn n (EMadd1 G n) := + begin + induction n with n IH, + { apply is_conn_EM1 }, + { rewrite EMadd1_succ, esimp, exact _ } + end + + definition is_trunc_EMadd1 [instance] (n : ℕ) : is_trunc (n+1) (EMadd1 G n) := + begin + cases n with n, + { apply is_trunc_EM1 }, + { apply is_trunc_trunc } + end + + /- loops of an EM-space -/ + definition loop_EMadd1 (n : ℕ) : EMadd1 G n ≃* Ω (EMadd1 G (succ n)) := + begin + cases n with n, + { exact !loop_EM2⁻¹ᵉ* }, + { rewrite [EMadd1_succ G (succ n)], + refine (ptrunc_pequiv (succ n + 1) _ _)⁻¹ᵉ* ⬝e* _ ⬝e* (loop_ptrunc_pequiv _ _)⁻¹ᵉ*, + have succ n + 1 ≤ 2 * succ n, from add_mul_le_mul_add n 1 1, + refine freudenthal_pequiv _ this } + end + + definition loopn_EMadd1_pequiv_EM1 (G : CommGroup) (n : ℕ) : EM1 G ≃* Ω[n] (EMadd1 G n) := + begin + induction n with n e, + { reflexivity }, + { refine _ ⬝e* !loopn_succ_in⁻¹ᵉ*, + refine _ ⬝e* loopn_pequiv_loopn n !loop_EMadd1, + exact e } + end + + -- use loopn_EMadd1_pequiv_EM1 in this definition? + definition loopn_EMadd1 (G : CommGroup) (n : ℕ) : G ≃* Ω[succ n] (EMadd1 G n) := + begin + induction n with n e, + { apply loop_EM1 }, + { refine _ ⬝e* !loopn_succ_in⁻¹ᵉ*, + refine _ ⬝e* loopn_pequiv_loopn (succ n) !loop_EMadd1, + exact e } + end + + definition loopn_EMadd1_succ [unfold_full] (G : CommGroup) (n : ℕ) : loopn_EMadd1 G (succ n) ~* + !loopn_succ_in⁻¹ᵉ* ∘* apn (succ n) !loop_EMadd1 ∘* loopn_EMadd1 G n := + by reflexivity + + definition EM_up {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ (succ n)] X ≃* G) + : Ω[succ n] (Ω X) ≃* G := + !loopn_succ_in⁻¹ᵉ* ⬝e* e + + definition is_homomorphism_EM_up {G : CommGroup} {X : Type*} {n : ℕ} + (e : Ω[succ (succ n)] X ≃* G) + (r : Π(p q : Ω[succ (succ n)] X), e (p ⬝ q) = e p * e q) + (p q : Ω[succ n] (Ω X)) : EM_up e (p ⬝ q) = EM_up e p * EM_up e q := + begin + refine _ ⬝ !r, apply ap e, esimp, apply apn_con + end + + definition EMadd1_pmap [unfold 8] {G : CommGroup} {X : Type*} (n : ℕ) + (e : Ω[succ n] X ≃* G) + (r : Πp q, e (p ⬝ q) = e p * e q) + [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n →* X := + begin + revert X e r H1 H2, induction n with n f: intro X e r H1 H2, + { exact EM1_pmap e⁻¹ᵉ* (equiv.inv_preserve_binary e concat mul r) }, + rewrite [EMadd1_succ], + exact ptrunc.elim ((succ n).+1) + (psusp.elim (f _ (EM_up e) (is_homomorphism_EM_up e r) _ _)), + end + + definition EMadd1_pmap_succ {G : CommGroup} {X : Type*} (n : ℕ) (e : Ω[succ (succ n)] X ≃* G) + r [H1 : is_conn (succ n) X] [H2 : is_trunc ((succ n).+1) X] : EMadd1_pmap (succ n) e r = + ptrunc.elim ((succ n).+1) (psusp.elim (EMadd1_pmap n (EM_up e) (is_homomorphism_EM_up e r))) := + by reflexivity + + definition loop_EMadd1_pmap {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ (succ n)] X ≃* G) + (r : Πp q, e (p ⬝ q) = e p * e q) + [H1 : is_conn (succ n) X] [H2 : is_trunc ((succ n).+1) X] : + Ω→(EMadd1_pmap (succ n) e r) ∘* loop_EMadd1 G n ~* + EMadd1_pmap n (EM_up e) (is_homomorphism_EM_up e r) := + begin + cases n with n, + { apply hopf_delooping_elim }, + { refine !passoc⁻¹* ⬝* _, + rewrite [EMadd1_pmap_succ (succ n)], + refine pwhisker_right _ !ap1_ptrunc_elim ⬝* _, + refine !passoc⁻¹* ⬝* _, + refine pwhisker_right _ (ptrunc_elim_freudenthal_pequiv + (succ n) (succ (succ n)) (add_mul_le_mul_add n 1 1) _) ⬝* _, + reflexivity } + end + + definition loopn_EMadd1_pmap' {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃* G) + (r : Πp q, e (p ⬝ q) = e p * e q) + [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : + Ω→[succ n](EMadd1_pmap n e r) ∘* loopn_EMadd1 G n ~* e⁻¹ᵉ* := + begin + revert X e r H1 H2, induction n with n IH: intro X e r H1 H2, + { apply loop_EM1_pmap }, + refine pwhisker_left _ !loopn_EMadd1_succ ⬝* _, + refine !passoc⁻¹* ⬝* _, + refine pwhisker_right _ !loopn_succ_in_inv_natural ⬝* _, + refine !passoc ⬝* _, + refine pwhisker_left _ (!passoc⁻¹* ⬝* + pwhisker_right _ (!apn_pcompose⁻¹* ⬝* apn_phomotopy _ !loop_EMadd1_pmap) ⬝* + !IH ⬝* !pinv_trans_pinv_left) ⬝* _, + apply pinv_pcompose_cancel_left + end + + definition EMadd1_pequiv' {G : CommGroup} {X : Type*} (n : ℕ) (e : Ω[succ n] X ≃* G) + (r : Π(p q : Ω[succ n] X), e (p ⬝ q) = e p * e q) + [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X := + begin + apply pequiv_of_pmap (EMadd1_pmap n e r), + have is_conn 0 (EMadd1 G n), from is_conn_of_le _ (zero_le_of_nat n), + have is_trunc (n.+1) (EMadd1 G n), from !is_trunc_EMadd1, + refine whitehead_principle_pointed (n.+1) _ _, + intro k, apply @nat.lt_by_cases k (succ n): intro H, + { apply @is_equiv_of_is_contr, + do 2 exact trivial_homotopy_group_of_is_conn _ (le_of_lt_succ H)}, + { cases H, esimp, apply is_equiv_trunc_functor, esimp, + apply is_equiv.homotopy_closed, rotate 1, + { symmetry, exact phomotopy_pinv_right_of_phomotopy (loopn_EMadd1_pmap' _ _) }, + apply is_equiv_compose (e⁻¹ᵉ*)}, + { apply @is_equiv_of_is_contr, + do 2 exact trivial_homotopy_group_of_is_trunc _ H} + end + + definition EMadd1_pequiv {G : CommGroup} {X : Type*} (n : ℕ) (e : πg[n+1] X ≃g G) + [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X := + begin + have is_set (Ω[succ n] X), from !is_set_loopn, + apply EMadd1_pequiv' n ((ptrunc_pequiv _ _ _)⁻¹ᵉ* ⬝e* pequiv_of_isomorphism e), + intro p q, esimp, exact to_respect_mul e (tr p) (tr q) + end + + definition EMadd1_pequiv_succ {G : CommGroup} {X : Type*} (n : ℕ) (e : πag[n+2] X ≃g G) + [H1 : is_conn (n.+1) X] [H2 : is_trunc (n.+2) X] : EMadd1 G (succ n) ≃* X := + EMadd1_pequiv (succ n) e + + definition ghomotopy_group_EMadd1 (n : ℕ) : πg[n+1] (EMadd1 G n) ≃g G := + begin + change π₁ (Ω[n] (EMadd1 G n)) ≃g G, + refine homotopy_group_isomorphism_of_pequiv 0 (loopn_EMadd1_pequiv_EM1 G n)⁻¹ᵉ* ⬝g _, + apply fundamental_group_EM1, + end + + definition EMadd1_pequiv_type (X : Type*) (n : ℕ) [is_conn (n+1) X] [is_trunc (n+1+1) X] + : EMadd1 (πag[n+2] X) (succ n) ≃* X := + EMadd1_pequiv_succ n !isomorphism.refl + + /- K(G, n) -/ + definition EM (G : CommGroup) : ℕ → Type* + | 0 := G + | (k+1) := EMadd1 G k + + namespace ops + abbreviation K := @EM + end ops + open ops + + definition homotopy_group_EM (n : ℕ) : π[n] (EM G n) ≃* G := + begin + cases n with n, + { rexact ptrunc_pequiv 0 (G) _}, + { exact pequiv_of_isomorphism (ghomotopy_group_EMadd1 G n)} + end + + definition ghomotopy_group_EM (n : ℕ) : πg[n+1] (EM G (n+1)) ≃g G := + ghomotopy_group_EMadd1 G n + + definition is_conn_EM [instance] (n : ℕ) : is_conn (n.-1) (EM G n) := + begin + cases n with n, + { apply is_conn_minus_one, apply tr, unfold [EM], exact 1}, + { apply is_conn_EMadd1} + end + + definition is_conn_EM_succ [instance] (n : ℕ) : is_conn n (EM G (succ n)) := + is_conn_EM G (succ n) + + definition is_trunc_EM [instance] (n : ℕ) : is_trunc n (EM G n) := + begin + cases n with n, + { unfold [EM], apply semigroup.is_set_carrier}, + { apply is_trunc_EMadd1} + end + + definition loop_EM (n : ℕ) : Ω (K G (succ n)) ≃* K G n := + begin + cases n with n, + { refine _ ⬝e* pequiv_of_isomorphism (fundamental_group_EM1 G), + symmetry, apply ptrunc_pequiv, exact _}, + { exact !loop_EMadd1⁻¹ᵉ* } + end + + open circle int + definition EM_pequiv_circle : K agℤ 1 ≃* S¹* := + EM1_pequiv fundamental_group_of_circle⁻¹ᵍ + + /- Functorial action of Eilenberg-Maclane spaces -/ + + definition EM1_functor [constructor] {G H : Group} (φ : G →g H) : EM1 G →* EM1 H := + begin + fconstructor, + { intro g, induction g, + { exact base }, + { exact pth (φ g) }, + { exact ap pth (to_respect_mul φ g h) ⬝ resp_mul (φ g) (φ h) }}, + { reflexivity } + end + + definition EMadd1_functor [constructor] {G H : CommGroup} (φ : G →g H) (n : ℕ) : + EMadd1 G n →* EMadd1 H n := + begin + induction n with n ψ, + { exact EM1_functor φ }, + { apply ptrunc_functor, apply psusp_functor, exact ψ } + end + + definition EM_functor [unfold 4] {G H : CommGroup} (φ : G →g H) (n : ℕ) : + K G n →* K H n := + begin + cases n with n, + { exact pmap_of_homomorphism φ }, + { exact EMadd1_functor φ n } + end + + -- TODO: (K G n →* K H n) ≃ (G →g H) + + /- Equivalence of Groups and pointed connected 1-truncated types -/ + + definition ptruncconntype10_pequiv (X Y : 1-Type*[0]) (e : π₁ X ≃g π₁ Y) : X ≃* Y := + (EM1_pequiv !isomorphism.refl)⁻¹ᵉ* ⬝e* EM1_pequiv e + + definition EM1_pequiv_ptruncconntype10 (X : 1-Type*[0]) : EM1 (π₁ X) ≃* X := + EM1_pequiv_type X + + definition Group_equiv_ptruncconntype10 [constructor] : Group ≃ 1-Type*[0] := + equiv.MK (λG, ptruncconntype.mk (EM1 G) _ pt !is_conn_EM1) + (λX, π₁ X) + begin intro X, apply ptruncconntype_eq, esimp, exact EM1_pequiv_type X end + begin intro G, apply eq_of_isomorphism, apply fundamental_group_EM1 end + + /- Equivalence of CommGroups and pointed n-connected (n+1)-truncated types (n ≥ 1) -/ + + open trunc_index + definition ptruncconntype_pequiv : Π(n : ℕ) (X Y : (n.+1)-Type*[n]) + (e : πg[n+1] X ≃g πg[n+1] Y), X ≃* Y + | 0 X Y e := ptruncconntype10_pequiv X Y e + | (succ n) X Y e := + begin + refine (EMadd1_pequiv_succ n _)⁻¹ᵉ* ⬝e* EMadd1_pequiv_succ n !isomorphism.refl, + exact e + end + + definition EM1_pequiv_ptruncconntype (n : ℕ) (X : (n+1+1)-Type*[n+1]) : + EMadd1 (πag[n+2] X) (succ n) ≃* X := + EMadd1_pequiv_type X n + + definition CommGroup_equiv_ptruncconntype' [constructor] (n : ℕ) : + CommGroup ≃ (n + 1 + 1)-Type*[n+1] := + equiv.MK + (λG, ptruncconntype.mk (EMadd1 G (n+1)) _ pt _) + (λX, πag[n+2] X) + begin intro X, apply ptruncconntype_eq, apply EMadd1_pequiv_type end + begin intro G, apply CommGroup_eq_of_isomorphism, exact ghomotopy_group_EMadd1 G (n+1) end + + definition CommGroup_equiv_ptruncconntype [constructor] (n : ℕ) : + CommGroup ≃ (n.+2)-Type*[n.+1] := + CommGroup_equiv_ptruncconntype' n + + print axioms CommGroup_equiv_ptruncconntype + +end EMnew diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean index c8fce49..1c15223 100644 --- a/homotopy/cohomology.hlean +++ b/homotopy/cohomology.hlean @@ -6,9 +6,12 @@ Authors: Floris van Doorn Reduced cohomology -/ -import .EM algebra.arrow_group +import .EM algebra.arrow_group .spectrum -open eq spectrum int trunc pointed EM group algebra circle sphere nat +open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops + +definition EM_spectrum /-[constructor]-/ (G : CommGroup) : spectrum := +spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*) definition cohomology (X : Type*) (Y : spectrum) (n : ℤ) : CommGroup := CommGroup_pmap X (πag[2] (Y (2+n))) diff --git a/homotopy/degree.hlean b/homotopy/degree.hlean index 5d3d2e2..249b88c 100644 --- a/homotopy/degree.hlean +++ b/homotopy/degree.hlean @@ -51,7 +51,7 @@ namespace sphere end definition deg {n : ℕ} [H : is_succ n] (f : S* n →* S* n) : ℤ := - by induction H with n; exact πnSn n ((π→g[n+1] f) (tr surf)) + by induction H with n; exact πnSn n (π→g[n+1] f (tr surf)) definition deg_id (n : ℕ) [H : is_succ n] : deg (pid (S* n)) = (1 : ℤ) := by induction H with n; @@ -94,7 +94,7 @@ namespace sphere apply eq_one_or_eq_neg_one_of_mul_eq_one (deg f⁻¹ᵉ*), refine !deg_compose⁻¹ ⬝ _, refine deg_phomotopy (pright_inv f) ⬝ _, - apply deg_id, + apply deg_id end end sphere diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean index 85e5285..2bf7e8f 100644 --- a/homotopy/smash.hlean +++ b/homotopy/smash.hlean @@ -244,8 +244,8 @@ namespace smash begin induction x with x x, { refine (pushout.glue pt)⁻¹ }, - { }, - { } + { exact sorry }, + { exact sorry } end definition smash_of_pcofiber_of_smash (x : smash A B) : diff --git a/move_to_lib.hlean b/move_to_lib.hlean index c978b6d..718a77e 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -14,6 +14,23 @@ attribute isomorphism._trans_of_to_hom [unfold 3] attribute homomorphism.struct [unfold 3] attribute pequiv.trans pequiv.symm [constructor] +namespace equiv + + variables {A B : Type} (f : A ≃ B) {a : A} {b : B} + definition to_eq_of_eq_inv (p : a = f⁻¹ b) : f a = b := + ap f p ⬝ right_inv f b + + definition to_eq_of_inv_eq (p : f⁻¹ b = a) : b = f a := + (eq_of_eq_inv p⁻¹)⁻¹ + + definition to_inv_eq_of_eq (p : b = f a) : f⁻¹ b = a := + ap f⁻¹ p ⬝ left_inv f a + + definition to_eq_inv_of_eq (p : f a = b) : a = f⁻¹ b := + (inv_eq_of_eq p⁻¹)⁻¹ + +end equiv open equiv + namespace sigma definition sigma_equiv_sigma_left' [constructor] {A A' : Type} {B : A' → Type} (Hf : A ≃ A') : (Σa, B (Hf a)) ≃ (Σa', B a') := @@ -77,8 +94,124 @@ namespace group abbreviation gid [constructor] := @homomorphism_id + definition comm_group.to_has_mul {A : Type} (H : comm_group A) : has_mul A := _ + local attribute comm_group.to_has_mul [coercion] + + definition comm_group_eq {A : Type} {G H : comm_group A} + (same_mul : Π(g h : A), @mul A G g h = @mul A H g h) + : G = H := + begin + have g_eq : @comm_group.to_group A G = @comm_group.to_group A H, from group_eq same_mul, + cases G with Gm Gs Gh1 G1 Gh2 Gh3 Gi Gh4 Gh5, + cases H with Hm Hs Hh1 H1 Hh2 Hh3 Hi Hh4 Hh5, + have pm : Gm = Hm, from ap (@mul _ ∘ _) g_eq, + have pi : Gi = Hi, from ap (@inv _ ∘ _) g_eq, + have p1 : G1 = H1, from ap (@one _ ∘ _) g_eq, + induction pm, induction pi, induction p1, + have ps : Gs = Hs, from !is_prop.elim, + have ph1 : Gh1 = Hh1, from !is_prop.elim, + have ph2 : Gh2 = Hh2, from !is_prop.elim, + have ph3 : Gh3 = Hh3, from !is_prop.elim, + have ph4 : Gh4 = Hh4, from !is_prop.elim, + have ph5 : Gh5 = Hh5, from !is_prop.elim, + induction ps, induction ph1, induction ph2, induction ph3, induction ph4, induction ph5, + reflexivity + end + + definition comm_group_pathover {A B : Type} {G : comm_group A} {H : comm_group B} {p : A = B} + (resp_mul : Π(g h : A), cast p (g * h) = cast p g * cast p h) : G =[p] H := + begin + induction p, + apply pathover_idp_of_eq, exact comm_group_eq (resp_mul) + end + + definition CommGroup_eq_of_isomorphism {G₁ G₂ : CommGroup} (φ : G₁ ≃g G₂) : G₁ = G₂ := + begin + induction G₁, induction G₂, + apply apd011 CommGroup.mk (ua (equiv_of_isomorphism φ)), + apply comm_group_pathover, + intro g h, exact !cast_ua ⬝ respect_mul φ g h ⬝ ap011 mul !cast_ua⁻¹ !cast_ua⁻¹ + end + end group open group +namespace trunc + + -- TODO: make argument in ptrunc_pequiv implicit + + definition ptr [constructor] (n : ℕ₋₂) (A : Type*) : A →* ptrunc n A := + pmap.mk tr idp + + definition puntrunc [constructor] (n : ℕ₋₂) (A : Type*) [is_trunc n A] : ptrunc n A →* A := + pmap.mk untrunc_of_is_trunc idp + + definition ptrunc.elim [constructor] (n : ℕ₋₂) {X Y : Type*} [is_trunc n Y] (f : X →* Y) : + ptrunc n X →* Y := + pmap.mk (trunc.elim f) (respect_pt f) + + definition ptrunc_elim_ptr [constructor] (n : ℕ₋₂) {X Y : Type*} [is_trunc n Y] (f : X →* Y) : + ptrunc.elim n f ∘* ptr n X ~* f := + begin + fapply phomotopy.mk, + { reflexivity }, + { reflexivity } + end + + definition ptrunc_elim_phomotopy (n : ℕ₋₂) {X Y : Type*} [is_trunc n Y] {f g : X →* Y} + (H : f ~* g) : ptrunc.elim n f ~* ptrunc.elim n g := + begin + fapply phomotopy.mk, + { intro x, induction x with x, exact H x }, + { exact to_homotopy_pt H } + end + + definition ap1_ptrunc_functor (n : ℕ₋₂) {A B : Type*} (f : A →* B) : + Ω→ (ptrunc_functor (n.+1) f) ∘* (loop_ptrunc_pequiv n A)⁻¹ᵉ* ~* + (loop_ptrunc_pequiv n B)⁻¹ᵉ* ∘* ptrunc_functor n (Ω→ f) := + begin + fapply phomotopy.mk, + { intro p, induction p with p, + refine (!ap_inv⁻¹ ◾ !ap_compose⁻¹ ◾ idp) ⬝ _ ⬝ !ap_con⁻¹, + apply whisker_right, refine _ ⬝ !ap_con⁻¹, exact whisker_left _ !ap_compose }, + { induction B with B b, induction f with f p, esimp at f, esimp at p, induction p, reflexivity } + end + + definition ap1_ptrunc_elim (n : ℕ₋₂) {A B : Type*} (f : A →* B) [is_trunc (n.+1) B] : + Ω→ (ptrunc.elim (n.+1) f) ∘* (loop_ptrunc_pequiv n A)⁻¹ᵉ* ~* + ptrunc.elim n (Ω→ f) := + begin + fapply phomotopy.mk, + { intro p, induction p with p, exact idp ◾ !ap_compose⁻¹ ◾ idp }, + { reflexivity } + end + + definition ap1_ptr (n : ℕ₋₂) (A : Type*) : + Ω→ (ptr (n.+1) A) ~* (loop_ptrunc_pequiv n A)⁻¹ᵉ* ∘* ptr n (Ω A) := + begin + fapply phomotopy.mk, + { intro p, apply idp_con }, + { reflexivity } + end + + -- definition ap1_ptr' (n : ℕ₋₂) (A : Type*) : + -- loop_ptrunc_pequiv n A ∘* Ω→ (ptr (n.+1) A) ~* ptr n (Ω A) := + -- begin + -- fapply phomotopy.mk, + -- { intro p, refine ap trunc.encode !idp_con ⬝ _, esimp, }, + -- { reflexivity } + -- end + + definition ptrunc_elim_ptrunc_functor (n : ℕ₋₂) {A B C : Type*} (g : B →* C) (f : A →* B) + [is_trunc n C] : + ptrunc.elim n g ∘* ptrunc_functor n f ~* ptrunc.elim n (g ∘* f) := + begin + fapply phomotopy.mk, + { intro x, induction x with a, reflexivity }, + { esimp, exact !idp_con ⬝ whisker_right !ap_compose _ }, + end + +end trunc open trunc + namespace pi -- move to types.arrow definition pmap_eq_idp {X Y : Type*} (f : X →* Y) : @@ -218,6 +351,73 @@ namespace pointed infixr ` ∘*ᵉ `:60 := pequiv_compose + definition pcompose2 {A B C : Type*} {g g' : B →* C} {f f' : A →* B} (p : f ~* f') (q : g ~* g') : + g ∘* f ~* g' ∘* f' := + pwhisker_right f q ⬝* pwhisker_left g' p + + infixr ` ◾* `:80 := pcompose2 + + definition phomotopy_pinv_of_phomotopy_pid {A B : Type*} {f : A →* B} {g : B ≃* A} + (p : g ∘* f ~* pid A) : f ~* g⁻¹ᵉ* := + phomotopy_pinv_left_of_phomotopy p ⬝* !pcompose_pid + + definition phomotopy_pinv_of_phomotopy_pid' {A B : Type*} {f : A →* B} {g : B ≃* A} + (p : f ∘* g ~* pid B) : f ~* g⁻¹ᵉ* := + phomotopy_pinv_right_of_phomotopy p ⬝* !pid_pcompose + + definition pinv_phomotopy_of_pid_phomotopy {A B : Type*} {f : A →* B} {g : B ≃* A} + (p : pid A ~* g ∘* f) : g⁻¹ᵉ* ~* f := + (phomotopy_pinv_of_phomotopy_pid p⁻¹*)⁻¹* + + definition pinv_phomotopy_of_pid_phomotopy' {A B : Type*} {f : A →* B} {g : B ≃* A} + (p : pid B ~* f ∘* g) : g⁻¹ᵉ* ~* f := + (phomotopy_pinv_of_phomotopy_pid' p⁻¹*)⁻¹* + + definition pinv_pinv {A B : Type*} (f : A ≃* B) : (f⁻¹ᵉ*)⁻¹ᵉ* ~* f := + (phomotopy_pinv_of_phomotopy_pid (pleft_inv f))⁻¹* + + definition pinv2 {A B : Type*} {f f' : A ≃* B} (p : f ~* f') : f⁻¹ᵉ* ~* f'⁻¹ᵉ* := + phomotopy_pinv_of_phomotopy_pid (pinv_right_phomotopy_of_phomotopy (!pid_pcompose ⬝* p)⁻¹*) + + postfix [parsing_only] `⁻²*`:(max+10) := pinv2 + + definition trans_pinv {A B C : Type*} (f : A ≃* B) (g : B ≃* C) : + (f ⬝e* g)⁻¹ᵉ* ~* f⁻¹ᵉ* ∘* g⁻¹ᵉ* := + begin + refine (phomotopy_pinv_of_phomotopy_pid _)⁻¹*, + refine !passoc ⬝* _, + refine pwhisker_left _ (!passoc⁻¹* ⬝* pwhisker_right _ !pright_inv ⬝* !pid_pcompose) ⬝* _, + apply pright_inv + end + + definition pinv_trans_pinv_left {A B C : Type*} (f : B ≃* A) (g : B ≃* C) : + (f⁻¹ᵉ* ⬝e* g)⁻¹ᵉ* ~* f ∘* g⁻¹ᵉ* := + !trans_pinv ⬝* pwhisker_right _ !pinv_pinv + + definition pinv_trans_pinv_right {A B C : Type*} (f : A ≃* B) (g : C ≃* B) : + (f ⬝e* g⁻¹ᵉ*)⁻¹ᵉ* ~* f⁻¹ᵉ* ∘* g := + !trans_pinv ⬝* pwhisker_left _ !pinv_pinv + + definition pinv_trans_pinv_pinv {A B C : Type*} (f : B ≃* A) (g : C ≃* B) : + (f⁻¹ᵉ* ⬝e* g⁻¹ᵉ*)⁻¹ᵉ* ~* f ∘* g := + !trans_pinv ⬝* !pinv_pinv ◾* !pinv_pinv + + definition pinv_pcompose_cancel_left {A B C : Type*} (g : B ≃* C) (f : A →* B) : + g⁻¹ᵉ* ∘* (g ∘* f) ~* f := + !passoc⁻¹* ⬝* pwhisker_right f !pleft_inv ⬝* !pid_pcompose + + definition pcompose_pinv_cancel_left {A B C : Type*} (g : C ≃* B) (f : A →* B) : + g ∘* (g⁻¹ᵉ* ∘* f) ~* f := + !passoc⁻¹* ⬝* pwhisker_right f !pright_inv ⬝* !pid_pcompose + + definition pinv_pcompose_cancel_right {A B C : Type*} (g : B →* C) (f : B ≃* A) : + (g ∘* f⁻¹ᵉ*) ∘* f ~* g := + !passoc ⬝* pwhisker_left g !pleft_inv ⬝* !pcompose_pid + + definition pcompose_pinv_cancel_right {A B C : Type*} (g : B →* C) (f : A ≃* B) : + (g ∘* f) ∘* f⁻¹ᵉ* ~* g := + !passoc ⬝* pwhisker_left g !pright_inv ⬝* !pcompose_pid + definition pmap.sigma_char [constructor] {A B : Type*} : (A →* B) ≃ Σ(f : A → B), f pt = pt := begin fapply equiv.MK : intros f, @@ -270,31 +470,6 @@ namespace pointed ... -/ ≃ (A →* Ω B) : pmap.sigma_char) (by reflexivity) - -- definition ppcompose_left {A B C : Type*} (g : B →* C) : ppmap A B →* ppmap A C := - -- pmap.mk (pcompose g) (eq_of_phomotopy (phomotopy.mk (λa, resp_pt g) (idp_con _)⁻¹)) - - -- definition is_equiv_ppcompose_left [instance] {A B C : Type*} (g : B →* C) [H : is_equiv g] : is_equiv (@ppcompose_left A B C g) := - -- begin - -- fapply is_equiv.adjointify, - -- { exact (ppcompose_left (pequiv_of_pmap g H)⁻¹ᵉ*) }, - -- all_goals (intros f; esimp; apply eq_of_phomotopy), - -- { exact calc g ∘* ((pequiv_of_pmap g H)⁻¹ᵉ* ∘* f) ~* (g ∘* (pequiv_of_pmap g H)⁻¹ᵉ*) ∘* f : passoc - -- ... ~* pid _ ∘* f : pwhisker_right f (pright_inv (pequiv_of_pmap g H)) - -- ... ~* f : pid_pcompose f }, - -- { exact calc (pequiv_of_pmap g H)⁻¹ᵉ* ∘* (g ∘* f) ~* ((pequiv_of_pmap g H)⁻¹ᵉ* ∘* g) ∘* f : passoc - -- ... ~* pid _ ∘* f : pwhisker_right f (pleft_inv (pequiv_of_pmap g H)) - -- ... ~* f : pid_pcompose f } - -- end - - -- definition pequiv_ppcompose_left {A B C : Type*} (g : B ≃* C) : ppmap A B ≃* ppmap A C := - -- pequiv_of_pmap (ppcompose_left g) _ - - -- definition pcompose_pconst {A B C : Type*} (f : B →* C) : f ∘* pconst A B ~* pconst A C := - -- phomotopy.mk (λa, respect_pt f) (idp_con _)⁻¹ - - -- definition pconst_pcompose {A B C : Type*} (f : A →* B) : pconst B C ∘* f ~* pconst A C := - -- phomotopy.mk (λa, rfl) (ap_constant _ _)⁻¹ - definition ap1_pconst (A B : Type*) : Ω→(pconst A B) ~* pconst (Ω A) (Ω B) := phomotopy.mk (λp, idp_con _ ⬝ ap_constant p pt) rfl @@ -470,6 +645,18 @@ namespace susp { exact psusp_functor g } end + definition iterate_psusp_succ_in (n : ℕ) (A : Type*) : + iterate_psusp (succ n) A ≃* iterate_psusp n (psusp A) := + begin + induction n with n IH, + { reflexivity}, + { exact psusp_equiv IH} + end + + definition is_conn_psusp [instance] (n : trunc_index) (A : Type*) + [H : is_conn n A] : is_conn (n .+1) (psusp A) := + is_conn_susp n A + end susp namespace is_conn -- homotopy.connectedness @@ -674,26 +861,46 @@ namespace new_susp { reflexivity } end + definition psusp.elim [constructor] {X Y : Type*} (f : X →* Ω Y) : psusp X →* Y := + loop_psusp_counit Y ∘* psusp_functor f + + definition loop_psusp_intro [constructor] {X Y : Type*} (f : psusp X →* Y) : X →* Ω Y := + ap1 f ∘* loop_psusp_unit X + + definition psusp_adjoint_loop_right_inv {X Y : Type*} (g : X →* Ω Y) : + loop_psusp_intro (psusp.elim g) ~* g := + begin + refine !pwhisker_right !ap1_pcompose ⬝* _, + refine !passoc ⬝* _, + refine !pwhisker_left !loop_psusp_unit_natural⁻¹* ⬝* _, + refine !passoc⁻¹* ⬝* _, + refine !pwhisker_right !loop_psusp_counit_unit ⬝* _, + apply pid_pcompose + end + + definition psusp_adjoint_loop_left_inv {X Y : Type*} (f : psusp X →* Y) : + psusp.elim (loop_psusp_intro f) ~* f := + begin + refine !pwhisker_left !psusp_functor_compose ⬝* _, + refine !passoc⁻¹* ⬝* _, + refine !pwhisker_right !loop_psusp_counit_natural⁻¹* ⬝* _, + refine !passoc ⬝* _, + refine !pwhisker_left !loop_psusp_unit_counit ⬝* _, + apply pcompose_pid + end + + definition ap1_psusp_elim {A : Type*} {X : Type*} (p : A →* Ω X) : + Ω→(psusp.elim p) ∘* loop_psusp_unit A ~* p := + psusp_adjoint_loop_right_inv p + -- TODO: rename to psusp_adjoint_loop (also in above lemmas) definition psusp_adjoint_loop_unpointed [constructor] (X Y : Type*) : psusp X →* Y ≃ X →* Ω Y := begin fapply equiv.MK, - { intro f, exact ap1 f ∘* loop_psusp_unit X }, - { intro g, exact loop_psusp_counit Y ∘* psusp_functor g }, - { intro g, apply eq_of_phomotopy, esimp, - refine !pwhisker_right !ap1_pcompose ⬝* _, - refine !passoc ⬝* _, - refine !pwhisker_left !loop_psusp_unit_natural⁻¹* ⬝* _, - refine !passoc⁻¹* ⬝* _, - refine !pwhisker_right !loop_psusp_counit_unit ⬝* _, - apply pid_pcompose }, - { intro f, apply eq_of_phomotopy, esimp, - refine !pwhisker_left !psusp_functor_compose ⬝* _, - refine !passoc⁻¹* ⬝* _, - refine !pwhisker_right !loop_psusp_counit_natural⁻¹* ⬝* _, - refine !passoc ⬝* _, - refine !pwhisker_left !loop_psusp_unit_counit ⬝* _, - apply pcompose_pid }, + { exact loop_psusp_intro }, + { exact psusp.elim }, + { intro g, apply eq_of_phomotopy, exact psusp_adjoint_loop_right_inv g }, + { intro f, apply eq_of_phomotopy, exact psusp_adjoint_loop_left_inv f } end definition psusp_adjoint_loop_pconst (X Y : Type*) : @@ -710,8 +917,120 @@ namespace new_susp apply psusp_adjoint_loop_pconst end + -- in freudenthal + open trunc + local attribute ptrunc_pequiv_ptrunc_of_le [constructor] + definition to_pmap_freudenthal_pequiv {A : Type*} (n k : ℕ) [is_conn n A] (H : k ≤ 2 * n) + : freudenthal_pequiv A H ~* ptrunc_functor k (loop_psusp_unit A) := + begin + fapply phomotopy.mk, + { intro x, induction x with a, reflexivity }, + { refine !idp_con ⬝ _, refine _ ⬝ ap02 _ !idp_con⁻¹, refine _ ⬝ !ap_compose, apply ap_compose } + end + + definition ptrunc_elim_freudenthal_pequiv {A B : Type*} (n k : ℕ) [is_conn n A] (H : k ≤ 2 * n) + (f : A →* Ω B) [is_trunc (k.+1) (B)] : + ptrunc.elim k (Ω→ (psusp.elim f)) ∘* freudenthal_pequiv A H ~* ptrunc.elim k f := + begin + refine pwhisker_left _ !to_pmap_freudenthal_pequiv ⬝* _, + refine !ptrunc_elim_ptrunc_functor ⬝* _, + exact ptrunc_elim_phomotopy k !ap1_psusp_elim, + end + + open susp + definition iterated_freudenthal_pequiv (A : Type*) {n k m : ℕ} [HA : is_conn n A] (H : k ≤ 2 * n) + : ptrunc k A ≃* ptrunc k (Ω[m] (iterate_psusp m A)) := + begin + revert A n k HA H, induction m with m IH: intro A n k HA H, + { reflexivity}, + { have H2 : succ k ≤ 2 * succ n, + from calc + succ k ≤ succ (2 * n) : succ_le_succ H + ... ≤ 2 * succ n : self_le_succ, + exact calc + ptrunc k A ≃* ptrunc k (Ω (psusp A)) : freudenthal_pequiv A H + ... ≃* Ω (ptrunc (succ k) (psusp A)) : loop_ptrunc_pequiv + ... ≃* Ω (ptrunc (succ k) (Ω[m] (iterate_psusp m (psusp A)))) : + loop_pequiv_loop (IH (psusp A) (succ n) (succ k) _ H2) + ... ≃* ptrunc k (Ω[succ m] (iterate_psusp m (psusp A))) : loop_ptrunc_pequiv + ... ≃* ptrunc k (Ω[succ m] (iterate_psusp (succ m) A)) : + ptrunc_pequiv_ptrunc _ (loopn_pequiv_loopn _ !iterate_psusp_succ_in)} + end + + definition iterate_psusp_adjoint_loopn [constructor] (X Y : Type*) (n : ℕ) : + ppmap (iterate_psusp n X) Y ≃* ppmap X (Ω[n] Y) := + begin + revert X Y, induction n with n IH: intro X Y, + { reflexivity }, + { refine !psusp_adjoint_loop ⬝e* !IH ⬝e* _, apply pequiv_ppcompose_left, + symmetry, apply loopn_succ_in } + end + end new_susp open new_susp +namespace hopf + + definition my_transport_codes_merid.{u} (A : Type.{u}) [T : is_trunc 1 A] [K : is_conn 0 A] + [H : h_space A] (a a' : A) : transport (hopf A) (merid a) a' = a * a' :> A := + ap10 (elim_type_merid _ _ _ a) a' + + definition my_transport_codes_merid_one_inv.{u} (A : Type.{u}) [T : is_trunc 1 A] + [K : is_conn 0 A] [H : h_space A] (a : A) : transport (hopf A) (merid 1)⁻¹ a = a := + ap10 (elim_type_merid_inv _ _ _ 1) a ⬝ + begin apply to_inv_eq_of_eq, esimp, refine !one_mul⁻¹ end + + definition my_encode_decode' (A : Type) [T : is_trunc 1 A] [K : is_conn 0 A] + [H : h_space A] (a : A) : encode A (decode' A a) = a := + begin + esimp [encode, decode', encode₀], +-- refine ap (λp, transport (hopf A) p a) _ ⬝ _ + refine !con_tr ⬝ _, + refine (ap (transport _ _) !my_transport_codes_merid ⬝ !my_transport_codes_merid_one_inv) ⬝ _, + apply mul_one + end + + definition to_pmap_main_lemma_point_pinv (A : Type) [T : is_trunc 1 A] [K : is_conn 0 A] + [H : h_space A] (coh : one_mul 1 = mul_one 1 :> (1 * 1 = 1 :> A)) + : (main_lemma_point A coh)⁻¹ᵉ* ~* !ptr ∘* loop_psusp_unit (pointed.MK A 1) := + begin + apply pinv_phomotopy_of_pid_phomotopy, + fapply phomotopy.mk, + { intro a, exact (my_encode_decode' A a)⁻¹ }, + { esimp [main_lemma_point, main_lemma, encode], + apply inv_con_eq_of_eq_con, + refine !ap_compose'⁻¹ ⬝ _, esimp, + esimp [my_encode_decode'], + unfold [encode₀], + exact sorry + -- assert p : Π(A : Type) (a a' : A) (p : a = a') (B : A → Type) (b : B a), + -- ap (λ p, p ▸ b) (con.right_inv p) = con_tr p p⁻¹ b ⬝ (ap (transport B p⁻¹) + -- (transport_codes_merid A b b ⬝ mul_one 1) ⬝ transport_codes_merid_one_inv A 1), + + } + end + + definition to_pmap_delooping_pinv (A : Type) [T : is_trunc 1 A] [K : is_conn 0 A] [H : h_space A] + (coh : one_mul 1 = mul_one 1 :> (1 * 1 = 1 :> A)) + : (hopf.delooping A coh)⁻¹ᵉ* ~* Ω→ !ptr ∘* loop_psusp_unit (pointed.MK A 1) := + begin + refine !trans_pinv ⬝* _, + refine pwhisker_left _ !to_pmap_main_lemma_point_pinv ⬝* _, + refine !passoc⁻¹* ⬝* _, + refine pwhisker_right _ !ap1_ptr⁻¹*, + end + + definition hopf_delooping_elim {A : Type} {B : Type*} [T : is_trunc 1 A] [K : is_conn 0 A] + [H : h_space A] (coh : one_mul 1 = mul_one 1 :> (1 * 1 = 1 :> A)) (f : pointed.MK A 1 →* Ω B) + /-[H1 : is_conn 1 B]-/ [H2 : is_trunc 2 B] : + Ω→(ptrunc.elim 2 (psusp.elim f)) ∘* (hopf.delooping A coh)⁻¹ᵉ* ~* f := + begin + refine pwhisker_left _ !to_pmap_delooping_pinv ⬝* _, + refine !passoc⁻¹* ⬝* _, + refine pwhisker_right _ (!ap1_pcompose⁻¹* ⬝* ap1_phomotopy !ptrunc_elim_ptr) ⬝* _, + apply ap1_psusp_elim + end + +end hopf -- this should replace corresponding definitions in homotopy.sphere namespace new_sphere From b08457c77f1b57d21c5b1ca95074951f92293ff4 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 23 Nov 2016 23:54:57 -0500 Subject: [PATCH 5/5] move things to the Lean library, and update after changes in the Lean library --- algebra/arrow_group.hlean | 16 +- algebra/direct_sum.hlean | 18 +- algebra/exact_couple.hlean | 36 +- algebra/free_commutative_group.hlean | 40 +- algebra/free_group.hlean | 2 +- algebra/group_constructions.hlean | 16 +- algebra/module.hlean | 10 +- algebra/product_group.hlean | 12 +- algebra/quotient_group.hlean | 64 +- algebra/subgroup.hlean | 40 +- colim.hlean | 2 +- homotopy/EM.hlean | 317 -------- homotopy/EMnew.hlean | 518 ------------- homotopy/cohomology.hlean | 18 +- homotopy/degree.hlean | 2 +- homotopy/sample.hlean | 2 +- homotopy/smash.hlean | 202 +---- homotopy/spectrum.hlean | 24 +- homotopy/spherical_fibrations.hlean | 2 +- move_to_lib.hlean | 1038 +------------------------- pointed_pi.hlean | 15 +- 21 files changed, 200 insertions(+), 2194 deletions(-) delete mode 100644 homotopy/EM.hlean delete mode 100644 homotopy/EMnew.hlean diff --git a/algebra/arrow_group.hlean b/algebra/arrow_group.hlean index d90f763..cfaa89e 100644 --- a/algebra/arrow_group.hlean +++ b/algebra/arrow_group.hlean @@ -21,12 +21,12 @@ namespace group definition Group_arrow (A : Type) (G : Group) : Group := Group.mk (A → G) _ - definition comm_group_arrow [instance] (A B : Type) [comm_group B] : comm_group (A → B) := - ⦃comm_group, group_arrow A B, + definition ab_group_arrow [instance] (A B : Type) [ab_group B] : ab_group (A → B) := + ⦃ab_group, group_arrow A B, mul_comm := by intros; apply eq_of_homotopy; intro a; apply mul.comm⦄ - definition CommGroup_arrow (A : Type) (G : CommGroup) : CommGroup := - CommGroup.mk (A → G) _ + definition AbGroup_arrow (A : Type) (G : AbGroup) : AbGroup := + AbGroup.mk (A → G) _ definition pgroup_ppmap [instance] (A B : Type*) [pgroup B] : pgroup (ppmap A B) := begin @@ -44,12 +44,12 @@ namespace group definition Group_pmap (A : Type*) (G : Group) : Group := Group_of_pgroup (ppmap A (pType_of_Group G)) - definition CommGroup_pmap (A : Type*) (G : CommGroup) : CommGroup := - CommGroup.mk (A →* pType_of_Group G) - ⦃ comm_group, Group.struct (Group_pmap A G), + definition AbGroup_pmap (A : Type*) (G : AbGroup) : AbGroup := + AbGroup.mk (A →* pType_of_Group G) + ⦃ ab_group, Group.struct (Group_pmap A G), mul_comm := by intro f g; apply pmap_eq_of_homotopy; intro a; apply mul.comm ⦄ - definition Group_pmap_homomorphism [constructor] {A A' : Type*} (f : A' →* A) (G : CommGroup) : + definition Group_pmap_homomorphism [constructor] {A A' : Type*} (f : A' →* A) (G : AbGroup) : Group_pmap A G →g Group_pmap A' G := begin fapply homomorphism.mk, diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean index 46ea343..074d1d1 100644 --- a/algebra/direct_sum.hlean +++ b/algebra/direct_sum.hlean @@ -13,21 +13,21 @@ open eq algebra is_trunc set_quotient relation sigma prod sum list trunc functio namespace group variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G} - {A B : CommGroup} + {A B : AbGroup} variables (X : Set) {l l' : list (X ⊎ X)} section - parameters {I : Set} (Y : I → CommGroup) - variables {A' : CommGroup} + parameters {I : Set} (Y : I → AbGroup) + variables {A' : AbGroup} - definition dirsum_carrier : CommGroup := free_comm_group (trunctype.mk (Σi, Y i) _) - local abbreviation ι [constructor] := @free_comm_group_inclusion + definition dirsum_carrier : AbGroup := free_ab_group (trunctype.mk (Σi, Y i) _) + local abbreviation ι [constructor] := @free_ab_group_inclusion inductive dirsum_rel : dirsum_carrier → Type := | rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ * ι ⟨i, y₂⟩ * (ι ⟨i, y₁ * y₂⟩)⁻¹) - definition dirsum : CommGroup := quotient_comm_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥) + definition dirsum : AbGroup := quotient_ab_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥) -- definition dirsum_carrier_incl [constructor] (i : I) : Y i →g dirsum_carrier := @@ -36,7 +36,7 @@ namespace group begin intro g h, symmetry, apply gqg_eq_of_rel, apply tr, apply dirsum_rel.rmk end definition dirsum_elim_resp_quotient (f : Πi, Y i →g A') (g : dirsum_carrier) - (r : ∥dirsum_rel g∥) : free_comm_group_elim (λv, f v.1 v.2) g = 1 := + (r : ∥dirsum_rel g∥) : free_ab_group_elim (λv, f v.1 v.2) g = 1 := begin induction r with r, induction r, rewrite [to_respect_mul, to_respect_inv], apply mul_inv_eq_of_eq_mul, @@ -44,7 +44,7 @@ namespace group end definition dirsum_elim [constructor] (f : Πi, Y i →g A') : dirsum →g A' := - gqg_elim _ (free_comm_group_elim (λv, f v.1 v.2)) (dirsum_elim_resp_quotient f) + gqg_elim _ (free_ab_group_elim (λv, f v.1 v.2)) (dirsum_elim_resp_quotient f) definition dirsum_elim_compute (f : Πi, Y i →g A') (i : I) : dirsum_elim f ∘g dirsum_incl i ~ f i := @@ -56,7 +56,7 @@ namespace group (H : Πi, k ∘g dirsum_incl i ~ f i) : k ~ dirsum_elim f := begin apply gqg_elim_unique, - apply free_comm_group_elim_unique, + apply free_ab_group_elim_unique, intro x, induction x with i y, exact H i y end diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean index 68507ce..78f14a5 100644 --- a/algebra/exact_couple.hlean +++ b/algebra/exact_couple.hlean @@ -11,50 +11,50 @@ import algebra.group_theory hit.set_quotient types.sigma types.list types.sum .q open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function group trunc equiv -structure is_exact {A B C : CommGroup} (f : A →g B) (g : B →g C) := +structure is_exact {A B C : AbGroup} (f : A →g B) (g : B →g C) := ( im_in_ker : Π(a:A), g (f a) = 1) - ( ker_in_im : Π(b:B), (g b = 1) → ∃(a:A), f a = b) + ( ker_in_im : Π(b:B), (g b = 1) → ∃(a:A), f a = b) -definition is_differential {B : CommGroup} (d : B →g B) := Π(b:B), d (d b) = 1 +definition is_differential {B : AbGroup} (d : B →g B) := Π(b:B), d (d b) = 1 -definition image_subgroup_of_diff {B : CommGroup} (d : B →g B) (H : is_differential d) : subgroup_rel (comm_kernel d) := +definition image_subgroup_of_diff {B : AbGroup} (d : B →g B) (H : is_differential d) : subgroup_rel (ab_kernel d) := subgroup_rel_of_subgroup (image_subgroup d) (kernel_subgroup d) begin - intro g p, + intro g p, induction p with f, induction f with h p, - rewrite [p⁻¹], + rewrite [p⁻¹], esimp, - exact H h + exact H h end -definition homology {B : CommGroup} (d : B →g B) (H : is_differential d) : CommGroup := - @quotient_comm_group (comm_kernel d) (image_subgroup_of_diff d H) +definition homology {B : AbGroup} (d : B →g B) (H : is_differential d) : AbGroup := + @quotient_ab_group (ab_kernel d) (image_subgroup_of_diff d H) -structure exact_couple (A B : CommGroup) : Type := +structure exact_couple (A B : AbGroup) : Type := ( i : A →g A) (j : A →g B) (k : B →g A) ( exact_ij : is_exact i j) ( exact_jk : is_exact j k) ( exact_ki : is_exact k i) -definition differential {A B : CommGroup} (EC : exact_couple A B) : B →g B := +definition differential {A B : AbGroup} (EC : exact_couple A B) : B →g B := (exact_couple.j EC) ∘g (exact_couple.k EC) -definition differential_is_differential {A B : CommGroup} (EC : exact_couple A B) : is_differential (differential EC) := +definition differential_is_differential {A B : AbGroup} (EC : exact_couple A B) : is_differential (differential EC) := begin - induction EC, - induction exact_jk, + induction EC, + induction exact_jk, intro b, exact (ap (group_fun j) (im_in_ker (group_fun k b))) ⬝ (respect_one j) end section derived_couple - variables {A B : CommGroup} (EC : exact_couple A B) + variables {A B : AbGroup} (EC : exact_couple A B) -definition derived_couple_A : CommGroup := - comm_subgroup (image_subgroup (exact_couple.i EC)) +definition derived_couple_A : AbGroup := + ab_subgroup (image_subgroup (exact_couple.i EC)) -definition derived_couple_B : CommGroup := +definition derived_couple_B : AbGroup := homology (differential EC) (differential_is_differential EC) definition derived_couple_i : derived_couple_A EC →g derived_couple_A EC := diff --git a/algebra/free_commutative_group.hlean b/algebra/free_commutative_group.hlean index 26d9af7..a459968 100644 --- a/algebra/free_commutative_group.hlean +++ b/algebra/free_commutative_group.hlean @@ -12,12 +12,12 @@ open eq algebra is_trunc set_quotient relation sigma sigma.ops prod sum list tru namespace group - variables {G G' : Group} {g g' h h' k : G} {A B : CommGroup} + variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup} variables (X : Set) {l l' : list (X ⊎ X)} - /- Free Commutative Group of a set -/ - namespace free_comm_group + /- Free Abelian Group of a set -/ + namespace free_ab_group inductive fcg_rel : list (X ⊎ X) → list (X ⊎ X) → Type := | rrefl : Πl, fcg_rel l l @@ -133,22 +133,22 @@ namespace group rewrite [-append_concat], apply IH} end end - end free_comm_group open free_comm_group + end free_ab_group open free_ab_group variables (X) - definition group_free_comm_group [constructor] : comm_group (fcg_carrier X) := - comm_group.mk fcg_mul _ fcg_mul_assoc fcg_one fcg_one_mul fcg_mul_one + definition group_free_ab_group [constructor] : ab_group (fcg_carrier X) := + ab_group.mk fcg_mul _ fcg_mul_assoc fcg_one fcg_one_mul fcg_mul_one fcg_inv fcg_mul_left_inv fcg_mul_comm - definition free_comm_group [constructor] : CommGroup := - CommGroup.mk _ (group_free_comm_group X) + definition free_ab_group [constructor] : AbGroup := + AbGroup.mk _ (group_free_ab_group X) /- The universal property of the free commutative group -/ variables {X A} - definition free_comm_group_inclusion [constructor] (x : X) : free_comm_group X := + definition free_ab_group_inclusion [constructor] (x : X) : free_ab_group X := class_of [inl x] - theorem fgh_helper_respect_comm_rel (f : X → A) (r : fcg_rel X l l') + theorem fgh_helper_respect_fcg_rel (f : X → A) (r : fcg_rel X l l') : Π(g : A), foldl (fgh_helper f) g l = foldl (fgh_helper f) g l' := begin induction r with l x x x y l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂: intro g, @@ -160,22 +160,22 @@ namespace group { exact !IH₁ ⬝ !IH₂} end - definition free_comm_group_elim [constructor] (f : X → A) : free_comm_group X →g A := + definition free_ab_group_elim [constructor] (f : X → A) : free_ab_group X →g A := begin fapply homomorphism.mk, { intro g, refine set_quotient.elim _ _ g, { intro l, exact foldl (fgh_helper f) 1 l}, { intro l l' r, esimp at *, refine trunc.rec _ r, clear r, intro r, - exact fgh_helper_respect_comm_rel f r 1}}, + exact fgh_helper_respect_fcg_rel f r 1}}, { refine set_quotient.rec_prop _, intro l, refine set_quotient.rec_prop _, intro l', esimp, refine !foldl_append ⬝ _, esimp, apply fgh_helper_mul} end - definition fn_of_free_comm_group_elim [unfold_full] (φ : free_comm_group X →g A) : X → A := - φ ∘ free_comm_group_inclusion + definition fn_of_free_ab_group_elim [unfold_full] (φ : free_ab_group X →g A) : X → A := + φ ∘ free_ab_group_inclusion - definition free_comm_group_elim_unique [constructor] (f : X → A) (k : free_comm_group X →g A) - (H : k ∘ free_comm_group_inclusion ~ f) : k ~ free_comm_group_elim f := + definition free_ab_group_elim_unique [constructor] (f : X → A) (k : free_ab_group X →g A) + (H : k ∘ free_ab_group_inclusion ~ f) : k ~ free_ab_group_elim f := begin refine set_quotient.rec_prop _, intro l, esimp, induction l with s l IH, @@ -187,13 +187,13 @@ namespace group end variables (X A) - definition free_comm_group_elim_equiv_fn [constructor] : (free_comm_group X →g A) ≃ (X → A) := + definition free_ab_group_elim_equiv_fn [constructor] : (free_ab_group X →g A) ≃ (X → A) := begin fapply equiv.MK, - { exact fn_of_free_comm_group_elim}, - { exact free_comm_group_elim}, + { exact fn_of_free_ab_group_elim}, + { exact free_ab_group_elim}, { intro f, apply eq_of_homotopy, intro x, esimp, unfold [foldl], apply one_mul}, - { intro k, symmetry, apply homomorphism_eq, apply free_comm_group_elim_unique, + { intro k, symmetry, apply homomorphism_eq, apply free_ab_group_elim_unique, reflexivity } end diff --git a/algebra/free_group.hlean b/algebra/free_group.hlean index d502b69..c46d923 100644 --- a/algebra/free_group.hlean +++ b/algebra/free_group.hlean @@ -12,7 +12,7 @@ open eq algebra is_trunc set_quotient relation sigma sigma.ops prod sum list tru namespace group - variables {G G' : Group} {g g' h h' k : G} {A B : CommGroup} + variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup} /- Free Group of a set -/ variables (X : Set) {l l' : list (X ⊎ X)} diff --git a/algebra/group_constructions.hlean b/algebra/group_constructions.hlean index f768db1..d7c9a36 100644 --- a/algebra/group_constructions.hlean +++ b/algebra/group_constructions.hlean @@ -11,29 +11,29 @@ import .free_commutative_group open eq algebra is_trunc sigma sigma.ops prod trunc function equiv namespace group - variables {G G' : Group} {g g' h h' k : G} {A B : CommGroup} + variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup} /- Tensor group (WIP) -/ /- namespace tensor_group variables {A B} - local abbreviation ι := @free_comm_group_inclusion + local abbreviation ι := @free_ab_group_inclusion - inductive tensor_rel_type : free_comm_group (Set_of_Group A ×t Set_of_Group B) → Type := + inductive tensor_rel_type : free_ab_group (Set_of_Group A ×t Set_of_Group B) → Type := | mul_left : Π(a₁ a₂ : A) (b : B), tensor_rel_type (ι (a₁, b) * ι (a₂, b) * (ι (a₁ * a₂, b))⁻¹) | mul_right : Π(a : A) (b₁ b₂ : B), tensor_rel_type (ι (a, b₁) * ι (a, b₂) * (ι (a, b₁ * b₂))⁻¹) open tensor_rel_type - definition tensor_rel' (x : free_comm_group (Set_of_Group A ×t Set_of_Group B)) : Prop := + definition tensor_rel' (x : free_ab_group (Set_of_Group A ×t Set_of_Group B)) : Prop := ∥ tensor_rel_type x ∥ - definition tensor_group_rel (A B : CommGroup) - : normal_subgroup_rel (free_comm_group (Set_of_Group A ×t Set_of_Group B)) := + definition tensor_group_rel (A B : AbGroup) + : normal_subgroup_rel (free_ab_group (Set_of_Group A ×t Set_of_Group B)) := sorry /- relation generated by tensor_rel'-/ - definition tensor_group [constructor] : CommGroup := - quotient_comm_group (tensor_group_rel A B) + definition tensor_group [constructor] : AbGroup := + quotient_ab_group (tensor_group_rel A B) end tensor_group-/ diff --git a/algebra/module.hlean b/algebra/module.hlean index f6496d2..7475fb7 100644 --- a/algebra/module.hlean +++ b/algebra/module.hlean @@ -17,7 +17,7 @@ infixl ` • `:73 := has_scalar.smul /- modules over a ring -/ -structure left_module (R M : Type) [ringR : ring R] extends has_scalar R M, comm_group M renaming +structure left_module (R M : Type) [ringR : ring R] extends has_scalar R M, ab_group M renaming mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero inv→neg mul_left_inv→add_left_inv mul_comm→add_comm := (smul_left_distrib : Π (r : R) (x y : M), smul r (add x y) = (add (smul r x) (smul r y))) @@ -26,12 +26,12 @@ structure left_module (R M : Type) [ringR : ring R] extends has_scalar R M, comm (one_smul : Π x, smul one x = x) /- we make it a class now (and not as part of the structure) to avoid - left_module.to_comm_group to be an instance -/ + left_module.to_ab_group to be an instance -/ attribute left_module [class] -definition add_comm_group_of_left_module [reducible] [trans_instance] (R M : Type) [K : ring R] - [H : left_module R M] : add_comm_group M := -@left_module.to_comm_group R M K H +definition add_ab_group_of_left_module [reducible] [trans_instance] (R M : Type) [K : ring R] + [H : left_module R M] : add_ab_group M := +@left_module.to_ab_group R M K H definition has_scalar_of_left_module [reducible] [trans_instance] (R M : Type) [K : ring R] [H : left_module R M] : has_scalar R M := diff --git a/algebra/product_group.hlean b/algebra/product_group.hlean index c585007..800650f 100644 --- a/algebra/product_group.hlean +++ b/algebra/product_group.hlean @@ -13,7 +13,7 @@ open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum namespace group variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G} - {A B : CommGroup} + {A B : AbGroup} /- Binary products (direct product) of Groups -/ definition product_one [constructor] : G × G' := (one, one) @@ -39,7 +39,7 @@ namespace group theorem product_mul_left_inv (g : G × G') : g⁻¹ * g = 1 := prod_eq !mul.left_inv !mul.left_inv - theorem product_mul_comm {G G' : CommGroup} (g h : G × G') : g * h = h * g := + theorem product_mul_comm {G G' : AbGroup} (g h : G × G') : g * h = h * g := prod_eq !mul.comm !mul.comm end @@ -52,11 +52,11 @@ namespace group definition product [constructor] : Group := Group.mk _ (group_prod G G') - definition comm_group_prod [constructor] (G G' : CommGroup) : comm_group (G × G') := - ⦃comm_group, group_prod G G', mul_comm := product_mul_comm⦄ + definition ab_group_prod [constructor] (G G' : AbGroup) : ab_group (G × G') := + ⦃ab_group, group_prod G G', mul_comm := product_mul_comm⦄ - definition comm_product [constructor] (G G' : CommGroup) : CommGroup := - CommGroup.mk _ (comm_group_prod G G') + definition ab_product [constructor] (G G' : AbGroup) : AbGroup := + AbGroup.mk _ (ab_group_prod G G') infix ` ×g `:30 := group.product diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean index 314ba15..a3d87f0 100644 --- a/algebra/quotient_group.hlean +++ b/algebra/quotient_group.hlean @@ -13,7 +13,7 @@ open eq algebra is_trunc set_quotient relation sigma sigma.ops prod trunc functi namespace group variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G} - variables {A B : CommGroup} + variables {A B : AbGroup} /- Quotient Group -/ @@ -113,7 +113,7 @@ namespace group exact ap class_of !mul.left_inv end - theorem quotient_mul_comm {G : CommGroup} {N : normal_subgroup_rel G} (g h : qg N) + theorem quotient_mul_comm {G : AbGroup} {N : normal_subgroup_rel G} (g h : qg N) : g * h = h * g := begin refine set_quotient.rec_prop _ g, clear g, intro g, @@ -131,18 +131,18 @@ namespace group definition quotient_group [constructor] : Group := Group.mk _ (group_qg N) - definition comm_group_qg [constructor] {G : CommGroup} (N : normal_subgroup_rel G) - : comm_group (qg N) := - ⦃comm_group, group_qg N, mul_comm := quotient_mul_comm⦄ + definition ab_group_qg [constructor] {G : AbGroup} (N : normal_subgroup_rel G) + : ab_group (qg N) := + ⦃ab_group, group_qg N, mul_comm := quotient_mul_comm⦄ - definition quotient_comm_group [constructor] {G : CommGroup} (N : subgroup_rel G) - : CommGroup := - CommGroup.mk _ (comm_group_qg (normal_subgroup_rel_comm N)) + definition quotient_ab_group [constructor] {G : AbGroup} (N : subgroup_rel G) + : AbGroup := + AbGroup.mk _ (ab_group_qg (normal_subgroup_rel_ab N)) definition qg_map [constructor] : G →g quotient_group N := homomorphism.mk class_of (λ g h, idp) - definition comm_gq_map {G : CommGroup} (N : subgroup_rel G) : G →g quotient_comm_group N := + definition ab_gq_map {G : AbGroup} (N : subgroup_rel G) : G →g quotient_ab_group N := begin fapply homomorphism.mk, exact class_of, @@ -166,7 +166,7 @@ namespace group unfold quotient_rel, rewrite e, exact H end - definition comm_gq_map_eq_one {K : subgroup_rel A} (g :A) (H : K g) : comm_gq_map K g = 1 := + definition ab_gq_map_eq_one {K : subgroup_rel A} (g :A) (H : K g) : ab_gq_map K g = 1 := begin apply eq_of_rel, have e : (g * 1⁻¹ = g), @@ -237,17 +237,17 @@ namespace group {fapply is_prop.elimo} } end -definition comm_group_quotient_homomorphism (A B : CommGroup)(K : subgroup_rel A)(L : subgroup_rel B) (f : A →g B) - (p : Π(a:A), K(a) → L(f a)) : quotient_comm_group K →g quotient_comm_group L := +definition ab_group_quotient_homomorphism (A B : AbGroup)(K : subgroup_rel A)(L : subgroup_rel B) (f : A →g B) + (p : Π(a:A), K(a) → L(f a)) : quotient_ab_group K →g quotient_ab_group L := begin fapply quotient_group_elim, - exact (comm_gq_map L) ∘g f, + exact (ab_gq_map L) ∘g f, intro a, intro k, - exact @comm_gq_map_eq_one B L (f a) (p a k), + exact @ab_gq_map_eq_one B L (f a) (p a k), end -definition comm_group_first_iso_thm (A B : CommGroup) (f : A →g B) : quotient_comm_group (kernel_subgroup f) ≃g comm_image f := +definition ab_group_first_iso_thm (A B : AbGroup) (f : A →g B) : quotient_ab_group (kernel_subgroup f) ≃g ab_image f := begin fapply isomorphism.mk, fapply quotient_group_elim, @@ -260,7 +260,7 @@ definition comm_group_first_iso_thm (A B : CommGroup) (f : A →g B) : quotient_ -- show that the above map is injective and surjective. end -definition comm_group_kernel_factor {A B C: CommGroup} (f : A →g B)(g : A →g C){i : C →g B}(H : f = i ∘g g ) +definition ab_group_kernel_factor {A B C: AbGroup} (f : A →g B)(g : A →g C){i : C →g B}(H : f = i ∘g g ) : Π a:A , kernel_subgroup(g)(a) → kernel_subgroup(f)(a) := begin intro a, @@ -271,12 +271,12 @@ definition comm_group_kernel_factor {A B C: CommGroup} (f : A →g B)(g : A →g ... = 1 : respect_one i end -definition comm_group_kernel_equivalent {A B : CommGroup} (C : CommGroup) (f : A →g B)(g : A →g C)(i : C →g B)(H : f = i ∘g g )(K : is_embedding i) +definition ab_group_kernel_equivalent {A B : AbGroup} (C : AbGroup) (f : A →g B)(g : A →g C)(i : C →g B)(H : f = i ∘g g )(K : is_embedding i) : Π a:A , kernel_subgroup(g)(a) ↔ kernel_subgroup(f)(a) := begin intro a, fapply iff.intro, - exact comm_group_kernel_factor f g H a, + exact ab_group_kernel_factor f g H a, intro p, apply @is_injective_of_is_embedding _ _ i _ (g a) 1, exact calc @@ -285,23 +285,23 @@ begin ... = i 1 : (respect_one i)⁻¹ end -definition comm_group_kernel_image_lift (A B : CommGroup) (f : A →g B) +definition ab_group_kernel_image_lift (A B : AbGroup) (f : A →g B) : Π a : A, kernel_subgroup(image_lift(f))(a) ↔ kernel_subgroup(f)(a) := begin - fapply comm_group_kernel_equivalent (comm_image f) (f) (image_lift(f)) (image_incl(f)), + fapply ab_group_kernel_equivalent (ab_image f) (f) (image_lift(f)) (image_incl(f)), exact image_factor f, exact is_embedding_of_is_injective (image_incl_injective(f)), end -definition comm_group_kernel_quotient_to_image {A B : CommGroup} (f : A →g B) - : quotient_comm_group (kernel_subgroup f) →g comm_image (f) := +definition ab_group_kernel_quotient_to_image {A B : AbGroup} (f : A →g B) + : quotient_ab_group (kernel_subgroup f) →g ab_image (f) := begin -fapply quotient_group_elim (image_lift f), intro a, intro p, -apply iff.mpr (comm_group_kernel_image_lift _ _ f a) p +fapply quotient_group_elim (image_lift f), intro a, intro p, +apply iff.mpr (ab_group_kernel_image_lift _ _ f a) p end -definition is_surjective_kernel_quotient_to_image {A B : CommGroup} (f : A →g B) - : is_surjective (comm_group_kernel_quotient_to_image f) := +definition is_surjective_kernel_quotient_to_image {A B : AbGroup} (f : A →g B) + : is_surjective (ab_group_kernel_quotient_to_image f) := begin intro b, exact sorry -- have H : is_surjective (image_lift f) @@ -312,8 +312,8 @@ print iff.mpr section - parameters {A₁ : CommGroup} (S : A₁ → Prop) - variable {A₂ : CommGroup} + parameters {A₁ : AbGroup} (S : A₁ → Prop) + variable {A₂ : AbGroup} inductive generating_relation' : A₁ → Type := | rincl : Π{g}, S g → generating_relation' g @@ -337,9 +337,9 @@ print iff.mpr Rmul := gr_mul⦄ parameter (A₁) - definition quotient_comm_group_gen : CommGroup := quotient_comm_group normal_generating_relation + definition quotient_ab_group_gen : AbGroup := quotient_ab_group normal_generating_relation - definition gqg_map [constructor] : A₁ →g quotient_comm_group_gen := + definition gqg_map [constructor] : A₁ →g quotient_ab_group_gen := qg_map _ parameter {A₁} @@ -347,7 +347,7 @@ print iff.mpr eq_of_rel (tr (rincl H)) definition gqg_elim [constructor] (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1) - : quotient_comm_group_gen →g A₂ := + : quotient_ab_group_gen →g A₂ := begin apply quotient_group_elim f, intro g r, induction r with r, @@ -365,7 +365,7 @@ print iff.mpr end definition gqg_elim_unique (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1) - (k : quotient_comm_group_gen →g A₂) : ( k ∘g gqg_map ~ f ) → k ~ gqg_elim f H := + (k : quotient_ab_group_gen →g A₂) : ( k ∘g gqg_map ~ f ) → k ~ gqg_elim f H := !gelim_unique end diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean index c6d4640..d7198d5 100644 --- a/algebra/subgroup.hlean +++ b/algebra/subgroup.hlean @@ -130,12 +130,12 @@ namespace group abbreviation is_normal_subgroup [unfold 2] := @normal_subgroup_rel.is_normal_subgroup variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G} - {A B : CommGroup} + {A B : AbGroup} theorem is_normal_subgroup' (h : G) (r : N g) : N (h⁻¹ * g * h) := inv_inv h ▸ is_normal_subgroup N h⁻¹ r - definition normal_subgroup_rel_comm.{u} [constructor] (R : subgroup_rel.{_ u} A) + definition normal_subgroup_rel_ab.{u} [constructor] (R : subgroup_rel.{_ u} A) : normal_subgroup_rel.{_ u} A := ⦃normal_subgroup_rel, R, is_normal_subgroup := abstract begin @@ -209,7 +209,7 @@ namespace group theorem subgroup_mul_left_inv (g : sg H) : g⁻¹ * g = 1 := subtype_eq !mul.left_inv - theorem subgroup_mul_comm {G : CommGroup} {H : subgroup_rel G} (g h : sg H) + theorem subgroup_mul_comm {G : AbGroup} {H : subgroup_rel G} (g h : sg H) : g * h = h * g := subtype_eq !mul.comm @@ -223,17 +223,17 @@ namespace group definition subgroup [constructor] : Group := Group.mk _ (group_sg H) - definition comm_group_sg [constructor] {G : CommGroup} (H : subgroup_rel G) - : comm_group (sg H) := - ⦃comm_group, group_sg H, mul_comm := subgroup_mul_comm⦄ + definition ab_group_sg [constructor] {G : AbGroup} (H : subgroup_rel G) + : ab_group (sg H) := + ⦃ab_group, group_sg H, mul_comm := subgroup_mul_comm⦄ - definition comm_subgroup [constructor] {G : CommGroup} (H : subgroup_rel G) - : CommGroup := - CommGroup.mk _ (comm_group_sg H) + definition ab_subgroup [constructor] {G : AbGroup} (H : subgroup_rel G) + : AbGroup := + AbGroup.mk _ (ab_group_sg H) definition kernel {G H : Group} (f : G →g H) : Group := subgroup (kernel_subgroup f) - definition comm_kernel {G H : CommGroup} (f : G →g H) : CommGroup := comm_subgroup (kernel_subgroup f) + definition ab_kernel {G H : AbGroup} (f : G →g H) : AbGroup := ab_subgroup (kernel_subgroup f) definition incl_of_subgroup [constructor] {G : Group} (H : subgroup_rel G) : subgroup H →g G := begin @@ -258,24 +258,24 @@ namespace group definition image {G H : Group} (f : G →g H) : Group := subgroup (image_subgroup f) - definition CommGroup_of_Group.{u} (G : Group.{u}) (H : Π (g h : G), mul g h = mul h g) : CommGroup.{u} := + definition AbGroup_of_Group.{u} (G : Group.{u}) (H : Π (g h : G), mul g h = mul h g) : AbGroup.{u} := begin induction G, induction struct, - fapply CommGroup.mk, + fapply AbGroup.mk, exact carrier, - fapply comm_group.mk, - repeat assumption, + fapply ab_group.mk, + repeat assumption, exact H end - definition comm_image {G : CommGroup} {H : Group} (f : G →g H) : CommGroup := - CommGroup_of_Group (image f) + definition ab_image {G : AbGroup} {H : Group} (f : G →g H) : AbGroup := + AbGroup_of_Group (image f) begin intro g h, induction g with x t, induction h with y s, fapply subtype_eq, - induction t with p, induction s with q, induction p with g p, induction q with h q, induction p, induction q, + induction t with p, induction s with q, induction p with g p, induction q with h q, induction p, induction q, refine (((respect_mul f g h)⁻¹ ⬝ _) ⬝ (respect_mul f h g)), apply (ap f), induction G, induction struct, apply mul_comm @@ -297,9 +297,9 @@ namespace group definition image_lift {G H : Group} (f : G →g H) : G →g image f := begin fapply hom_lift f, - intro g, + intro g, apply tr, - fapply fiber.mk, + fapply fiber.mk, exact g, reflexivity end @@ -315,7 +315,7 @@ namespace group intro p, fapply subtype_eq, exact p - end + end definition image_incl_eq_one {G H : Group} (f : G →g H) : Π (x : image f), (image_incl f x = 1) → x = 1 := begin diff --git a/colim.hlean b/colim.hlean index ee761ee..0d9cd8f 100644 --- a/colim.hlean +++ b/colim.hlean @@ -389,7 +389,7 @@ namespace seq_colim rewrite [▸*, +ap_con, ap_inv, +succ_add_tr_rep_succ, con_inv, inv_con_inv_right, +con.assoc], apply whisker_left, rewrite [- +con.assoc], apply whisker_right, rewrite [- +ap_compose'], - note s := (eq_top_of_square (natural_square + note s := (eq_top_of_square (natural_square_tr (λx, fn_tr_eq_tr_fn (succ_add n k) f x ⬝ (tr_ap A succ (succ_add n k) (f x))⁻¹) p))⁻¹, rewrite [inv_con_inv_right at s, -con.assoc at s], exact s end diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean deleted file mode 100644 index a4d8113..0000000 --- a/homotopy/EM.hlean +++ /dev/null @@ -1,317 +0,0 @@ -/- -Copyright (c) 2016 Floris van Doorn. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Authors: Floris van Doorn - -Eilenberg MacLane spaces --/ - -import homotopy.EM .spectrum - -open eq is_equiv equiv is_conn is_trunc unit function pointed nat group algebra trunc trunc_index - fiber prod pointed susp EM.ops - -namespace EM - - /- Functorial action of Eilenberg-Maclane spaces -/ - - definition pEM1_functor [constructor] {G H : Group} (φ : G →g H) : pEM1 G →* pEM1 H := - begin - fconstructor, - { intro g, induction g, - { exact base }, - { exact pth (φ g) }, - { exact ap pth (respect_mul φ g h) ⬝ resp_mul (φ g) (φ h) }}, - { reflexivity } - end - - definition EMadd1_functor [constructor] {G H : CommGroup} (φ : G →g H) (n : ℕ) : - EMadd1 G n →* EMadd1 H n := - begin - apply ptrunc_functor, - apply iterate_psusp_functor, - apply pEM1_functor, - exact φ - end - - definition EM_functor [unfold 4] {G H : CommGroup} (φ : G →g H) (n : ℕ) : - K G n →* K H n := - begin - cases n with n, - { exact pmap_of_homomorphism φ }, - { exact EMadd1_functor φ n } - end - - -- TODO: (K G n →* K H n) ≃ (G →g H) - - /- Equivalence of Groups and pointed connected 1-truncated types -/ - - definition pEM1_pequiv_ptruncconntype (X : 1-Type*[0]) : pEM1 (π₁ X) ≃* X := - pEM1_pequiv_type - - definition Group_equiv_ptruncconntype [constructor] : Group ≃ 1-Type*[0] := - equiv.MK (λG, ptruncconntype.mk (pEM1 G) _ pt !is_conn_pEM1) - (λX, π₁ X) - begin intro X, apply ptruncconntype_eq, esimp, exact pEM1_pequiv_type end - begin intro G, apply eq_of_isomorphism, apply fundamental_group_pEM1 end - - /- Higher EM-spaces -/ - - /- K(G, 2) is unique (see below for general case) -/ - definition loopn_EMadd1 (G : CommGroup) (n : ℕ) : Ω[succ n] (EMadd1 G n) ≃* pType_of_Group G := - begin - refine _ ⬝e* loop_pEM1 G, - cases n with n, - { refine !loop_ptrunc_pequiv ⬝e* _, refine ptrunc_pequiv _ _ _, - apply is_trunc_eq, apply is_trunc_EM1}, - induction n with n IH, - { exact loop_pequiv_loop (loop_EM2 G)}, - refine _ ⬝e* IH, - refine !homotopy_group_pequiv_loop_ptrunc⁻¹ᵉ* ⬝e* _ ⬝e* !homotopy_group_pequiv_loop_ptrunc, - apply iterate_psusp_stability_pequiv, - rexact add_mul_le_mul_add n 1 1 - end - - definition EM2_map [unfold 7] {G : CommGroup} {X : Type*} (e : Ω[2] X ≃ G) - (r : Π(p q : Ω[2] X), e (@concat (Ω X) idp idp idp p q) = e p * e q) - [is_conn 1 X] [is_trunc 2 X] : EMadd1 G 1 → X := - begin - change trunc 2 (susp (EM1 G)) → X, intro x, - induction x with x, induction x with x, - { exact pt}, - { exact pt}, - { change carrier (Ω X), refine EM1_map e r x} - end - - definition pEM2_pmap [constructor] {G : CommGroup} {X : Type*} (e : Ω[2] X ≃ G) - (r : Π(p q : Ω[2] X), e (@concat (Ω X) idp idp idp p q) = e p * e q) - [is_conn 1 X] [is_trunc 2 X] : EMadd1 G 1 →* X := - pmap.mk (EM2_map e r) idp - - definition loop_pEM2_pmap {G : CommGroup} {X : Type*} (e : Ω[2] X ≃ G) - (r : Π(p q : Ω[2] X), e (@concat (Ω X) idp idp idp p q) = e p * e q) - [is_conn 1 X] [is_trunc 2 X] : - Ω→[2](pEM2_pmap e r) ~ e⁻¹ᵉ ∘ loopn_EMadd1 G 1 := - begin - exact sorry - end - - -- TODO: make arguments in trivial_homotopy_group_of_is_trunc implicit - attribute is_conn_EMadd1 is_trunc_EMadd1 [instance] - definition pEM2_pequiv' {G : CommGroup} {X : Type*} (e : Ω[2] X ≃ G) - (r : Π(p q : Ω[2] X), e (@concat (Ω X) idp idp idp p q) = e p * e q) - [is_conn 1 X] [is_trunc 2 X] : EMadd1 G 1 ≃* X := - begin - apply pequiv_of_pmap (pEM2_pmap e r), - have is_conn 0 (EMadd1 G 1), from !is_conn_of_is_conn_succ, - have is_trunc 2 (EMadd1 G 1), from !is_trunc_EMadd1, - refine whitehead_principle_pointed 2 _ _, - intro k, apply @nat.lt_by_cases k 2: intro H, - { apply @is_equiv_of_is_contr, - do 2 exact trivial_homotopy_group_of_is_conn _ (le_of_lt_succ H)}, - { cases H, esimp, apply is_equiv_trunc_functor, esimp, - apply is_equiv.homotopy_closed, rotate 1, - { symmetry, exact loop_pEM2_pmap _ _}, - apply is_equiv_compose, apply pequiv.to_is_equiv, apply to_is_equiv}, - { apply @is_equiv_of_is_contr, - exact trivial_homotopy_group_of_is_trunc _ H, - apply @trivial_homotopy_group_of_is_trunc, rotate 1, exact H, exact _inst_2} - end - - definition pEM2_pequiv {G : CommGroup} {X : Type*} (e : πg[1+1] X ≃g G) - [is_conn 1 X] [is_trunc 2 X] : EMadd1 G 1 ≃* X := - begin - have is_set (Ω[2] X), from !is_trunc_eq, - apply pEM2_pequiv' (!trunc_equiv⁻¹ᵉ ⬝e equiv_of_isomorphism e), - intro p q, esimp, exact to_respect_mul e (tr p) (tr q) - end - - -- general case - definition EMadd1_map [unfold 8] {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G) - (r : Π(p q : Ω (Ω[n] X)), e (p ⬝ q) = e p * e q) - [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n → X := - begin - revert X e r H1 H2, induction n with n f: intro X e r H1 H2, - { change trunc 1 (EM1 G) → X, intro x, induction x with x, exact EM1_map e r x}, - change trunc (n.+2) (susp (iterate_psusp n (pEM1 G))) → X, intro x, - induction x with x, induction x with x, - { exact pt}, - { exact pt}, - change carrier (Ω X), refine f _ _ _ _ _ (tr x), - { refine _⁻¹ᵉ ⬝e e, apply equiv_of_pequiv, apply loopn_succ_in}, - exact abstract begin - intro p q, refine _ ⬝ !r, apply ap e, esimp, - apply inv_eq_of_eq, - refine _⁻¹ ⬝ !loopn_succ_in_con⁻¹, - exact to_right_inv (loopn_succ_in X (succ n)) p ◾ to_right_inv (loopn_succ_in X (succ n)) q - end end - end - - definition pEMadd1_pmap [constructor] {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G) - (r : Π(p q : Ω[succ n] X), e (@concat (Ω[n] X) pt pt pt p q) = e p * e q) - [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n →* X := - pmap.mk (EMadd1_map e r) begin cases n with n: reflexivity end - - definition loopn_pEMadd1_pmap {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G) - (r : Π(p q : Ω[succ n] X), e (@concat (Ω[n] X) pt pt pt p q) = e p * e q) - [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : - Ω→[succ n](pEMadd1_pmap e r) ~ e⁻¹ᵉ ∘ loopn_EMadd1 G n := - begin - apply homotopy_of_inv_homotopy_pre (loopn_EMadd1 G n), - intro g, esimp at *, - revert X e r H1 H2, induction n with n IH: intro X e r H1 H2, - { refine !idp_con ⬝ _, refine !ap_compose'⁻¹ ⬝ _, apply elim_pth}, - { replace (succ (succ n)) with ((succ n) + 1), rewrite [apn_succ], - exact sorry} - -- exact !idp_con ⬝ !elim_pth - end - - -- definition is_conn_of_le (n : ℕ₋₂) (A : Type) [is_conn (n.+1) A] : - -- is_conn n A := - -- is_trunc_trunc_of_le A -2 (trunc_index.self_le_succ n) - -- attribute is_conn_EMadd1 is_trunc_EMadd1 [instance] - - definition pEMadd1_pequiv' {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G) - (r : Π(p q : Ω[succ n] X), e (@concat (Ω[n] X) pt pt pt p q) = e p * e q) - [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X := - begin - apply pequiv_of_pmap (pEMadd1_pmap e r), - have is_conn 0 (EMadd1 G n), from is_conn_of_le _ (zero_le_of_nat n), - have is_trunc (n.+1) (EMadd1 G n), from !is_trunc_EMadd1, - refine whitehead_principle_pointed (n.+1) _ _, - intro k, apply @nat.lt_by_cases k (succ n): intro H, - { apply @is_equiv_of_is_contr, - do 2 exact trivial_homotopy_group_of_is_conn _ (le_of_lt_succ H)}, - { cases H, esimp, apply is_equiv_trunc_functor, esimp, - apply is_equiv.homotopy_closed, rotate 1, - { symmetry, exact loopn_pEMadd1_pmap _ _}, - apply is_equiv_compose, apply pequiv.to_is_equiv}, - { apply @is_equiv_of_is_contr, - do 2 exact trivial_homotopy_group_of_is_trunc _ H} - end - - definition pEMadd1_pequiv {G : CommGroup} {X : Type*} {n : ℕ} (e : πg[n+1] X ≃g G) - [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X := - begin - have is_set (Ω[succ n] X), from !is_set_loopn, - apply pEMadd1_pequiv' (!trunc_equiv⁻¹ᵉ ⬝e equiv_of_isomorphism e), - intro p q, esimp, exact to_respect_mul e (tr p) (tr q) - end - - definition EM_pequiv_succ {G : CommGroup} {X : Type*} {n : ℕ} (e : πg[n+1] X ≃g G) - [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EM G (succ n) ≃* X := - pEMadd1_pequiv e - - definition EM_pequiv_zero {G : CommGroup} {X : Type*} (e : X ≃* pType_of_Group G) : EM G 0 ≃* X := - proof e⁻¹ᵉ* qed - - /- uniqueness of K(G,n), method 2: -/ - --- definition freudenthal_homotopy_group_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n) --- : π[k + 1] (psusp A) ≃* π[k] A := --- calc --- π[k + 1] (psusp A) ≃* π[k] (Ω (psusp A)) : homotopy_group_succ_in --- ... ≃* Ω[k] (ptrunc k (Ω (psusp A))) : homotopy_group_pequiv_loop_ptrunc k (Ω (psusp A)) --- ... ≃* Ω[k] (ptrunc k A) : loopn_pequiv_loopn k (freudenthal_pequiv A H) --- ... ≃* π[k] A : (homotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ* - - definition iterate_psusp_succ_pequiv (n : ℕ) (A : Type*) : - iterate_psusp (succ n) A ≃* iterate_psusp n (psusp A) := - begin - induction n with n IH, - { reflexivity}, - { exact psusp_equiv IH} - end - - definition is_conn_psusp [instance] (n : trunc_index) (A : Type*) - [H : is_conn n A] : is_conn (n .+1) (psusp A) := - is_conn_susp n A - - definition iterated_freudenthal_pequiv (A : Type*) {n k m : ℕ} [HA : is_conn n A] (H : k ≤ 2 * n) - : ptrunc k A ≃* ptrunc k (Ω[m] (iterate_psusp m A)) := - begin - revert A n k HA H, induction m with m IH: intro A n k HA H, - { reflexivity}, - { have H2 : succ k ≤ 2 * succ n, - from calc - succ k ≤ succ (2 * n) : succ_le_succ H - ... ≤ 2 * succ n : self_le_succ, - exact calc - ptrunc k A ≃* ptrunc k (Ω (psusp A)) : freudenthal_pequiv A H - ... ≃* Ω (ptrunc (succ k) (psusp A)) : loop_ptrunc_pequiv - ... ≃* Ω (ptrunc (succ k) (Ω[m] (iterate_psusp m (psusp A)))) : - loop_pequiv_loop (IH (psusp A) (succ n) (succ k) _ H2) - ... ≃* ptrunc k (Ω[succ m] (iterate_psusp m (psusp A))) : loop_ptrunc_pequiv - ... ≃* ptrunc k (Ω[succ m] (iterate_psusp (succ m) A)) : - ptrunc_pequiv_ptrunc _ (loopn_pequiv_loopn _ !iterate_psusp_succ_pequiv)} - end - - definition pmap_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) : f = g := - pmap_eq (to_homotopy p) (to_homotopy_pt p)⁻¹ - - definition pmap_equiv_pmap_right {A B : Type*} (C : Type*) (f : A ≃* B) : C →* A ≃ C →* B := - begin - fapply equiv.MK, - { exact pcompose f}, - { exact pcompose f⁻¹ᵉ*}, - { intro f, apply pmap_eq_of_phomotopy, - exact !passoc⁻¹* ⬝* pwhisker_right _ !pright_inv ⬝* !pid_pcompose}, - { intro f, apply pmap_eq_of_phomotopy, - exact !passoc⁻¹* ⬝* pwhisker_right _ !pleft_inv ⬝* !pid_pcompose} - end - - definition iterate_psusp_adjoint_loopn [constructor] (X Y : Type*) (n : ℕ) : - iterate_psusp n X →* Y ≃ X →* Ω[n] Y := - begin - revert X Y, induction n with n IH: intro X Y, - { reflexivity}, - { refine !susp_adjoint_loop ⬝e !IH ⬝e _, apply pmap_equiv_pmap_right, - symmetry, apply loopn_succ_in} - end - - /- new method of uniqueness, define K(G,n+1) as the truncation of the suspension of K(G,n) -/ - - definition EMadd2 (G : CommGroup) (n : ℕ) : Type* := ptrunc (n.+2) (psusp (EMadd1 G n)) - - definition EMadd2_map [constructor] {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[n+2] X ≃ G) - (r : Π(p q : Ω[n+2] X), e (@concat (Ω[n+1] X) pt pt pt p q) = e p * e q) - [H1 : is_conn (n.+1) X] [H2 : is_trunc (n.+2) X] : EMadd2 G n → X := - begin - intro x, induction x with x, induction x with x, - { exact pt }, - { exact pt }, - { refine EMadd1_map ((loopn_succ_in _ (n+1))⁻¹ᵉ ⬝e e) _ x, - exact abstract begin - intro p q, refine _ ⬝ !r, apply ap e, esimp, - refine @inv_eq_of_eq _ _ (pequiv.to_equiv (loopn_succ_in X (n + 1))) _ _ _ _, - refine _⁻¹ ⬝ !loopn_succ_in_con⁻¹, - exact to_right_inv (loopn_succ_in X (succ n)) p ◾ to_right_inv (loopn_succ_in X (succ n)) q - end end } - end - - -- -- general case - -- definition EMadd1_map [unfold 8] {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G) - -- (r : Π(p q : Ω (Ω[n] X)), e (p ⬝ q) = e p * e q) - -- [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n → X := - -- begin - -- revert X e r H1 H2, induction n with n f: intro X e r H1 H2, - -- { change trunc 1 (EM1 G) → X, intro x, induction x with x, exact EM1_map e r x}, - -- change trunc (n.+2) (susp (iterate_psusp n (pEM1 G))) → X, intro x, - -- induction x with x, induction x with x, - -- { exact pt}, - -- { exact pt}, - -- change carrier (Ω X), refine f _ _ _ _ _ (tr x), - -- { refine _⁻¹ᵉ ⬝e e, apply equiv_of_pequiv, apply loopn_succ_in}, - -- exact abstract begin - -- intro p q, refine _ ⬝ !r, apply ap e, esimp, - -- apply inv_eq_of_eq, - -- refine _⁻¹ ⬝ !loopn_succ_in_con⁻¹, - -- exact to_right_inv (loopn_succ_in X (succ n)) p ◾ to_right_inv (loopn_succ_in X (succ n)) q - -- end end - -- end - -end EM --- cohomology ∥ X → K(G,n) ∥ --- reduced cohomology ∥ X →* K(G,n) ∥ --- but we probably want to do this for any spectrum diff --git a/homotopy/EMnew.hlean b/homotopy/EMnew.hlean deleted file mode 100644 index a768547..0000000 --- a/homotopy/EMnew.hlean +++ /dev/null @@ -1,518 +0,0 @@ -/- -Copyright (c) 2016 Floris van Doorn. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Authors: Floris van Doorn - -Eilenberg MacLane spaces - -This file replaces the file in the HoTT library --/ - -import hit.groupoid_quotient homotopy.hopf homotopy.freudenthal homotopy.homotopy_group - ..move_to_lib -open algebra pointed nat eq category group is_trunc iso unit trunc equiv is_conn function is_equiv - trunc_index - -local attribute pType_of_Group [coercion] - -namespace EMnew - open groupoid_quotient - - variables {G : Group} - definition EM1' (G : Group) : Type := - groupoid_quotient (Groupoid_of_Group G) - definition EM1 [constructor] (G : Group) : Type* := - pointed.MK (EM1' G) (elt star) - - definition base : EM1' G := elt star - definition pth : G → base = base := pth - definition resp_mul (g h : G) : pth (g * h) = pth g ⬝ pth h := resp_comp h g - definition resp_one : pth (1 : G) = idp := - resp_id star - - definition resp_inv (g : G) : pth (g⁻¹) = (pth g)⁻¹ := - resp_inv g - - local attribute pointed.MK pointed.carrier EM1 EM1' [reducible] - protected definition rec {P : EM1' G → Type} [H : Π(x : EM1' G), is_trunc 1 (P x)] - (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb) - (Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h) (x : EM1' G) : P x := - begin - induction x, - { induction g, exact Pb}, - { induction a, induction b, exact Pp f}, - { induction a, induction b, induction c, exact Pmul f g} - end - - protected definition rec_on {P : EM1' G → Type} [H : Π(x : EM1' G), is_trunc 1 (P x)] - (x : EM1' G) (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb) - (Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h) : P x := - EMnew.rec Pb Pp Pmul x - - protected definition set_rec {P : EM1' G → Type} [H : Π(x : EM1' G), is_set (P x)] - (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb) (x : EM1' G) : P x := - EMnew.rec Pb Pp !center x - - protected definition prop_rec {P : EM1' G → Type} [H : Π(x : EM1' G), is_prop (P x)] - (Pb : P base) (x : EM1' G) : P x := - EMnew.rec Pb !center !center x - - definition rec_pth {P : EM1' G → Type} [H : Π(x : EM1' G), is_trunc 1 (P x)] - {Pb : P base} {Pp : Π(g : G), Pb =[pth g] Pb} - (Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h) - (g : G) : apd (EMnew.rec Pb Pp Pmul) (pth g) = Pp g := - proof !rec_pth qed - - protected definition elim {P : Type} [is_trunc 1 P] (Pb : P) (Pp : Π(g : G), Pb = Pb) - (Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) (x : EM1' G) : P := - begin - induction x, - { exact Pb}, - { exact Pp f}, - { exact Pmul f g} - end - - protected definition elim_on [reducible] {P : Type} [is_trunc 1 P] (x : EM1' G) - (Pb : P) (Pp : G → Pb = Pb) (Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) : P := - EMnew.elim Pb Pp Pmul x - - protected definition set_elim [reducible] {P : Type} [is_set P] (Pb : P) (Pp : G → Pb = Pb) - (x : EM1' G) : P := - EMnew.elim Pb Pp !center x - - protected definition prop_elim [reducible] {P : Type} [is_prop P] (Pb : P) (x : EM1' G) : P := - EMnew.elim Pb !center !center x - - definition elim_pth {P : Type} [is_trunc 1 P] {Pb : P} {Pp : G → Pb = Pb} - (Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) (g : G) : ap (EMnew.elim Pb Pp Pmul) (pth g) = Pp g := - proof !elim_pth qed - - protected definition elim_set.{u} (Pb : Set.{u}) (Pp : Π(g : G), Pb ≃ Pb) - (Pmul : Π(g h : G) (x : Pb), Pp (g * h) x = Pp h (Pp g x)) (x : EM1' G) : Set.{u} := - groupoid_quotient.elim_set (λu, Pb) (λu v, Pp) (λu v w g h, proof Pmul h g qed) x - - theorem elim_set_pth {Pb : Set} {Pp : Π(g : G), Pb ≃ Pb} - (Pmul : Π(g h : G) (x : Pb), Pp (g * h) x = Pp h (Pp g x)) (g : G) : - transport (EMnew.elim_set Pb Pp Pmul) (pth g) = Pp g := - !elim_set_pth - -end EMnew - -attribute EMnew.base [constructor] -attribute EMnew.rec EMnew.elim [unfold 7] [recursor 7] -attribute EMnew.rec_on EMnew.elim_on [unfold 4] -attribute EMnew.set_rec EMnew.set_elim [unfold 6] -attribute EMnew.prop_rec EMnew.prop_elim EMnew.elim_set [unfold 5] - -namespace EMnew - open groupoid_quotient - - variables (G : Group) - definition base_eq_base_equiv : (base = base :> EM1 G) ≃ G := - !elt_eq_elt_equiv - - definition fundamental_group_EM1 : π₁ (EM1 G) ≃g G := - begin - fapply isomorphism_of_equiv, - { exact trunc_equiv_trunc 0 !base_eq_base_equiv ⬝e trunc_equiv 0 G}, - { intros g h, induction g with p, induction h with q, - exact encode_con p q} - end - - proposition is_trunc_EM1 [instance] : is_trunc 1 (EM1 G) := - !is_trunc_groupoid_quotient - - proposition is_trunc_EM1' [instance] : is_trunc 1 (EM1' G) := - !is_trunc_groupoid_quotient - - proposition is_conn_EM1' [instance] : is_conn 0 (EM1' G) := - by apply @is_conn_groupoid_quotient; esimp; exact _ - - proposition is_conn_EM1 [instance] : is_conn 0 (EM1 G) := - is_conn_EM1' G - - variable {G} - definition EM1_map [unfold 7] {X : Type*} (e : G → Ω X) - (r : Πg h, e (g * h) = e g ⬝ e h) [is_conn 0 X] [is_trunc 1 X] : EM1 G → X := - begin - intro x, induction x using EMnew.elim, - { exact Point X }, - { exact e g }, - { exact r g h } - end - - /- Uniqueness of K(G, 1) -/ - - definition EM1_pmap [constructor] {X : Type*} (e : G → Ω X) - (r : Πg h, e (g * h) = e g ⬝ e h) [is_conn 0 X] [is_trunc 1 X] : EM1 G →* X := - pmap.mk (EM1_map e r) idp - - variable (G) - definition loop_EM1 [constructor] : G ≃* Ω (EM1 G) := - (pequiv_of_equiv (base_eq_base_equiv G) idp)⁻¹ᵉ* - - variable {G} - definition loop_EM1_pmap {X : Type*} (e : G →* Ω X) - (r : Πg h, e (g * h) = e g ⬝ e h) [is_conn 0 X] [is_trunc 1 X] : - Ω→(EM1_pmap e r) ∘* loop_EM1 G ~* e := - begin - fapply phomotopy.mk, - { intro g, refine !idp_con ⬝ elim_pth r g }, - { apply is_set.elim } - end - - definition EM1_pequiv'.{u} {G : Group.{u}} {X : pType.{u}} (e : G ≃* Ω X) - (r : Πg h, e (g * h) = e g ⬝ e h) [is_conn 0 X] [is_trunc 1 X] : EM1 G ≃* X := - begin - apply pequiv_of_pmap (EM1_pmap e r), - apply whitehead_principle_pointed 1, - intro k, cases k with k, - { apply @is_equiv_of_is_contr, - all_goals (esimp; exact _)}, - { cases k with k, - { apply is_equiv_trunc_functor, esimp, - apply is_equiv.homotopy_closed, rotate 1, - { symmetry, exact phomotopy_pinv_right_of_phomotopy (loop_EM1_pmap _ _) }, - apply is_equiv_compose e }, - { apply @is_equiv_of_is_contr, - do 2 exact trivial_homotopy_group_of_is_trunc _ (succ_lt_succ !zero_lt_succ)}} - end - - definition EM1_pequiv.{u} {G : Group.{u}} {X : pType.{u}} (e : G ≃g π₁ X) - [is_conn 0 X] [is_trunc 1 X] : EM1 G ≃* X := - begin - apply EM1_pequiv' (pequiv_of_isomorphism e ⬝e* ptrunc_pequiv _ _ _), - refine is_equiv.preserve_binary_of_inv_preserve _ mul concat _, - intro p q, - exact to_respect_mul e⁻¹ᵍ (tr p) (tr q) - end - - definition EM1_pequiv_type (X : Type*) [is_conn 0 X] [is_trunc 1 X] : EM1 (π₁ X) ≃* X := - EM1_pequiv !isomorphism.refl - -end EMnew - -open hopf new_susp susp -namespace EMnew - /- EM1 G is an h-space if G is an abelian group. This allows us to construct K(G,n) for n ≥ 2 -/ - variables {G : CommGroup} (n : ℕ) - - definition EM1_mul [unfold 2 3] (x x' : EM1' G) : EM1' G := - begin - induction x, - { exact x'}, - { induction x' using EMnew.set_rec, - { exact pth g}, - { exact abstract begin apply loop_pathover, apply square_of_eq, - refine !resp_mul⁻¹ ⬝ _ ⬝ !resp_mul, - exact ap pth !mul.comm end end}}, - { refine EMnew.prop_rec _ x', apply resp_mul } - end - - variable (G) - definition EM1_mul_one (x : EM1' G) : EM1_mul x base = x := - begin - induction x using EMnew.set_rec, - { reflexivity}, - { apply eq_pathover_id_right, apply hdeg_square, refine EMnew.elim_pth _ g} - end - - definition h_space_EM1 [constructor] [instance] : h_space (EM1' G) := - begin - fapply h_space.mk, - { exact EM1_mul}, - { exact base}, - { intro x', reflexivity}, - { apply EM1_mul_one} - end - - /- K(G, n+1) -/ - definition EMadd1 : ℕ → Type* - | 0 := EM1 G - | (n+1) := ptrunc (n+2) (psusp (EMadd1 n)) - - definition EMadd1_succ [unfold_full] (n : ℕ) : - EMadd1 G (succ n) = ptrunc (n.+2) (psusp (EMadd1 G n)) := - idp - - definition loop_EM2 : Ω[1] (EMadd1 G 1) ≃* EM1 G := - hopf.delooping (EM1' G) idp - - definition is_conn_EMadd1 [instance] (n : ℕ) : is_conn n (EMadd1 G n) := - begin - induction n with n IH, - { apply is_conn_EM1 }, - { rewrite EMadd1_succ, esimp, exact _ } - end - - definition is_trunc_EMadd1 [instance] (n : ℕ) : is_trunc (n+1) (EMadd1 G n) := - begin - cases n with n, - { apply is_trunc_EM1 }, - { apply is_trunc_trunc } - end - - /- loops of an EM-space -/ - definition loop_EMadd1 (n : ℕ) : EMadd1 G n ≃* Ω (EMadd1 G (succ n)) := - begin - cases n with n, - { exact !loop_EM2⁻¹ᵉ* }, - { rewrite [EMadd1_succ G (succ n)], - refine (ptrunc_pequiv (succ n + 1) _ _)⁻¹ᵉ* ⬝e* _ ⬝e* (loop_ptrunc_pequiv _ _)⁻¹ᵉ*, - have succ n + 1 ≤ 2 * succ n, from add_mul_le_mul_add n 1 1, - refine freudenthal_pequiv _ this } - end - - definition loopn_EMadd1_pequiv_EM1 (G : CommGroup) (n : ℕ) : EM1 G ≃* Ω[n] (EMadd1 G n) := - begin - induction n with n e, - { reflexivity }, - { refine _ ⬝e* !loopn_succ_in⁻¹ᵉ*, - refine _ ⬝e* loopn_pequiv_loopn n !loop_EMadd1, - exact e } - end - - -- use loopn_EMadd1_pequiv_EM1 in this definition? - definition loopn_EMadd1 (G : CommGroup) (n : ℕ) : G ≃* Ω[succ n] (EMadd1 G n) := - begin - induction n with n e, - { apply loop_EM1 }, - { refine _ ⬝e* !loopn_succ_in⁻¹ᵉ*, - refine _ ⬝e* loopn_pequiv_loopn (succ n) !loop_EMadd1, - exact e } - end - - definition loopn_EMadd1_succ [unfold_full] (G : CommGroup) (n : ℕ) : loopn_EMadd1 G (succ n) ~* - !loopn_succ_in⁻¹ᵉ* ∘* apn (succ n) !loop_EMadd1 ∘* loopn_EMadd1 G n := - by reflexivity - - definition EM_up {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ (succ n)] X ≃* G) - : Ω[succ n] (Ω X) ≃* G := - !loopn_succ_in⁻¹ᵉ* ⬝e* e - - definition is_homomorphism_EM_up {G : CommGroup} {X : Type*} {n : ℕ} - (e : Ω[succ (succ n)] X ≃* G) - (r : Π(p q : Ω[succ (succ n)] X), e (p ⬝ q) = e p * e q) - (p q : Ω[succ n] (Ω X)) : EM_up e (p ⬝ q) = EM_up e p * EM_up e q := - begin - refine _ ⬝ !r, apply ap e, esimp, apply apn_con - end - - definition EMadd1_pmap [unfold 8] {G : CommGroup} {X : Type*} (n : ℕ) - (e : Ω[succ n] X ≃* G) - (r : Πp q, e (p ⬝ q) = e p * e q) - [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n →* X := - begin - revert X e r H1 H2, induction n with n f: intro X e r H1 H2, - { exact EM1_pmap e⁻¹ᵉ* (equiv.inv_preserve_binary e concat mul r) }, - rewrite [EMadd1_succ], - exact ptrunc.elim ((succ n).+1) - (psusp.elim (f _ (EM_up e) (is_homomorphism_EM_up e r) _ _)), - end - - definition EMadd1_pmap_succ {G : CommGroup} {X : Type*} (n : ℕ) (e : Ω[succ (succ n)] X ≃* G) - r [H1 : is_conn (succ n) X] [H2 : is_trunc ((succ n).+1) X] : EMadd1_pmap (succ n) e r = - ptrunc.elim ((succ n).+1) (psusp.elim (EMadd1_pmap n (EM_up e) (is_homomorphism_EM_up e r))) := - by reflexivity - - definition loop_EMadd1_pmap {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ (succ n)] X ≃* G) - (r : Πp q, e (p ⬝ q) = e p * e q) - [H1 : is_conn (succ n) X] [H2 : is_trunc ((succ n).+1) X] : - Ω→(EMadd1_pmap (succ n) e r) ∘* loop_EMadd1 G n ~* - EMadd1_pmap n (EM_up e) (is_homomorphism_EM_up e r) := - begin - cases n with n, - { apply hopf_delooping_elim }, - { refine !passoc⁻¹* ⬝* _, - rewrite [EMadd1_pmap_succ (succ n)], - refine pwhisker_right _ !ap1_ptrunc_elim ⬝* _, - refine !passoc⁻¹* ⬝* _, - refine pwhisker_right _ (ptrunc_elim_freudenthal_pequiv - (succ n) (succ (succ n)) (add_mul_le_mul_add n 1 1) _) ⬝* _, - reflexivity } - end - - definition loopn_EMadd1_pmap' {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃* G) - (r : Πp q, e (p ⬝ q) = e p * e q) - [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : - Ω→[succ n](EMadd1_pmap n e r) ∘* loopn_EMadd1 G n ~* e⁻¹ᵉ* := - begin - revert X e r H1 H2, induction n with n IH: intro X e r H1 H2, - { apply loop_EM1_pmap }, - refine pwhisker_left _ !loopn_EMadd1_succ ⬝* _, - refine !passoc⁻¹* ⬝* _, - refine pwhisker_right _ !loopn_succ_in_inv_natural ⬝* _, - refine !passoc ⬝* _, - refine pwhisker_left _ (!passoc⁻¹* ⬝* - pwhisker_right _ (!apn_pcompose⁻¹* ⬝* apn_phomotopy _ !loop_EMadd1_pmap) ⬝* - !IH ⬝* !pinv_trans_pinv_left) ⬝* _, - apply pinv_pcompose_cancel_left - end - - definition EMadd1_pequiv' {G : CommGroup} {X : Type*} (n : ℕ) (e : Ω[succ n] X ≃* G) - (r : Π(p q : Ω[succ n] X), e (p ⬝ q) = e p * e q) - [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X := - begin - apply pequiv_of_pmap (EMadd1_pmap n e r), - have is_conn 0 (EMadd1 G n), from is_conn_of_le _ (zero_le_of_nat n), - have is_trunc (n.+1) (EMadd1 G n), from !is_trunc_EMadd1, - refine whitehead_principle_pointed (n.+1) _ _, - intro k, apply @nat.lt_by_cases k (succ n): intro H, - { apply @is_equiv_of_is_contr, - do 2 exact trivial_homotopy_group_of_is_conn _ (le_of_lt_succ H)}, - { cases H, esimp, apply is_equiv_trunc_functor, esimp, - apply is_equiv.homotopy_closed, rotate 1, - { symmetry, exact phomotopy_pinv_right_of_phomotopy (loopn_EMadd1_pmap' _ _) }, - apply is_equiv_compose (e⁻¹ᵉ*)}, - { apply @is_equiv_of_is_contr, - do 2 exact trivial_homotopy_group_of_is_trunc _ H} - end - - definition EMadd1_pequiv {G : CommGroup} {X : Type*} (n : ℕ) (e : πg[n+1] X ≃g G) - [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X := - begin - have is_set (Ω[succ n] X), from !is_set_loopn, - apply EMadd1_pequiv' n ((ptrunc_pequiv _ _ _)⁻¹ᵉ* ⬝e* pequiv_of_isomorphism e), - intro p q, esimp, exact to_respect_mul e (tr p) (tr q) - end - - definition EMadd1_pequiv_succ {G : CommGroup} {X : Type*} (n : ℕ) (e : πag[n+2] X ≃g G) - [H1 : is_conn (n.+1) X] [H2 : is_trunc (n.+2) X] : EMadd1 G (succ n) ≃* X := - EMadd1_pequiv (succ n) e - - definition ghomotopy_group_EMadd1 (n : ℕ) : πg[n+1] (EMadd1 G n) ≃g G := - begin - change π₁ (Ω[n] (EMadd1 G n)) ≃g G, - refine homotopy_group_isomorphism_of_pequiv 0 (loopn_EMadd1_pequiv_EM1 G n)⁻¹ᵉ* ⬝g _, - apply fundamental_group_EM1, - end - - definition EMadd1_pequiv_type (X : Type*) (n : ℕ) [is_conn (n+1) X] [is_trunc (n+1+1) X] - : EMadd1 (πag[n+2] X) (succ n) ≃* X := - EMadd1_pequiv_succ n !isomorphism.refl - - /- K(G, n) -/ - definition EM (G : CommGroup) : ℕ → Type* - | 0 := G - | (k+1) := EMadd1 G k - - namespace ops - abbreviation K := @EM - end ops - open ops - - definition homotopy_group_EM (n : ℕ) : π[n] (EM G n) ≃* G := - begin - cases n with n, - { rexact ptrunc_pequiv 0 (G) _}, - { exact pequiv_of_isomorphism (ghomotopy_group_EMadd1 G n)} - end - - definition ghomotopy_group_EM (n : ℕ) : πg[n+1] (EM G (n+1)) ≃g G := - ghomotopy_group_EMadd1 G n - - definition is_conn_EM [instance] (n : ℕ) : is_conn (n.-1) (EM G n) := - begin - cases n with n, - { apply is_conn_minus_one, apply tr, unfold [EM], exact 1}, - { apply is_conn_EMadd1} - end - - definition is_conn_EM_succ [instance] (n : ℕ) : is_conn n (EM G (succ n)) := - is_conn_EM G (succ n) - - definition is_trunc_EM [instance] (n : ℕ) : is_trunc n (EM G n) := - begin - cases n with n, - { unfold [EM], apply semigroup.is_set_carrier}, - { apply is_trunc_EMadd1} - end - - definition loop_EM (n : ℕ) : Ω (K G (succ n)) ≃* K G n := - begin - cases n with n, - { refine _ ⬝e* pequiv_of_isomorphism (fundamental_group_EM1 G), - symmetry, apply ptrunc_pequiv, exact _}, - { exact !loop_EMadd1⁻¹ᵉ* } - end - - open circle int - definition EM_pequiv_circle : K agℤ 1 ≃* S¹* := - EM1_pequiv fundamental_group_of_circle⁻¹ᵍ - - /- Functorial action of Eilenberg-Maclane spaces -/ - - definition EM1_functor [constructor] {G H : Group} (φ : G →g H) : EM1 G →* EM1 H := - begin - fconstructor, - { intro g, induction g, - { exact base }, - { exact pth (φ g) }, - { exact ap pth (to_respect_mul φ g h) ⬝ resp_mul (φ g) (φ h) }}, - { reflexivity } - end - - definition EMadd1_functor [constructor] {G H : CommGroup} (φ : G →g H) (n : ℕ) : - EMadd1 G n →* EMadd1 H n := - begin - induction n with n ψ, - { exact EM1_functor φ }, - { apply ptrunc_functor, apply psusp_functor, exact ψ } - end - - definition EM_functor [unfold 4] {G H : CommGroup} (φ : G →g H) (n : ℕ) : - K G n →* K H n := - begin - cases n with n, - { exact pmap_of_homomorphism φ }, - { exact EMadd1_functor φ n } - end - - -- TODO: (K G n →* K H n) ≃ (G →g H) - - /- Equivalence of Groups and pointed connected 1-truncated types -/ - - definition ptruncconntype10_pequiv (X Y : 1-Type*[0]) (e : π₁ X ≃g π₁ Y) : X ≃* Y := - (EM1_pequiv !isomorphism.refl)⁻¹ᵉ* ⬝e* EM1_pequiv e - - definition EM1_pequiv_ptruncconntype10 (X : 1-Type*[0]) : EM1 (π₁ X) ≃* X := - EM1_pequiv_type X - - definition Group_equiv_ptruncconntype10 [constructor] : Group ≃ 1-Type*[0] := - equiv.MK (λG, ptruncconntype.mk (EM1 G) _ pt !is_conn_EM1) - (λX, π₁ X) - begin intro X, apply ptruncconntype_eq, esimp, exact EM1_pequiv_type X end - begin intro G, apply eq_of_isomorphism, apply fundamental_group_EM1 end - - /- Equivalence of CommGroups and pointed n-connected (n+1)-truncated types (n ≥ 1) -/ - - open trunc_index - definition ptruncconntype_pequiv : Π(n : ℕ) (X Y : (n.+1)-Type*[n]) - (e : πg[n+1] X ≃g πg[n+1] Y), X ≃* Y - | 0 X Y e := ptruncconntype10_pequiv X Y e - | (succ n) X Y e := - begin - refine (EMadd1_pequiv_succ n _)⁻¹ᵉ* ⬝e* EMadd1_pequiv_succ n !isomorphism.refl, - exact e - end - - definition EM1_pequiv_ptruncconntype (n : ℕ) (X : (n+1+1)-Type*[n+1]) : - EMadd1 (πag[n+2] X) (succ n) ≃* X := - EMadd1_pequiv_type X n - - definition CommGroup_equiv_ptruncconntype' [constructor] (n : ℕ) : - CommGroup ≃ (n + 1 + 1)-Type*[n+1] := - equiv.MK - (λG, ptruncconntype.mk (EMadd1 G (n+1)) _ pt _) - (λX, πag[n+2] X) - begin intro X, apply ptruncconntype_eq, apply EMadd1_pequiv_type end - begin intro G, apply CommGroup_eq_of_isomorphism, exact ghomotopy_group_EMadd1 G (n+1) end - - definition CommGroup_equiv_ptruncconntype [constructor] (n : ℕ) : - CommGroup ≃ (n.+2)-Type*[n.+1] := - CommGroup_equiv_ptruncconntype' n - - print axioms CommGroup_equiv_ptruncconntype - -end EMnew diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean index 1c15223..a0ea060 100644 --- a/homotopy/cohomology.hlean +++ b/homotopy/cohomology.hlean @@ -6,29 +6,29 @@ Authors: Floris van Doorn Reduced cohomology -/ -import .EM algebra.arrow_group .spectrum +import algebra.arrow_group .spectrum homotopy.EM open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops -definition EM_spectrum /-[constructor]-/ (G : CommGroup) : spectrum := +definition EM_spectrum /-[constructor]-/ (G : AbGroup) : spectrum := spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*) -definition cohomology (X : Type*) (Y : spectrum) (n : ℤ) : CommGroup := -CommGroup_pmap X (πag[2] (Y (2+n))) +definition cohomology (X : Type*) (Y : spectrum) (n : ℤ) : AbGroup := +AbGroup_pmap X (πag[2] (Y (2+n))) -definition ordinary_cohomology [reducible] (X : Type*) (G : CommGroup) (n : ℤ) : CommGroup := +definition ordinary_cohomology [reducible] (X : Type*) (G : AbGroup) (n : ℤ) : AbGroup := cohomology X (EM_spectrum G) n -definition ordinary_cohomology_Z [reducible] (X : Type*) (n : ℤ) : CommGroup := +definition ordinary_cohomology_Z [reducible] (X : Type*) (n : ℤ) : AbGroup := ordinary_cohomology X agℤ n notation `H^` n `[`:0 X:0 `, ` Y:0 `]`:0 := cohomology X Y n notation `H^` n `[`:0 X:0 `]`:0 := ordinary_cohomology_Z X n -check H^3[S¹*,EM_spectrum agℤ] -check H^3[S¹*] +-- check H^3[S¹*,EM_spectrum agℤ] +-- check H^3[S¹*] -definition unpointed_cohomology (X : Type) (Y : spectrum) (n : ℤ) : CommGroup := +definition unpointed_cohomology (X : Type) (Y : spectrum) (n : ℤ) : AbGroup := cohomology X₊ Y n definition cohomology_homomorphism [constructor] {X X' : Type*} (f : X' →* X) (Y : spectrum) diff --git a/homotopy/degree.hlean b/homotopy/degree.hlean index 249b88c..7d44180 100644 --- a/homotopy/degree.hlean +++ b/homotopy/degree.hlean @@ -55,7 +55,7 @@ namespace sphere definition deg_id (n : ℕ) [H : is_succ n] : deg (pid (S* n)) = (1 : ℤ) := by induction H with n; - exact ap (πnSn n) (phomotopy_group_functor_pid (succ n) (S* (succ n)) (tr surf)) ⬝ πnSn_surf n + exact ap (πnSn n) (homotopy_group_functor_pid (succ n) (S* (succ n)) (tr surf)) ⬝ πnSn_surf n definition deg_phomotopy {n : ℕ} [H : is_succ n] {f g : S* n →* S* n} (p : f ~* g) : deg f = deg g := diff --git a/homotopy/sample.hlean b/homotopy/sample.hlean index b53cc0d..54a787c 100644 --- a/homotopy/sample.hlean +++ b/homotopy/sample.hlean @@ -175,7 +175,7 @@ namespace homotopy apply trunc.rec, intro a', apply pathover_of_tr_eq, - rewrite [transport_eq_Fr,idp_con], + rewrite [eq_transport_Fr,idp_con], revert H, induction n with [n, IH], { intro H, apply is_prop.elim }, { intros H, diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean index 2bf7e8f..a8a26eb 100644 --- a/homotopy/smash.hlean +++ b/homotopy/smash.hlean @@ -1,181 +1,9 @@ -- Authors: Floris van Doorn -/- - In this file we define the smash type. This is the cofiber of the map - wedge A B → A × B - However, we define it (equivalently) as the pushout of the maps A + B → 2 and A + B → A × B. --/ - -import homotopy.circle homotopy.join types.pointed homotopy.cofiber ..move_to_lib +import homotopy.smash open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge -namespace smash - - variables {A B : Type*} - - section - open pushout - - definition prod_of_sum [unfold 3] (u : A + B) : A × B := - by induction u with a b; exact (a, pt); exact (pt, b) - - definition bool_of_sum [unfold 3] (u : A + B) : bool := - by induction u; exact ff; exact tt - - definition smash' (A B : Type*) : Type := pushout (@prod_of_sum A B) (@bool_of_sum A B) - protected definition mk (a : A) (b : B) : smash' A B := inl (a, b) - - definition pointed_smash' [instance] [constructor] (A B : Type*) : pointed (smash' A B) := - pointed.mk (smash.mk pt pt) - definition smash [constructor] (A B : Type*) : Type* := - pointed.mk' (smash' A B) - - definition auxl : smash A B := inr ff - definition auxr : smash A B := inr tt - definition gluel (a : A) : smash.mk a pt = auxl :> smash A B := glue (inl a) - definition gluer (b : B) : smash.mk pt b = auxr :> smash A B := glue (inr b) - - end - - definition gluel' (a a' : A) : smash.mk a pt = smash.mk a' pt :> smash A B := - gluel a ⬝ (gluel a')⁻¹ - definition gluer' (b b' : B) : smash.mk pt b = smash.mk pt b' :> smash A B := - gluer b ⬝ (gluer b')⁻¹ - definition glue (a : A) (b : B) : smash.mk a pt = smash.mk pt b := - gluel' a pt ⬝ gluer' pt b - - definition glue_pt_left (b : B) : glue (Point A) b = gluer' pt b := - whisker_right !con.right_inv _ ⬝ !idp_con - - definition glue_pt_right (a : A) : glue a (Point B) = gluel' a pt := - proof whisker_left _ !con.right_inv qed - - definition ap_mk_left {a a' : A} (p : a = a') : ap (λa, smash.mk a (Point B)) p = gluel' a a' := - by induction p; exact !con.right_inv⁻¹ - - definition ap_mk_right {b b' : B} (p : b = b') : ap (smash.mk (Point A)) p = gluer' b b' := - by induction p; exact !con.right_inv⁻¹ - - protected definition rec {P : smash A B → Type} (Pmk : Πa b, P (smash.mk a b)) - (Pl : P auxl) (Pr : P auxr) (Pgl : Πa, Pmk a pt =[gluel a] Pl) - (Pgr : Πb, Pmk pt b =[gluer b] Pr) (x : smash' A B) : P x := - begin - induction x with x b u, - { induction x with a b, exact Pmk a b }, - { induction b, exact Pl, exact Pr }, - { induction u: esimp, - { apply Pgl }, - { apply Pgr }} - end - - -- a rec which is easier to prove, but with worse computational properties - protected definition rec' {P : smash A B → Type} (Pmk : Πa b, P (smash.mk a b)) - (Pg : Πa b, Pmk a pt =[glue a b] Pmk pt b) (x : smash' A B) : P x := - begin - induction x using smash.rec, - { apply Pmk }, - { exact gluel pt ▸ Pmk pt pt }, - { exact gluer pt ▸ Pmk pt pt }, - { refine change_path _ (Pg a pt ⬝o !pathover_tr), - refine whisker_right !glue_pt_right _ ⬝ _, esimp, refine !con.assoc ⬝ _, - apply whisker_left, apply con.left_inv }, - { refine change_path _ ((Pg pt b)⁻¹ᵒ ⬝o !pathover_tr), - refine whisker_right !glue_pt_left⁻² _ ⬝ _, - refine whisker_right !inv_con_inv_right _ ⬝ _, refine !con.assoc ⬝ _, - apply whisker_left, apply con.left_inv } - end - - theorem rec_gluel {P : smash A B → Type} {Pmk : Πa b, P (smash.mk a b)} - {Pl : P auxl} {Pr : P auxr} (Pgl : Πa, Pmk a pt =[gluel a] Pl) - (Pgr : Πb, Pmk pt b =[gluer b] Pr) (a : A) : - apd (smash.rec Pmk Pl Pr Pgl Pgr) (gluel a) = Pgl a := - !pushout.rec_glue - - theorem rec_gluer {P : smash A B → Type} {Pmk : Πa b, P (smash.mk a b)} - {Pl : P auxl} {Pr : P auxr} (Pgl : Πa, Pmk a pt =[gluel a] Pl) - (Pgr : Πb, Pmk pt b =[gluer b] Pr) (b : B) : - apd (smash.rec Pmk Pl Pr Pgl Pgr) (gluer b) = Pgr b := - !pushout.rec_glue - - theorem rec_glue {P : smash A B → Type} {Pmk : Πa b, P (smash.mk a b)} - {Pl : P auxl} {Pr : P auxr} (Pgl : Πa, Pmk a pt =[gluel a] Pl) - (Pgr : Πb, Pmk pt b =[gluer b] Pr) (a : A) (b : B) : - apd (smash.rec Pmk Pl Pr Pgl Pgr) (glue a b) = - (Pgl a ⬝o (Pgl pt)⁻¹ᵒ) ⬝o (Pgr pt ⬝o (Pgr b)⁻¹ᵒ) := - by rewrite [↑glue, ↑gluel', ↑gluer', +apd_con, +apd_inv, +rec_gluel, +rec_gluer] - - protected definition elim {P : Type} (Pmk : Πa b, P) (Pl Pr : P) - (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (x : smash' A B) : P := - smash.rec Pmk Pl Pr (λa, pathover_of_eq _ (Pgl a)) (λb, pathover_of_eq _ (Pgr b)) x - - -- an elim which is easier to prove, but with worse computational properties - protected definition elim' {P : Type} (Pmk : Πa b, P) (Pg : Πa b, Pmk a pt = Pmk pt b) - (x : smash' A B) : P := - smash.rec' Pmk (λa b, pathover_of_eq _ (Pg a b)) x - - theorem elim_gluel {P : Type} {Pmk : Πa b, P} {Pl Pr : P} - (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (a : A) : - ap (smash.elim Pmk Pl Pr Pgl Pgr) (gluel a) = Pgl a := - begin - apply eq_of_fn_eq_fn_inv !(pathover_constant (@gluel A B a)), - rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑smash.elim,rec_gluel], - end - - theorem elim_gluer {P : Type} {Pmk : Πa b, P} {Pl Pr : P} - (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (b : B) : - ap (smash.elim Pmk Pl Pr Pgl Pgr) (gluer b) = Pgr b := - begin - apply eq_of_fn_eq_fn_inv !(pathover_constant (@gluer A B b)), - rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑smash.elim,rec_gluer], - end - - theorem elim_glue {P : Type} {Pmk : Πa b, P} {Pl Pr : P} - (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (a : A) (b : B) : - ap (smash.elim Pmk Pl Pr Pgl Pgr) (glue a b) = (Pgl a ⬝ (Pgl pt)⁻¹) ⬝ (Pgr pt ⬝ (Pgr b)⁻¹) := - by rewrite [↑glue, ↑gluel', ↑gluer', +ap_con, +ap_inv, +elim_gluel, +elim_gluer] - -end smash -open smash -attribute smash.mk auxl auxr [constructor] -attribute smash.rec smash.elim [unfold 9] [recursor 9] -attribute smash.rec' smash.elim' [unfold 6] - -namespace smash - - variables {A B : Type*} - - definition of_smash_pbool [unfold 2] (x : smash A pbool) : A := - begin - induction x, - { induction b, exact pt, exact a }, - { exact pt }, - { exact pt }, - { reflexivity }, - { induction b: reflexivity } - end - - definition smash_pbool_equiv [constructor] (A : Type*) : smash A pbool ≃* A := - begin - fapply pequiv_of_equiv, - { fapply equiv.MK, - { exact of_smash_pbool }, - { intro a, exact smash.mk a tt }, - { intro a, reflexivity }, - { exact abstract begin intro x, induction x using smash.rec', - { induction b, exact (glue a tt)⁻¹, reflexivity }, - { apply eq_pathover_id_right, induction b: esimp, - { refine ap02 _ !glue_pt_right ⬝ph _, - refine ap_compose (λx, smash.mk x _) _ _ ⬝ph _, - refine ap02 _ (!ap_con ⬝ (!elim_gluel ◾ (!ap_inv ⬝ !elim_gluel⁻²))) ⬝ph _, - apply hinverse, apply square_of_eq, - esimp, refine (!glue_pt_right ◾ !glue_pt_left)⁻¹ }, - { apply square_of_eq, refine !con.left_inv ⬝ _, esimp, symmetry, - refine ap_compose (λx, smash.mk x _) _ _ ⬝ _, - exact ap02 _ !elim_glue }} end end }}, - { reflexivity } - end - /- smash A (susp B) = susp (smash A B) <- this follows from associativity and smash with S¹-/ /- To prove: Σ(X × Y) ≃ ΣX ∨ ΣY ∨ Σ(X ∧ Y) (notation means suspension, wedge, smash), @@ -185,7 +13,11 @@ namespace smash /- smash A B ≃ pcofiber (pprod_of_pwedge A B) -/ - definition prod_of_wedge [unfold 3] (v : pwedge' A B) : A × B := +namespace smash + + variables {A B : Type*} + + definition prod_of_wedge [unfold 3] (v : pwedge A B) : A × B := begin induction v with a b , { exact (a, pt) }, @@ -194,7 +26,7 @@ namespace smash end variables (A B) - definition pprod_of_pwedge [constructor] : pwedge' A B →* A ×* B := + definition pprod_of_pwedge [constructor] : pwedge A B →* A ×* B := begin fconstructor, { exact prod_of_wedge }, @@ -203,7 +35,7 @@ namespace smash variables {A B} attribute pcofiber [constructor] - definition pcofiber_of_smash [unfold 3] (x : smash A B) : pcofiber' (@pprod_of_pwedge A B) := + definition pcofiber_of_smash [unfold 3] (x : smash A B) : pcofiber (@pprod_of_pwedge A B) := begin induction x, { exact pushout.inr (a, b) }, @@ -218,7 +50,7 @@ namespace smash (p : x = x') : ap (λx, f (g x) (h x)) p = ap011 f (ap g p) (ap h p) := by induction p; reflexivity - definition smash_of_pcofiber_glue [unfold 3] (x : pwedge' A B) : + definition smash_of_pcofiber_glue [unfold 3] (x : pwedge A B) : Point (smash A B) = smash.mk (prod_of_wedge x).1 (prod_of_wedge x).2 := begin induction x with a b: esimp, @@ -231,7 +63,7 @@ namespace smash exact !con.right_inv ⬝ !con.right_inv⁻¹ } end - definition smash_of_pcofiber [unfold 3] (x : pcofiber' (pprod_of_pwedge A B)) : smash A B := + definition smash_of_pcofiber [unfold 3] (x : pcofiber (pprod_of_pwedge A B)) : smash A B := begin induction x with x x, { exact smash.mk pt pt }, @@ -239,7 +71,7 @@ namespace smash { exact smash_of_pcofiber_glue x } end - definition pcofiber_of_smash_of_pcofiber (x : pcofiber' (pprod_of_pwedge A B)) : + definition pcofiber_of_smash_of_pcofiber (x : pcofiber (pprod_of_pwedge A B)) : pcofiber_of_smash (smash_of_pcofiber x) = x := begin induction x with x x, @@ -257,16 +89,16 @@ namespace smash { apply gluer }, { apply eq_pathover_id_right, refine ap_compose smash_of_pcofiber _ _ ⬝ph _, refine ap02 _ !elim_gluel ⬝ph _, refine !ap_inv ⬝ph _, refine !pushout.elim_glue⁻² ⬝ph _, - esimp, apply square_of_eq, refine !idp_con ⬝ _ ⬝ whisker_right !inv_con_inv_right⁻¹ _, + esimp, apply square_of_eq, refine !idp_con ⬝ _ ⬝ whisker_right _ !inv_con_inv_right⁻¹, exact !inv_con_cancel_right⁻¹ }, { apply eq_pathover_id_right, refine ap_compose smash_of_pcofiber _ _ ⬝ph _, refine ap02 _ !elim_gluer ⬝ph _, refine !ap_inv ⬝ph _, refine !pushout.elim_glue⁻² ⬝ph _, - esimp, apply square_of_eq, refine !idp_con ⬝ _ ⬝ whisker_right !inv_con_inv_right⁻¹ _, + esimp, apply square_of_eq, refine !idp_con ⬝ _ ⬝ whisker_right _ !inv_con_inv_right⁻¹, exact !inv_con_cancel_right⁻¹ }, end variables (A B) - definition smash_pequiv_pcofiber : smash A B ≃* pcofiber' (pprod_of_pwedge A B) := + definition smash_pequiv_pcofiber : smash A B ≃* pcofiber (pprod_of_pwedge A B) := begin fapply pequiv_of_equiv, { fapply equiv.MK, @@ -315,7 +147,7 @@ exit -- the definitions below compile, but take a long time to do so and have so apply square_of_eq, rewrite [+con.assoc], apply whisker_left, apply whisker_left, symmetry, apply con_eq_of_eq_inv_con, esimp, apply con_eq_of_eq_con_inv, refine _⁻² ⬝ !con_inv, refine _ ⬝ !con.assoc, - refine _ ⬝ whisker_right !inv_con_cancel_right⁻¹ _, refine _ ⬝ !con.right_inv⁻¹, + refine _ ⬝ whisker_right _ !inv_con_cancel_right⁻¹, refine _ ⬝ !con.right_inv⁻¹, refine !con.right_inv ◾ _, refine _ ◾ !con.right_inv, refine !ap_mk_right ⬝ !con.right_inv end end } end @@ -328,7 +160,7 @@ exit -- the definitions below compile, but take a long time to do so and have so begin refine ap02 _ !elim_gluer ⬝ph _, induction b, - { apply square_of_eq, exact whisker_right !con.right_inv _ }, + { apply square_of_eq, exact whisker_right _ !con.right_inv }, { apply square_pathover', exact sorry } end @@ -361,7 +193,7 @@ exit -- the definitions below compile, but take a long time to do so and have so refine ap_compose smash_pcircle_of_psusp _ _ ⬝ph _, refine ap02 _ !elim_gluer ⬝ph _, induction b, - { apply square_of_eq, exact whisker_right !con.right_inv _ }, + { apply square_of_eq, exact whisker_right _ !con.right_inv }, { exact sorry} }}}, { reflexivity } diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index 88be0b1..63dc0db 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -6,6 +6,7 @@ Authors: Michael Shulman, Floris van Doorn -/ import homotopy.LES_of_homotopy_groups .splice homotopy.susp ..move_to_lib ..colim + ..pointed_pi open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group seq_colim @@ -190,7 +191,7 @@ namespace spectrum -- Suspension prespectra are one that's naturally indexed on the natural numbers definition psp_susp (X : Type*) : gen_prespectrum +ℕ := - gen_prespectrum.mk (λn, psuspn n X) (λn, loop_susp_unit (psuspn n X)) + gen_prespectrum.mk (λn, psuspn n X) (λn, loop_psusp_unit (psuspn n X)) /- Truncations -/ @@ -210,7 +211,7 @@ namespace spectrum -- read off the homotopy groups without any tedious case-analysis of -- n. We increment by 2 in order to ensure that they are all -- automatically abelian groups. - definition shomotopy_group [constructor] (n : ℤ) (E : spectrum) : CommGroup := πag[0+2] (E (2 - n)) + definition shomotopy_group [constructor] (n : ℤ) (E : spectrum) : AbGroup := πag[0+2] (E (2 - n)) notation `πₛ[`:95 n:0 `]`:0 := shomotopy_group n @@ -234,9 +235,10 @@ namespace spectrum -- Sections of parametrized spectra ---------------------------------------- - definition spi {N : succ_str} (A : Type) (E : A -> gen_spectrum N) : gen_spectrum N := - spectrum.MK (λn, ppi (λa, E a n)) - (λn, (loop_ppi_commute (λa, E a (S n)))⁻¹ᵉ* ∘*ᵉ equiv_ppi_right (λa, equiv_glue (E a) n)) + -- this definition must be changed to use dependent maps respecting the basepoint, presumably + -- definition spi {N : succ_str} (A : Type) (E : A -> gen_spectrum N) : gen_spectrum N := + -- spectrum.MK (λn, ppi (λa, E a n)) + -- (λn, (loop_ppi_commute (λa, E a (S n)))⁻¹ᵉ* ∘*ᵉ equiv_ppi_right (λa, equiv_glue (E a) n)) /----------------------------------------- Fibers and long exact sequences @@ -311,12 +313,12 @@ namespace spectrum example (n : ℤ) : cc_to_fn LES_of_shomotopy_groups (n, 1) = πₛ→[n] (spoint f) := idp -- the maps are ugly for (n, 2) - definition comm_group_LES_of_shomotopy_groups : Π(v : +3ℤ), comm_group (LES_of_shomotopy_groups v) - | (n, fin.mk 0 H) := proof CommGroup.struct (πₛ[n] Y) qed - | (n, fin.mk 1 H) := proof CommGroup.struct (πₛ[n] X) qed - | (n, fin.mk 2 H) := proof CommGroup.struct (πₛ[n] (sfiber f)) qed + definition ab_group_LES_of_shomotopy_groups : Π(v : +3ℤ), ab_group (LES_of_shomotopy_groups v) + | (n, fin.mk 0 H) := proof AbGroup.struct (πₛ[n] Y) qed + | (n, fin.mk 1 H) := proof AbGroup.struct (πₛ[n] X) qed + | (n, fin.mk 2 H) := proof AbGroup.struct (πₛ[n] (sfiber f)) qed | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - local attribute comm_group_LES_of_shomotopy_groups [instance] + local attribute ab_group_LES_of_shomotopy_groups [instance] definition is_homomorphism_LES_of_shomotopy_groups : Π(v : +3ℤ), is_homomorphism (cc_to_fn LES_of_shomotopy_groups v) @@ -330,7 +332,7 @@ namespace spectrum -- In the comments below is a start on an explicit description of the LES for spectra -- Maybe it's slightly nicer to work with than the above version --- definition shomotopy_groups [reducible] : -3ℤ → CommGroup +-- definition shomotopy_groups [reducible] : -3ℤ → AbGroup -- | (n, fin.mk 0 H) := πₛ[n] Y -- | (n, fin.mk 1 H) := πₛ[n] X -- | (n, fin.mk k H) := πₛ[n] (sfiber f) diff --git a/homotopy/spherical_fibrations.hlean b/homotopy/spherical_fibrations.hlean index 288b9f5..a53c6ea 100644 --- a/homotopy/spherical_fibrations.hlean +++ b/homotopy/spherical_fibrations.hlean @@ -90,7 +90,7 @@ namespace spherical_fibrations 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), + apply sigma.mk (smash 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 diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 718a77e..fe4027c 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -5,212 +5,26 @@ import homotopy.sphere2 homotopy.cofiber homotopy.wedge open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group is_trunc function sphere -attribute equiv.symm equiv.trans is_equiv.is_equiv_ap fiber.equiv_postcompose - fiber.equiv_precompose pequiv.to_pmap pequiv._trans_of_to_pmap ghomotopy_group_succ_in - isomorphism_of_eq pmap_bool_equiv sphere_equiv_bool psphere_pequiv_pbool fiber_eq_equiv int.equiv_succ - [constructor] -attribute is_equiv.eq_of_fn_eq_fn' [unfold 3] -attribute isomorphism._trans_of_to_hom [unfold 3] -attribute homomorphism.struct [unfold 3] -attribute pequiv.trans pequiv.symm [constructor] - -namespace equiv - - variables {A B : Type} (f : A ≃ B) {a : A} {b : B} - definition to_eq_of_eq_inv (p : a = f⁻¹ b) : f a = b := - ap f p ⬝ right_inv f b - - definition to_eq_of_inv_eq (p : f⁻¹ b = a) : b = f a := - (eq_of_eq_inv p⁻¹)⁻¹ - - definition to_inv_eq_of_eq (p : b = f a) : f⁻¹ b = a := - ap f⁻¹ p ⬝ left_inv f a - - definition to_eq_inv_of_eq (p : f a = b) : a = f⁻¹ b := - (inv_eq_of_eq p⁻¹)⁻¹ - -end equiv open equiv - -namespace sigma - - definition sigma_equiv_sigma_left' [constructor] {A A' : Type} {B : A' → Type} (Hf : A ≃ A') : (Σa, B (Hf a)) ≃ (Σa', B a') := - sigma_equiv_sigma Hf (λa, erfl) - -end sigma -open sigma - namespace group open is_trunc -- some extra instances for type class inference - definition is_homomorphism_comm_homomorphism [instance] {G G' : CommGroup} (φ : G →g G') - : @is_homomorphism G G' (@comm_group.to_group _ (CommGroup.struct G)) - (@comm_group.to_group _ (CommGroup.struct G')) φ := - homomorphism.struct φ + -- definition is_homomorphism_comm_homomorphism [instance] {G G' : AbGroup} (φ : G →g G') + -- : @is_homomorphism G G' (@ab_group.to_group _ (AbGroup.struct G)) + -- (@ab_group.to_group _ (AbGroup.struct G')) φ := + -- homomorphism.struct φ - definition is_homomorphism_comm_homomorphism1 [instance] {G G' : CommGroup} (φ : G →g G') - : @is_homomorphism G G' _ - (@comm_group.to_group _ (CommGroup.struct G')) φ := - homomorphism.struct φ + -- definition is_homomorphism_comm_homomorphism1 [instance] {G G' : AbGroup} (φ : G →g G') + -- : @is_homomorphism G G' _ + -- (@ab_group.to_group _ (AbGroup.struct G')) φ := + -- homomorphism.struct φ - definition is_homomorphism_comm_homomorphism2 [instance] {G G' : CommGroup} (φ : G →g G') - : @is_homomorphism G G' (@comm_group.to_group _ (CommGroup.struct G)) _ φ := - homomorphism.struct φ - - theorem inv_eq_one {A : Type} [group A] {a : A} (H : a = 1) : a⁻¹ = 1 := - iff.mpr (inv_eq_one_iff_eq_one a) H - - definition pSet_of_Group (G : Group) : Set* := ptrunctype.mk G _ 1 - - definition pmap_of_isomorphism [constructor] {G₁ : Group} {G₂ : Group} - (φ : G₁ ≃g G₂) : pType_of_Group G₁ →* pType_of_Group G₂ := - pequiv_of_isomorphism φ - - definition pequiv_of_isomorphism_of_eq {G₁ G₂ : Group} (p : G₁ = G₂) : - pequiv_of_isomorphism (isomorphism_of_eq p) = pequiv_of_eq (ap pType_of_Group p) := - begin - induction p, - apply pequiv_eq, - fapply pmap_eq, - { intro g, reflexivity}, - { apply is_prop.elim} - end - - definition homomorphism_change_fun [constructor] {G₁ G₂ : Group} - (φ : G₁ →g G₂) (f : G₁ → G₂) (p : φ ~ f) : G₁ →g G₂ := - homomorphism.mk f (λg h, (p (g * h))⁻¹ ⬝ to_respect_mul φ g h ⬝ ap011 mul (p g) (p h)) - - definition Group_of_pgroup (G : Type*) [pgroup G] : Group := - Group.mk G _ - - definition pgroup_pType_of_Group [instance] (G : Group) : pgroup (pType_of_Group G) := - ⦃ pgroup, Group.struct G, - pt_mul := one_mul, - mul_pt := mul_one, - mul_left_inv_pt := mul.left_inv ⦄ - - definition comm_group_pType_of_Group [instance] (G : CommGroup) : comm_group (pType_of_Group G) := - CommGroup.struct G - - abbreviation gid [constructor] := @homomorphism_id - - definition comm_group.to_has_mul {A : Type} (H : comm_group A) : has_mul A := _ - local attribute comm_group.to_has_mul [coercion] - - definition comm_group_eq {A : Type} {G H : comm_group A} - (same_mul : Π(g h : A), @mul A G g h = @mul A H g h) - : G = H := - begin - have g_eq : @comm_group.to_group A G = @comm_group.to_group A H, from group_eq same_mul, - cases G with Gm Gs Gh1 G1 Gh2 Gh3 Gi Gh4 Gh5, - cases H with Hm Hs Hh1 H1 Hh2 Hh3 Hi Hh4 Hh5, - have pm : Gm = Hm, from ap (@mul _ ∘ _) g_eq, - have pi : Gi = Hi, from ap (@inv _ ∘ _) g_eq, - have p1 : G1 = H1, from ap (@one _ ∘ _) g_eq, - induction pm, induction pi, induction p1, - have ps : Gs = Hs, from !is_prop.elim, - have ph1 : Gh1 = Hh1, from !is_prop.elim, - have ph2 : Gh2 = Hh2, from !is_prop.elim, - have ph3 : Gh3 = Hh3, from !is_prop.elim, - have ph4 : Gh4 = Hh4, from !is_prop.elim, - have ph5 : Gh5 = Hh5, from !is_prop.elim, - induction ps, induction ph1, induction ph2, induction ph3, induction ph4, induction ph5, - reflexivity - end - - definition comm_group_pathover {A B : Type} {G : comm_group A} {H : comm_group B} {p : A = B} - (resp_mul : Π(g h : A), cast p (g * h) = cast p g * cast p h) : G =[p] H := - begin - induction p, - apply pathover_idp_of_eq, exact comm_group_eq (resp_mul) - end - - definition CommGroup_eq_of_isomorphism {G₁ G₂ : CommGroup} (φ : G₁ ≃g G₂) : G₁ = G₂ := - begin - induction G₁, induction G₂, - apply apd011 CommGroup.mk (ua (equiv_of_isomorphism φ)), - apply comm_group_pathover, - intro g h, exact !cast_ua ⬝ respect_mul φ g h ⬝ ap011 mul !cast_ua⁻¹ !cast_ua⁻¹ - end + -- definition is_homomorphism_comm_homomorphism2 [instance] {G G' : AbGroup} (φ : G →g G') + -- : @is_homomorphism G G' (@ab_group.to_group _ (AbGroup.struct G)) _ φ := + -- homomorphism.struct φ end group open group -namespace trunc - - -- TODO: make argument in ptrunc_pequiv implicit - - definition ptr [constructor] (n : ℕ₋₂) (A : Type*) : A →* ptrunc n A := - pmap.mk tr idp - - definition puntrunc [constructor] (n : ℕ₋₂) (A : Type*) [is_trunc n A] : ptrunc n A →* A := - pmap.mk untrunc_of_is_trunc idp - - definition ptrunc.elim [constructor] (n : ℕ₋₂) {X Y : Type*} [is_trunc n Y] (f : X →* Y) : - ptrunc n X →* Y := - pmap.mk (trunc.elim f) (respect_pt f) - - definition ptrunc_elim_ptr [constructor] (n : ℕ₋₂) {X Y : Type*} [is_trunc n Y] (f : X →* Y) : - ptrunc.elim n f ∘* ptr n X ~* f := - begin - fapply phomotopy.mk, - { reflexivity }, - { reflexivity } - end - - definition ptrunc_elim_phomotopy (n : ℕ₋₂) {X Y : Type*} [is_trunc n Y] {f g : X →* Y} - (H : f ~* g) : ptrunc.elim n f ~* ptrunc.elim n g := - begin - fapply phomotopy.mk, - { intro x, induction x with x, exact H x }, - { exact to_homotopy_pt H } - end - - definition ap1_ptrunc_functor (n : ℕ₋₂) {A B : Type*} (f : A →* B) : - Ω→ (ptrunc_functor (n.+1) f) ∘* (loop_ptrunc_pequiv n A)⁻¹ᵉ* ~* - (loop_ptrunc_pequiv n B)⁻¹ᵉ* ∘* ptrunc_functor n (Ω→ f) := - begin - fapply phomotopy.mk, - { intro p, induction p with p, - refine (!ap_inv⁻¹ ◾ !ap_compose⁻¹ ◾ idp) ⬝ _ ⬝ !ap_con⁻¹, - apply whisker_right, refine _ ⬝ !ap_con⁻¹, exact whisker_left _ !ap_compose }, - { induction B with B b, induction f with f p, esimp at f, esimp at p, induction p, reflexivity } - end - - definition ap1_ptrunc_elim (n : ℕ₋₂) {A B : Type*} (f : A →* B) [is_trunc (n.+1) B] : - Ω→ (ptrunc.elim (n.+1) f) ∘* (loop_ptrunc_pequiv n A)⁻¹ᵉ* ~* - ptrunc.elim n (Ω→ f) := - begin - fapply phomotopy.mk, - { intro p, induction p with p, exact idp ◾ !ap_compose⁻¹ ◾ idp }, - { reflexivity } - end - - definition ap1_ptr (n : ℕ₋₂) (A : Type*) : - Ω→ (ptr (n.+1) A) ~* (loop_ptrunc_pequiv n A)⁻¹ᵉ* ∘* ptr n (Ω A) := - begin - fapply phomotopy.mk, - { intro p, apply idp_con }, - { reflexivity } - end - - -- definition ap1_ptr' (n : ℕ₋₂) (A : Type*) : - -- loop_ptrunc_pequiv n A ∘* Ω→ (ptr (n.+1) A) ~* ptr n (Ω A) := - -- begin - -- fapply phomotopy.mk, - -- { intro p, refine ap trunc.encode !idp_con ⬝ _, esimp, }, - -- { reflexivity } - -- end - - definition ptrunc_elim_ptrunc_functor (n : ℕ₋₂) {A B C : Type*} (g : B →* C) (f : A →* B) - [is_trunc n C] : - ptrunc.elim n g ∘* ptrunc_functor n f ~* ptrunc.elim n (g ∘* f) := - begin - fapply phomotopy.mk, - { intro x, induction x with a, reflexivity }, - { esimp, exact !idp_con ⬝ whisker_right !ap_compose _ }, - end - -end trunc open trunc namespace pi -- move to types.arrow @@ -243,377 +57,30 @@ end pi open pi namespace eq - -- types.eq - definition loop_equiv_eq_closed [constructor] {A : Type} {a a' : A} (p : a = a') - : (a = a) ≃ (a' = a') := - eq_equiv_eq_closed p p - - -- init.path - definition tr_ap {A B : Type} {x y : A} (P : B → Type) (f : A → B) (p : x = y) (z : P (f x)) : - transport P (ap f p) z = transport (P ∘ f) p z := - (tr_compose P f p z)⁻¹ - - - definition pathover_eq_Fl' {A B : Type} {f : A → B} {a₁ a₂ : A} {b : B} (p : a₁ = a₂) (q : f a₂ = b) : (ap f p) ⬝ q =[p] q := - by induction p; induction q; exact idpo - - -- this should be renamed square_pathover. The one in cubical.cube should be renamed - definition square_pathover' {A B : Type} {a a' : A} {b₁ b₂ b₃ b₄ : A → B} - {f₁ : b₁ ~ b₂} {f₂ : b₃ ~ b₄} {f₃ : b₁ ~ b₃} {f₄ : b₂ ~ b₄} {p : a = a'} - {q : square (f₁ a) (f₂ a) (f₃ a) (f₄ a)} - {r : square (f₁ a') (f₂ a') (f₃ a') (f₄ a')} - (s : cube (natural_square_tr f₁ p) (natural_square_tr f₂ p) - (natural_square_tr f₃ p) (natural_square_tr f₄ p) q r) : q =[p] r := - by induction p; apply pathover_idp_of_eq; exact eq_of_deg12_cube s - - -- define natural_square_tr this way. Also, natural_square_tr and natural_square should swap names - definition natural_square_tr_eq {A B : Type} {a a' : A} {f g : A → B} - (p : f ~ g) (q : a = a') : natural_square_tr p q = square_of_pathover (apd p q) := - by induction q; reflexivity - - section - variables {A : Type} {a₀₀₀ a₂₀₀ a₀₂₀ a₂₂₀ a₀₀₂ a₂₀₂ a₀₂₂ a₂₂₂ : A} - {p₁₀₀ : a₀₀₀ = a₂₀₀} {p₀₁₀ : a₀₀₀ = a₀₂₀} {p₀₀₁ : a₀₀₀ = a₀₀₂} - {p₁₂₀ : a₀₂₀ = a₂₂₀} {p₂₁₀ : a₂₀₀ = a₂₂₀} {p₂₀₁ : a₂₀₀ = a₂₀₂} - {p₁₀₂ : a₀₀₂ = a₂₀₂} {p₀₁₂ : a₀₀₂ = a₀₂₂} {p₀₂₁ : a₀₂₀ = a₀₂₂} - {p₁₂₂ : a₀₂₂ = a₂₂₂} {p₂₁₂ : a₂₀₂ = a₂₂₂} {p₂₂₁ : a₂₂₀ = a₂₂₂} - {s₁₁₀ : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀} - {s₁₁₂ : square p₀₁₂ p₂₁₂ p₁₀₂ p₁₂₂} - {s₀₁₁ : square p₀₁₀ p₀₁₂ p₀₀₁ p₀₂₁} - {s₂₁₁ : square p₂₁₀ p₂₁₂ p₂₀₁ p₂₂₁} - {s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁} - {s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁} - - -- move to cubical.cube - definition eq_concat1 {s₀₁₁' : square p₀₁₀ p₀₁₂ p₀₀₁ p₀₂₁} (r : s₀₁₁' = s₀₁₁) - (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : cube s₀₁₁' s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂ := - by induction r; exact c - - definition concat1_eq {s₂₁₁' : square p₂₁₀ p₂₁₂ p₂₀₁ p₂₂₁} - (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) (r : s₂₁₁ = s₂₁₁') - : cube s₀₁₁ s₂₁₁' s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂ := - by induction r; exact c - - definition eq_concat2 {s₁₀₁' : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁} (r : s₁₀₁' = s₁₀₁) - (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : cube s₀₁₁ s₂₁₁ s₁₀₁' s₁₂₁ s₁₁₀ s₁₁₂ := - by induction r; exact c - - definition concat2_eq {s₁₂₁' : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁} - (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) (r : s₁₂₁ = s₁₂₁') - : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁' s₁₁₀ s₁₁₂ := - by induction r; exact c - - definition eq_concat3 {s₁₁₀' : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀} (r : s₁₁₀' = s₁₁₀) - (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀' s₁₁₂ := - by induction r; exact c - - definition concat3_eq {s₁₁₂' : square p₀₁₂ p₂₁₂ p₁₀₂ p₁₂₂} - (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) (r : s₁₁₂ = s₁₁₂') - : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂' := - by induction r; exact c - - end - - infix ` ⬝1 `:75 := cube_concat1 - infix ` ⬝2 `:75 := cube_concat2 - infix ` ⬝3 `:75 := cube_concat3 - infix ` ⬝p1 `:75 := eq_concat1 - infix ` ⬝1p `:75 := concat1_eq - infix ` ⬝p2 `:75 := eq_concat3 - infix ` ⬝2p `:75 := concat2_eq - infix ` ⬝p3 `:75 := eq_concat3 - infix ` ⬝3p `:75 := concat3_eq + -- definition natural_square_tr_eq {A B : Type} {a a' : A} {f g : A → B} + -- (p : f ~ g) (q : a = a') : natural_square p q = square_of_pathover (apd p q) := + -- idp end eq open eq namespace pointed - -- in init.pointed `pointed_carrier` should be [unfold 1] instead of [constructor] - definition ptransport [constructor] {A : Type} (B : A → Type*) {a a' : A} (p : a = a') - : B a →* B a' := - pmap.mk (transport B p) (apdt (λa, Point (B a)) p) + -- /- the pointed type of (unpointed) dependent maps -/ + -- definition pupi [constructor] {A : Type} (P : A → Type*) : Type* := + -- pointed.mk' (Πa, P a) - definition ptransport_change_eq [constructor] {A : Type} (B : A → Type*) {a a' : A} {p q : a = a'} - (r : p = q) : ptransport B p ~* ptransport B q := - phomotopy.mk (λb, ap (λp, transport B p b) r) begin induction r, exact !idp_con end + -- definition loop_pupi_commute {A : Type} (B : A → Type*) : Ω(pupi B) ≃* pupi (λa, Ω (B a)) := + -- pequiv_of_equiv eq_equiv_homotopy rfl - definition pnatural_square {A B : Type} (X : B → Type*) {f g : A → B} - (h : Πa, X (f a) →* X (g a)) {a a' : A} (p : a = a') : - h a' ∘* ptransport X (ap f p) ~* ptransport X (ap g p) ∘* h a := - by induction p; exact !pcompose_pid ⬝* !pid_pcompose⁻¹* - - definition pequiv_ap [constructor] {A : Type} (B : A → Type*) {a a' : A} (p : a = a') - : B a ≃* B a' := - pequiv_of_pmap (ptransport B p) !is_equiv_tr - - definition pequiv_compose {A B C : Type*} (g : B ≃* C) (f : A ≃* B) : A ≃* C := - pequiv_of_pmap (g ∘* f) (is_equiv_compose g f) - - infixr ` ∘*ᵉ `:60 := pequiv_compose - - definition pcompose2 {A B C : Type*} {g g' : B →* C} {f f' : A →* B} (p : f ~* f') (q : g ~* g') : - g ∘* f ~* g' ∘* f' := - pwhisker_right f q ⬝* pwhisker_left g' p - - infixr ` ◾* `:80 := pcompose2 - - definition phomotopy_pinv_of_phomotopy_pid {A B : Type*} {f : A →* B} {g : B ≃* A} - (p : g ∘* f ~* pid A) : f ~* g⁻¹ᵉ* := - phomotopy_pinv_left_of_phomotopy p ⬝* !pcompose_pid - - definition phomotopy_pinv_of_phomotopy_pid' {A B : Type*} {f : A →* B} {g : B ≃* A} - (p : f ∘* g ~* pid B) : f ~* g⁻¹ᵉ* := - phomotopy_pinv_right_of_phomotopy p ⬝* !pid_pcompose - - definition pinv_phomotopy_of_pid_phomotopy {A B : Type*} {f : A →* B} {g : B ≃* A} - (p : pid A ~* g ∘* f) : g⁻¹ᵉ* ~* f := - (phomotopy_pinv_of_phomotopy_pid p⁻¹*)⁻¹* - - definition pinv_phomotopy_of_pid_phomotopy' {A B : Type*} {f : A →* B} {g : B ≃* A} - (p : pid B ~* f ∘* g) : g⁻¹ᵉ* ~* f := - (phomotopy_pinv_of_phomotopy_pid' p⁻¹*)⁻¹* - - definition pinv_pinv {A B : Type*} (f : A ≃* B) : (f⁻¹ᵉ*)⁻¹ᵉ* ~* f := - (phomotopy_pinv_of_phomotopy_pid (pleft_inv f))⁻¹* - - definition pinv2 {A B : Type*} {f f' : A ≃* B} (p : f ~* f') : f⁻¹ᵉ* ~* f'⁻¹ᵉ* := - phomotopy_pinv_of_phomotopy_pid (pinv_right_phomotopy_of_phomotopy (!pid_pcompose ⬝* p)⁻¹*) - - postfix [parsing_only] `⁻²*`:(max+10) := pinv2 - - definition trans_pinv {A B C : Type*} (f : A ≃* B) (g : B ≃* C) : - (f ⬝e* g)⁻¹ᵉ* ~* f⁻¹ᵉ* ∘* g⁻¹ᵉ* := - begin - refine (phomotopy_pinv_of_phomotopy_pid _)⁻¹*, - refine !passoc ⬝* _, - refine pwhisker_left _ (!passoc⁻¹* ⬝* pwhisker_right _ !pright_inv ⬝* !pid_pcompose) ⬝* _, - apply pright_inv - end - - definition pinv_trans_pinv_left {A B C : Type*} (f : B ≃* A) (g : B ≃* C) : - (f⁻¹ᵉ* ⬝e* g)⁻¹ᵉ* ~* f ∘* g⁻¹ᵉ* := - !trans_pinv ⬝* pwhisker_right _ !pinv_pinv - - definition pinv_trans_pinv_right {A B C : Type*} (f : A ≃* B) (g : C ≃* B) : - (f ⬝e* g⁻¹ᵉ*)⁻¹ᵉ* ~* f⁻¹ᵉ* ∘* g := - !trans_pinv ⬝* pwhisker_left _ !pinv_pinv - - definition pinv_trans_pinv_pinv {A B C : Type*} (f : B ≃* A) (g : C ≃* B) : - (f⁻¹ᵉ* ⬝e* g⁻¹ᵉ*)⁻¹ᵉ* ~* f ∘* g := - !trans_pinv ⬝* !pinv_pinv ◾* !pinv_pinv - - definition pinv_pcompose_cancel_left {A B C : Type*} (g : B ≃* C) (f : A →* B) : - g⁻¹ᵉ* ∘* (g ∘* f) ~* f := - !passoc⁻¹* ⬝* pwhisker_right f !pleft_inv ⬝* !pid_pcompose - - definition pcompose_pinv_cancel_left {A B C : Type*} (g : C ≃* B) (f : A →* B) : - g ∘* (g⁻¹ᵉ* ∘* f) ~* f := - !passoc⁻¹* ⬝* pwhisker_right f !pright_inv ⬝* !pid_pcompose - - definition pinv_pcompose_cancel_right {A B C : Type*} (g : B →* C) (f : B ≃* A) : - (g ∘* f⁻¹ᵉ*) ∘* f ~* g := - !passoc ⬝* pwhisker_left g !pleft_inv ⬝* !pcompose_pid - - definition pcompose_pinv_cancel_right {A B C : Type*} (g : B →* C) (f : A ≃* B) : - (g ∘* f) ∘* f⁻¹ᵉ* ~* g := - !passoc ⬝* pwhisker_left g !pright_inv ⬝* !pcompose_pid - - definition pmap.sigma_char [constructor] {A B : Type*} : (A →* B) ≃ Σ(f : A → B), f pt = pt := - begin - fapply equiv.MK : intros f, - { exact ⟨to_fun f , resp_pt f⟩ }, - all_goals cases f with f p, - { exact pmap.mk f p }, - all_goals reflexivity - end - - definition is_trunc_pmap [instance] (n : ℕ₋₂) (A B : Type*) [is_trunc n B] : is_trunc n (A →* B) := - is_trunc_equiv_closed_rev _ !pmap.sigma_char - - definition is_trunc_ppmap [instance] (n : ℕ₋₂) {A B : Type*} [is_trunc n B] : - is_trunc n (ppmap A B) := - !is_trunc_pmap - - definition pmap_eq_of_homotopy {A B : Type*} {f g : A →* B} [is_set B] (p : f ~ g) : f = g := - pmap_eq p !is_set.elim - - definition phomotopy.sigma_char [constructor] {A B : Type*} (f g : A →* B) : (f ~* g) ≃ Σ(p : f ~ g), p pt ⬝ resp_pt g = resp_pt f := - begin - fapply equiv.MK : intros h, - { exact ⟨h , to_homotopy_pt h⟩ }, - all_goals cases h with h p, - { exact phomotopy.mk h p }, - all_goals reflexivity - end - - definition pmap_eq_equiv {A B : Type*} (f g : A →* B) : (f = g) ≃ (f ~* g) := - calc (f = g) ≃ pmap.sigma_char f = pmap.sigma_char g - : eq_equiv_fn_eq pmap.sigma_char f g - ... ≃ Σ(p : pmap.to_fun f = pmap.to_fun g), pathover (λh, h pt = pt) (resp_pt f) p (resp_pt g) - : sigma_eq_equiv _ _ - ... ≃ Σ(p : pmap.to_fun f = pmap.to_fun g), resp_pt f = ap (λh, h pt) p ⬝ resp_pt g - : sigma_equiv_sigma_right (λp, pathover_eq_equiv_Fl p (resp_pt f) (resp_pt g)) - ... ≃ Σ(p : pmap.to_fun f = pmap.to_fun g), resp_pt f = ap10 p pt ⬝ resp_pt g - : sigma_equiv_sigma_right (λp, equiv_eq_closed_right _ (whisker_right (ap_eq_apd10 p _) _)) - ... ≃ Σ(p : pmap.to_fun f ~ pmap.to_fun g), resp_pt f = p pt ⬝ resp_pt g - : sigma_equiv_sigma_left' eq_equiv_homotopy - ... ≃ Σ(p : pmap.to_fun f ~ pmap.to_fun g), p pt ⬝ resp_pt g = resp_pt f - : sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _) - ... ≃ (f ~* g) : phomotopy.sigma_char f g - - definition loop_pmap_commute (A B : Type*) : Ω(ppmap A B) ≃* (ppmap A (Ω B)) := - pequiv_of_equiv - (calc Ω(ppmap A B) /- ≃ (pconst A B = pconst A B) : erfl - ... -/ ≃ (pconst A B ~* pconst A B) : pmap_eq_equiv _ _ - ... ≃ Σ(p : pconst A B ~ pconst A B), p pt ⬝ rfl = rfl : phomotopy.sigma_char - ... /- ≃ Σ(f : A → Ω B), f pt = pt : erfl - ... -/ ≃ (A →* Ω B) : pmap.sigma_char) - (by reflexivity) - - definition ap1_pconst (A B : Type*) : Ω→(pconst A B) ~* pconst (Ω A) (Ω B) := - phomotopy.mk (λp, idp_con _ ⬝ ap_constant p pt) rfl - - definition apn_pconst (A B : Type*) (n : ℕ) : - apn n (pconst A B) ~* pconst (Ω[n] A) (Ω[n] B) := - begin - induction n with n IH, - { reflexivity }, - { exact ap1_phomotopy IH ⬝* !ap1_pconst } - end - - definition loop_ppi_commute {A : Type} (B : A → Type*) : Ω(ppi B) ≃* Π*a, Ω (B a) := - pequiv_of_equiv eq_equiv_homotopy rfl - - definition equiv_ppi_right {A : Type} {P Q : A → Type*} (g : Πa, P a ≃* Q a) - : (Π*a, P a) ≃* (Π*a, Q a) := - pequiv_of_equiv (pi_equiv_pi_right g) - begin esimp, apply eq_of_homotopy, intros a, esimp, exact (respect_pt (g a)) end - - definition pcast_commute [constructor] {A : Type} {B C : A → Type*} (f : Πa, B a →* C a) - {a₁ a₂ : A} (p : a₁ = a₂) : pcast (ap C p) ∘* f a₁ ~* f a₂ ∘* pcast (ap B p) := - phomotopy.mk - begin induction p, reflexivity end - begin induction p, esimp, refine !idp_con ⬝ !idp_con ⬝ !ap_id⁻¹ end - - definition pequiv_of_eq_commute [constructor] {A : Type} {B C : A → Type*} (f : Πa, B a →* C a) - {a₁ a₂ : A} (p : a₁ = a₂) : pequiv_of_eq (ap C p) ∘* f a₁ ~* f a₂ ∘* pequiv_of_eq (ap B p) := - pcast_commute f p - - definition papply [constructor] {A : Type*} (B : Type*) (a : A) : ppmap A B →* B := - pmap.mk (λ(f : A →* B), f a) idp - - definition papply_pcompose [constructor] {A : Type*} (B : Type*) (a : A) : ppmap A B →* B := - pmap.mk (λ(f : A →* B), f a) idp - - open bool --also rename pmap_bool_equiv -> pmap_pbool_equiv - - definition pbool_pmap [constructor] {A : Type*} (a : A) : pbool →* A := - pmap.mk (bool.rec pt a) idp - - definition pmap_pbool_pequiv [constructor] (B : Type*) : ppmap pbool B ≃* B := - begin - fapply pequiv.MK, - { exact papply B tt }, - { exact pbool_pmap }, - { intro f, fapply pmap_eq, - { intro b, cases b, exact !respect_pt⁻¹, reflexivity }, - { exact !con.left_inv⁻¹ }}, - { intro b, reflexivity }, - end - - definition papn_pt [constructor] (n : ℕ) (A B : Type*) : ppmap A B →* ppmap (Ω[n] A) (Ω[n] B) := - pmap.mk (λf, apn n f) (eq_of_phomotopy !apn_pconst) - - definition papn_fun [constructor] {n : ℕ} {A : Type*} (B : Type*) (p : Ω[n] A) : - ppmap A B →* Ω[n] B := - papply _ p ∘* papn_pt n A B - - definition loopn_succ_in_natural {A B : Type*} (n : ℕ) (f : A →* B) : - loopn_succ_in B n ∘* Ω→[n+1] f ~* Ω→[n] (Ω→ f) ∘* loopn_succ_in A n := - !apn_succ_phomotopy_in - - definition loopn_succ_in_inv_natural {A B : Type*} (n : ℕ) (f : A →* B) : - Ω→[n + 1] f ∘* (loopn_succ_in A n)⁻¹ᵉ* ~* (loopn_succ_in B n)⁻¹ᵉ* ∘* Ω→[n] (Ω→ f):= - begin - apply pinv_right_phomotopy_of_phomotopy, - refine _ ⬝* !passoc⁻¹*, - apply phomotopy_pinv_left_of_phomotopy, - apply apn_succ_phomotopy_in - end + -- definition equiv_pupi_right {A : Type} {P Q : A → Type*} (g : Πa, P a ≃* Q a) + -- : pupi P ≃* pupi Q := + -- pequiv_of_equiv (pi_equiv_pi_right g) + -- begin esimp, apply eq_of_homotopy, intros a, esimp, exact (respect_pt (g a)) end end pointed open pointed namespace fiber - definition pfiber.sigma_char [constructor] {A B : Type*} (f : A →* B) - : pfiber f ≃* pointed.MK (Σa, f a = pt) ⟨pt, respect_pt f⟩ := - pequiv_of_equiv (fiber.sigma_char f pt) idp - - definition ppoint_sigma_char [constructor] {A B : Type*} (f : A →* B) - : ppoint f ~* pmap.mk pr1 idp ∘* pfiber.sigma_char f := - !phomotopy.refl - - definition pfiber_loop_space {A B : Type*} (f : A →* B) : pfiber (Ω→ f) ≃* Ω (pfiber f) := - pequiv_of_equiv - (calc pfiber (Ω→ f) ≃ Σ(p : Point A = Point A), ap1 f p = rfl - : (fiber.sigma_char (ap1 f) (Point (Ω B))) - ... ≃ Σ(p : Point A = Point A), (respect_pt f) = ap f p ⬝ (respect_pt f) - : (sigma_equiv_sigma_right (λp, - calc (ap1 f p = rfl) ≃ !respect_pt⁻¹ ⬝ (ap f p ⬝ !respect_pt) = rfl - : equiv_eq_closed_left _ (con.assoc _ _ _) - ... ≃ ap f p ⬝ (respect_pt f) = (respect_pt f) - : eq_equiv_inv_con_eq_idp - ... ≃ (respect_pt f) = ap f p ⬝ (respect_pt f) - : eq_equiv_eq_symm)) - ... ≃ fiber.mk (Point A) (respect_pt f) = fiber.mk pt (respect_pt f) - : fiber_eq_equiv - ... ≃ Ω (pfiber f) - : erfl) - (begin cases f with f p, cases A with A a, cases B with B b, esimp at p, esimp at f, - induction p, reflexivity end) - - definition pfiber_equiv_of_phomotopy {A B : Type*} {f g : A →* B} (h : f ~* g) - : pfiber f ≃* pfiber g := - begin - fapply pequiv_of_equiv, - { refine (fiber.sigma_char f pt ⬝e _ ⬝e (fiber.sigma_char g pt)⁻¹ᵉ), - apply sigma_equiv_sigma_right, intros a, - apply equiv_eq_closed_left, apply (to_homotopy h) }, - { refine (fiber_eq rfl _), - change (h pt)⁻¹ ⬝ respect_pt f = idp ⬝ respect_pt g, - rewrite idp_con, apply inv_con_eq_of_eq_con, symmetry, exact (to_homotopy_pt h) } - end - - definition transport_fiber_equiv [constructor] {A B : Type} (f : A → B) {b1 b2 : B} (p : b1 = b2) - : fiber f b1 ≃ fiber f b2 := - calc fiber f b1 ≃ Σa, f a = b1 : fiber.sigma_char - ... ≃ Σa, f a = b2 : sigma_equiv_sigma_right (λa, equiv_eq_closed_right (f a) p) - ... ≃ fiber f b2 : fiber.sigma_char - - definition pequiv_postcompose {A B B' : Type*} (f : A →* B) (g : B ≃* B') - : pfiber (g ∘* f) ≃* pfiber f := - begin - fapply pequiv_of_equiv, esimp, - refine transport_fiber_equiv (g ∘* f) (respect_pt g)⁻¹ ⬝e fiber.equiv_postcompose f g (Point B), - esimp, apply (ap (fiber.mk (Point A))), refine !con.assoc ⬝ _, apply inv_con_eq_of_eq_con, - rewrite [con.assoc, con.right_inv, con_idp, -ap_compose'], apply ap_con_eq_con - end - - definition pequiv_precompose {A A' B : Type*} (f : A →* B) (g : A' ≃* A) - : pfiber (f ∘* g) ≃* pfiber f := - begin - fapply pequiv_of_equiv, esimp, - refine fiber.equiv_precompose f g (Point B), - esimp, apply (eq_of_fn_eq_fn (fiber.sigma_char _ _)), fapply sigma_eq: esimp, - { apply respect_pt g }, - { apply pathover_eq_Fl' } - end - - definition pfiber_equiv_of_square {A B C D : Type*} {f : A →* B} {g : C →* D} (h : A ≃* C) - (k : B ≃* D) (s : k ∘* f ~* g ∘* h) : pfiber f ≃* pfiber g := - calc pfiber f ≃* pfiber (k ∘* f) : pequiv_postcompose - ... ≃* pfiber (g ∘* h) : pfiber_equiv_of_phomotopy s - ... ≃* pfiber g : pequiv_precompose definition ap1_ppoint_phomotopy {A B : Type*} (f : A →* B) : Ω→ (ppoint f) ∘* pfiber_loop_space f ~* ppoint (Ω→ f) := @@ -628,137 +95,6 @@ namespace fiber end fiber -namespace eq --algebra.homotopy_group - - definition phomotopy_group_functor_pid (n : ℕ) (A : Type*) : π→[n] (pid A) ~* pid (π[n] A) := - ptrunc_functor_phomotopy 0 !apn_pid ⬝* !ptrunc_functor_pid - -end eq - -namespace susp - - definition iterate_psusp_functor (n : ℕ) {A B : Type*} (f : A →* B) : - iterate_psusp n A →* iterate_psusp n B := - begin - induction n with n g, - { exact f }, - { exact psusp_functor g } - end - - definition iterate_psusp_succ_in (n : ℕ) (A : Type*) : - iterate_psusp (succ n) A ≃* iterate_psusp n (psusp A) := - begin - induction n with n IH, - { reflexivity}, - { exact psusp_equiv IH} - end - - definition is_conn_psusp [instance] (n : trunc_index) (A : Type*) - [H : is_conn n A] : is_conn (n .+1) (psusp A) := - is_conn_susp n A - -end susp - -namespace is_conn -- homotopy.connectedness - - structure conntype (n : ℕ₋₂) : Type := - (carrier : Type) - (struct : is_conn n carrier) - - notation `Type[`:95 n:0 `]`:0 := conntype n - - attribute conntype.carrier [coercion] - attribute conntype.struct [instance] [priority 1300] - - section - universe variable u - structure pconntype (n : ℕ₋₂) extends conntype.{u} n, pType.{u} - - notation `Type*[`:95 n:0 `]`:0 := pconntype n - - /- - There are multiple coercions from pconntype to Type. Type class inference doesn't recognize - that all of them are definitionally equal (for performance reasons). One instance is - automatically generated, and we manually add the missing instances. - -/ - - definition is_conn_pconntype [instance] {n : ℕ₋₂} (X : Type*[n]) : is_conn n X := - conntype.struct X - - /- Now all the instances work -/ - example {n : ℕ₋₂} (X : Type*[n]) : is_conn n X := _ - example {n : ℕ₋₂} (X : Type*[n]) : is_conn n (pconntype.to_pType X) := _ - example {n : ℕ₋₂} (X : Type*[n]) : is_conn n (pconntype.to_conntype X) := _ - example {n : ℕ₋₂} (X : Type*[n]) : is_conn n (pconntype._trans_of_to_pType X) := _ - example {n : ℕ₋₂} (X : Type*[n]) : is_conn n (pconntype._trans_of_to_conntype X) := _ - - structure truncconntype (n k : ℕ₋₂) extends trunctype.{u} n, - conntype.{u} k renaming struct→conn_struct - - notation n `-Type[`:95 k:0 `]`:0 := truncconntype n k - - definition is_conn_truncconntype [instance] {n k : ℕ₋₂} (X : n-Type[k]) : - is_conn k (truncconntype._trans_of_to_trunctype X) := - conntype.struct X - - definition is_trunc_truncconntype [instance] {n k : ℕ₋₂} (X : n-Type[k]) : is_trunc n X := - trunctype.struct X - - structure ptruncconntype (n k : ℕ₋₂) extends ptrunctype.{u} n, - pconntype.{u} k renaming struct→conn_struct - - notation n `-Type*[`:95 k:0 `]`:0 := ptruncconntype n k - - attribute ptruncconntype._trans_of_to_pconntype ptruncconntype._trans_of_to_ptrunctype - ptruncconntype._trans_of_to_pconntype_1 ptruncconntype._trans_of_to_ptrunctype_1 - ptruncconntype._trans_of_to_pconntype_2 ptruncconntype._trans_of_to_ptrunctype_2 - ptruncconntype.to_pconntype ptruncconntype.to_ptrunctype - truncconntype._trans_of_to_conntype truncconntype._trans_of_to_trunctype - truncconntype.to_conntype truncconntype.to_trunctype [unfold 3] - attribute pconntype._trans_of_to_conntype pconntype._trans_of_to_pType - pconntype.to_pType pconntype.to_conntype [unfold 2] - - definition is_conn_ptruncconntype [instance] {n k : ℕ₋₂} (X : n-Type*[k]) : - is_conn k (ptruncconntype._trans_of_to_ptrunctype X) := - conntype.struct X - - definition is_trunc_ptruncconntype [instance] {n k : ℕ₋₂} (X : n-Type*[k]) : - is_trunc n (ptruncconntype._trans_of_to_pconntype X) := - trunctype.struct X - - definition ptruncconntype_eq {n k : ℕ₋₂} {X Y : n-Type*[k]} (p : X ≃* Y) : X = Y := - begin - induction X with X Xt Xp Xc, induction Y with Y Yt Yp Yc, - note q := pType_eq_elim (eq_of_pequiv p), - cases q with r s, esimp at *, induction r, - exact ap0111 (ptruncconntype.mk X) !is_prop.elim (eq_of_pathover_idp s) !is_prop.elim - end - - end - - -end is_conn - -namespace succ_str - variables {N : succ_str} - - protected definition add [reducible] (n : N) (k : ℕ) : N := - iterate S k n - - infix ` +' `:65 := succ_str.add - - definition add_succ (n : N) (k : ℕ) : n +' (k + 1) = (S n) +' k := - by induction k with k p; reflexivity; exact ap S p - - -end succ_str - -namespace join - - definition pjoin [constructor] (A B : Type*) : Type* := pointed.MK (join A B) (inl pt) - -end join - namespace circle @@ -769,11 +105,11 @@ namespace circle to the square which defined H on the path constructor -/ - definition natural_square_tr_elim_loop {A : Type} {f g : S¹ → A} (p : f base = g base) + definition natural_square_elim_loop {A : Type} {f g : S¹ → A} (p : f base = g base) (q : square p p (ap f loop) (ap g loop)) - : natural_square_tr (circle.rec p (eq_pathover q)) loop = q := + : natural_square (circle.rec p (eq_pathover q)) loop = q := begin - refine !natural_square_tr_eq ⬝ _, + -- refine !natural_square_eq ⬝ _, refine ap square_of_pathover !rec_loop ⬝ _, exact to_right_inv !eq_pathover_equiv_square q end @@ -781,294 +117,8 @@ namespace circle end circle --- this should replace various definitions in homotopy.susp, lines 241 - 338 -namespace new_susp - - variables {X Y Z : Type*} - - definition loop_psusp_unit [constructor] (X : Type*) : X →* Ω(psusp X) := - begin - fconstructor, - { intro x, exact merid x ⬝ (merid pt)⁻¹ }, - { apply con.right_inv }, - end - - definition loop_psusp_unit_natural (f : X →* Y) - : loop_psusp_unit Y ∘* f ~* ap1 (psusp_functor f) ∘* loop_psusp_unit X := - begin - induction X with X x, induction Y with Y y, induction f with f pf, esimp at *, induction pf, - fconstructor, - { intro x', esimp [psusp_functor], symmetry, - exact - !idp_con ⬝ - (!ap_con ⬝ - whisker_left _ !ap_inv) ⬝ - (!elim_merid ◾ (inverse2 !elim_merid)) }, - { rewrite [▸*,idp_con (con.right_inv _)], - apply inv_con_eq_of_eq_con, - refine _ ⬝ !con.assoc', - rewrite inverse2_right_inv, - refine _ ⬝ !con.assoc', - rewrite [ap_con_right_inv], - xrewrite [idp_con_idp, -ap_compose (concat idp)] }, - end - - definition loop_psusp_counit [constructor] (X : Type*) : psusp (Ω X) →* X := - begin - fconstructor, - { intro x, induction x, exact pt, exact pt, exact a }, - { reflexivity }, - end - - definition loop_psusp_counit_natural (f : X →* Y) - : f ∘* loop_psusp_counit X ~* loop_psusp_counit Y ∘* (psusp_functor (ap1 f)) := - begin - induction X with X x, induction Y with Y y, induction f with f pf, esimp at *, induction pf, - fconstructor, - { intro x', induction x' with p, - { reflexivity }, - { reflexivity }, - { esimp, apply eq_pathover, apply hdeg_square, - xrewrite [ap_compose' f, ap_compose' (susp.elim (f x) (f x) (λ (a : f x = f x), a)),▸*], - xrewrite [+elim_merid,▸*,idp_con] }}, - { reflexivity } - end - - definition loop_psusp_counit_unit (X : Type*) - : ap1 (loop_psusp_counit X) ∘* loop_psusp_unit (Ω X) ~* pid (Ω X) := - begin - induction X with X x, fconstructor, - { intro p, esimp, - refine !idp_con ⬝ - (!ap_con ⬝ - whisker_left _ !ap_inv) ⬝ - (!elim_merid ◾ inverse2 !elim_merid) }, - { rewrite [▸*,inverse2_right_inv (elim_merid id idp)], - refine !con.assoc ⬝ _, - xrewrite [ap_con_right_inv (susp.elim x x (λa, a)) (merid idp),idp_con_idp,-ap_compose] } - end - - definition loop_psusp_unit_counit (X : Type*) - : loop_psusp_counit (psusp X) ∘* psusp_functor (loop_psusp_unit X) ~* pid (psusp X) := - begin - induction X with X x, fconstructor, - { intro x', induction x', - { reflexivity }, - { exact merid pt }, - { apply eq_pathover, - xrewrite [▸*, ap_id, ap_compose' (susp.elim north north (λa, a)), +elim_merid,▸*], - apply square_of_eq, exact !idp_con ⬝ !inv_con_cancel_right⁻¹ }}, - { reflexivity } - end - - definition psusp.elim [constructor] {X Y : Type*} (f : X →* Ω Y) : psusp X →* Y := - loop_psusp_counit Y ∘* psusp_functor f - - definition loop_psusp_intro [constructor] {X Y : Type*} (f : psusp X →* Y) : X →* Ω Y := - ap1 f ∘* loop_psusp_unit X - - definition psusp_adjoint_loop_right_inv {X Y : Type*} (g : X →* Ω Y) : - loop_psusp_intro (psusp.elim g) ~* g := - begin - refine !pwhisker_right !ap1_pcompose ⬝* _, - refine !passoc ⬝* _, - refine !pwhisker_left !loop_psusp_unit_natural⁻¹* ⬝* _, - refine !passoc⁻¹* ⬝* _, - refine !pwhisker_right !loop_psusp_counit_unit ⬝* _, - apply pid_pcompose - end - - definition psusp_adjoint_loop_left_inv {X Y : Type*} (f : psusp X →* Y) : - psusp.elim (loop_psusp_intro f) ~* f := - begin - refine !pwhisker_left !psusp_functor_compose ⬝* _, - refine !passoc⁻¹* ⬝* _, - refine !pwhisker_right !loop_psusp_counit_natural⁻¹* ⬝* _, - refine !passoc ⬝* _, - refine !pwhisker_left !loop_psusp_unit_counit ⬝* _, - apply pcompose_pid - end - - definition ap1_psusp_elim {A : Type*} {X : Type*} (p : A →* Ω X) : - Ω→(psusp.elim p) ∘* loop_psusp_unit A ~* p := - psusp_adjoint_loop_right_inv p - - -- TODO: rename to psusp_adjoint_loop (also in above lemmas) - definition psusp_adjoint_loop_unpointed [constructor] (X Y : Type*) : psusp X →* Y ≃ X →* Ω Y := - begin - fapply equiv.MK, - { exact loop_psusp_intro }, - { exact psusp.elim }, - { intro g, apply eq_of_phomotopy, exact psusp_adjoint_loop_right_inv g }, - { intro f, apply eq_of_phomotopy, exact psusp_adjoint_loop_left_inv f } - end - - definition psusp_adjoint_loop_pconst (X Y : Type*) : - psusp_adjoint_loop_unpointed X Y (pconst (psusp X) Y) ~* pconst X (Ω Y) := - begin - refine pwhisker_right _ !ap1_pconst ⬝* _, - apply pconst_pcompose - end - - definition psusp_adjoint_loop [constructor] (X Y : Type*) : ppmap (psusp X) Y ≃* ppmap X (Ω Y) := - begin - apply pequiv_of_equiv (psusp_adjoint_loop_unpointed X Y), - apply eq_of_phomotopy, - apply psusp_adjoint_loop_pconst - end - - -- in freudenthal - open trunc - local attribute ptrunc_pequiv_ptrunc_of_le [constructor] - definition to_pmap_freudenthal_pequiv {A : Type*} (n k : ℕ) [is_conn n A] (H : k ≤ 2 * n) - : freudenthal_pequiv A H ~* ptrunc_functor k (loop_psusp_unit A) := - begin - fapply phomotopy.mk, - { intro x, induction x with a, reflexivity }, - { refine !idp_con ⬝ _, refine _ ⬝ ap02 _ !idp_con⁻¹, refine _ ⬝ !ap_compose, apply ap_compose } - end - - definition ptrunc_elim_freudenthal_pequiv {A B : Type*} (n k : ℕ) [is_conn n A] (H : k ≤ 2 * n) - (f : A →* Ω B) [is_trunc (k.+1) (B)] : - ptrunc.elim k (Ω→ (psusp.elim f)) ∘* freudenthal_pequiv A H ~* ptrunc.elim k f := - begin - refine pwhisker_left _ !to_pmap_freudenthal_pequiv ⬝* _, - refine !ptrunc_elim_ptrunc_functor ⬝* _, - exact ptrunc_elim_phomotopy k !ap1_psusp_elim, - end - - open susp - definition iterated_freudenthal_pequiv (A : Type*) {n k m : ℕ} [HA : is_conn n A] (H : k ≤ 2 * n) - : ptrunc k A ≃* ptrunc k (Ω[m] (iterate_psusp m A)) := - begin - revert A n k HA H, induction m with m IH: intro A n k HA H, - { reflexivity}, - { have H2 : succ k ≤ 2 * succ n, - from calc - succ k ≤ succ (2 * n) : succ_le_succ H - ... ≤ 2 * succ n : self_le_succ, - exact calc - ptrunc k A ≃* ptrunc k (Ω (psusp A)) : freudenthal_pequiv A H - ... ≃* Ω (ptrunc (succ k) (psusp A)) : loop_ptrunc_pequiv - ... ≃* Ω (ptrunc (succ k) (Ω[m] (iterate_psusp m (psusp A)))) : - loop_pequiv_loop (IH (psusp A) (succ n) (succ k) _ H2) - ... ≃* ptrunc k (Ω[succ m] (iterate_psusp m (psusp A))) : loop_ptrunc_pequiv - ... ≃* ptrunc k (Ω[succ m] (iterate_psusp (succ m) A)) : - ptrunc_pequiv_ptrunc _ (loopn_pequiv_loopn _ !iterate_psusp_succ_in)} - end - - definition iterate_psusp_adjoint_loopn [constructor] (X Y : Type*) (n : ℕ) : - ppmap (iterate_psusp n X) Y ≃* ppmap X (Ω[n] Y) := - begin - revert X Y, induction n with n IH: intro X Y, - { reflexivity }, - { refine !psusp_adjoint_loop ⬝e* !IH ⬝e* _, apply pequiv_ppcompose_left, - symmetry, apply loopn_succ_in } - end - -end new_susp open new_susp - -namespace hopf - - definition my_transport_codes_merid.{u} (A : Type.{u}) [T : is_trunc 1 A] [K : is_conn 0 A] - [H : h_space A] (a a' : A) : transport (hopf A) (merid a) a' = a * a' :> A := - ap10 (elim_type_merid _ _ _ a) a' - - definition my_transport_codes_merid_one_inv.{u} (A : Type.{u}) [T : is_trunc 1 A] - [K : is_conn 0 A] [H : h_space A] (a : A) : transport (hopf A) (merid 1)⁻¹ a = a := - ap10 (elim_type_merid_inv _ _ _ 1) a ⬝ - begin apply to_inv_eq_of_eq, esimp, refine !one_mul⁻¹ end - - definition my_encode_decode' (A : Type) [T : is_trunc 1 A] [K : is_conn 0 A] - [H : h_space A] (a : A) : encode A (decode' A a) = a := - begin - esimp [encode, decode', encode₀], --- refine ap (λp, transport (hopf A) p a) _ ⬝ _ - refine !con_tr ⬝ _, - refine (ap (transport _ _) !my_transport_codes_merid ⬝ !my_transport_codes_merid_one_inv) ⬝ _, - apply mul_one - end - - definition to_pmap_main_lemma_point_pinv (A : Type) [T : is_trunc 1 A] [K : is_conn 0 A] - [H : h_space A] (coh : one_mul 1 = mul_one 1 :> (1 * 1 = 1 :> A)) - : (main_lemma_point A coh)⁻¹ᵉ* ~* !ptr ∘* loop_psusp_unit (pointed.MK A 1) := - begin - apply pinv_phomotopy_of_pid_phomotopy, - fapply phomotopy.mk, - { intro a, exact (my_encode_decode' A a)⁻¹ }, - { esimp [main_lemma_point, main_lemma, encode], - apply inv_con_eq_of_eq_con, - refine !ap_compose'⁻¹ ⬝ _, esimp, - esimp [my_encode_decode'], - unfold [encode₀], - exact sorry - -- assert p : Π(A : Type) (a a' : A) (p : a = a') (B : A → Type) (b : B a), - -- ap (λ p, p ▸ b) (con.right_inv p) = con_tr p p⁻¹ b ⬝ (ap (transport B p⁻¹) - -- (transport_codes_merid A b b ⬝ mul_one 1) ⬝ transport_codes_merid_one_inv A 1), - - } - end - - definition to_pmap_delooping_pinv (A : Type) [T : is_trunc 1 A] [K : is_conn 0 A] [H : h_space A] - (coh : one_mul 1 = mul_one 1 :> (1 * 1 = 1 :> A)) - : (hopf.delooping A coh)⁻¹ᵉ* ~* Ω→ !ptr ∘* loop_psusp_unit (pointed.MK A 1) := - begin - refine !trans_pinv ⬝* _, - refine pwhisker_left _ !to_pmap_main_lemma_point_pinv ⬝* _, - refine !passoc⁻¹* ⬝* _, - refine pwhisker_right _ !ap1_ptr⁻¹*, - end - - definition hopf_delooping_elim {A : Type} {B : Type*} [T : is_trunc 1 A] [K : is_conn 0 A] - [H : h_space A] (coh : one_mul 1 = mul_one 1 :> (1 * 1 = 1 :> A)) (f : pointed.MK A 1 →* Ω B) - /-[H1 : is_conn 1 B]-/ [H2 : is_trunc 2 B] : - Ω→(ptrunc.elim 2 (psusp.elim f)) ∘* (hopf.delooping A coh)⁻¹ᵉ* ~* f := - begin - refine pwhisker_left _ !to_pmap_delooping_pinv ⬝* _, - refine !passoc⁻¹* ⬝* _, - refine pwhisker_right _ (!ap1_pcompose⁻¹* ⬝* ap1_phomotopy !ptrunc_elim_ptr) ⬝* _, - apply ap1_psusp_elim - end - -end hopf --- this should replace corresponding definitions in homotopy.sphere -namespace new_sphere - - open sphere sphere.ops - - -- the definition was wrong for n = 0 - definition new.surf {n : ℕ} : Ω[n] (S* n) := - begin - induction n with n s, - { exact south }, - { exact (loopn_succ_in (S* (succ n)) n)⁻¹ᵉ* (apn n (equator n) s), } - end - - - definition psphere_pmap_pequiv' (A : Type*) (n : ℕ) : ppmap (S* n) A ≃* Ω[n] A := - begin - revert A, induction n with n IH: intro A, - { refine _ ⬝e* !pmap_pbool_pequiv, exact pequiv_ppcompose_right psphere_pequiv_pbool⁻¹ᵉ* }, - { refine psusp_adjoint_loop (S* n) A ⬝e* IH (Ω A) ⬝e* !loopn_succ_in⁻¹ᵉ* } - end - - definition psphere_pmap_pequiv (A : Type*) (n : ℕ) : ppmap (S* n) A ≃* Ω[n] A := - begin - fapply pequiv_change_fun, - { exact psphere_pmap_pequiv' A n }, - { exact papn_fun A new.surf }, - { revert A, induction n with n IH: intro A, - { reflexivity }, - { intro f, refine ap !loopn_succ_in⁻¹ᵉ* (IH (Ω A) _ ⬝ !apn_pcompose _) ⬝ _, - exact !loopn_succ_in_inv_natural⁻¹* _ }} - end - -end new_sphere - namespace sphere - open sphere.ops new_sphere - -- definition constant_sphere_map_sphere {n m : ℕ} (H : n < m) (f : S* n →* S* m) : -- f ~* pconst (S* n) (S* m) := -- begin @@ -1080,39 +130,3 @@ namespace sphere -- end end sphere - -namespace cofiber - - -- replace with the definition of pcofiber (and remove primes in homotopy.smash) - definition pcofiber' [constructor] {A B : Type*} (f : A →* B) : Type* := - pointed.MK (cofiber f) !cofiber.base - attribute pcofiber [constructor] - -- move ppushout attribute out namespace - - protected definition elim {A : Type} {B : Type} {f : A → B} {P : Type} - (Pinl : P) (Pinr : B → P) (Pglue : Π (x : A), Pinl = Pinr (f x)) (y : cofiber f) : P := - begin - induction y using pushout.elim with x x x, induction x, exact Pinl, exact Pinr x, exact Pglue x, - end - -end cofiber -attribute cofiber.rec cofiber.elim [recursor 8] [unfold 8] - -namespace wedge - open pushout unit - definition wedge (A B : Type*) : Type := ppushout (pconst punit A) (pconst punit B) - local attribute wedge [reducible] - definition pwedge' (A B : Type*) : Type* := pointed.mk' (wedge A B) - - protected definition rec {A B : Type*} {P : wedge A B → Type} (Pinl : Π(x : A), P (inl x)) - (Pinr : Π(x : B), P (inr x)) (Pglue : pathover P (Pinl pt) (glue ⋆) (Pinr pt)) - (y : wedge A B) : P y := - by induction y; apply Pinl; apply Pinr; induction x; exact Pglue - - protected definition elim {A B : Type*} {P : Type} (Pinl : A → P) - (Pinr : B → P) (Pglue : Pinl pt = Pinr pt) (y : wedge A B) : P := - by induction y with a b x; exact Pinl a; exact Pinr b; induction x; exact Pglue - -end wedge - -attribute wedge.rec wedge.elim [recursor 7] [unfold 7] diff --git a/pointed_pi.hlean b/pointed_pi.hlean index 7b895d7..e0e3585 100644 --- a/pointed_pi.hlean +++ b/pointed_pi.hlean @@ -13,7 +13,7 @@ open eq pointed equiv sigma of the type of pointed maps, giving the connectivity of the domain and the truncation level of the codomain. This is is_trunc_pmap at the end. - + First we define the type of dependent pointed maps as a tool, because these appear in the more general statement is_trunc_ppi (the generality needed for induction). @@ -24,13 +24,6 @@ open eq pointed equiv sigma namespace pointed - -- needs another name! (one more p?) - structure ppi (A : Type*) (P : A → Type*) := - (to_fun : Π a : A, P a) - (resp_pt : to_fun (Point A) = Point (P (Point A))) - - attribute ppi.to_fun [coercion] - abbreviation ppi_resp_pt [unfold 3] := @ppi.resp_pt definition pointed_ppi [instance] [constructor] {A : Type*} @@ -79,7 +72,7 @@ namespace pointed esimp at *, fapply apd011 ppi.mk, { apply eq_of_homotopy h }, - { esimp, apply concato_eq, apply pathover_eq_Fl, apply inv_con_eq_of_eq_con, + { esimp, apply concato_eq, apply eq_pathover_Fl, apply inv_con_eq_of_eq_con, rewrite [ap_eq_apd10, apd10_eq_of_homotopy], exact r } end @@ -105,11 +98,11 @@ namespace pointed ... ≃ Σ(p : ppi.to_fun f = ppi.to_fun g), ppi_resp_pt f = ap (λh, h pt) p ⬝ ppi_resp_pt g : sigma_equiv_sigma_right - (λp, pathover_eq_equiv_Fl p (ppi_resp_pt f) (ppi_resp_pt g)) + (λp, eq_pathover_equiv_Fl p (ppi_resp_pt f) (ppi_resp_pt g)) ... ≃ Σ(p : ppi.to_fun f = ppi.to_fun g), ppi_resp_pt f = apd10 p pt ⬝ ppi_resp_pt g : sigma_equiv_sigma_right - (λp, equiv_eq_closed_right _ (whisker_right (ap_eq_apd10 p _) _)) + (λp, equiv_eq_closed_right _ (whisker_right _ (ap_eq_apd10 p _))) ... ≃ Σ(p : f ~ g), ppi_resp_pt f = p pt ⬝ ppi_resp_pt g : sigma_equiv_sigma_left' eq_equiv_homotopy ... ≃ Σ(p : f ~ g), p pt ⬝ ppi_resp_pt g = ppi_resp_pt f