From 8362498b564839da4d69aa11520db3e7b10aad98 Mon Sep 17 00:00:00 2001 From: favonia Date: Thu, 8 Jun 2017 17:48:26 -0600 Subject: [PATCH 1/5] Remove AddGroup symbol. --- algebra/direct_sum.hlean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean index e4fdeef..e691287 100644 --- a/algebra/direct_sum.hlean +++ b/algebra/direct_sum.hlean @@ -124,7 +124,7 @@ namespace group dirsum_elim (λi, dirsum_incl Y' i ∘g f i) theorem dirsum_functor_compose (f' : Πi, Y' i →g Y'' i) (f : Πi, Y i →g Y' i) : - dirsum_functor f' ∘a dirsum_functor f ~ dirsum_functor (λi, f' i ∘a f i) := + dirsum_functor f' ∘g dirsum_functor f ~ dirsum_functor (λi, f' i ∘g f i) := begin apply dirsum_homotopy, intro i y, reflexivity, From c0ea92a0b514a300998ca7000d19a504dd205bb1 Mon Sep 17 00:00:00 2001 From: favonia Date: Thu, 8 Jun 2017 17:51:25 -0600 Subject: [PATCH 2/5] Add dirsum_functor_isomorphism. --- algebra/direct_sum.hlean | 30 ++++++++++++++++++++++++++++-- 1 file changed, 28 insertions(+), 2 deletions(-) diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean index e691287..aeb3142 100644 --- a/algebra/direct_sum.hlean +++ b/algebra/direct_sum.hlean @@ -1,7 +1,7 @@ /- -Copyright (c) 2015 Floris van Doorn. All rights reserved. +Copyright (c) 2015 Floris van Doorn, Egbert Rijke, Favonia. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Floris van Doorn, Egbert Rijke +Authors: Floris van Doorn, Egbert Rijke, Favonia Constructions with groups -/ @@ -156,4 +156,30 @@ namespace group definition dirsum_functor_left [constructor] (f : J → I) : dirsum (Y ∘ f) →g dirsum Y := dirsum_elim (λj, dirsum_incl Y (f j)) + definition dirsum_functor_isomorphism [constructor] (f : Πi, Y i ≃g Y' i) : dirsum Y ≃g dirsum Y' := + let to_hom := dirsum_functor (λ i, f i) in + let from_hom := dirsum_functor (λ i, (f i)⁻¹ᵍ) in + begin + fapply isomorphism.mk, + exact dirsum_functor (λ i, f i), + fapply is_equiv.adjointify, + exact dirsum_functor (λ i, (f i)⁻¹ᵍ), + { intro ds, + refine (homomorphism_comp_compute (dirsum_functor (λ i, f i)) (dirsum_functor (λ i, (f i)⁻¹ᵍ)) _)⁻¹ ⬝ _, + refine dirsum_functor_compose (λ i, f i) (λ i, (f i)⁻¹ᵍ) ds ⬝ _, + refine @dirsum_functor_homotopy I Y' Y' _ (λ i, !gid) (λ i, to_right_inv (equiv_of_isomorphism (f i))) ds ⬝ _, + exact !dirsum_functor_gid + }, + { intro ds, + refine (homomorphism_comp_compute (dirsum_functor (λ i, (f i)⁻¹ᵍ)) (dirsum_functor (λ i, f i)) _)⁻¹ ⬝ _, + refine dirsum_functor_compose (λ i, (f i)⁻¹ᵍ) (λ i, f i) ds ⬝ _, + refine @dirsum_functor_homotopy I Y Y _ (λ i, !gid) (λ i x, + proof + to_left_inv (equiv_of_isomorphism (f i)) x + qed + ) ds ⬝ _, + exact !dirsum_functor_gid + } + end + end group From 56d97200d63dccac6d1cee238884c2cbcb0bb982 Mon Sep 17 00:00:00 2001 From: favonia Date: Thu, 8 Jun 2017 18:06:59 -0600 Subject: [PATCH 3/5] Fix the naming. --- algebra/direct_sum.hlean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean index aeb3142..b21ccd3 100644 --- a/algebra/direct_sum.hlean +++ b/algebra/direct_sum.hlean @@ -156,7 +156,7 @@ namespace group definition dirsum_functor_left [constructor] (f : J → I) : dirsum (Y ∘ f) →g dirsum Y := dirsum_elim (λj, dirsum_incl Y (f j)) - definition dirsum_functor_isomorphism [constructor] (f : Πi, Y i ≃g Y' i) : dirsum Y ≃g dirsum Y' := + definition dirsum_isomorphism [constructor] (f : Πi, Y i ≃g Y' i) : dirsum Y ≃g dirsum Y' := let to_hom := dirsum_functor (λ i, f i) in let from_hom := dirsum_functor (λ i, (f i)⁻¹ᵍ) in begin From e4168439c0793514255843a5d54e36fe74f78507 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 8 Jun 2017 20:09:48 -0400 Subject: [PATCH 4/5] work on homotopy group of prespectrum --- algebra/seq_colim.hlean | 29 ++++++++++++++++++----------- homology/homology.hlean | 16 ++++++++++------ homotopy/spectrum.hlean | 27 +++++++++++++++++++++++---- 3 files changed, 51 insertions(+), 21 deletions(-) diff --git a/algebra/seq_colim.hlean b/algebra/seq_colim.hlean index ef1605e..d19c4fe 100644 --- a/algebra/seq_colim.hlean +++ b/algebra/seq_colim.hlean @@ -6,7 +6,7 @@ namespace group section - parameters (A : @trunctype.mk 0 ℕ _ → AbGroup) (f : Πi , A i → A (i + 1)) + parameters (A : ℕ → AbGroup) (f : Πi , A i → A (i + 1)) variables {A' : AbGroup} definition seq_colim_carrier : AbGroup := dirsum A @@ -15,17 +15,18 @@ namespace group definition seq_colim : AbGroup := quotient_ab_group_gen seq_colim_carrier (λa, ∥seq_colim_rel a∥) + parameters {A f} definition seq_colim_incl [constructor] (i : ℕ) : A i →g seq_colim := gqg_map _ _ ∘g dirsum_incl A i definition seq_colim_quotient (h : Πi, A i →g A') (k : Πi a, h i a = h (succ i) (f i a)) (v : seq_colim_carrier) (r : ∥seq_colim_rel v∥) : dirsum_elim h v = 1 := begin - induction r with r, induction r, + induction r with r, induction r, refine !to_respect_mul ⬝ _, - refine ap (λγ, group_fun (dirsum_elim h) (group_fun (dirsum_incl A i) a) * group_fun (dirsum_elim h) γ) + refine ap (λγ, group_fun (dirsum_elim h) (group_fun (dirsum_incl A i) a) * group_fun (dirsum_elim h) γ) (!to_respect_inv)⁻¹ ⬝ _, - refine ap (λγ, γ * group_fun (dirsum_elim h) (group_fun (dirsum_incl A (succ i)) (f i a)⁻¹)) + refine ap (λγ, γ * group_fun (dirsum_elim h) (group_fun (dirsum_incl A (succ i)) (f i a)⁻¹)) !dirsum_elim_compute ⬝ _, refine ap (λγ, (h i a) * γ) !dirsum_elim_compute ⬝ _, refine ap (λγ, γ * group_fun (h (succ i)) (f i a)⁻¹) !k ⬝ _, @@ -38,7 +39,7 @@ namespace group gqg_elim _ (dirsum_elim h) (seq_colim_quotient h k) definition seq_colim_compute (h : Πi, A i →g A') - (k : Πi a, h i a = h (succ i) (f i a)) (i : ℕ) (a : A i) : + (k : Πi a, h i a = h (succ i) (f i a)) (i : ℕ) (a : A i) : (seq_colim_elim h k) (seq_colim_incl i a) = h i a := begin refine gqg_elim_compute (λa, ∥seq_colim_rel a∥) (dirsum_elim h) (seq_colim_quotient h k) (dirsum_incl A i a) ⬝ _, @@ -47,17 +48,17 @@ namespace group definition seq_colim_glue {i : @trunctype.mk 0 ℕ _} {a : A i} : seq_colim_incl i a = seq_colim_incl (succ i) (f i a) := begin - refine !grp_comp_comp ⬝ _, - refine gqg_eq_of_rel _ _ ⬝ (!grp_comp_comp)⁻¹, - exact tr (seq_colim_rel.rmk _ _) + refine !homomorphism_comp_compute ⬝ _, + refine gqg_eq_of_rel _ _ ⬝ (!homomorphism_comp_compute)⁻¹, + exact tr (seq_colim_rel.rmk _ _) end section local abbreviation h (m : seq_colim →g A') : Πi, A i →g A' := λi, m ∘g (seq_colim_incl i) - local abbreviation k (m : seq_colim →g A') : Πi a, h m i a = h m (succ i) (f i a) := - λ i a, !grp_comp_comp ⬝ ap m (@seq_colim_glue i a) ⬝ !grp_comp_comp⁻¹ + local abbreviation k (m : seq_colim →g A') : Πi a, h m i a = h m (succ i) (f i a) := + λ i a, !homomorphism_comp_compute ⬝ ap m (@seq_colim_glue i a) ⬝ !homomorphism_comp_compute⁻¹ - definition seq_colim_unique (m : seq_colim →g A') : + definition seq_colim_unique (m : seq_colim →g A') : Πv, seq_colim_elim (h m) (k m) v = m v := begin intro v, refine (gqg_elim_unique _ (dirsum_elim (h m)) _ m _ _)⁻¹ ⬝ _, @@ -69,4 +70,10 @@ namespace group end + definition seq_colim_functor [constructor] {A A' : ℕ → AbGroup} + {f : Πi , A i →g A (i + 1)} {f' : Πi , A' i →g A' (i + 1)} + (h : Πi, A i →g A' i) : seq_colim A f →g seq_colim A' f' := + sorry --_ ∘g _ + + end group diff --git a/homology/homology.hlean b/homology/homology.hlean index f5e029b..00fc5d1 100644 --- a/homology/homology.hlean +++ b/homology/homology.hlean @@ -14,7 +14,6 @@ open eq spectrum int pointed group algebra sphere nat equiv susp is_trunc namespace homology /- homology theory -/ - structure homology_theory.{u} : Type.{u+1} := (HH : ℤ → pType.{u} → AbGroup.{u}) (Hh : Π(n : ℤ) {X Y : Type*} (f : X →* Y), HH n X →g HH n Y) @@ -89,8 +88,12 @@ namespace homology end -/- homology theory associated to a spectrum -/ -definition homology (X : Type*) (E : spectrum) (n : ℤ) : AbGroup := +/- homology theory associated to a prespectrum -/ +definition homology (X : Type*) (E : prespectrum) (n : ℤ) : AbGroup := +pshomotopy_group n (smash_prespectrum X E) + +/- an alternative definition, which might be a bit harder to work with -/ +definition homology_spectrum (X : Type*) (E : spectrum) (n : ℤ) : AbGroup := shomotopy_group n (smash_spectrum X E) definition parametrized_homology {X : Type*} (E : X → spectrum) (n : ℤ) : AbGroup := @@ -109,12 +112,13 @@ notation `pH_` n `[`:0 binders `, ` r:(scoped E, parametrized_homology E n) `]`: definition unpointed_homology (X : Type) (E : spectrum) (n : ℤ) : AbGroup := H_ n[X₊, E] -definition homology_functor [constructor] {X Y : Type*} {E F : spectrum} (f : X →* Y) (g : E →ₛ F) (n : ℤ) : homology X E n →g homology Y F n := -shomotopy_group_fun n (smash_spectrum_fun f g) +definition homology_functor [constructor] {X Y : Type*} {E F : spectrum} (f : X →* Y) (g : E →ₛ F) (n : ℤ) + : homology X E n →g homology Y F n := +pshomotopy_group_fun n (smash_prespectrum_fun f g) definition homology_theory_spectrum.{u} [constructor] (E : spectrum.{u}) : homology_theory.{u} := begin - refine homology_theory.mk _ _ _ _ _ _ _ _, + fapply homology_theory.mk, exact (λn X, H_ n[X, E]), exact (λn X Y f, homology_functor f (sid E) n), exact sorry, -- Hid is uninteresting but potentially very hard to prove diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index 7e4fdb2..96ea66e 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -5,9 +5,9 @@ Authors: Michael Shulman, Floris van Doorn -/ -import homotopy.LES_of_homotopy_groups .splice ..colim types.pointed2 .EM ..pointed_pi .smash_adjoint +import homotopy.LES_of_homotopy_groups .splice ..colim types.pointed2 .EM ..pointed_pi .smash_adjoint ..algebra.seq_colim open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group - seq_colim succ_str EM EM.ops + seq_colim succ_str EM EM.ops function /--------------------- Basic definitions @@ -227,6 +227,25 @@ namespace spectrum notation `πₛ→[`:95 n:0 `]`:0 := shomotopy_group_fun n + /- homotopy group of a prespectrum -/ + + definition pshomotopy_group (n : ℤ) (E : prespectrum) : AbGroup := + group.seq_colim (λ(k : ℕ), πag[k+2] (E (-n - 2 + k))) + begin + intro k, + refine _ ∘ π→g[k+2] (glue E _), + refine (homotopy_group_succ_in _ (k+2))⁻¹ᵉ* ∘ _, + refine homotopy_group_pequiv (k+2) (loop_pequiv_loop (pequiv_of_eq (ap E !add.assoc))) + end + + notation `πₚₛ[`:95 n:0 `]`:0 := pshomotopy_group n + + definition pshomotopy_group_fun (n : ℤ) {E F : prespectrum} (f : E →ₛ F) : + πₚₛ[n] E →g πₚₛ[n] F := + sorry --group.seq_colim_functor _ _ + + notation `πₚₛ→[`:95 n:0 `]`:0 := pshomotopy_group_fun n + /------------------------------- Cotensor of spectra by types -------------------------------/ @@ -401,7 +420,7 @@ namespace spectrum spectrify_type_fun' X n (succ k) ~* Ω→ (spectrify_type_fun' X n k) := begin refine _ ⬝* !ap1_pcompose⁻¹*, - apply !pwhisker_right, + apply !pwhisker_right, refine !to_pinv_pequiv_MK2 end @@ -452,7 +471,7 @@ namespace spectrum refine _ ◾* (spectrify_type_fun_zero X n ⬝* !pid_pcompose⁻¹*), refine !passoc ⬝* pwhisker_left _ !pseq_colim_pequiv_pinclusion ⬝* _, refine pwhisker_left _ (pwhisker_left _ (ap1_pid) ⬝* !pcompose_pid) ⬝* _, - refine !passoc ⬝* pwhisker_left _ !seq_colim_equiv_constant_pinclusion ⬝* _, + refine !passoc ⬝* pwhisker_left _ !seq_colim_equiv_constant_pinclusion ⬝* _, apply pinv_left_phomotopy_of_phomotopy, exact !pseq_colim_loop_pinclusion⁻¹* } From b2ab29c3c3b6abeb40e367493a9fa89f74916bd4 Mon Sep 17 00:00:00 2001 From: spiceghello Date: Thu, 8 Jun 2017 18:28:15 -0600 Subject: [PATCH 5/5] on colim.elim o pinclusion, and corollary on spectra --- colim.hlean | 36 ++++++++++++++++++++++++++++++---- homotopy/spectrum.hlean | 43 +++++++++++++++++++++++++++-------------- 2 files changed, 60 insertions(+), 19 deletions(-) diff --git a/colim.hlean b/colim.hlean index 7619b49..57daa6b 100644 --- a/colim.hlean +++ b/colim.hlean @@ -399,8 +399,8 @@ namespace seq_colim equiv.mk _ !is_equiv_seq_colim_rec end functor - definition pseq_colim.elim' [constructor] {A : ℕ → Type*} {B : Type*} {f : Π{n}, A n →* A (n+1)} - (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f ~ g n) : pseq_colim @f →* B := + definition pseq_colim.elim' [constructor] {A : ℕ → Type*} {B : Type*} {f : Πn, A n →* A (n+1)} + (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f n ~ g n) : pseq_colim f →* B := begin fapply pmap.mk, { intro x, induction x with n a n a, @@ -409,10 +409,38 @@ namespace seq_colim { esimp, apply respect_pt } end - definition pseq_colim.elim [constructor] {A : ℕ → Type*} {B : Type*} {f : Π{n}, A n →* A (n+1)} - (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f ~* g n) : pseq_colim @f →* B := + definition pseq_colim.elim [constructor] {A : ℕ → Type*} {B : Type*} {f : Πn, A n →* A (n+1)} + (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f n ~* g n) : pseq_colim @f →* B := pseq_colim.elim' g p + definition pseq_colim.elim_pinclusion {A : ℕ → Type*} {B : Type*} {f : Πn, A n →* A (n+1)} + (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f n ~* g n) (n : ℕ) : + pseq_colim.elim g p ∘* pinclusion f n ~* g n := + begin + refine phomotopy.mk phomotopy.rfl _, + refine !idp_con ⬝ _, + esimp, + induction n with n IH, + { esimp, esimp[inclusion_pt], exact !idp_con⁻¹ }, + { esimp, esimp[inclusion_pt], + rewrite ap_con, rewrite ap_con, + rewrite elim_glue, + rewrite [-ap_inv], + rewrite [-ap_compose'], esimp, + rewrite [(eq_con_inv_of_con_eq (!to_homotopy_pt))], + rewrite [IH], + rewrite [con_inv], + rewrite [-+con.assoc], + refine _ ⬝ whisker_right _ !con.assoc⁻¹, + rewrite [con.left_inv], esimp, + refine _ ⬝ !con.assoc⁻¹, + rewrite [con.left_inv], esimp, + rewrite [ap_inv], + rewrite [-con.assoc], + refine !idp_con⁻¹ ⬝ whisker_right _ !con.left_inv⁻¹, + } + end + definition prep0 [constructor] {A : ℕ → Type*} (f : pseq_diagram A) (k : ℕ) : A 0 →* A k := pmap.mk (rep0 (λn x, f x) k) begin induction k with k p, reflexivity, exact ap (@f k) p ⬝ !respect_pt end diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index 96ea66e..2565806 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -477,28 +477,41 @@ namespace spectrum } end + definition spectrify.elim_n {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N} + (f : X →ₛ Y) (n : N) : (spectrify X) n →* Y n := + begin + fapply pseq_colim.elim, + { intro k, refine !equiv_gluen⁻¹ᵉ* ∘* apn k (f (n +' k)) }, + { intro k, refine !passoc ⬝* pwhisker_right _ !equiv_gluen_inv_succ ⬝* _, + refine !passoc ⬝* _, apply pwhisker_left, + refine !passoc ⬝* _, + refine pwhisker_left _ ((passoc _ _ (_ ∘* _))⁻¹*) ⬝* _, + refine pwhisker_left _ !passoc⁻¹* ⬝* _, + refine pwhisker_left _ (pwhisker_right _ (phomotopy_pinv_right_of_phomotopy (!loopn_succ_in_natural)⁻¹*)⁻¹*) ⬝* _, + refine pwhisker_right _ !apn_pinv ⬝* _, + refine (phomotopy_pinv_left_of_phomotopy _)⁻¹*, + refine pwhisker_right _ !pmap_eta⁻¹* ⬝* _, + refine apn_psquare k _, + refine pwhisker_right _ _ ⬝* psquare_of_phomotopy !smap.glue_square, + exact !pmap_eta⁻¹* + } + end + definition spectrify.elim {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N} (f : X →ₛ Y) : spectrify X →ₛ Y := begin fapply smap.mk, - { intro n, fapply pseq_colim.elim, - { intro k, refine !equiv_gluen⁻¹ᵉ* ∘* apn k (f (n +' k)) }, - { intro k, refine !passoc ⬝* pwhisker_right _ !equiv_gluen_inv_succ ⬝* _, - refine !passoc ⬝* _, apply pwhisker_left, - refine !passoc ⬝* _, - refine pwhisker_left _ ((passoc _ _ (_ ∘* _))⁻¹*) ⬝* _, - refine pwhisker_left _ !passoc⁻¹* ⬝* _, - refine pwhisker_left _ (pwhisker_right _ (phomotopy_pinv_right_of_phomotopy (!loopn_succ_in_natural)⁻¹*)⁻¹*) ⬝* _, - refine pwhisker_right _ !apn_pinv ⬝* _, - refine (phomotopy_pinv_left_of_phomotopy _)⁻¹*, - refine pwhisker_right _ !pmap_eta⁻¹* ⬝* _, - refine apn_psquare k _, - refine pwhisker_right _ _ ⬝* psquare_of_phomotopy !smap.glue_square, - exact !pmap_eta⁻¹* - }}, + { intro n, exact spectrify.elim_n f n }, { intro n, exact sorry } end + definition phomotopy_spectrify.elim {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N} + (f : X →ₛ Y) (n : N) : spectrify.elim_n f n ∘* spectrify_map n ~* f n := + begin + refine pseq_colim.elim_pinclusion _ _ 0 ⬝* _, + exact !pid_pcompose + end + definition spectrify_fun {N : succ_str} {X Y : gen_prespectrum N} (f : X →ₛ Y) : spectrify X →ₛ spectrify Y := spectrify.elim ((@spectrify_map _ Y) ∘ₛ f)