From c0b7740f13d912c26456edfa948e80428bc0de4b Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 2 Feb 2017 17:14:48 -0500 Subject: [PATCH] order of arguments in group.mk has changed --- algebra/arrow_group.hlean | 4 ++-- algebra/free_commutative_group.hlean | 2 +- algebra/free_group.hlean | 4 ++-- algebra/product_group.hlean | 2 +- algebra/quotient_group.hlean | 2 +- algebra/subgroup.hlean | 2 +- colim.hlean | 4 ++-- homotopy/cohomology.hlean | 22 +++++++++++++++++++++- move_to_lib.hlean | 10 +++++----- 9 files changed, 36 insertions(+), 16 deletions(-) diff --git a/algebra/arrow_group.hlean b/algebra/arrow_group.hlean index cfaa89e..607ed8a 100644 --- a/algebra/arrow_group.hlean +++ b/algebra/arrow_group.hlean @@ -8,8 +8,8 @@ namespace group definition group_arrow [instance] (A B : Type) [group B] : group (A → B) := begin fapply group.mk, - { intro f g a, exact f a * g a }, { 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 }, @@ -31,9 +31,9 @@ namespace group 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 }, - { apply is_trunc_pmap }, { 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 }, diff --git a/algebra/free_commutative_group.hlean b/algebra/free_commutative_group.hlean index a459968..03eabf9 100644 --- a/algebra/free_commutative_group.hlean +++ b/algebra/free_commutative_group.hlean @@ -137,7 +137,7 @@ namespace group variables (X) 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 + 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_ab_group [constructor] : AbGroup := diff --git a/algebra/free_group.hlean b/algebra/free_group.hlean index c46d923..125332d 100644 --- a/algebra/free_group.hlean +++ b/algebra/free_group.hlean @@ -112,8 +112,8 @@ namespace group -- export [reduce_hints] free_group variables (X) definition group_free_group [constructor] : group (free_group_carrier X) := - group.mk free_group_mul _ free_group_mul_assoc free_group_one free_group_one_mul free_group_mul_one - free_group_inv free_group_mul_left_inv + group.mk _ free_group_mul free_group_mul_assoc free_group_one free_group_one_mul + free_group_mul_one free_group_inv free_group_mul_left_inv definition free_group [constructor] : Group := Group.mk _ (group_free_group X) diff --git a/algebra/product_group.hlean b/algebra/product_group.hlean index 800650f..a07cb61 100644 --- a/algebra/product_group.hlean +++ b/algebra/product_group.hlean @@ -46,7 +46,7 @@ namespace group variables (G G') definition group_prod [constructor] : group (G × G') := - group.mk product_mul _ product_mul_assoc product_one product_one_mul product_mul_one + group.mk _ product_mul product_mul_assoc product_one product_one_mul product_mul_one product_inv product_mul_left_inv definition product [constructor] : Group := diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean index 1d202b2..7e448fd 100644 --- a/algebra/quotient_group.hlean +++ b/algebra/quotient_group.hlean @@ -125,7 +125,7 @@ namespace group variable (N) definition group_qg [constructor] : group (qg N) := - group.mk quotient_mul _ quotient_mul_assoc quotient_one quotient_one_mul quotient_mul_one + group.mk _ quotient_mul quotient_mul_assoc quotient_one quotient_one_mul quotient_mul_one quotient_inv quotient_mul_left_inv definition quotient_group [constructor] : Group := diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean index 532d3f2..088ca44 100644 --- a/algebra/subgroup.hlean +++ b/algebra/subgroup.hlean @@ -214,7 +214,7 @@ namespace group variable (H) definition group_sg [constructor] : group (sg H) := - group.mk subgroup_mul _ subgroup_mul_assoc subgroup_one subgroup_one_mul subgroup_mul_one + group.mk _ subgroup_mul subgroup_mul_assoc subgroup_one subgroup_one_mul subgroup_mul_one subgroup_inv subgroup_mul_left_inv definition subgroup [constructor] : Group := diff --git a/colim.hlean b/colim.hlean index d55460b..1f96637 100644 --- a/colim.hlean +++ b/colim.hlean @@ -188,12 +188,12 @@ namespace seq_colim seq_diagram (λn, Πx, A x n) := λn f x, g (f x) - namespace seq_colim.ops + namespace ops abbreviation ι [constructor] := @inclusion abbreviation pι [constructor] {A} (f) {n} := @pinclusion A f n abbreviation pι' [constructor] [parsing_only] := @pinclusion abbreviation ι' [constructor] [parsing_only] {A} (f n) := @inclusion A f n - end seq_colim.ops + end ops open seq_colim.ops definition rep0_glue (k : ℕ) (a : A 0) : ι f (rep0 f k a) = ι f a := diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean index a0ea060..5353142 100644 --- a/homotopy/cohomology.hlean +++ b/homotopy/cohomology.hlean @@ -8,7 +8,9 @@ Reduced cohomology import algebra.arrow_group .spectrum homotopy.EM -open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops +open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops equiv susp + +namespace cohomology definition EM_spectrum /-[constructor]-/ (G : AbGroup) : spectrum := spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*) @@ -43,3 +45,21 @@ definition cohomology_homomorphism_compose {X X' X'' : Type*} (g : 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⁻¹* + +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/move_to_lib.hlean b/move_to_lib.hlean index 41db314..158d3ac 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -858,8 +858,8 @@ namespace category begin have foo : Π(g : A), @inv A G g = (@inv A G g * g) * @inv A H g, from λg, !mul_inv_cancel_right⁻¹, - cases G with Gm Gs Gh1 G1 Gh2 Gh3 Gi Gh4, - cases H with Hm Hs Hh1 H1 Hh2 Hh3 Hi Hh4, + cases G with Gs Gm Gh1 G1 Gh2 Gh3 Gi Gh4, + cases H with Hs Hm Hh1 H1 Hh2 Hh3 Hi Hh4, change Gi ~ Hi, intro g, have p' : Gm ~2 Hm, from p, calc Gi g = Hm (Hm (Gi g) g) (Hi g) : foo @@ -910,9 +910,9 @@ namespace category induction G with G g, induction H with H h, esimp [Group.sigma_char2] at p, induction p, refine !pathover_idp ⬝e _, - induction g with m s ma o om mo i mi, induction h with μ σ μa ε εμ με ι μι, - exact Group_eq_equiv_lemma2 (Group.sigma_char2 (Group.mk G (group.mk m s ma o om mo i mi))).2.2 - (Group.sigma_char2 (Group.mk G (group.mk μ σ μa ε εμ με ι μι))).2.2 + induction g with s m ma o om mo i mi, induction h with σ μ μa ε εμ με ι μι, + exact Group_eq_equiv_lemma2 (Group.sigma_char2 (Group.mk G (group.mk s m ma o om mo i mi))).2.2 + (Group.sigma_char2 (Group.mk G (group.mk σ μ μa ε εμ με ι μι))).2.2 end definition isomorphism.sigma_char (G H : Group) : (G ≃g H) ≃ Σ(e : G ≃ H), is_mul_hom e :=