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⁻¹* }