From 81fe7df61f34425b4e4d1ce5545da0109cd025a6 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sat, 18 Feb 2017 16:56:38 -0500 Subject: [PATCH] fix definition of spectrum cohomology, and prove that spectrum cohomology forms a cohomology theory --- algebra/arrow_group.hlean | 193 +++++++++++++++++++++++++++------ choice.hlean | 77 +++++++++++++ colim.hlean | 8 +- homotopy/cohomology.hlean | 220 +++++++++++++++++++++++++++++++++----- homotopy/fwedge.hlean | 132 +++++++++++++++++++++++ homotopy/pushout.hlean | 92 +++++++++++----- homotopy/smash.hlean | 5 +- homotopy/spectrum.hlean | 3 +- homotopy/splice.hlean | 2 +- move_to_lib.hlean | 83 ++++++++++++-- pointed_pi.hlean | 2 +- 11 files changed, 707 insertions(+), 110 deletions(-) create mode 100644 choice.hlean create mode 100644 homotopy/fwedge.hlean diff --git a/algebra/arrow_group.hlean b/algebra/arrow_group.hlean index 607ed8a..b2bb0cb 100644 --- a/algebra/arrow_group.hlean +++ b/algebra/arrow_group.hlean @@ -1,14 +1,104 @@ -import algebra.group_theory ..move_to_lib -open pi pointed algebra group eq equiv is_trunc +import algebra.group_theory ..move_to_lib eq2 +open pi pointed algebra group eq equiv is_trunc trunc namespace group + -- definition pmap_mul [constructor] {A B : Type*} [inf_pgroup B] (f g : A →* B) : A →* B := + -- pmap.mk (λa, f a * g a) (ap011 mul (respect_pt f) (respect_pt g) ⬝ !one_mul) + + -- definition pmap_inv [constructor] {A B : Type*} [inf_pgroup B] (f : A →* B) : A →* B := + -- pmap.mk (λa, (f a)⁻¹) (ap inv (respect_pt f) ⬝ !one_inv) + + definition pmap_mul [constructor] {A B : Type*} (f g : A →* Ω B) : A →* Ω B := + pmap.mk (λa, f a ⬝ g a) (respect_pt f ◾ respect_pt g ⬝ !idp_con) + + definition pmap_inv [constructor] {A B : Type*} (f : A →* Ω B) : A →* Ω B := + pmap.mk (λa, (f a)⁻¹ᵖ) (respect_pt f)⁻² + + definition inf_group_pmap [constructor] [instance] (A B : Type*) : inf_group (A →* Ω B) := + begin + fapply inf_group.mk, + { exact pmap_mul }, + { intro f g h, fapply pmap_eq, + { intro a, exact con.assoc (f a) (g a) (h a) }, + { rexact eq_of_square (con2_assoc (respect_pt f) (respect_pt g) (respect_pt h)) }}, + { apply pconst }, + { intros f, fapply pmap_eq, + { intro a, exact one_mul (f a) }, + { esimp, apply eq_of_square, refine _ ⬝vp !ap_id, apply natural_square_tr }}, + { intros f, fapply pmap_eq, + { intro a, exact mul_one (f a) }, + { reflexivity }}, + { exact pmap_inv }, + { intro f, fapply pmap_eq, + { intro a, exact con.left_inv (f a) }, + { exact !con_left_inv_idp⁻¹ }}, + end + + definition group_trunc_pmap [constructor] [instance] (A B : Type*) : group (trunc 0 (A →* Ω B)) := + !trunc_group + + definition Group_trunc_pmap [reducible] [constructor] (A B : Type*) : Group := + Group.mk (trunc 0 (A →* Ω (Ω B))) _ + + definition Group_trunc_pmap_homomorphism [constructor] {A A' B : Type*} (f : A' →* A) : + Group_trunc_pmap A B →g Group_trunc_pmap A' B := + begin + fapply homomorphism.mk, + { apply trunc_functor, intro g, exact g ∘* f}, + { intro g h, induction g with g, induction h with h, apply ap tr, + fapply pmap_eq, + { intro a, reflexivity }, + { refine _ ⬝ !idp_con⁻¹, + refine whisker_right _ !ap_con_fn ⬝ _, apply con2_con_con2 }} + end + + definition Group_trunc_pmap_pid [constructor] {A B : Type*} (f : Group_trunc_pmap A B) : + Group_trunc_pmap_homomorphism (pid A) f = f := + begin + induction f with f, apply ap tr, apply eq_of_phomotopy, apply pcompose_pid + end + + definition Group_trunc_pmap_pconst [constructor] {A A' B : Type*} (f : Group_trunc_pmap A B) : + Group_trunc_pmap_homomorphism (pconst A' A) f = 1 := + begin + induction f with f, apply ap tr, apply eq_of_phomotopy, apply pcompose_pconst + end + + definition Group_trunc_pmap_pcompose [constructor] {A A' A'' B : Type*} (f : A' →* A) (f' : A'' →* A') + (g : Group_trunc_pmap A B) : Group_trunc_pmap_homomorphism (f ∘* f') g = + Group_trunc_pmap_homomorphism f' (Group_trunc_pmap_homomorphism f g) := + begin + induction g with g, apply ap tr, apply eq_of_phomotopy, exact !passoc⁻¹* + end + + definition Group_trunc_pmap_phomotopy [constructor] {A A' B : Type*} {f f' : A' →* A} (p : f ~* f') : + @Group_trunc_pmap_homomorphism _ _ B f ~ Group_trunc_pmap_homomorphism f' := + begin + intro f, induction f, exact ap tr (eq_of_phomotopy (pwhisker_left a p)) + end + + definition ab_inf_group_pmap [constructor] [instance] (A B : Type*) : ab_inf_group (A →* Ω (Ω B)) := + ⦃ab_inf_group, inf_group_pmap A (Ω B), mul_comm := + begin + intro f g, fapply pmap_eq, + { intro a, exact eckmann_hilton (f a) (g a) }, + { rexact eq_of_square (eckmann_hilton_con2 (respect_pt f) (respect_pt g)) } + end⦄ + + definition ab_group_trunc_pmap [constructor] [instance] (A B : Type*) : + ab_group (trunc 0 (A →* Ω (Ω B))) := + !trunc_ab_group + + definition AbGroup_trunc_pmap [reducible] [constructor] (A B : Type*) : AbGroup := + AbGroup.mk (trunc 0 (A →* Ω (Ω B))) _ + /- Group of functions whose codomain is a group -/ - definition group_arrow [instance] (A B : Type) [group B] : group (A → B) := + definition group_pi [instance] [constructor] {A : Type} (P : A → Type) [Πa, group (P a)] : group (Πa, P a) := begin fapply group.mk, - { apply is_trunc_arrow }, + { apply is_trunc_pi }, { intro f g a, exact f a * g a }, { intros, apply eq_of_homotopy, intro a, apply mul.assoc }, { intro a, exact 1 }, @@ -18,43 +108,78 @@ namespace group { intros, apply eq_of_homotopy, intro a, apply mul.left_inv } end - definition Group_arrow (A : Type) (G : Group) : Group := - Group.mk (A → G) _ + definition Group_pi [constructor] {A : Type} (P : A → Group) : Group := + Group.mk (Πa, P a) _ - 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⦄ + /- we use superscript in the following notation, because otherwise we can never write something + like `Πg h : G, _` anymore -/ - definition AbGroup_arrow (A : Type) (G : AbGroup) : AbGroup := - AbGroup.mk (A → G) _ + notation `Πᵍ` binders `, ` r:(scoped P, Group_pi P) := r - definition pgroup_ppmap [instance] (A B : Type*) [pgroup B] : pgroup (ppmap A B) := + definition Group_pi_intro [constructor] {A : Type} {G : Group} {P : A → Group} (f : Πa, G →g P a) + : G →g Πᵍ a, P a := begin - fapply pgroup.mk, - { apply is_trunc_pmap }, - { intro f g, apply pmap.mk (λa, f a * g a), - exact ap011 mul (respect_pt f) (respect_pt g) ⬝ !one_mul }, - { intros, apply pmap_eq_of_homotopy, intro a, apply mul.assoc }, - { intro f, apply pmap.mk (λa, (f a)⁻¹), apply inv_eq_one, apply respect_pt }, - { intros, apply pmap_eq_of_homotopy, intro a, apply one_mul }, - { intros, apply pmap_eq_of_homotopy, intro a, apply mul_one }, - { intros, apply pmap_eq_of_homotopy, intro a, apply mul.left_inv } + fconstructor, + { intro g a, exact f a g }, + { intro g h, apply eq_of_homotopy, intro a, exact respect_mul (f a) g h } end - definition Group_pmap (A : Type*) (G : Group) : Group := - Group_of_pgroup (ppmap A (pType_of_Group G)) + -- definition AbGroup_trunc_pmap_homomorphism [constructor] {A A' B : Type*} (f : A' →* A) : + -- AbGroup_trunc_pmap A B →g AbGroup_trunc_pmap A' B := + -- Group_trunc_pmap_homomorphism f - 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 : AbGroup) : - Group_pmap A G →g Group_pmap A' G := - begin - fapply homomorphism.mk, - { intro g, exact g ∘* f}, - { intro g h, apply pmap_eq_of_homotopy, intro a, reflexivity } - end + /- Group of functions whose codomain is a group -/ + -- definition group_arrow [instance] (A B : Type) [group B] : group (A → B) := + -- begin + -- fapply group.mk, + -- { apply is_trunc_arrow }, + -- { intro f g a, exact f a * g a }, + -- { intros, apply eq_of_homotopy, intro a, apply mul.assoc }, + -- { intro a, exact 1 }, + -- { intros, apply eq_of_homotopy, intro a, apply one_mul }, + -- { intros, apply eq_of_homotopy, intro a, apply mul_one }, + -- { intro f a, exact (f a)⁻¹ }, + -- { intros, apply eq_of_homotopy, intro a, apply mul.left_inv } + -- end + + -- definition Group_arrow (A : Type) (G : Group) : Group := + -- Group.mk (A → G) _ + + -- 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 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 + -- fapply pgroup.mk, + -- { apply is_trunc_pmap }, + -- { intro f g, apply pmap.mk (λa, f a * g a), + -- exact ap011 mul (respect_pt f) (respect_pt g) ⬝ !one_mul }, + -- { intros, apply pmap_eq_of_homotopy, intro a, apply mul.assoc }, + -- { intro f, apply pmap.mk (λa, (f a)⁻¹), apply inv_eq_one, apply respect_pt }, + -- { intros, apply pmap_eq_of_homotopy, intro a, apply one_mul }, + -- { intros, apply pmap_eq_of_homotopy, intro a, apply mul_one }, + -- { intros, apply pmap_eq_of_homotopy, intro a, apply mul.left_inv } + -- end + + -- definition Group_pmap (A : Type*) (G : Group) : Group := + -- Group_of_pgroup (ppmap A (pType_of_Group 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 : AbGroup) : + -- Group_pmap A G →g Group_pmap A' G := + -- begin + -- fapply homomorphism.mk, + -- { intro g, exact g ∘* f}, + -- { intro g h, apply pmap_eq_of_homotopy, intro a, reflexivity } + -- end end group diff --git a/choice.hlean b/choice.hlean new file mode 100644 index 0000000..9f210dc --- /dev/null +++ b/choice.hlean @@ -0,0 +1,77 @@ +import types.trunc types.sum + +open pi prod sum unit bool trunc is_trunc is_equiv eq equiv + +namespace choice + +-- the following brilliant name is from Agda +definition unchoose [unfold 4] (n : ℕ₋₂) {X : Type} (A : X → Type) : trunc n (Πx, A x) → Πx, trunc n (A x) := +trunc.elim (λf x, tr (f x)) + +definition has_choice.{u} (n : ℕ₋₂) (X : Type.{u}) : Type.{u+1} := +Π(A : X → Type.{u}), is_equiv (unchoose n A) + +definition choice_equiv.{u} [constructor] {n : ℕ₋₂} {X : Type.{u}} (H : has_choice n X) (A : X → Type.{u}) + : trunc n (Πx, A x) ≃ (Πx, trunc n (A x)) := +equiv.mk _ (H A) + +definition has_choice_of_succ (X : Type) (H : Πk, has_choice (k.+1) X) (n : ℕ₋₂) : has_choice n X := +begin + cases n with n, + { intro A, apply is_equiv_of_is_contr }, + { exact H n } +end + +definition has_choice_empty (n : ℕ₋₂) : has_choice n empty := +begin + intro A, fapply adjointify, + { intro f, apply tr, intro x, induction x }, + { intro f, apply eq_of_homotopy, intro x, induction x }, + { intro g, induction g with g, apply ap tr, apply eq_of_homotopy, intro x, induction x } +end + +definition is_trunc_is_contr_fiber [instance] [priority 900] (n : ℕ₋₂) {A B : Type} (f : A → B) + (b : B) [is_trunc n A] [is_trunc n B] : is_trunc n (is_contr (fiber f b)) := +begin + cases n, + { apply is_contr_of_inhabited_prop, apply is_contr_fun_of_is_equiv, + apply is_equiv_of_is_contr }, + { apply is_trunc_succ_of_is_prop } +end + +definition has_choice_unit : Πn, has_choice n unit := +begin + intro n A, fapply adjointify, + { intro f, induction f ⋆ with a, apply tr, intro u, induction u, exact a }, + { intro f, apply eq_of_homotopy, intro u, induction u, esimp, generalize f ⋆, intro a, + induction a, reflexivity }, + { intro g, induction g with g, apply ap tr, apply eq_of_homotopy, + intro u, induction u, reflexivity } +end + +definition has_choice_sum.{u} (n : ℕ₋₂) {A B : Type.{u}} (hA : has_choice n A) (hB : has_choice n B) + : has_choice n (A ⊎ B) := +begin + intro P, fapply is_equiv_of_equiv_of_homotopy, + { exact calc + trunc n (Πx, P x) ≃ trunc n ((Πa, P (inl a)) × Πb, P (inr b)) + : trunc_equiv_trunc n !equiv_sum_rec⁻¹ᵉ + ... ≃ trunc n (Πa, P (inl a)) × trunc n (Πb, P (inr b)) : trunc_prod_equiv + ... ≃ (Πa, trunc n (P (inl a))) × Πb, trunc n (P (inr b)) + : by exact prod_equiv_prod (choice_equiv hA _) (choice_equiv hB _) + ... ≃ Πx, trunc n (P x) : equiv_sum_rec }, + { intro f, induction f, apply eq_of_homotopy, intro x, esimp, induction x with a b: reflexivity } +end + +/- currently we prove it using univalence -/ +definition has_choice_equiv_closed.{u} (n : ℕ₋₂) {A B : Type.{u}} (f : A ≃ B) (hA : has_choice n B) + : has_choice n A := +begin + induction f using rec_on_ua_idp, assumption +end + +definition has_choice_bool (n : ℕ₋₂) : has_choice n bool := +has_choice_equiv_closed n bool_equiv_unit_sum_unit + (has_choice_sum n (has_choice_unit n) (has_choice_unit n)) + +end choice diff --git a/colim.hlean b/colim.hlean index 1f96637..9a6bb9d 100644 --- a/colim.hlean +++ b/colim.hlean @@ -10,7 +10,11 @@ namespace seq_colim definition inclusion_pt [constructor] {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ) : inclusion f (Point (X n)) = Point (pseq_colim f) := - by induction n with n p; reflexivity; exact (ap (sι f) !respect_pt)⁻¹ ⬝ !glue ⬝ p + begin + induction n with n p, + reflexivity, + exact (ap (sι f) (respect_pt _))⁻¹ᵖ ⬝ !glue ⬝ p + end definition pinclusion [constructor] {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ) : X n →* pseq_colim f := @@ -390,7 +394,7 @@ namespace seq_colim apply whisker_left, rewrite [- +con.assoc], apply whisker_right, rewrite [- +ap_compose'], 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))⁻¹, + (λ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/cohomology.hlean b/homotopy/cohomology.hlean index 5353142..f02691d 100644 --- a/homotopy/cohomology.hlean +++ b/homotopy/cohomology.hlean @@ -6,9 +6,83 @@ Authors: Floris van Doorn Reduced cohomology -/ -import algebra.arrow_group .spectrum homotopy.EM +import .spectrum .EM ..algebra.arrow_group .fwedge ..choice .pushout ..move_to_lib -open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops equiv susp +open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops equiv susp is_trunc + function fwedge cofiber bool lift sigma is_equiv choice pushout algebra + +-- TODO: move +structure is_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) := + ( im_in_ker : Π(a:A), g (f a) = pt) + ( ker_in_im : Π(b:B), (g b = pt) → image f b) + +definition is_exact_g {A B C : Group} (f : A →g B) (g : B →g C) := +is_exact f g + +definition is_exact_g.mk {A B C : Group} {f : A →g B} {g : B →g C} + (H₁ : Πa, g (f a) = 1) (H₂ : Πb, g b = 1 → image f b) : is_exact_g f g := +is_exact.mk H₁ H₂ + +definition is_exact_trunc_functor {A B : Type} {C : Type*} {f : A → B} {g : B → C} + (H : is_exact_t f g) : @is_exact _ _ (ptrunc 0 C) (trunc_functor 0 f) (trunc_functor 0 g) := +begin + constructor, + { intro a, esimp, induction a with a, + exact ap tr (is_exact_t.im_in_ker H a) }, + { intro b p, induction b with b, note q := !tr_eq_tr_equiv p, induction q with q, + induction is_exact_t.ker_in_im H b q with a r, + exact image.mk (tr a) (ap tr r) } +end + +definition is_exact_homotopy {A B C : Type*} {f f' : A → B} {g g' : B → C} + (p : f ~ f') (q : g ~ g') (H : is_exact f g) : is_exact f' g' := +begin + induction p using homotopy.rec_on_idp, + induction q using homotopy.rec_on_idp, + assumption +end + +-- move to arrow group + +definition ap1_pmap_mul {X Y : Type*} (f g : X →* Ω Y) : + Ω→ (pmap_mul f g) ~* pmap_mul (Ω→ f) (Ω→ g) := +begin + fconstructor, + { intro p, esimp, + refine ap1_gen_con_left p (respect_pt f) (respect_pt f) + (respect_pt g) (respect_pt g) ⬝ _, + refine !whisker_right_idp ◾ !whisker_left_idp2, }, + { refine !con.assoc ⬝ _, + refine _ ◾ idp ⬝ _, rotate 1, + rexact ap1_gen_con_left_idp (respect_pt f) (respect_pt g), esimp, + refine !con.assoc ⬝ _, + apply whisker_left, apply inv_con_eq_idp, + refine !con2_con_con2 ⬝ ap011 concat2 _ _: + refine eq_of_square (!natural_square ⬝hp !ap_id) ⬝ !con_idp } +end + +definition pmap_mul_pcompose {A B C : Type*} (g h : B →* Ω C) (f : A →* B) : + pmap_mul g h ∘* f ~* pmap_mul (g ∘* f) (h ∘* f) := +begin + fconstructor, + { intro p, reflexivity }, + { esimp, refine !idp_con ⬝ _, refine !con2_con_con2⁻¹ ⬝ whisker_right _ _, + refine !ap_eq_ap011⁻¹ } +end + +definition pcompose_pmap_mul {A B C : Type*} (h : B →* C) (f g : A →* Ω B) : + Ω→ h ∘* pmap_mul f g ~* pmap_mul (Ω→ h ∘* f) (Ω→ h ∘* g) := +begin + fconstructor, + { intro p, exact ap1_con2 h (f p) (g p) }, + { refine whisker_left _ !con2_con_con2⁻¹ ⬝ _, refine !con.assoc⁻¹ ⬝ _, + refine whisker_right _ (eq_of_square !ap1_gen_con_natural) ⬝ _, + refine !con.assoc ⬝ whisker_left _ _, apply ap1_gen_con_idp } +end + +definition loop_psusp_intro_pmap_mul {X Y : Type*} (f g : psusp X →* Ω Y) : + loop_psusp_intro (pmap_mul f g) ~* pmap_mul (loop_psusp_intro f) (loop_psusp_intro g) := +pwhisker_right _ !ap1_pmap_mul ⬝* !pmap_mul_pcompose namespace cohomology @@ -16,7 +90,7 @@ definition EM_spectrum /-[constructor]-/ (G : AbGroup) : spectrum := spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*) definition cohomology (X : Type*) (Y : spectrum) (n : ℤ) : AbGroup := -AbGroup_pmap X (πag[2] (Y (2+n))) +AbGroup_trunc_pmap X (Y (n+2)) definition ordinary_cohomology [reducible] (X : Type*) (G : AbGroup) (n : ℤ) : AbGroup := cohomology X (EM_spectrum G) n @@ -33,33 +107,123 @@ notation `H^` n `[`:0 X:0 `]`:0 := ordinary_cohomology_Z X n 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) +/- functoriality -/ + +definition cohomology_functor [constructor] {X X' : Type*} (f : X' →* X) (Y : spectrum) (n : ℤ) : cohomology X Y n →g cohomology X' Y n := -Group_pmap_homomorphism f (πag[2] (Y (2+n))) +Group_trunc_pmap_homomorphism f -definition cohomology_homomorphism_id (X : Type*) (Y : spectrum) (n : ℤ) (f : H^n[X, Y]) : - cohomology_homomorphism (pid X) Y n f ~* f := -!pcompose_pid +definition cohomology_functor_pid (X : Type*) (Y : spectrum) (n : ℤ) (f : H^n[X, Y]) : + cohomology_functor (pid X) Y n f = f := +!Group_trunc_pmap_pid -definition cohomology_homomorphism_compose {X X' X'' : Type*} (g : X'' →* X') (f : X' →* X) - (Y : spectrum) (n : ℤ) (h : H^n[X, Y]) : cohomology_homomorphism (f ∘* g) Y n h ~* - cohomology_homomorphism g Y n (cohomology_homomorphism f Y n h) := -!passoc⁻¹* +definition cohomology_functor_pcompose {X X' X'' : Type*} (f : X' →* X) (g : X'' →* X') + (Y : spectrum) (n : ℤ) (h : H^n[X, Y]) : cohomology_functor (f ∘* g) Y n h = + cohomology_functor g Y n (cohomology_functor f Y n h) := +!Group_trunc_pmap_pcompose + +definition cohomology_functor_phomotopy {X X' : Type*} {f g : X' →* X} (p : f ~* g) + (Y : spectrum) (n : ℤ) : cohomology_functor f Y n ~ cohomology_functor g Y n := +Group_trunc_pmap_phomotopy p + +definition cohomology_functor_pconst {X X' : Type*} (Y : spectrum) (n : ℤ) (f : H^n[X, Y]) : + cohomology_functor (pconst X' X) Y n f = 1 := +!Group_trunc_pmap_pconst + +/- suspension axiom -/ + +definition cohomology_psusp_2 (Y : spectrum) (n : ℤ) : + Ω (Ω[2] (Y ((n+1)+2))) ≃* Ω[2] (Y (n+2)) := +begin + apply loopn_pequiv_loopn 2, + exact loop_pequiv_loop (pequiv_of_eq (ap Y (add_comm_right n 1 2))) ⬝e* !equiv_glue⁻¹ᵉ* +end + +definition cohomology_psusp_1 (X : Type*) (Y : spectrum) (n : ℤ) : + psusp X →* Ω (Ω (Y (n + 1 + 2))) ≃ X →* Ω (Ω (Y (n+2))) := +calc + psusp X →* Ω[2] (Y (n + 1 + 2)) ≃ X →* Ω (Ω[2] (Y (n + 1 + 2))) : psusp_adjoint_loop_unpointed + ... ≃ X →* Ω[2] (Y (n+2)) : equiv_of_pequiv (pequiv_ppcompose_left + (cohomology_psusp_2 Y n)) + +definition cohomology_psusp_1_pmap_mul {X : Type*} {Y : spectrum} {n : ℤ} + (f g : psusp X →* Ω (Ω (Y (n + 1 + 2)))) : cohomology_psusp_1 X Y n (pmap_mul f g) ~* + pmap_mul (cohomology_psusp_1 X Y n f) (cohomology_psusp_1 X Y n g) := +begin + unfold [cohomology_psusp_1], + refine pwhisker_left _ !loop_psusp_intro_pmap_mul ⬝* _, + apply pcompose_pmap_mul +end + +definition cohomology_psusp_equiv (X : Type*) (Y : spectrum) (n : ℤ) : + H^n+1[psusp X, Y] ≃ H^n[X, Y] := +trunc_equiv_trunc _ (cohomology_psusp_1 X Y n) + +definition cohomology_psusp (X : Type*) (Y : spectrum) (n : ℤ) : + H^n+1[psusp X, Y] ≃g H^n[X, Y] := +isomorphism_of_equiv (cohomology_psusp_equiv X Y n) + begin + intro f₁ f₂, induction f₁ with f₁, induction f₂ with f₂, + apply ap tr, apply eq_of_phomotopy, exact cohomology_psusp_1_pmap_mul f₁ f₂ + end + +definition cohomology_psusp_natural {X X' : Type*} (f : X →* X') (Y : spectrum) (n : ℤ) : + cohomology_psusp X Y n ∘ cohomology_functor (psusp_functor f) Y (n+1) ~ + cohomology_functor f Y n ∘ cohomology_psusp X' Y n := +begin + refine (trunc_functor_compose _ _ _)⁻¹ʰᵗʸ ⬝hty _ ⬝hty trunc_functor_compose _ _ _, + apply trunc_functor_homotopy, intro g, + apply eq_of_phomotopy, refine _ ⬝* !passoc⁻¹*, apply pwhisker_left, + apply loop_psusp_intro_natural +end + +/- exactness -/ + +definition cohomology_exact {X X' : Type*} (f : X →* X') (Y : spectrum) (n : ℤ) : + is_exact_g (cohomology_functor (pcod f) Y n) (cohomology_functor f Y n) := +is_exact_trunc_functor (cofiber_exact f) + +/- additivity -/ + +definition additive_hom [constructor] {I : Type} (X : I → Type*) (Y : spectrum) (n : ℤ) : + H^n[⋁X, Y] →g Πᵍ i, H^n[X i, Y] := +Group_pi_intro (λi, cohomology_functor (pinl i) Y n) + +definition additive_equiv.{u} {I : Type.{u}} (H : has_choice 0 I) (X : I → Type*) (Y : spectrum) + (n : ℤ) : H^n[⋁X, Y] ≃ Πᵍ i, H^n[X i, Y] := +trunc_fwedge_pmap_equiv H X (Ω[2] (Y (n+2))) + +definition additive {I : Type} (H : has_choice 0 I) (X : I → Type*) (Y : spectrum) (n : ℤ) : + is_equiv (additive_hom X Y n) := +is_equiv_of_equiv_of_homotopy (additive_equiv H X Y n) begin intro f, induction f, reflexivity end + +/- cohomology theory -/ + +structure cohomology_theory.{u} : Type.{u+1} := + (H : ℤ → pType.{u} → AbGroup.{u}) + (Hh : Π(n : ℤ) {X Y : Type*} (f : X →* Y), H n Y →g H n X) + (Hh_id : Π(n : ℤ) {X : Type*} (x : H n X), Hh n (pid X) x = x) + (Hh_compose : Π(n : ℤ) {X Y Z : Type*} (g : Y →* Z) (f : X →* Y) (z : H n Z), + Hh n (g ∘* f) z = Hh n f (Hh n g z)) + (Hsusp : Π(n : ℤ) (X : Type*), H (succ n) (psusp X) ≃g H n X) + (Hsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y), + Hsusp n X ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hsusp n Y) + (Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n (pcod f)) (Hh n f)) + (Hadditive : Π(n : ℤ) {I : Type.{u}} (X : I → Type*), has_choice 0 I → + is_equiv (Group_pi_intro (λi, Hh n (pinl i)) : H n (⋁ X) → Πᵍ i, H n (X i))) + +structure ordinary_theory.{u} extends cohomology_theory.{u} : Type.{u+1} := + (Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (H n (plift pbool))) + +definition cohomology_theory_spectrum [constructor] (Y : spectrum) : cohomology_theory := +cohomology_theory.mk + (λn A, H^n[A, Y]) + (λn A B f, cohomology_functor f Y n) + (λn A x, cohomology_functor_pid A Y n x) + (λn A B C g f x, cohomology_functor_pcompose g f Y n x) + (λn A, cohomology_psusp A Y n) + (λn A B f, cohomology_psusp_natural f Y n) + (λn A B f, cohomology_exact f Y n) + (λn I A H, additive H A Y n) end cohomology - -exit -definition cohomology_psusp (X : Type*) (Y : spectrum) (n : ℤ) : - H^n+1[psusp X, Y] ≃ H^n[X, Y] := -calc - H^n+1[psusp X, Y] ≃ psusp X →* πg[2] (Y (2+(n+1))) : by reflexivity - ... ≃ X →* Ω (πg[2] (Y (2+(n+1)))) : psusp_adjoint_loop_unpointed --- ... ≃ X →* πg[3] (Y (2+(n+1))) : _ ---... ≃ X →* πag[3] (Y ((2+n)+1)) : _ - ... ≃ X →* πg[2] (Y (2+n)) : - begin - refine equiv_of_pequiv (pequiv_ppcompose_left _), - refine !homotopy_group_succ_o ⬝ _, - exact sorry --refine _ ⬝e* _ ⬝e* _ - end - ... ≃ H^n[X, Y] : by reflexivity diff --git a/homotopy/fwedge.hlean b/homotopy/fwedge.hlean new file mode 100644 index 0000000..86a7e58 --- /dev/null +++ b/homotopy/fwedge.hlean @@ -0,0 +1,132 @@ +/- +Copyright (c) 2016 Jakob von Raumer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jakob von Raumer, Ulrik Buchholtz + +The Wedge Sum of a family of Pointed Types +-/ +import homotopy.wedge ..move_to_lib ..choice + +open eq pushout pointed unit trunc_index sigma bool equiv trunc choice + +definition fwedge' {I : Type} (F : I → Type*) : Type := pushout (λi, ⟨i, Point (F i)⟩) (λi, ⋆) +definition pt' [constructor] {I : Type} {F : I → Type*} : fwedge' F := inr ⋆ +definition fwedge [constructor] {I : Type} (F : I → Type*) : Type* := pointed.MK (fwedge' F) pt' + +notation `⋁` := fwedge + +namespace fwedge + variables {I : Type} {F : I → Type*} + + definition il {i : I} (x : F i) : ⋁F := inl ⟨i, x⟩ + definition inl (i : I) (x : F i) : ⋁F := il x + definition pinl [constructor] (i : I) : F i →* ⋁F := pmap.mk (inl i) (glue i) + definition glue (i : I) : inl i pt = pt :> ⋁ F := glue i + + protected definition rec {P : ⋁F → Type} (Pinl : Π(i : I) (x : F i), P (il x)) + (Pinr : P pt) (Pglue : Πi, pathover P (Pinl i pt) (glue i) (Pinr)) (y : fwedge' F) : P y := + begin induction y, induction x, apply Pinl, induction x, apply Pinr, apply Pglue end + + protected definition elim {P : Type} (Pinl : Π(i : I) (x : F i), P) + (Pinr : P) (Pglue : Πi, Pinl i pt = Pinr) (y : fwedge' F) : P := + begin induction y with x u, induction x with i x, exact Pinl i x, induction u, apply Pinr, apply Pglue end + + protected definition elim_glue {P : Type} {Pinl : Π(i : I) (x : F i), P} + {Pinr : P} (Pglue : Πi, Pinl i pt = Pinr) (i : I) + : ap (fwedge.elim Pinl Pinr Pglue) (fwedge.glue i) = Pglue i := + !pushout.elim_glue + + protected definition rec_glue {P : ⋁F → Type} {Pinl : Π(i : I) (x : F i), P (il x)} + {Pinr : P pt} (Pglue : Πi, pathover P (Pinl i pt) (glue i) (Pinr)) (i : I) + : apd (fwedge.rec Pinl Pinr Pglue) (fwedge.glue i) = Pglue i := + !pushout.rec_glue + +end fwedge + +attribute fwedge.rec fwedge.elim [recursor 7] [unfold 7] +attribute fwedge.il fwedge.inl [constructor] + +namespace fwedge + + definition fwedge_of_pwedge [unfold 3] {A B : Type*} (x : A ∨ B) : ⋁(bool.rec A B) := + begin + induction x with a b, + { exact inl ff a }, + { exact inl tt b }, + { exact glue ff ⬝ (glue tt)⁻¹ } + end + + definition pwedge_of_fwedge [unfold 3] {A B : Type*} (x : ⋁(bool.rec A B)) : A ∨ B := + begin + induction x with b x b, + { induction b, exact pushout.inl x, exact pushout.inr x }, + { exact pushout.inr pt }, + { induction b, exact pushout.glue ⋆, reflexivity } + end + + definition pwedge_pequiv_fwedge [constructor] (A B : Type*) : A ∨ B ≃* ⋁(bool.rec A B) := + begin + fapply pequiv_of_equiv, + { fapply equiv.MK, + { exact fwedge_of_pwedge }, + { exact pwedge_of_fwedge }, + { exact abstract begin intro x, induction x with b x b, + { induction b: reflexivity }, + { exact glue tt }, + { apply eq_pathover_id_right, + refine ap_compose fwedge_of_pwedge _ _ ⬝ ap02 _ !elim_glue ⬝ph _, + induction b, exact !elim_glue ⬝ph whisker_bl _ hrfl, apply square_of_eq idp } + end end }, + { exact abstract begin intro x, induction x with a b, + { reflexivity }, + { reflexivity }, + { apply eq_pathover_id_right, + refine ap_compose pwedge_of_fwedge _ _ ⬝ ap02 _ !elim_glue ⬝ !ap_con ⬝ + !elim_glue ◾ (!ap_inv ⬝ !elim_glue⁻²) ⬝ph _, exact hrfl } end end}}, + { exact glue ff } + end + + definition fwedge_pmap [constructor] {I : Type} {F : I → Type*} {X : Type*} (f : Πi, F i →* X) : ⋁F →* X := + begin + fconstructor, + { intro x, induction x, + exact f i x, + exact pt, + exact respect_pt (f i) }, + { reflexivity } + end + + definition fwedge_pmap_beta [constructor] {I : Type} {F : I → Type*} {X : Type*} (f : Πi, F i →* X) (i : I) : + fwedge_pmap f ∘* pinl i ~* f i := + begin + fconstructor, + { reflexivity }, + { exact !idp_con ⬝ !fwedge.elim_glue⁻¹ } + end + + definition fwedge_pmap_eta [constructor] {I : Type} {F : I → Type*} {X : Type*} (g : ⋁F →* X) : + fwedge_pmap (λi, g ∘* pinl i) ~* g := + begin + fconstructor, + { intro x, induction x, + reflexivity, + exact (respect_pt g)⁻¹, + apply eq_pathover, refine !elim_glue ⬝ph _, apply whisker_lb, exact hrfl }, + { exact con.left_inv (respect_pt g) } + end + + definition fwedge_pmap_equiv [constructor] {I : Type} (F : I → Type*) (X : Type*) : + ⋁F →* X ≃ Πi, F i →* X := + begin + fapply equiv.MK, + { intro g i, exact g ∘* pinl i }, + { exact fwedge_pmap }, + { intro f, apply eq_of_homotopy, intro i, apply eq_of_phomotopy, apply fwedge_pmap_beta f i }, + { intro g, apply eq_of_phomotopy, exact fwedge_pmap_eta g } + end + + definition trunc_fwedge_pmap_equiv.{u} {n : ℕ₋₂} {I : Type.{u}} (H : has_choice n I) + (F : I → pType.{u}) (X : pType.{u}) : trunc n (⋁F →* X) ≃ Πi, trunc n (F i →* X) := + trunc_equiv_trunc n (fwedge_pmap_equiv F X) ⬝e choice_equiv H (λi, F i →* X) + +end fwedge diff --git a/homotopy/pushout.hlean b/homotopy/pushout.hlean index 6b6d76e..9bbc3df 100644 --- a/homotopy/pushout.hlean +++ b/homotopy/pushout.hlean @@ -1,7 +1,7 @@ import ..move_to_lib -open eq function is_trunc sigma prod lift is_equiv equiv pointed sum unit bool +open eq function is_trunc sigma prod lift is_equiv equiv pointed sum unit bool cofiber namespace pushout @@ -268,43 +268,43 @@ namespace pushout /- pushout where one map is constant is a cofiber -/ definition pushout_const_equiv_to [unfold 6] {A B C : Type} {f : A → B} {c₀ : C} - (x : pushout (const A c₀) f) : cofiber (sum_functor f (const unit c₀)) := + (x : pushout f (const A c₀)) : cofiber (sum_functor f (const unit c₀)) := begin - induction x with c b a, - { exact inr (sum.inr c) }, - { exact inr (sum.inl b) }, - { exact (glue (sum.inr ⋆))⁻¹ ⬝ glue (sum.inl a) } + induction x with b c a, + { exact !cod (sum.inl b) }, + { exact !cod (sum.inr c) }, + { exact glue (sum.inl a) ⬝ (glue (sum.inr ⋆))⁻¹ } end definition pushout_const_equiv_from [unfold 6] {A B C : Type} {f : A → B} {c₀ : C} - (x : cofiber (sum_functor f (const unit c₀))) : pushout (const A c₀) f := + (x : cofiber (sum_functor f (const unit c₀))) : pushout f (const A c₀) := begin induction x with v v, - { exact inl c₀ }, - { induction v with b c, exact inr b, exact inl c }, + { induction v with b c, exact inl b, exact inr c }, + { exact inr c₀ }, { induction v with a u, exact glue a, reflexivity } end definition pushout_const_equiv [constructor] {A B C : Type} (f : A → B) (c₀ : C) : - pushout (const A c₀) f ≃ cofiber (sum_functor f (const unit c₀)) := + pushout f (const A c₀) ≃ cofiber (sum_functor f (const unit c₀)) := begin fapply equiv.MK, { exact pushout_const_equiv_to }, { exact pushout_const_equiv_from }, { intro x, induction x with v v, - { exact (glue (sum.inr ⋆))⁻¹ }, { induction v with b c, reflexivity, reflexivity }, + { exact glue (sum.inr ⋆) }, { apply eq_pathover_id_right, refine ap_compose pushout_const_equiv_to _ _ ⬝ ap02 _ !elim_glue ⬝ph _, induction v with a u, - { refine !elim_glue ⬝ph _, esimp, apply whisker_tl, exact hrfl }, - { induction u, exact square_of_eq !con.left_inv }}}, + { refine !elim_glue ⬝ph _, apply whisker_bl, exact hrfl }, + { induction u, exact square_of_eq idp }}}, { intro x, induction x with c b a, { reflexivity }, { reflexivity }, { apply eq_pathover_id_right, apply hdeg_square, refine ap_compose pushout_const_equiv_from _ _ ⬝ ap02 _ !elim_glue ⬝ _, - refine !ap_con ⬝ (!ap_inv ⬝ !elim_glue⁻²) ◾ !elim_glue ⬝ !idp_con }} + refine !ap_con ⬝ !elim_glue ◾ (!ap_inv ⬝ !elim_glue⁻²) }} end /- wedge is the cofiber of the map 2 -> A + B -/ @@ -320,7 +320,6 @@ namespace pushout definition wedge_equiv_pushout_sum [constructor] (A B : Type*) : wedge A B ≃ cofiber (sum_of_bool A B) := begin - refine !pushout.symm ⬝e _, refine pushout_const_equiv _ _ ⬝e _, fapply pushout.equiv, exact bool_equiv_unit_sum_unit⁻¹ᵉ, @@ -425,9 +424,9 @@ namespace pushout open sigma.ops definition cofiber_pushout_helper' {A : Type} {B : A → Type} {a₀₀ a₀₂ a₂₀ a₂₂ : A} {p₀₁ : a₀₀ = a₀₂} {p₁₀ : a₀₀ = a₂₀} {p₂₁ : a₂₀ = a₂₂} {p₁₂ : a₀₂ = a₂₂} {s : square p₀₁ p₂₁ p₁₀ p₁₂} - {b₀₀ : B a₀₀} {b₂₀ b₂₀' : B a₂₀} {b₀₂ : B a₀₂} {b₂₂ : B a₂₂} {q₁₀ : b₀₀ =[p₁₀] b₂₀} - {q₀₁ : b₀₀ =[p₀₁] b₀₂} {q₂₁ : b₂₀' =[p₂₁] b₂₂} {q₁₂ : b₀₂ =[p₁₂] b₂₂} : - Σ(r : b₂₀' = b₂₀), squareover B s q₀₁ (r ▸ q₂₁) q₁₀ q₁₂ := + {b₀₀ : B a₀₀} {b₂₀ : B a₂₀} {b₀₂ : B a₀₂} {b₂₂ b₂₂' : B a₂₂} {q₁₀ : b₀₀ =[p₁₀] b₂₀} + {q₀₁ : b₀₀ =[p₀₁] b₀₂} {q₂₁ : b₂₀ =[p₂₁] b₂₂'} {q₁₂ : b₀₂ =[p₁₂] b₂₂} : + Σ(r : b₂₂' = b₂₂), squareover B s q₀₁ (r ▸ q₂₁) q₁₀ q₁₂ := begin induction s, induction q₀₁ using idp_rec_on, @@ -438,29 +437,66 @@ namespace pushout end definition cofiber_pushout_helper {A B C D : Type} {f : A → B} {g : A → C} {h : pushout f g → D} - {P : cofiber h → Type} {Pbase : P (cofiber.base h)} {Pcod : Πd, P (cofiber.cod h d)} - (Pgluel : Π(b : B), Pbase =[cofiber.glue (inl b)] Pcod (h (inl b))) - (Pgluer : Π(c : C), Pbase =[cofiber.glue (inr c)] Pcod (h (inr c))) + {P : cofiber h → Type} {Pcod : Πd, P (cofiber.cod h d)} {Pbase : P (cofiber.base h)} + (Pgluel : Π(b : B), Pcod (h (inl b)) =[cofiber.glue (inl b)] Pbase) + (Pgluer : Π(c : C), Pcod (h (inr c)) =[cofiber.glue (inr c)] Pbase) (a : A) : Σ(p : Pbase = Pbase), squareover P (natural_square cofiber.glue (glue a)) - (Pgluel (f a)) (p ▸ Pgluer (g a)) - (pathover_ap P (λa, cofiber.base h) (apd (λa, Pbase) (glue a))) - (pathover_ap P (λa, cofiber.cod h (h a)) (apd (λa, Pcod (h a)) (glue a))) := + (Pgluel (f a)) (p ▸ Pgluer (g a)) + (pathover_ap P (λa, cofiber.cod h (h a)) (apd (λa, Pcod (h a)) (glue a))) + (pathover_ap P (λa, cofiber.base h) (apd (λa, Pbase) (glue a))) := !cofiber_pushout_helper' definition cofiber_pushout_rec {A B C D : Type} {f : A → B} {g : A → C} {h : pushout f g → D} - {P : cofiber h → Type} (Pbase : P (cofiber.base h)) (Pcod : Πd, P (cofiber.cod h d)) - (Pgluel : Π(b : B), Pbase =[cofiber.glue (inl b)] Pcod (h (inl b))) - (Pgluer : Π(c : C), Pbase =[cofiber.glue (inr c)] Pcod (h (inr c))) + {P : cofiber h → Type} (Pcod : Πd, P (cofiber.cod h d)) (Pbase : P (cofiber.base h)) + (Pgluel : Π(b : B), Pcod (h (inl b)) =[cofiber.glue (inl b)] Pbase) + (Pgluer : Π(c : C), Pcod (h (inr c)) =[cofiber.glue (inr c)] Pbase) (r : C → A) (p : Πa, r (g a) = a) (x : cofiber h) : P x := begin induction x with d x, - { exact Pbase }, { exact Pcod d }, + { exact Pbase }, { induction x with b c a, { exact Pgluel b }, { exact (cofiber_pushout_helper Pgluel Pgluer (r c)).1 ▸ Pgluer c }, { apply pathover_pathover, rewrite [p a], exact (cofiber_pushout_helper Pgluel Pgluer a).2 }} end + /- universal property of cofiber -/ + + structure is_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) := + ( im_in_ker : Π(a:A), g (f a) = pt) + ( ker_in_im : Π(b:B), (g b = pt) → fiber f b) + + definition cofiber_exact_1 {X Y Z : Type*} (f : X →* Y) (g : pcofiber f →* Z) : + (g ∘* pcod f) ∘* f ~* pconst X Z := + !passoc ⬝* pwhisker_left _ !pcod_pcompose ⬝* !pcompose_pconst + + protected definition pcofiber.elim [constructor] {X Y Z : Type*} {f : X →* Y} (g : Y →* Z) + (p : g ∘* f ~* pconst X Z) : pcofiber f →* Z := + begin + fapply pmap.mk, + { intro w, induction w with y x, exact g y, exact pt, exact p x }, + { reflexivity } + end + + protected definition pcofiber.elim_pcod {X Y Z : Type*} {f : X →* Y} {g : Y →* Z} + (p : g ∘* f ~* pconst X Z) : pcofiber.elim g p ∘* pcod f ~* g := + begin + fapply phomotopy.mk, + { intro y, reflexivity }, + { esimp, refine !idp_con ⬝ _, + refine _ ⬝ (!ap_con ⬝ (!ap_compose'⁻¹ ⬝ !ap_inv) ◾ !elim_glue)⁻¹, + apply eq_inv_con_of_con_eq, exact (to_homotopy_pt p)⁻¹ } + end + + definition cofiber_exact {X Y Z : Type*} (f : X →* Y) : + is_exact_t (@ppcompose_right _ _ Z (pcod f)) (ppcompose_right f) := + begin + constructor, + { intro g, apply eq_of_phomotopy, apply cofiber_exact_1 }, + { intro g p, note q := phomotopy_of_eq p, + exact fiber.mk (pcofiber.elim g q) (eq_of_phomotopy (pcofiber.elim_pcod q)) } + end + end pushout diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean index 46b0b7e..75337bf 100644 --- a/homotopy/smash.hlean +++ b/homotopy/smash.hlean @@ -314,7 +314,7 @@ namespace pushout A + B <-- 2 --> 1 -/ definition pushout_wedge_of_sum_equiv_unit : pushout (@wedge_of_sum A B) bool_of_sum ≃ unit := begin - refine pushout_hcompose_equiv (sum_of_bool A B) (wedge_equiv_pushout_sum A B) + refine pushout_hcompose_equiv (sum_of_bool A B) (wedge_equiv_pushout_sum A B ⬝e !pushout.symm) _ _ ⬝e _, exact erfl, intro x, induction x, @@ -350,7 +350,6 @@ namespace smash definition smash_equiv_cofiber : smash A B ≃ cofiber (@prod_of_wedge A B) := begin unfold [smash, cofiber, smash'], symmetry, - refine !pushout.symm ⬝e _, fapply pushout_vcompose_equiv wedge_of_sum, { symmetry, apply equiv_unit_of_is_contr, apply is_contr_pushout_wedge_of_sum }, { intro x, reflexivity }, @@ -367,7 +366,7 @@ namespace smash definition smash_pequiv_pcofiber [constructor] : smash A B ≃* pcofiber (pprod_of_pwedge A B) := begin apply pequiv_of_equiv (smash_equiv_cofiber A B), - exact (cofiber.glue pt)⁻¹ + exact cofiber.glue pt end variables {A B} diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index 8390f88..e6dde02 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -5,8 +5,7 @@ Authors: Michael Shulman, Floris van Doorn -/ -import homotopy.LES_of_homotopy_groups .splice homotopy.susp ..move_to_lib ..colim - ..pointed_pi +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 diff --git a/homotopy/splice.hlean b/homotopy/splice.hlean index 53cb2f4..8c6c05d 100644 --- a/homotopy/splice.hlean +++ b/homotopy/splice.hlean @@ -29,7 +29,7 @@ So far, the splicing seems to be only needed for k = 3, so it seems to be suffic -/ -import homotopy.chain_complex ..move_to_lib +import homotopy.chain_complex open prod prod.ops succ_str fin pointed nat algebra eq is_trunc equiv is_equiv diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 158d3ac..c4e6eb5 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -3,7 +3,7 @@ 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 + is_trunc function sphere unit sum prod attribute equiv_unit_of_is_contr [constructor] attribute pwedge pushout.symm pushout.equiv pushout.is_equiv_functor [constructor] @@ -13,9 +13,33 @@ attribute pushout.transpose [unfold 6] attribute ap_eq_apd10 [unfold 5] attribute eq_equiv_eq_symm [constructor] +definition add_comm_right {A : Type} [add_comm_semigroup A] (n m k : A) : n + m + k = n + k + m := +!add.assoc ⬝ ap (add n) !add.comm ⬝ !add.assoc⁻¹ + +namespace algebra + definition inf_group_loopn (n : ℕ) (A : Type*) [H : is_succ n] : inf_group (Ω[n] A) := + by induction H; exact _ +end algebra namespace eq + definition con2_assoc {A : Type} {x y z t : A} {p p' : x = y} {q q' : y = z} {r r' : z = t} + (h : p = p') (h' : q = q') (h'' : r = r') : + square ((h ◾ h') ◾ h'') (h ◾ (h' ◾ h'')) (con.assoc p q r) (con.assoc p' q' r') := + by induction h; induction h'; induction h''; exact hrfl + + definition con_left_inv_idp {A : Type} {x : A} {p : x = x} (q : p = idp) + : con.left_inv p = q⁻² ◾ q := + by cases q; reflexivity + + definition eckmann_hilton_con2 {A : Type} {x : A} {p p' q q': idp = idp :> x = x} + (h : p = p') (h' : q = q') : square (h ◾ h') (h' ◾ h) (eckmann_hilton p q) (eckmann_hilton p' q') := + by induction h; induction h'; exact hrfl + + definition ap_con_fn {A B : Type} {a a' : A} {b : B} (g h : A → b = b) (p : a = a') : + ap (λa, g a ⬝ h a) p = ap g p ◾ ap h p := + by induction p; reflexivity + protected definition homotopy.rfl [reducible] [unfold_full] {A B : Type} {f : A → B} : f ~ f := homotopy.refl f @@ -48,16 +72,6 @@ namespace eq end eq open eq -namespace cofiber - - -- replace the one in homotopy.cofiber, which has an superfluous argument - protected theorem elim_glue' {A B : Type} {f : A → B} {P : Type} (Pbase : P) (Pcod : B → P) - (Pglue : Π (x : A), Pbase = Pcod (f x)) (a : A) - : ap (cofiber.elim Pbase Pcod Pglue) (cofiber.glue a) = Pglue a := - !pushout.elim_glue - -end cofiber - namespace wedge open pushout unit protected definition glue (A B : Type*) : inl pt = inr pt :> wedge A B := @@ -87,6 +101,48 @@ namespace pointed { apply is_set.elim } end + definition ap1_gen {A B : Type} (f : A → B) {a a' : A} (p : a = a') + {b b' : B} (q : f a = b) (q' : f a' = b') : b = b' := + q⁻¹ ⬝ ap f p ⬝ q' + + definition ap1_gen_con {A B : Type} (f : A → B) {a₁ a₂ a₃ : A} (p₁ : a₁ = a₂) (p₂ : a₂ = a₃) + {b₁ b₂ b₃ : B} (q₁ : f a₁ = b₁) (q₂ : f a₂ = b₂) (q₃ : f a₃ = b₃) : + ap1_gen f (p₁ ⬝ p₂) q₁ q₃ = ap1_gen f p₁ q₁ q₂ ⬝ ap1_gen f p₂ q₂ q₃ := + begin induction p₂, induction q₃, induction q₂, reflexivity end + + definition ap1_gen_con_natural {A B : Type} (f : A → B) {a₁ a₂ a₃ : A} {p₁ p₁' : a₁ = a₂} + {p₂ p₂' : a₂ = a₃} + {b₁ b₂ b₃ : B} (q₁ : f a₁ = b₁) (q₂ : f a₂ = b₂) (q₃ : f a₃ = b₃) + (r₁ : p₁ = p₁') (r₂ : p₂ = p₂') : + square (ap1_gen_con f p₁ p₂ q₁ q₂ q₃) + (ap1_gen_con f p₁' p₂' q₁ q₂ q₃) + (ap (λp, ap1_gen f p q₁ q₃) (r₁ ◾ r₂)) + (ap (λp, ap1_gen f p q₁ q₂) r₁ ◾ ap (λp, ap1_gen f p q₂ q₃) r₂) := + begin induction r₁, induction r₂, exact vrfl end + + definition ap1_gen_con_idp {A B : Type} (f : A → B) {a : A} {b : B} (q : f a = b) : + ap1_gen_con f idp idp q q q ⬝ con.left_inv q ◾ con.left_inv q = con.left_inv q := + by induction q; reflexivity + + -- TODO: replace with ap1_con + definition ap1_con2 {A B : Type*} (f : A →* B) (p q : Ω A) : ap1 f (p ⬝ q) = ap1 f p ⬝ ap1 f q := + ap1_gen_con f p q (respect_pt f) (respect_pt f) (respect_pt f) + + + definition ap1_gen_con_left {A B : Type} {a a' : A} {b₀ b₁ b₂ : B} + {f : A → b₀ = b₁} {f' : A → b₁ = b₂} (p : a = a') {q₀ q₁ : b₀ = b₁} {q₀' q₁' : b₁ = b₂} + (r₀ : f a = q₀) (r₁ : f a' = q₁) (r₀' : f' a = q₀') (r₁' : f' a' = q₁') : + ap1_gen (λa, f a ⬝ f' a) p (r₀ ◾ r₀') (r₁ ◾ r₁') = + whisker_right q₀' (ap1_gen f p r₀ r₁) ⬝ whisker_left q₁ (ap1_gen f' p r₀' r₁') := + begin induction r₀, induction r₁, induction r₀', induction r₁', induction p, reflexivity end + + definition ap1_gen_con_left_idp {A B : Type} {a : A} {b₀ b₁ b₂ : B} + {f : A → b₀ = b₁} {f' : A → b₁ = b₂} {q₀ : b₀ = b₁} {q₁ : b₁ = b₂} + (r₀ : f a = q₀) (r₁ : f' a = q₁) : + ap1_gen_con_left idp r₀ r₀ r₁ r₁ = + !con.left_inv ⬝ (ap (whisker_right q₁) !con.left_inv ◾ ap (whisker_left _) !con.left_inv)⁻¹ := + begin induction r₀, induction r₁, reflexivity end + -- /- the pointed type of (unpointed) dependent maps -/ -- definition pupi [constructor] {A : Type} (P : A → Type*) : Type* := -- pointed.mk' (Πa, P a) @@ -713,6 +769,11 @@ end circle namespace susp + definition loop_psusp_intro_natural {X Y Z : Type*} (g : psusp Y →* Z) (f : X →* Y) : + loop_psusp_intro (g ∘* psusp_functor f) ~* loop_psusp_intro g ∘* f := + pwhisker_right _ !ap1_pcompose ⬝* !passoc ⬝* pwhisker_left _ !loop_psusp_unit_natural⁻¹* ⬝* + !passoc⁻¹* + definition psusp_functor_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) : psusp_functor f ~* psusp_functor g := begin diff --git a/pointed_pi.hlean b/pointed_pi.hlean index e0e3585..6441d21 100644 --- a/pointed_pi.hlean +++ b/pointed_pi.hlean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ulrik Buchholtz -/ -import move_to_lib +import .move_to_lib open eq pointed equiv sigma