From 32512bf47db3a1b932856e7ed7c7830b1fc07ef0 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 3 Oct 2018 19:39:08 -0400 Subject: [PATCH] compute unreduced cohomology of spheres --- algebra/arrow_group.hlean | 40 ++++++++++- algebra/exact_couple.hlean | 40 +++++------ algebra/product_group.hlean | 24 ++++++- algebra/spectral_sequence.hlean | 22 +++--- cohomology/basic.hlean | 124 ++++++++++++++++++++++++++++---- homotopy/susp.hlean | 5 ++ 6 files changed, 209 insertions(+), 46 deletions(-) diff --git a/algebra/arrow_group.hlean b/algebra/arrow_group.hlean index 539c227..ed58224 100644 --- a/algebra/arrow_group.hlean +++ b/algebra/arrow_group.hlean @@ -8,7 +8,7 @@ on trunc 0 (A →* Ω B) and the dependent version trunc 0 (ppi _ _), which are used in the definition of cohomology. -/ -import algebra.group_theory ..pointed ..pointed_pi eq2 +import algebra.group_theory ..pointed ..pointed_pi eq2 .product_group open pi pointed algebra group eq equiv is_trunc trunc susp nat function namespace group @@ -317,4 +317,42 @@ namespace group { intro g h, apply eq_of_homotopy, intro a, exact respect_mul (f a) g h } end + definition Group_pi_eval [constructor] {A : Type} (P : A → Group) (a : A) + : (Πᵍ a, P a) →g P a := + begin + fconstructor, + { intro h, exact h a }, + { intro g h, reflexivity } + end + + definition Group_pi_functor [constructor] {A B : Type} {P : A → Group} {Q : B → Group} + (f : B → A) (g : Πb, P (f b) →g Q b) : (Πᵍ a, P a) →g Πᵍ b, Q b := + Group_pi_intro (λb, g b ∘g Group_pi_eval P (f b)) + + definition Group_pi_functor_compose [constructor] {A B C : Type} {P : A → Group} {Q : B → Group} + {R : C → Group} (f : B → A) (f' : C → B) (g' : Πc, Q (f' c) →g R c) (g : Πb, P (f b) →g Q b) : + Group_pi_functor (f ∘ f') (λc, g' c ∘g g (f' c)) ~ + Group_pi_functor f' g' ∘ Group_pi_functor f g := + begin + intro h, reflexivity + end + + open bool prod is_equiv + definition Group_pi_isomorphism_Group_pi [constructor] {A B : Type} + {P : A → Group} {Q : B → Group} (f : B ≃ A) (g : Πb, P (f b) ≃g Q b) : + (Πᵍ a, P a) ≃g Πᵍ b, Q b := + isomorphism.mk (Group_pi_functor f g) (is_equiv_pi_functor f g) + + definition product_isomorphism_Group_pi [constructor] (G H : Group) : + G ×g H ≃g Group_pi (bool.rec G H) := + begin + fconstructor, + { exact Group_pi_intro (bool.rec (product_pr1 G H) (product_pr2 G H)) }, + { apply adjointify _ (λh, (h ff, h tt)), + { intro h, apply eq_of_homotopy, intro b, induction b: reflexivity }, + { intro gh, induction gh, reflexivity }} + end + + + end group diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean index 1d4321c..2cfdfad 100644 --- a/algebra/exact_couple.hlean +++ b/algebra/exact_couple.hlean @@ -538,33 +538,33 @@ namespace exact_couple local attribute [coercion] AddAbGroup_of_Ring definition Z2 [constructor] : AddAbGroup := rℤ ×aa rℤ - structure convergent_exact_couple.{u v w} {R : Ring} (E' : agℤ → agℤ → LeftModule.{u v} R) - (Dinf : agℤ → LeftModule.{u w} R) : Type.{max u (v+1) (w+1)} := + structure convergent_exact_couple.{u v w} {R : Ring} (E' : ℤ → ℤ → LeftModule.{u v} R) + (Dinf : ℤ → LeftModule.{u w} R) : Type.{max u (v+1) (w+1)} := (X : exact_couple.{u 0 w v} R Z2) (HH : is_bounded X) - (st : agℤ → Z2) - (HB : Π(n : agℤ), is_bounded.B' HH (deg (k X) (st n)) = 0) + (st : ℤ → Z2) + (HB : Π(n : ℤ), is_bounded.B' HH (deg (k X) (st n)) = 0) (e : Π(x : Z2), exact_couple.E X x ≃lm E' x.1 x.2) - (f : Π(n : agℤ), exact_couple.D X (deg (k X) (st n)) ≃lm Dinf n) + (f : Π(n : ℤ), exact_couple.D X (deg (k X) (st n)) ≃lm Dinf n) (deg_d : ℕ → Z2) (deg_d_eq0 : Π(r : ℕ), deg (d (page X r)) 0 = deg_d r) infix ` ⟹ `:25 := convergent_exact_couple -- todo: maybe this should define convergent_spectral_sequence - definition convergent_exact_couple_g [reducible] (E' : agℤ → agℤ → AbGroup) (Dinf : agℤ → AbGroup) : Type := + definition convergent_exact_couple_g [reducible] (E' : ℤ → ℤ → AbGroup) (Dinf : ℤ → AbGroup) : Type := (λn s, LeftModule_int_of_AbGroup (E' n s)) ⟹ (λn, LeftModule_int_of_AbGroup (Dinf n)) infix ` ⟹ᵍ `:25 := convergent_exact_couple_g section exact_couple open convergent_exact_couple - parameters {R : Ring} {E' : agℤ → agℤ → LeftModule R} {Dinf : agℤ → LeftModule R} (c : E' ⟹ Dinf) + parameters {R : Ring} {E' : ℤ → ℤ → LeftModule R} {Dinf : ℤ → LeftModule R} (c : E' ⟹ Dinf) local abbreviation X := X c local abbreviation i := i X local abbreviation HH := HH c local abbreviation st := st c - local abbreviation Dinfdiag (n : agℤ) (k : ℕ) := Dinfdiag HH (st n) k - local abbreviation Einfdiag (n : agℤ) (k : ℕ) := Einfdiag HH (st n) k + local abbreviation Dinfdiag (n : ℤ) (k : ℕ) := Dinfdiag HH (st n) k + local abbreviation Einfdiag (n : ℤ) (k : ℕ) := Einfdiag HH (st n) k definition deg_d_eq (r : ℕ) (ns : Z2) : (deg (d (page X r))) ns = ns + deg_d c r := !deg_eq ⬝ ap (λx, _ + x) (deg_d_eq0 c r) @@ -573,7 +573,7 @@ namespace exact_couple (deg (d (page X r)))⁻¹ᵉ ns = ns - deg_d c r := inv_eq_of_eq (!deg_d_eq ⬝ proof !neg_add_cancel_right qed)⁻¹ - definition convergent_exact_couple_isomorphism {E'' : agℤ → agℤ → LeftModule R} {Dinf' : graded_module R agℤ} + definition convergent_exact_couple_isomorphism {E'' : ℤ → ℤ → LeftModule R} {Dinf' : graded_module R ℤ} (e' : Πn s, E' n s ≃lm E'' n s) (f' : Πn, Dinf n ≃lm Dinf' n) : E'' ⟹ Dinf' := convergent_exact_couple.mk X HH st (HB c) begin intro x, induction x with n s, exact e c (n, s) ⬝lm e' n s end @@ -606,8 +606,8 @@ namespace exact_couple is_built_from (Dinf n) (Einfdiag n) := is_built_from_isomorphism_left (f c n) (is_built_from_infpage HH (st n) (HB c n)) - theorem is_contr_convergent_exact_couple_precise (n : agℤ) - (H : Π(n : agℤ) (l : ℕ), is_contr (E' ((deg i)^[l] (st n)).1 ((deg i)^[l] (st n)).2)) : + theorem is_contr_convergent_exact_couple_precise (n : ℤ) + (H : Π(n : ℤ) (l : ℕ), is_contr (E' ((deg i)^[l] (st n)).1 ((deg i)^[l] (st n)).2)) : is_contr (Dinf n) := begin assert H2 : Π(l : ℕ), is_contr (Einfdiag n l), @@ -616,11 +616,11 @@ namespace exact_couple exact is_contr_total (is_built_from_of_convergent_exact_couple n) H2 end - theorem is_contr_convergent_exact_couple (n : agℤ) (H : Π(n s : agℤ), is_contr (E' n s)) : + theorem is_contr_convergent_exact_couple (n : ℤ) (H : Π(n s : ℤ), is_contr (E' n s)) : is_contr (Dinf n) := is_contr_convergent_exact_couple_precise n (λn s, !H) - -- definition E_isomorphism {r₁ r₂ : ℕ} {n s : agℤ} (H : r₁ ≤ r₂) + -- definition E_isomorphism {r₁ r₂ : ℕ} {n s : ℤ} (H : r₁ ≤ r₂) -- (H1 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X ((n, s) - deg_d c r))) -- (H2 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X ((n, s) + deg_d c r))) : -- E (page X r₂) (n, s) ≃lm E (page X r₁) (n, s) := @@ -628,18 +628,18 @@ namespace exact_couple -- (λr Hr₁ Hr₂, transport (is_contr ∘ E X) (deg_d_inv_eq r (n, s))⁻¹ᵖ (H1 Hr₁ Hr₂)) -- (λr Hr₁ Hr₂, transport (is_contr ∘ E X) (deg_d_eq r (n, s))⁻¹ᵖ (H2 Hr₁ Hr₂)) - -- definition E_isomorphism0 {r : ℕ} {n s : agℤ} (H1 : Πr, is_contr (E X ((n, s) - deg_d c r))) + -- definition E_isomorphism0 {r : ℕ} {n s : ℤ} (H1 : Πr, is_contr (E X ((n, s) - deg_d c r))) -- (H2 : Πr, is_contr (E X ((n, s) + deg_d c r))) : E (page X r) (n, s) ≃lm E' n s := -- E_isomorphism (zero_le r) _ _ ⬝lm e c (n, s) - -- definition Einf_isomorphism (r₁ : ℕ) {n s : agℤ} + -- definition Einf_isomorphism (r₁ : ℕ) {n s : ℤ} -- (H1 : Π⦃r⦄, r₁ ≤ r → is_contr (E X ((n,s) - deg_d c r))) -- (H2 : Π⦃r⦄, r₁ ≤ r → is_contr (E X ((n,s) + deg_d c r))) : -- Einf HH (n, s) ≃lm E (page X r₁) (n, s) := -- Einf_isomorphism' HH r₁ (λr Hr₁, transport (is_contr ∘ E X) (deg_d_inv_eq r (n, s))⁻¹ᵖ (H1 Hr₁)) -- (λr Hr₁, transport (is_contr ∘ E X) (deg_d_eq r (n, s))⁻¹ᵖ (H2 Hr₁)) - -- definition Einf_isomorphism0 {n s : agℤ} + -- definition Einf_isomorphism0 {n s : ℤ} -- (H1 : Π⦃r⦄, is_contr (E X ((n,s) - deg_d c r))) -- (H2 : Π⦃r⦄, is_contr (E X ((n,s) + deg_d c r))) : -- Einf HH (n, s) ≃lm E' n s := @@ -647,9 +647,9 @@ namespace exact_couple end exact_couple - variables {E' : agℤ → agℤ → AbGroup} {Dinf : agℤ → AbGroup} - definition convergent_exact_couple_g_isomorphism {E'' : agℤ → agℤ → AbGroup} - {Dinf' : agℤ → AbGroup} (c : E' ⟹ᵍ Dinf) + variables {E' : ℤ → ℤ → AbGroup} {Dinf : ℤ → AbGroup} + definition convergent_exact_couple_g_isomorphism {E'' : ℤ → ℤ → AbGroup} + {Dinf' : ℤ → AbGroup} (c : E' ⟹ᵍ Dinf) (e' : Πn s, E' n s ≃g E'' n s) (f' : Πn, Dinf n ≃g Dinf' n) : E'' ⟹ᵍ Dinf' := convergent_exact_couple_isomorphism c (λn s, lm_iso_int.mk (e' n s)) (λn, lm_iso_int.mk (f' n)) diff --git a/algebra/product_group.hlean b/algebra/product_group.hlean index ad61754..b95d860 100644 --- a/algebra/product_group.hlean +++ b/algebra/product_group.hlean @@ -9,7 +9,7 @@ Constructions with groups import algebra.group_theory hit.set_quotient types.list types.sum .subgroup .quotient_group open eq algebra is_trunc set_quotient relation sigma prod prod.ops sum list trunc function - equiv + equiv is_equiv namespace group variables {G G' : Group} {g g' h h' k : G} @@ -98,4 +98,26 @@ namespace group definition product_group_mul_eq {G H : Group} (g h : G ×g H) : g * h = product_mul g h := idp + definition product_pr1 [constructor] (G H : Group) : G ×g H →g G := + homomorphism.mk (λx, x.1) (λx y, idp) + + definition product_pr2 [constructor] (G H : Group) : G ×g H →g H := + homomorphism.mk (λx, x.2) (λx y, idp) + + definition product_trivial_right [constructor] (G H : Group) (HH : is_contr H) : G ×g H ≃g G := + begin + apply isomorphism.mk (product_pr1 G H), + apply adjointify _ (product_inl G H), + { intro g, reflexivity }, + { intro gh, exact prod_eq idp !is_prop.elim } + end + + definition product_trivial_left [constructor] (G H : Group) (HH : is_contr G) : G ×g H ≃g H := + begin + apply isomorphism.mk (product_pr2 G H), + apply adjointify _ (product_inr G H), + { intro g, reflexivity }, + { intro gh, exact prod_eq !is_prop.elim idp } + end + end group diff --git a/algebra/spectral_sequence.hlean b/algebra/spectral_sequence.hlean index cc0dda3..eb235fb 100644 --- a/algebra/spectral_sequence.hlean +++ b/algebra/spectral_sequence.hlean @@ -11,8 +11,8 @@ open algebra is_trunc left_module is_equiv equiv eq function nat sigma set_quoti left_module group int prod prod.ops open exact_couple (Z2) -structure convergent_spectral_sequence.{u v w} {R : Ring} (E' : agℤ → agℤ → LeftModule.{u v} R) - (Dinf : agℤ → LeftModule.{u w} R) : Type.{max u (v+1) (w+1)} := +structure convergent_spectral_sequence.{u v w} {R : Ring} (E' : ℤ → ℤ → LeftModule.{u v} R) + (Dinf : ℤ → LeftModule.{u w} R) : Type.{max u (v+1) (w+1)} := (E : ℕ → graded_module.{u 0 v} R Z2) (d : Π(r : ℕ), E r →gm E r) (deg_d : ℕ → Z2) @@ -22,11 +22,11 @@ structure convergent_spectral_sequence.{u v w} {R : Ring} (E' : agℤ → agℤ (s₀ : Z2 → ℕ) (f : Π{r : ℕ} {x : Z2} (h : s₀ x ≤ r), E (s₀ x) x ≃lm E r x) (lb : ℤ → ℤ) - (HDinf : Π(n : agℤ), is_built_from (Dinf n) + (HDinf : Π(n : ℤ), is_built_from (Dinf n) (λ(k : ℕ), (λx, E (s₀ x) x) (n - (k + lb n), k + lb n))) -definition convergent_spectral_sequence_g [reducible] (E' : agℤ → agℤ → AbGroup) - (Dinf : agℤ → AbGroup) : Type := +definition convergent_spectral_sequence_g [reducible] (E' : ℤ → ℤ → AbGroup) + (Dinf : ℤ → AbGroup) : Type := convergent_spectral_sequence (λn s, LeftModule_int_of_AbGroup (E' n s)) (λn, LeftModule_int_of_AbGroup (Dinf n)) @@ -34,8 +34,8 @@ convergent_spectral_sequence (λn s, LeftModule_int_of_AbGroup (E' n s)) open exact_couple exact_couple.exact_couple exact_couple.convergent_exact_couple exact_couple.convergence_theorem exact_couple.derived_couple - definition convergent_spectral_sequence_of_exact_couple {R : Ring} {E' : agℤ → agℤ → LeftModule R} - {Dinf : agℤ → LeftModule R} (c : convergent_exact_couple E' Dinf) + definition convergent_spectral_sequence_of_exact_couple {R : Ring} {E' : ℤ → ℤ → LeftModule R} + {Dinf : ℤ → LeftModule R} (c : convergent_exact_couple E' Dinf) (st_eq : Πn, (st c n).1 + (st c n).2 = n) (deg_i_eq : deg (i (X c)) 0 = (- 1, 1)) : convergent_spectral_sequence E' Dinf := convergent_spectral_sequence.mk (λr, E (page (X c) r)) (λr, d (page (X c) r)) @@ -60,7 +60,7 @@ convergent_spectral_sequence (λn s, LeftModule_int_of_AbGroup (E' n s)) namespace spectral_sequence open convergent_spectral_sequence - variables {R : Ring} {E' : agℤ → agℤ → LeftModule R} {Dinf : agℤ → LeftModule R} + variables {R : Ring} {E' : ℤ → ℤ → LeftModule R} {Dinf : ℤ → LeftModule R} (c : convergent_spectral_sequence E' Dinf) -- (E : ℕ → graded_module.{u 0 v} R Z2) @@ -72,7 +72,7 @@ namespace spectral_sequence -- (s₀ : Z2 → ℕ) -- (f : Π{r : ℕ} {x : Z2} (h : s₀ x ≤ r), E (s₀ x) x ≃lm E r x) -- (lb : ℤ → ℤ) - -- (HDinf : Π(n : agℤ), is_built_from (Dinf n) + -- (HDinf : Π(n : ℤ), is_built_from (Dinf n) -- (λ(k : ℕ), (λx, E (s₀ x) x) (n - (k + lb n), k + lb n))) definition Einf (x : Z2) : LeftModule R := E c (s₀ c x) x @@ -115,7 +115,7 @@ namespace spectral_sequence exact H3 H (le.refl _) end - definition E_isomorphism0 {r : ℕ} {n s : agℤ} + definition E_isomorphism0 {r : ℕ} {n s : ℤ} (H1 : Πr', r' < r → is_contr (E' (n - (deg_d c r').1) (s - (deg_d c r').2))) (H2 : Πr', r' < r → is_contr (E' (n + (deg_d c r').1) (s + (deg_d c r').2))) : E c r (n, s) ≃lm E' n s := @@ -133,7 +133,7 @@ namespace spectral_sequence exact f c Hr end - definition Einf_isomorphism0 {n s : agℤ} + definition Einf_isomorphism0 {n s : ℤ} (H1 : Πr, is_contr (E' (n - (deg_d c r).1) (s - (deg_d c r).2))) (H2 : Πr, is_contr (E' (n + (deg_d c r).1) (s + (deg_d c r).2))) : Einf c (n, s) ≃lm E' n s := diff --git a/cohomology/basic.hlean b/cohomology/basic.hlean index fbad479..5ce09d2 100644 --- a/cohomology/basic.hlean +++ b/cohomology/basic.hlean @@ -6,7 +6,8 @@ Authors: Floris van Doorn, Ulrik Buchholtz Reduced cohomology of spectra and cohomology theories -/ -import ..spectrum.basic ..algebra.arrow_group ..homotopy.fwedge ..choice ..homotopy.pushout ..algebra.product_group +import ..spectrum.basic ..algebra.arrow_group ..algebra.product_group ..choice + ..homotopy.fwedge ..homotopy.pushout ..homotopy.EM ..homotopy.wedge 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 is_conn @@ -103,6 +104,8 @@ definition cohomology_functor [constructor] {X X' : Type*} (f : X' →* X) (Y : (n : ℤ) : cohomology X Y n →g cohomology X' Y n := Group_trunc_pmap_homomorphism f +notation `H^→` n `[`:0 f:0 `, ` Y:0 `]`:0 := cohomology_functor f Y n + definition cohomology_functor_pid (X : Type*) (Y : spectrum) (n : ℤ) (f : H^n[X, Y]) : cohomology_functor (pid X) Y n f = f := !Group_trunc_pmap_pid @@ -116,6 +119,8 @@ definition cohomology_functor_phomotopy {X X' : Type*} {f g : X' →* X} (p : f (Y : spectrum) (n : ℤ) : cohomology_functor f Y n ~ cohomology_functor g Y n := Group_trunc_pmap_phomotopy p +notation `H^~` n `[`:0 h:0 `, ` Y:0 `]`:0 := cohomology_functor_phomotopy h Y n + definition cohomology_functor_phomotopy_refl {X X' : Type*} (f : X' →* X) (Y : spectrum) (n : ℤ) (x : H^n[X, Y]) : cohomology_functor_phomotopy (phomotopy.refl f) Y n x = idp := Group_trunc_pmap_phomotopy_refl f x @@ -128,8 +133,10 @@ definition cohomology_isomorphism {X X' : Type*} (f : X' ≃* X) (Y : spectrum) H^n[X, Y] ≃g H^n[X', Y] := Group_trunc_pmap_isomorphism f +notation `H^≃` n `[`:0 e:0 `, ` Y:0 `]`:0 := cohomology_isomorphism e Y n + definition cohomology_isomorphism_refl (X : Type*) (Y : spectrum) (n : ℤ) (x : H^n[X,Y]) : - cohomology_isomorphism (pequiv.refl X) Y n x = x := + H^≃n[pequiv.refl X, Y] x = x := !Group_trunc_pmap_isomorphism_refl definition cohomology_isomorphism_right (X : Type*) {Y Y' : spectrum} (e : Πn, Y n ≃* Y' n) @@ -284,9 +291,13 @@ definition spectrum_additive {I : Type} (H : has_choice 0 I) (X : I → Type*) ( (n : ℤ) : is_equiv (additive_hom X Y n) := is_equiv_of_equiv_of_homotopy (additive_equiv H X Y n) begin intro f, induction f, reflexivity end +definition cohomology_fwedge.{u} {I : Type.{u}} (H : has_choice 0 I) (X : I → Type*) (Y : spectrum) + (n : ℤ) : H^n[⋁X, Y] ≃g Πᵍ i, H^n[X i, Y] := +isomorphism.mk (additive_hom X Y n) (spectrum_additive H X Y n) + /- dimension axiom for ordinary cohomology -/ open is_conn trunc_index -theorem EM_dimension' (G : AbGroup) (n : ℤ) (H : n ≠ 0) : +theorem ordinary_cohomology_dimension (G : AbGroup) (n : ℤ) (H : n ≠ 0) : is_contr (oH^n[pbool, G]) := begin apply is_conn_equiv_closed 0 !pmap_pbool_equiv⁻¹ᵉ, @@ -299,19 +310,104 @@ begin apply is_trunc_of_le _ (zero_le_of_nat n) _ } end -theorem EM_dimension (G : AbGroup) (n : ℤ) (H : n ≠ 0) : - is_contr (ordinary_cohomology (plift pbool) G n) := +theorem ordinary_cohomology_dimension_plift (G : AbGroup) (n : ℤ) (H : n ≠ 0) : + is_contr (oH^n[plift pbool, G]) := is_trunc_equiv_closed_rev -2 (equiv_of_isomorphism (cohomology_isomorphism (pequiv_plift pbool) _ _)) - (EM_dimension' G n H) + (ordinary_cohomology_dimension G n H) -open group algebra -theorem ordinary_cohomology_pbool (G : AbGroup) : oH^0[pbool, G] ≃g G := -sorry ---isomorphism_of_equiv (trunc_equiv_trunc 0 (ppmap_pbool_pequiv _ ⬝e _) ⬝e !trunc_equiv) sorry +definition cohomology_iterate_susp (X : Type*) (Y : spectrum) (n : ℤ) (k : ℕ) : + H^n+k[iterate_susp k X, Y] ≃g H^n[X, Y] := +begin + induction k with k IH, + { exact cohomology_change_int X Y !add_zero }, + { exact cohomology_change_int _ _ !add.assoc⁻¹ ⬝g cohomology_susp _ _ _ ⬝g IH } +end -theorem is_contr_cohomology_of_is_contr_spectrum (n : ℤ) (X : Type*) (Y : spectrum) (H : is_contr (Y n)) : - is_contr (H^n[X, Y]) := +definition ordinary_cohomology_pbool (G : AbGroup) : oH^0[pbool, G] ≃g G := +begin + refine cohomology_isomorphism_shomotopy_group_sp_cotensor _ _ !neg_neg ⬝g _, + change πg[2] (pbool →** EM G 2) ≃g G, + refine homotopy_group_isomorphism_of_pequiv 1 !ppmap_pbool_pequiv ⬝g ghomotopy_group_EM G 1 +end + +definition ordinary_cohomology_sphere (G : AbGroup) (n : ℕ) : oH^n[sphere n, G] ≃g G := +begin + refine cohomology_isomorphism_shomotopy_group_sp_cotensor _ _ !neg_neg ⬝g _, + change πg[2] (sphere n →** EM_spectrum G (2 - -n)) ≃g G, + refine homotopy_group_isomorphism_of_pequiv 1 _ ⬝g ghomotopy_group_EMadd1 G 1, + have p : 2 - (-n) = succ (1 + n), + from !sub_eq_add_neg ⬝ ap (add 2) !neg_neg ⬝ ap of_nat !succ_add, + refine !sphere_pmap_pequiv ⬝e* Ω≃[n] (pequiv_ap (EM_spectrum G) p) ⬝e* loopn_EMadd1_add G n 1, +end + +definition ordinary_cohomology_sphere_of_neq (G : AbGroup) {n : ℤ} {k : ℕ} (p : n ≠ k) : + is_contr (oH^n[sphere k, G]) := +begin + refine is_contr_equiv_closed_rev _ + (ordinary_cohomology_dimension G (n-k) (λh, p (eq_of_sub_eq_zero h))), + apply equiv_of_isomorphism, + exact cohomology_change_int _ _ !neg_add_cancel_right⁻¹ ⬝g + cohomology_iterate_susp pbool (EM_spectrum G) (n - k) k +end + +definition cohomology_punit (Y : spectrum) (n : ℤ) : + is_contr (H^n[punit, Y]) := +@is_trunc_trunc_of_is_trunc _ _ _ !is_contr_punit_pmap + +definition cohomology_wedge (X X' : Type*) (Y : spectrum) (n : ℤ) : + H^n[wedge X X', Y] ≃g H^n[X, Y] ×ag H^n[X', Y] := +H^≃n[(wedge_pequiv_fwedge X X')⁻¹ᵉ*, Y] ⬝g +cohomology_fwedge (has_choice_pbool 0) _ _ _ ⬝g +Group_pi_isomorphism_Group_pi erfl begin intro b, induction b: reflexivity end ⬝g +(product_isomorphism_Group_pi H^n[X, Y] H^n[X', Y])⁻¹ᵍ ⬝g +proof !isomorphism.refl qed + +definition cohomology_isomorphism_of_equiv {X X' : Type*} (e : X ≃ X') (Y : spectrum) (n : ℤ) : + H^n[X', Y] ≃g H^n[X, Y] := +!cohomology_susp⁻¹ᵍ ⬝g H^≃n+1[susp_pequiv_of_equiv e, Y] ⬝g !cohomology_susp + +definition unreduced_cohomology_split (X : Type*) (Y : spectrum) (n : ℤ) : + uH^n[X, Y] ≃g H^n[X, Y] ×ag H^n[pbool, Y] := +cohomology_isomorphism_of_equiv (wedge.wedge_pbool_equiv_add_point X) Y n ⬝g +cohomology_wedge X pbool Y n + +definition unreduced_ordinary_cohomology_nonzero (X : Type*) (G : AbGroup) (n : ℤ) (H : n ≠ 0) : + uoH^n[X, G] ≃g oH^n[X, G] := +unreduced_cohomology_split X (EM_spectrum G) n ⬝g +product_trivial_right _ _ (ordinary_cohomology_dimension _ _ H) + +definition unreduced_ordinary_cohomology_zero (X : Type*) (G : AbGroup) : + uoH^0[X, G] ≃g oH^0[X, G] ×ag G := +unreduced_cohomology_split X (EM_spectrum G) 0 ⬝g +(!isomorphism.refl ×≃g ordinary_cohomology_pbool G) + +definition unreduced_ordinary_cohomology_pbool (G : AbGroup) : uoH^0[pbool, G] ≃g G ×ag G := +unreduced_ordinary_cohomology_zero pbool G ⬝g (ordinary_cohomology_pbool G ×≃g !isomorphism.refl) + +definition unreduced_ordinary_cohomology_pbool_nonzero (G : AbGroup) (n : ℤ) (H : n ≠ 0) : + is_contr (uoH^n[pbool, G]) := +is_contr_equiv_closed_rev (equiv_of_isomorphism (unreduced_ordinary_cohomology_nonzero pbool G n H)) + (ordinary_cohomology_dimension G n H) + +definition unreduced_ordinary_cohomology_sphere_zero (G : AbGroup) (n : ℕ) (H : n ≠ 0) : + uoH^0[sphere n, G] ≃g G := +unreduced_ordinary_cohomology_zero (sphere n) G ⬝g +product_trivial_left _ _ (ordinary_cohomology_sphere_of_neq _ (λh, H h⁻¹)) + +definition unreduced_ordinary_cohomology_sphere (G : AbGroup) (n : ℕ) (H : n ≠ 0) : + uoH^n[sphere n, G] ≃g G := +unreduced_ordinary_cohomology_nonzero (sphere n) G n H ⬝g +ordinary_cohomology_sphere G n + +definition unreduced_ordinary_cohomology_sphere_of_neq (G : AbGroup) {n : ℤ} {k : ℕ} (p : n ≠ k) + (q : n ≠ 0) : is_contr (uoH^n[sphere k, G]) := +is_contr_equiv_closed_rev + (equiv_of_isomorphism (unreduced_ordinary_cohomology_nonzero (sphere k) G n q)) + (ordinary_cohomology_sphere_of_neq G p) + +theorem is_contr_cohomology_of_is_contr_spectrum (n : ℤ) (X : Type*) (Y : spectrum) + (H : is_contr (Y n)) : is_contr (H^n[X, Y]) := begin apply is_trunc_trunc_of_is_trunc, apply is_trunc_pmap, @@ -339,6 +435,8 @@ begin apply is_contr_EM_spectrum_neg end + + /- cohomology theory -/ structure cohomology_theory.{u} : Type.{u+1} := @@ -441,6 +539,6 @@ cohomology_theory.mk -- print equiv_lift -- print has_choice_equiv_closed definition ordinary_cohomology_theory_EM [constructor] (G : AbGroup) : ordinary_cohomology_theory := -⦃ordinary_cohomology_theory, cohomology_theory_spectrum (EM_spectrum G), Hdimension := EM_dimension G ⦄ +⦃ordinary_cohomology_theory, cohomology_theory_spectrum (EM_spectrum G), Hdimension := ordinary_cohomology_dimension_plift G ⦄ end cohomology diff --git a/homotopy/susp.hlean b/homotopy/susp.hlean index c340107..51f992c 100644 --- a/homotopy/susp.hlean +++ b/homotopy/susp.hlean @@ -5,6 +5,11 @@ open susp eq pointed function is_equiv lift equiv is_trunc nat namespace susp variables {X X' Y Y' Z : Type*} + definition susp_functor_of_fn [constructor] (f : X → Y) : susp X →* susp Y := + pmap.mk (susp_functor' f) idp + definition susp_pequiv_of_equiv [constructor] (f : X ≃ Y) : susp X ≃* susp Y := + pequiv_of_equiv (susp.equiv f) idp + definition iterate_susp_iterate_susp_rev (n m : ℕ) (A : Type*) : iterate_susp n (iterate_susp m A) ≃* iterate_susp (m + n) A := begin