diff --git a/algebra/seq_colim.hlean b/algebra/seq_colim.hlean index d19c4fe..b184bda 100644 --- a/algebra/seq_colim.hlean +++ b/algebra/seq_colim.hlean @@ -6,7 +6,7 @@ namespace group section - parameters (A : ℕ → AbGroup) (f : Πi , A i → A (i + 1)) + parameters (A : ℕ → AbGroup) (f : Πi , A i →g A (i + 1)) variables {A' : AbGroup} definition seq_colim_carrier : AbGroup := dirsum A @@ -72,8 +72,21 @@ namespace group 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 _ + (h : Πi, A i →g A' i) (p : Πi, hsquare (f i) (f' i) (h i) (h (i+1))) : + seq_colim A f →g seq_colim A' f' := + seq_colim_elim (λi, seq_colim_incl i ∘g h i) + begin + intro i a, + refine !homomorphism_comp_compute ⬝ _ ⬝ !homomorphism_comp_compute⁻¹, + refine _ ⬝ ap (seq_colim_incl (succ i)) (p i a)⁻¹, + apply seq_colim_glue + end + -- definition seq_colim_functor_compose [constructor] {A A' A'' : ℕ → AbGroup} + -- {f : Πi , A i →g A (i + 1)} {f' : Πi , A' i →g A' (i + 1)} {f'' : Πi , A'' i →g A'' (i + 1)} + -- (h : Πi, A i →g A' i) (p : Πi (a : A i), h (i+1) (f i a) = f' i (h i a)) + -- (h : Πi, A i →g A' i) (p : Πi (a : A i), h (i+1) (f i a) = f' i (h i a)) : + -- seq_colim A f →g seq_colim A' f' := + -- sorry end group diff --git a/colim.hlean b/colim.hlean index 57daa6b..1e5c279 100644 --- a/colim.hlean +++ b/colim.hlean @@ -377,6 +377,12 @@ namespace seq_colim exact !pcompose_pid end + definition seq_colim_equiv_zigzag (g : Π⦃n⦄, A n → A' n) (h : Π⦃n⦄, A' n → A (succ n)) + (p : Π⦃n⦄ (a : A n), h (g a) = f a) (q : Π⦃n⦄ (a : A' n), g (h a) = f' a) : + seq_colim f ≃ seq_colim f' := + sorry + + definition is_equiv_seq_colim_rec (P : seq_colim f → Type) : is_equiv (seq_colim_rec_unc : (Σ(Pincl : Π ⦃n : ℕ⦄ (a : A n), P (ι f a)), diff --git a/homology/homology.hlean b/homology/homology.hlean index f220b76..e656240 100644 --- a/homology/homology.hlean +++ b/homology/homology.hlean @@ -112,8 +112,8 @@ 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 := +definition homology_functor [constructor] {X Y : Type*} {E F : prespectrum} (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} := diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean index 82d5a98..1f0723e 100644 --- a/homotopy/smash.hlean +++ b/homotopy/smash.hlean @@ -664,7 +664,7 @@ namespace smash (!smash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans) ⬝pv** smash_functor_pconst_pcompose (pid A) (pid A) g - /- these lemmas are use to show that smash_functor_right is natural in all arguments -/ + /- Using these lemmas we show that smash_functor_right is natural in all arguments -/ definition smash_functor_right_natural_right (f : C →* C') : psquare (smash_functor_right A B C) (smash_functor_right A B C') (ppcompose_left f) (ppcompose_left (pid A ∧→ f)) := @@ -926,8 +926,8 @@ namespace smash refine _ ⬝hp (!ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluer)⁻¹, exact hrfl }, end - definition smash_flip_smash_functor (f : A →* C) (g : B →* D) : psquare - (smash_flip A B) (smash_flip C D) (f ∧→ g) (g ∧→ f) := + definition smash_flip_smash_functor (f : A →* C) (g : B →* D) : + psquare (smash_flip A B) (smash_flip C D) (f ∧→ g) (g ∧→ f) := begin apply phomotopy.mk (smash_flip_smash_functor' f g), refine !idp_con ⬝ _ ⬝ !idp_con⁻¹, refine !ap_ap011 ⬝ _, apply ap011_flip, diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index 0be9bea..ce7c8df 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -98,7 +98,7 @@ namespace spectrum | succ_str.of_nat zero := z | succ_str.of_nat (succ k) := S (succ_str.of_nat k) - definition psp_of_gen_indexed [constructor] {N : succ_str} (z : N) (E : gen_prespectrum N) : gen_prespectrum +ℤ := + definition psp_of_gen_indexed [constructor] {N : succ_str} (z : N) (E : gen_prespectrum N) : prespectrum := psp_of_nat_indexed (gen_prespectrum.mk (λn, E (succ_str.of_nat z n)) (λn, gen_prespectrum.glue E (succ_str.of_nat z n))) definition is_spectrum_of_gen_indexed [instance] {N : succ_str} (z : N) (E : gen_prespectrum N) [H : is_spectrum E] @@ -257,20 +257,26 @@ namespace spectrum /- homotopy group of a prespectrum -/ - definition pshomotopy_group (n : ℤ) (E : prespectrum) : AbGroup := - group.seq_colim (λ(k : ℕ), πag[k+2] (E (-n - 2 + k))) + definition pshomotopy_group_hom (n : ℤ) (E : prespectrum) (k : ℕ) + : πag[k + 2] (E (-n - 2 + k)) →g πag[k + 3] (E (-n - 2 + (k + 1))) := 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))) + refine _ ∘g π→g[k+2] (glue E _), + refine (ghomotopy_group_succ_in _ (k+1))⁻¹ᵍ ∘g _, + refine homotopy_group_isomorphism_of_pequiv (k+1) + (loop_pequiv_loop (pequiv_of_eq (ap E !add.assoc))) end + definition pshomotopy_group (n : ℤ) (E : prespectrum) : AbGroup := + group.seq_colim (λ(k : ℕ), πag[k+2] (E (-n - 2 + k))) (pshomotopy_group_hom n E) + 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 _ _ + group.seq_colim_functor (λk, π→g[k+2] (f (-n - 2 +[ℤ] k))) + begin + exact sorry + end notation `πₚₛ→[`:95 n:0 `]`:0 := pshomotopy_group_fun n