diff --git a/algebra/arrow_group.hlean b/algebra/arrow_group.hlean index 3db123c..3b3a9ed 100644 --- a/algebra/arrow_group.hlean +++ b/algebra/arrow_group.hlean @@ -67,8 +67,9 @@ namespace group : Group.mk (trunc 0 (Π*(a : A), Ω B)) !trunc_group ≃g Group.mk (trunc 0 (A →* Ω B)) !trunc_group := begin - apply trunc_isomorphism_of_equiv (pppi_equiv_pmap A (Ω B)), - intro h k, induction h with h h_pt, induction k with k k_pt, reflexivity + reflexivity, + -- apply trunc_isomorphism_of_equiv (pppi_equiv_pmap A (Ω B)), + -- intro h k, induction h with h h_pt, induction k with k k_pt, reflexivity end section diff --git a/algebra/spectral_sequence.hlean b/algebra/spectral_sequence.hlean index 42eeb34..4f7152b 100644 --- a/algebra/spectral_sequence.hlean +++ b/algebra/spectral_sequence.hlean @@ -442,6 +442,17 @@ namespace left_module lemma Dinfdiag_stable {s : ℕ} (h : B (deg (k X) x) ≤ s) : is_contr (Dinfdiag s) := is_contr_D _ _ (Dub !deg_iterate_ik_commute h) + /- some useful immediate properties -/ + + definition short_exact_mod_infpage0 (bound_zero : B' (deg (k X) x) = 0) : + short_exact_mod (Einfdiag 0) (D X (deg (k X) x)) (Dinfdiag 1) := + begin + refine short_exact_mod_isomorphism _ _ _ (short_exact_mod_infpage 0), + { reflexivity }, + { exact (Dinfdiag0 bound_zero)⁻¹ˡᵐ }, + { reflexivity } + end + end end convergence_theorem diff --git a/cohomology/basic.hlean b/cohomology/basic.hlean index 4c88433..1c4a2da 100644 --- a/cohomology/basic.hlean +++ b/cohomology/basic.hlean @@ -9,13 +9,15 @@ Reduced cohomology of spectra and cohomology theories import ..spectrum.basic ..algebra.arrow_group ..homotopy.fwedge ..choice ..homotopy.pushout ..algebra.product_group 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 unit pi + function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit pi is_conn namespace cohomology /- The cohomology of X with coefficients in Y is trunc 0 (A →* Ω[2] (Y (n+2))) In the file arrow_group (in algebra) we construct the group structure on this type. + Equivalently, it's + πₛ[n] (sp_cotensor X Y) -/ definition cohomology (X : Type*) (Y : spectrum) (n : ℤ) : AbGroup := AbGroup_trunc_pmap X (Y (n+2)) @@ -60,16 +62,7 @@ notation `opH^` n `[`:0 binders `, ` r:(scoped G, ordinary_parametrized_cohomolo notation `upH^` n `[`:0 binders `, ` r:(scoped Y, unreduced_parametrized_cohomology Y n) `]`:0 := r notation `uopH^` n `[`:0 binders `, ` r:(scoped G, unreduced_ordinary_parametrized_cohomology G n) `]`:0 := r --- check H^3[S¹*,EM_spectrum agℤ] --- check H^3[S¹*] --- check pH^3[(x : S¹*), EM_spectrum agℤ] - /- an alternate definition of cohomology -/ -definition cohomology_equiv_shomotopy_group_sp_cotensor (X : Type*) (Y : spectrum) (n : ℤ) : - H^n[X, Y] ≃ πₛ[-n] (sp_cotensor X Y) := -trunc_equiv_trunc 0 (!pfunext ⬝e loop_pequiv_loop !pfunext ⬝e loopn_pequiv_loopn 2 - (pequiv_of_eq (ap (λn, ppmap X (Y n)) (add.comm n 2 ⬝ ap (add 2) !neg_neg⁻¹)))) - definition parametrized_cohomology_isomorphism_shomotopy_group_spi {X : Type*} (Y : X → spectrum) {n m : ℤ} (p : -m = n) : pH^n[(x : X), Y x] ≃g πₛ[m] (spi X Y) := begin @@ -145,6 +138,14 @@ cohomology_isomorphism_shomotopy_group_sp_cotensor X Y !neg_neg ⬝g shomotopy_group_isomorphism_of_pequiv (-n) (λk, pequiv_ppcompose_left (e k)) ⬝g (cohomology_isomorphism_shomotopy_group_sp_cotensor X Y' !neg_neg)⁻¹ᵍ +definition unreduced_cohomology_isomorphism {X X' : Type} (f : X' ≃ X) (Y : spectrum) (n : ℤ) : + uH^n[X, Y] ≃g uH^n[X', Y] := +cohomology_isomorphism (add_point_pequiv f) Y n + +definition unreduced_cohomology_isomorphism_right (X : Type) {Y Y' : spectrum} (e : Πn, Y n ≃* Y' n) + (n : ℤ) : uH^n[X, Y] ≃g uH^n[X, Y'] := +cohomology_isomorphism_right X₊ e n + definition parametrized_cohomology_isomorphism_right {X : Type*} {Y Y' : X → spectrum} (e : Πx n, Y x n ≃* Y' x n) (n : ℤ) : pH^n[(x : X), Y x] ≃g pH^n[(x : X), Y' x] := parametrized_cohomology_isomorphism_shomotopy_group_spi Y !neg_neg ⬝g @@ -178,6 +179,28 @@ parametrized_cohomology_isomorphism_right end n +definition pH_isomorphism_H {X : Type*} (Y : spectrum) (n : ℤ) : pH^n[(x : X), Y] ≃g H^n[X, Y] := +by reflexivity + +definition opH_isomorphism_oH {X : Type*} (G : AbGroup) (n : ℤ) : opH^n[(x : X), G] ≃g oH^n[X, G] := +by reflexivity + +definition upH_isomorphism_uH {X : Type} (Y : spectrum) (n : ℤ) : upH^n[(x : X), Y] ≃g uH^n[X, Y] := +unreduced_parametrized_cohomology_isomorphism_shomotopy_group_supi _ !neg_neg ⬝g +(unreduced_cohomology_isomorphism_shomotopy_group_sp_ucotensor _ _ !neg_neg)⁻¹ᵍ + +definition uopH_isomorphism_uoH {X : Type} (G : AbGroup) (n : ℤ) : + uopH^n[(x : X), G] ≃g uoH^n[X, G] := +!upH_isomorphism_uH + +definition uopH_isomorphism_uoH_of_is_conn {X : Type*} (G : X → AbGroup) (n : ℤ) (H : is_conn 1 X) : + uopH^n[(x : X), G x] ≃g uoH^n[X, G pt] := +begin + refine _ ⬝g !uopH_isomorphism_uoH, + apply unreduced_ordinary_parametrized_cohomology_isomorphism_right, + refine is_conn.elim 0 _ _, reflexivity +end + /- suspension axiom -/ definition cohomology_susp_2 (Y : spectrum) (n : ℤ) : diff --git a/cohomology/serre.hlean b/cohomology/serre.hlean index 035d1d3..4ec0db2 100644 --- a/cohomology/serre.hlean +++ b/cohomology/serre.hlean @@ -208,7 +208,9 @@ converges_to_g_isomorphism end unreduced_atiyah_hirzebruch section serre - variables {X : Type} (F : X → Type) (Y : spectrum) (s₀ : ℤ) (H : is_strunc s₀ Y) + universe variable u + variables {X : Type} (x₀ : X) (F : X → Type) {X₁ X₂ : pType.{u}} (f : X₁ →* X₂) + (Y : spectrum) (s₀ : ℤ) (H : is_strunc s₀ Y) include H definition serre_convergence : @@ -231,7 +233,25 @@ section serre apply shomotopy_group_isomorphism_of_pequiv, intro k, exact (sigma_pumap F (Y k))⁻¹ᵉ* end - qed + qed + + definition serre_convergence_of_is_conn (H2 : is_conn 1 X) : + (λn s, uoH^-(n-s)[X, uH^-s[F x₀, Y]]) ⟹ᵍ (λn, uH^-n[Σ(x : X), F x, Y]) := + proof + converges_to_g_isomorphism + (serre_convergence F Y s₀ H) + begin intro n s, exact @uopH_isomorphism_uoH_of_is_conn (pointed.MK X x₀) _ _ H2 end + begin intro n, reflexivity end + qed + + definition serre_convergence_of_pmap (H2 : is_conn 1 X₂) : + (λn s, uoH^-(n-s)[X₂, uH^-s[pfiber f, Y]]) ⟹ᵍ (λn, uH^-n[X₁, Y]) := + proof + converges_to_g_isomorphism + (serre_convergence_of_is_conn pt (λx, fiber f x) Y s₀ H H2) + begin intro n s, reflexivity end + begin intro n, apply unreduced_cohomology_isomorphism, exact !sigma_fiber_equiv⁻¹ᵉ end + qed end serre diff --git a/pointed.hlean b/pointed.hlean index 554e2c3..807e2d3 100644 --- a/pointed.hlean +++ b/pointed.hlean @@ -215,6 +215,43 @@ namespace pointed definition loop_punit : Ω punit ≃* punit := loop_pequiv_punit_of_is_set punit + definition add_point_functor' [unfold 4] {A B : Type} (e : A → B) (a : A₊) : B₊ := + begin induction a with a, exact none, exact some (e a) end + + definition add_point_functor [constructor] {A B : Type} (e : A → B) : A₊ →* B₊ := + pmap.mk (add_point_functor' e) idp + + definition add_point_functor_compose {A B C : Type} (f : B → C) (e : A → B) : + add_point_functor (f ∘ e) ~* add_point_functor f ∘* add_point_functor e := + begin + fapply phomotopy.mk, + { intro x, induction x: reflexivity }, + reflexivity + end + + definition add_point_functor_id (A : Type) : + add_point_functor id ~* pid A₊ := + begin + fapply phomotopy.mk, + { intro x, induction x: reflexivity }, + reflexivity + end + + definition add_point_functor_phomotopy {A B : Type} {e e' : A → B} (p : e ~ e') : + add_point_functor e ~* add_point_functor e' := + begin + fapply phomotopy.mk, + { intro x, induction x with a, reflexivity, exact ap some (p a) }, + reflexivity + end + + definition add_point_pequiv {A B : Type} (e : A ≃ B) : A₊ ≃* B₊ := + pequiv.MK (add_point_functor e) (add_point_functor e⁻¹ᵉ) + abstract !add_point_functor_compose⁻¹* ⬝* add_point_functor_phomotopy (left_inv e) ⬝* + !add_point_functor_id end + abstract !add_point_functor_compose⁻¹* ⬝* add_point_functor_phomotopy (right_inv e) ⬝* + !add_point_functor_id end + definition add_point_over [unfold 3] {A : Type} (B : A → Type*) : A₊ → Type* | (some a) := B a | none := plift punit