From b251465e72c82ce4645e04544d7c4aa8f5039b70 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 24 Oct 2018 21:19:26 -0400 Subject: [PATCH] continue on gysin sequence --- algebra/graded.hlean | 24 +++++++++++++++--- algebra/spectral_sequence.hlean | 18 ++++++++------ algebra/subgroup.hlean | 23 +++++++++++------ algebra/submodule.hlean | 42 ++++++++++++++++++++++++++----- cohomology/basic.hlean | 44 ++++++++++++++------------------- cohomology/gysin.hlean | 44 +++++++++++++++++++++++++++------ cohomology/serre.hlean | 23 ++++++++++++++++- move_to_lib.hlean | 25 +++++++++++++++++++ spectrum/trunc.hlean | 8 ++++++ 9 files changed, 193 insertions(+), 58 deletions(-) diff --git a/algebra/graded.hlean b/algebra/graded.hlean index 54b2532..2d222c1 100644 --- a/algebra/graded.hlean +++ b/algebra/graded.hlean @@ -17,9 +17,8 @@ variables {R : Ring} {I : AddGroup} {M M₁ M₂ M₃ : graded_module R I} /- morphisms between graded modules. The definition is unconventional in two ways: - (1) The degree is determined by an endofunction instead of a element of I (and in this case we - don't need to assume that I is a group). The "standard" degree i corresponds to the endofunction - which is addition with i on the right. However, this is more flexible. For example, the + (1) The degree is determined by an endofunction instead of a element of I, which is equal to adding + i on the right. This is more flexible. For example, the composition of two graded module homomorphisms φ₂ and φ₁ with degrees i₂ and i₁ has type M₁ i → M₂ ((i + i₁) + i₂). However, a homomorphism with degree i₁ + i₂ must have type @@ -32,7 +31,6 @@ variables {R : Ring} {I : AddGroup} {M M₁ M₂ M₃ : graded_module R I} but as a function taking a path as argument. Specifically, for every path deg f i = j we get a function M₁ i → M₂ j. - (3) Note: we do assume that I is a set. This is not strictly necessary, but it simplifies things -/ definition graded_hom_of_deg (d : I ≃ I) (M₁ M₂ : graded_module R I) : Type := @@ -158,11 +156,21 @@ begin refine cast_fn_cast_square fn _ _ !con.left_inv m end +definition graded_hom_square (f : M₁ →gm M₂) {i₁ i₂ j₁ j₂ : I} (p : deg f i₁ = j₁) (q : deg f i₂ = j₂) + (r : i₁ = i₂) (s : j₁ = j₂) : + hsquare (f ↘ p) (f ↘ q) (homomorphism_of_eq (ap M₁ r)) (homomorphism_of_eq (ap M₂ s)) := +begin + induction p, induction q, induction r, + have rfl = s, from !is_set.elim, induction this, + exact homotopy.rfl +end + variable (I) -- for some reason Lean needs to know what I is when applying this lemma definition graded_hom_eq_zero {f : M₁ →gm M₂} {i j k : I} {q : deg f i = j} {p : deg f i = k} (m : M₁ i) (r : f ↘ q m = 0) : f ↘ p m = 0 := have f ↘ p m = transport M₂ (q⁻¹ ⬝ p) (f ↘ q m), begin induction p, induction q, reflexivity end, this ⬝ ap (transport M₂ (q⁻¹ ⬝ p)) r ⬝ tr_eq_of_pathover (apd (λi, 0) (q⁻¹ ⬝ p)) + variable {I} definition graded_hom_change_image {f : M₁ →gm M₂} {i j k : I} {m : M₂ k} (p : deg f i = k) @@ -657,6 +665,14 @@ definition graded_homology_elim {g : M₂ →gm M₃} {f : M₁ →gm M₂} (h : (H : compose_constant h f) : graded_homology g f →gm M := graded_hom.mk (deg h) (deg_eq h) (λi, homology_elim (h i) (H _ _)) +definition graded_homology_isomorphism (g : M₂ →gm M₃) (f : M₁ →gm M₂) (x : I) : + graded_homology g f (deg f x) ≃lm homology (g (deg f x)) (f x) := +begin + refine homology_isomorphism_homology (isomorphism_of_eq (ap M₁ (left_inv (deg f) x))) + isomorphism.rfl isomorphism.rfl homotopy.rfl _, + exact graded_hom_square f (to_right_inv (deg f) (deg f x)) idp (to_left_inv (deg f) x) idp +end + definition image_of_graded_homology_intro_eq_zero {g : M₂ →gm M₃} {f : M₁ →gm M₂} ⦃i j : I⦄ (p : deg f i = j) (m : graded_kernel g j) (H : graded_homology_intro g f j m = 0) : image (f ↘ p) m.1 := diff --git a/algebra/spectral_sequence.hlean b/algebra/spectral_sequence.hlean index 4fb98cd..637487d 100644 --- a/algebra/spectral_sequence.hlean +++ b/algebra/spectral_sequence.hlean @@ -157,25 +157,29 @@ namespace spectral_sequence (normal3 : Π(r : ℕ), deg_d c r = (r+2, -(r+1))) open is_normal variable {c} - variable (d : is_normal c) - include d + variable (nc : is_normal c) + include nc definition stable_range {n s : ℤ} {r : ℕ} (H1 : n < r + 2) (H2 : s < r + 1) : Einf c (n, s) ≃lm E c r (n, s) := begin fapply Einf_isomorphism, - { intro r' Hr', apply is_contr_E, apply normal1 d, - refine lt_of_le_of_lt (le_of_eq (ap (λx, n - x.1) (normal3 d r'))) _, + { intro r' Hr', apply is_contr_E, apply normal1 nc, + refine lt_of_le_of_lt (le_of_eq (ap (λx, n - x.1) (normal3 nc r'))) _, apply sub_lt_left_of_lt_add, refine lt_of_lt_of_le H1 (le.trans _ (le_of_eq !add_zero⁻¹)), exact add_le_add_right (of_nat_le_of_nat_of_le Hr') 2 }, - { intro r' Hr', apply is_contr_E, apply normal2 d, - refine lt_of_le_of_lt (le_of_eq (ap (λx, s + x.2) (normal3 d r'))) _, + { intro r' Hr', apply is_contr_E, apply normal2 nc, + refine lt_of_le_of_lt (le_of_eq (ap (λx, s + x.2) (normal3 nc r'))) _, change s - (r' + 1) < 0, apply sub_lt_left_of_lt_add, refine lt_of_lt_of_le H2 (le.trans _ (le_of_eq !add_zero⁻¹)), exact add_le_add_right (of_nat_le_of_nat_of_le Hr') 1 }, end - omit d + + definition deg_d_normal_eq (r : ℕ) (x : Z2) : deg (d c r) x = x + (r+2, -(r+1)) := + deg_d_eq c r x ⬝ ap (add x) (is_normal.normal3 nc r) + + omit nc end spectral_sequence diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean index ad25140..fcb8c18 100644 --- a/algebra/subgroup.hlean +++ b/algebra/subgroup.hlean @@ -7,7 +7,7 @@ Basic concepts of group theory -/ import algebra.group_theory ..move_to_lib ..property -open eq algebra is_trunc sigma sigma.ops prod trunc property +open eq algebra is_trunc sigma sigma.ops prod trunc property is_equiv equiv namespace group @@ -456,12 +456,8 @@ end open function definition subgroup_functor_fun [unfold 7] (φ : G →g H) (h : Πg, g ∈ R → φ g ∈ S) - (x : subgroup R) : - subgroup S := - begin - induction x with g hg, - exact ⟨φ g, h g hg⟩ - end + (x : subgroup R) : subgroup S := + ⟨φ x.1, h x.1 x.2⟩ definition subgroup_functor [constructor] (φ : G →g H) (h : Πg, g ∈ R → φ g ∈ S) : subgroup R →g subgroup S := @@ -510,6 +506,19 @@ end exact subtype_eq (p g) end + definition subgroup_isomorphism_subgroup [constructor] (φ : G ≃g H) (hφ : Πg, g ∈ R ↔ φ g ∈ S) : + subgroup R ≃g subgroup S := + begin + apply isomorphism.mk (subgroup_functor φ (λg, iff.mp (hφ g))), + refine adjointify _ (subgroup_functor φ⁻¹ᵍ (λg gS, iff.mpr (hφ _) (transport S (right_inv φ g)⁻¹ gS))) _ _, + { refine subgroup_functor_compose _ _ _ _ ⬝hty + subgroup_functor_homotopy _ _ proof right_inv φ qed ⬝hty + subgroup_functor_gid }, + { refine subgroup_functor_compose _ _ _ _ ⬝hty + subgroup_functor_homotopy _ _ proof left_inv φ qed ⬝hty + subgroup_functor_gid } + end + definition subgroup_of_subgroup_incl {R S : property G} [is_subgroup G R] [is_subgroup G S] (H : Π (g : G), g ∈ R → g ∈ S) : subgroup R →g subgroup S := diff --git a/algebra/submodule.hlean b/algebra/submodule.hlean index 6fdd463..cec1193 100644 --- a/algebra/submodule.hlean +++ b/algebra/submodule.hlean @@ -7,7 +7,7 @@ open algebra eq group sigma sigma.ops is_trunc function trunc equiv is_equiv pro namespace left_module /- submodules -/ -variables {R : Ring} {M M₁ M₂ M₃ : LeftModule R} {m m₁ m₂ : M} +variables {R : Ring} {M M₁ M₁' M₂ M₂' M₃ M₃' : LeftModule R} {m m₁ m₂ : M} structure is_submodule [class] (M : LeftModule R) (S : property M) : Type := (zero_mem : 0 ∈ S) @@ -45,7 +45,7 @@ ab_subgroup_functor (smul_homomorphism M r) (λg, smul_mem S r) definition submodule_smul_right_distrib (r s : R) (n : submodule' S) : submodule_smul S (r + s) n = submodule_smul S r n + submodule_smul S s n := begin - refine subgroup_functor_homotopy _ _ _ n ⬝ !subgroup_functor_mul⁻¹, + refine subgroup_functor_homotopy _ _ _ n ⬝ !subgroup_functor_mul⁻¹ᵖ, intro m, exact to_smul_right_distrib r s m end @@ -135,6 +135,13 @@ definition submodule_isomorphism [constructor] (S : property M) [is_submodule M submodule S ≃lm M := isomorphism.mk (submodule_incl S) (is_equiv_incl_of_subgroup S h) +definition submodule_isomorphism_submodule [constructor] {S : property M₁} [is_submodule M₁ S] + {K : property M₂} [is_submodule M₂ K] + (φ : M₁ ≃lm M₂) (h : Π (m : M₁), m ∈ S ↔ φ m ∈ K) : submodule S ≃lm submodule K := +lm_isomorphism_of_group_isomorphism + (subgroup_isomorphism_subgroup (group_isomorphism_of_lm_isomorphism φ) h) + (by rexact to_respect_smul (submodule_functor φ (λg, iff.mp (h g)))) + /- quotient modules -/ definition quotient_module' (S : property M) [is_submodule M S] : AddAbGroup := @@ -289,7 +296,7 @@ begin refine total_image.rec _, intro m, exact image.mk m (subtype_eq idp) end -variables {ψ : M₂ →lm M₃} {φ : M₁ →lm M₂} {θ : M₁ →lm M₃} +variables {ψ : M₂ →lm M₃} {φ : M₁ →lm M₂} {θ : M₁ →lm M₃} {ψ' : M₂' →lm M₃'} {φ' : M₁' →lm M₂'} definition image_elim [constructor] (θ : M₁ →lm M₃) (h : Π⦃g⦄, φ g = 0 → θ g = 0) : image_module φ →lm M₃ := @@ -412,6 +419,29 @@ definition homology_isomorphism [constructor] (ψ : M₂ →lm M₃) (φ : M₁ (quotient_module_isomorphism (homology_quotient_property ψ φ) (eq_zero_of_mem_property_submodule_trivial (image_trivial _))) ⬝lm (kernel_module_isomorphism ψ _) +definition homology_functor [constructor] (α₁ : M₁ →lm M₁') (α₂ : M₂ →lm M₂') (α₃ : M₃ →lm M₃') + (p : hsquare ψ ψ' α₂ α₃) (q : hsquare φ φ' α₁ α₂) : homology ψ φ →lm homology ψ' φ' := +begin + fapply quotient_module_functor, + { apply submodule_functor α₂, intro m pm, refine (p m)⁻¹ ⬝ ap α₃ pm ⬝ to_respect_zero α₃ }, + { intro m pm, induction pm with m' pm', + refine image.mk (α₁ m') ((q m')⁻¹ ⬝ _), exact ap α₂ pm' } +end + +definition homology_isomorphism_homology [constructor] (α₁ : M₁ ≃lm M₁') (α₂ : M₂ ≃lm M₂') (α₃ : M₃ ≃lm M₃') + (p : hsquare ψ ψ' α₂ α₃) (q : hsquare φ φ' α₁ α₂) : homology ψ φ ≃lm homology ψ' φ' := +begin + fapply quotient_module_isomorphism_quotient_module, + { fapply submodule_isomorphism_submodule α₂, intro m, + exact iff.intro (λpm, (p m)⁻¹ ⬝ ap α₃ pm ⬝ to_respect_zero α₃) + (λpm, inj (equiv_of_isomorphism α₃) (p m ⬝ pm ⬝ (to_respect_zero α₃)⁻¹)) }, + { intro m, apply iff.intro, + { intro pm, induction pm with m' pm', refine image.mk (α₁ m') ((q m')⁻¹ ⬝ _), exact ap α₂ pm' }, + { intro pm, induction pm with m' pm', refine image.mk (α₁⁻¹ˡᵐ m') _, + refine (hvinverse' (equiv_of_isomorphism α₁) (equiv_of_isomorphism α₂) q m')⁻¹ ⬝ _, + exact ap α₂⁻¹ˡᵐ pm' ⬝ to_left_inv (equiv_of_isomorphism α₂) m.1 }} +end + definition ker_in_im_of_is_contr_homology (ψ : M₂ →lm M₃) {φ : M₁ →lm M₂} (H₁ : is_contr (homology ψ φ)) {m : M₂} (p : ψ m = 0) : image φ m := rel_of_is_contr_quotient_module _ H₁ ⟨m, p⟩ @@ -441,10 +471,10 @@ is_surjective_of_is_contr_homology_of_constant ψ H₁ (λm, @eq_of_is_contr _ H definition cokernel_module (φ : M₁ →lm M₂) : LeftModule R := quotient_module (image φ) -definition cokernel_module_isomorphism_homology (φ : M₁ →lm M₂) : - homology (trivial_homomorphism M₂ (trivial_LeftModule R)) φ ≃lm cokernel_module φ := +definition cokernel_module_isomorphism_homology (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) (H : Πm, ψ m = 0) : + homology ψ φ ≃lm cokernel_module φ := quotient_module_isomorphism_quotient_module - (submodule_isomorphism _ (λm, idp)) + (submodule_isomorphism _ H) begin intro m, reflexivity end open chain_complex fin nat diff --git a/cohomology/basic.hlean b/cohomology/basic.hlean index 6c485c2..8ee200f 100644 --- a/cohomology/basic.hlean +++ b/cohomology/basic.hlean @@ -10,10 +10,10 @@ 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 + function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit pi is_conn wedge namespace cohomology - +universe variables u u' v w /- 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. @@ -287,15 +287,15 @@ definition additive_hom [constructor] {I : Type} (X : I → Type*) (Y : spectrum H^n[⋁X, Y] →g Πᵍ i, H^n[X i, Y] := Group_pi_intro (λi, cohomology_functor (pinl i) Y n) -definition additive_equiv.{u} {I : Type.{u}} (H : has_choice 0 I) (X : I → Type*) (Y : spectrum) - (n : ℤ) : H^n[⋁X, Y] ≃ Πᵍ i, H^n[X i, Y] := +definition additive_equiv {I : Type.{u}} (H : has_choice.{u (max v w)} 0 I) (X : I → pType.{v}) + (Y : spectrum.{w}) (n : ℤ) : H^n[⋁X, Y] ≃ Πᵍ i, H^n[X i, Y] := trunc_fwedge_pmap_equiv H X (Ω[2] (Y (n+2))) definition spectrum_additive {I : Type} (H : has_choice 0 I) (X : I → Type*) (Y : spectrum) (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) +definition cohomology_fwedge {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) @@ -359,24 +359,25 @@ 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.{u} (X X' : Type*) (Y : spectrum.{u}) (n : ℤ) : +definition cohomology_wedge (X : pType.{u}) (X' : pType.{u'}) (Y : spectrum.{v}) (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_bool 0) _ _ _ ⬝g +H^≃n[(wedge_pequiv !pequiv_plift !pequiv_plift ⬝e* + wedge_pequiv_fwedge (plift.{u u'} X) (plift.{u' u} X'))⁻¹ᵉ*, Y] ⬝g +cohomology_fwedge (has_choice_bool _) _ Y n ⬝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 +(product_isomorphism_Group_pi H^n[plift.{u u'} X, Y] H^n[plift.{u' u} X', Y])⁻¹ᵍ ⬝g +proof H^≃n[!pequiv_plift, Y] ×≃g H^≃n[!pequiv_plift, Y] 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 : ℤ) : +definition unreduced_cohomology_split (X : pType.{u}) (Y : spectrum.{v}) (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_isomorphism_of_equiv (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) : +definition unreduced_ordinary_cohomology_nonzero (X : pType.{u}) (G : AbGroup.{v}) (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) @@ -386,7 +387,7 @@ definition unreduced_ordinary_cohomology_zero (X : Type*) (G : AbGroup) : 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 := +definition unreduced_ordinary_cohomology_pbool (G : AbGroup.{v}) : 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) : @@ -447,7 +448,7 @@ end /- cohomology theory -/ -structure cohomology_theory.{u} : Type.{u+1} := +structure cohomology_theory : Type := (HH : ℤ → pType.{u} → AbGroup.{u}) (Hiso : Π(n : ℤ) {X Y : Type*} (f : X ≃* Y), HH n Y ≃g HH n X) (Hiso_refl : Π(n : ℤ) (X : Type*) (x : HH n X), Hiso n pequiv.rfl x = x) @@ -465,7 +466,7 @@ structure cohomology_theory.{u} : Type.{u+1} := (Hadditive : Π(n : ℤ) {I : Type.{u}} (X : I → Type*), has_choice.{u u} 0 I → is_equiv (Group_pi_intro (λi, Hh n (pinl i)) : HH n (⋁ X) → Πᵍ i, HH n (X i))) -structure ordinary_cohomology_theory.{u} extends cohomology_theory.{u} : Type.{u+1} := +structure ordinary_cohomology_theory extends cohomology_theory.{u} : Type := (Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (HH n (plift pbool))) attribute cohomology_theory.HH [coercion] @@ -494,7 +495,7 @@ definition Hadditive_equiv (H : cohomology_theory) (n : ℤ) {I : Type} (X : I : H n (⋁ X) ≃g Πᵍ i, H n (X i) := isomorphism.mk _ (Hadditive H n X H2) -definition Hlift_empty.{u} (H : cohomology_theory.{u}) (n : ℤ) : +definition Hlift_empty (H : cohomology_theory.{u}) (n : ℤ) : is_contr (H n (plift punit)) := let P : lift empty → Type* := lift.rec empty.elim in let x := Hadditive H n P _ in @@ -524,7 +525,7 @@ end -- refine Hadditive_equiv H n _ _ ⬝g _ -- end -definition cohomology_theory_spectrum.{u} [constructor] (Y : spectrum.{u}) : cohomology_theory.{u} := +definition cohomology_theory_spectrum [constructor] (Y : spectrum.{u}) : cohomology_theory.{u} := cohomology_theory.mk (λn A, H^n[A, Y]) (λn A B f, cohomology_isomorphism f Y n) @@ -539,13 +540,6 @@ cohomology_theory.mk (λn A B f, cohomology_exact f Y n) (λn I A H, spectrum_additive H A Y n) --- set_option pp.universes true --- set_option pp.abbreviations false --- print cohomology_theory_spectrum --- print EM_spectrum --- print has_choice_lift --- 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 := ordinary_cohomology_dimension_plift G ⦄ diff --git a/cohomology/gysin.hlean b/cohomology/gysin.hlean index 5a33572..dfd4034 100644 --- a/cohomology/gysin.hlean +++ b/cohomology/gysin.hlean @@ -4,36 +4,64 @@ import .serre open eq pointed is_trunc is_conn is_equiv equiv sphere fiber chain_complex left_module spectrum nat - prod nat int algebra + prod nat int algebra function spectral_sequence namespace cohomology - +-- set_option pp.universes true +-- print unreduced_ordinary_cohomology_sphere_of_neq_nat +-- --set_option formatter.hide_full_terms false +-- exit definition gysin_sequence' {E B : Type*} (n : ℕ) (HB : is_conn 1 B) (f : E →* B) (e : pfiber f ≃* sphere (n+1)) (A : AbGroup) : chain_complex +3ℤ := -let c := serre_spectral_sequence_map_of_is_conn pt f (EM_spectrum A) 0 (is_strunc_EM_spectrum A) HB -in -left_module.LES_of_SESs _ _ _ (λm, convergent_spectral_sequence.d c n (m, n)) +let c := serre_spectral_sequence_map_of_is_conn pt f (EM_spectrum A) 0 (is_strunc_EM_spectrum A) HB in +let cn : is_normal c := !is_normal_serre_spectral_sequence_map_of_is_conn in +let deg_d_x : Π(m : ℤ), deg (convergent_spectral_sequence.d c n) ((m+1) - 3, n + 1) = (n + m - 0, 0) := +begin + intro m, refine deg_d_normal_eq cn _ _ ⬝ _, + refine prod_eq _ !add.right_inv, + refine add.comm4 (m+1) (-3) n 2 ⬝ _, + exact ap (λx, x - 1) (add.comm (m + 1) n ⬝ (add.assoc n m 1)⁻¹) ⬝ !add.assoc +end in +left_module.LES_of_SESs _ _ _ (λm, convergent_spectral_sequence.d c n (m - 3, n + 1)) begin intro m, fapply short_exact_mod_isomorphism, rotate 3, { fapply short_exact_mod_of_is_contr_submodules - (spectral_sequence.convergence_0 c (n + m) (λm, neg_zero)), + (convergence_0 c (n + m) (λm, neg_zero)), { exact zero_lt_succ n }, - { intro k Hk0 Hkn, apply spectral_sequence.is_contr_E, + { intro k Hk0 Hkn, apply is_contr_E, apply is_contr_ordinary_cohomology, refine is_contr_equiv_closed_rev _ (unreduced_ordinary_cohomology_sphere_of_neq_nat A Hkn Hk0), apply group.equiv_of_isomorphism, apply unreduced_ordinary_cohomology_isomorphism, exact e⁻¹ᵉ* }}, + { symmetry, refine Einf_isomorphism c (n+1) _ _ ⬝lm + convergent_spectral_sequence.α c n (n + m - 0, 0) ⬝lm + isomorphism_of_eq (ap (graded_homology _ _) _) ⬝lm + !graded_homology_isomorphism ⬝lm + cokernel_module_isomorphism_homology _ _ _, + { exact sorry }, + { exact sorry }, + { exact (deg_d_x m)⁻¹ }, + { intro x, apply @eq_of_is_contr, apply is_contr_E, + apply is_normal.normal2 cn, + refine lt_of_le_of_lt (@le_of_eq ℤ _ _ _ (ap (pr2 ∘ deg (convergent_spectral_sequence.d c n)) + (deg_d_x m) ⬝ ap pr2 (deg_d_normal_eq cn _ _))) _, + refine lt_of_le_of_lt (le_of_eq (zero_add (-(n+1)))) _, + apply neg_neg_of_pos, apply of_nat_succ_pos }}, + { reflexivity }, + { exact sorry } end + -- (λm, short_exact_mod_isomorphism -- _ -- isomorphism.rfl -- _ -- (short_exact_mod_of_is_contr_submodules --- (convergent_spectral_sequence.HDinf X _) +-- (convergent_HDinf X _) -- (zero_lt_succ n) -- _)) + end cohomology diff --git a/cohomology/serre.hlean b/cohomology/serre.hlean index 64d8a8d..720365f 100644 --- a/cohomology/serre.hlean +++ b/cohomology/serre.hlean @@ -371,7 +371,7 @@ section serre begin intro n, apply unreduced_cohomology_isomorphism, exact !sigma_fiber_equiv⁻¹ᵉ end qed - definition serre_spectral_sequence_map_of_is_conn (H2 : is_conn 1 B) : + definition serre_spectral_sequence_map_of_is_conn' (H2 : is_conn 1 B) : convergent_spectral_sequence_g (λp q, uoH^p[B, uH^q[fiber f b₀, Y]]) (λn, uH^n[X, Y]) := begin apply convergent_spectral_sequence_of_exact_couple (serre_convergence_map_of_is_conn b₀ f Y s₀ H H2), @@ -379,6 +379,27 @@ section serre { reflexivity } end + definition serre_spectral_sequence_map_of_is_conn (H2 : is_conn 1 B) : + convergent_spectral_sequence_g (λp q, uoH^p[B, uH^q[fiber f b₀, Y]]) (λn, uH^n[X, Y]) := + ⦃convergent_spectral_sequence, + deg_d := λ(r : ℕ), (r + 2, -(r + 1)), + lb := λx, -s₀, + serre_spectral_sequence_map_of_is_conn' b₀ f Y s₀ H H2⦄ + + omit H + definition is_normal_serre_spectral_sequence_map_of_is_conn (H' : is_strunc 0 Y) + (H2 : is_conn 1 B) : + spectral_sequence.is_normal (serre_spectral_sequence_map_of_is_conn b₀ f Y 0 H' H2) := + begin + apply spectral_sequence.is_normal.mk, + { intro p q Hp, exact is_contr_ordinary_cohomology_of_neg _ _ Hp }, + { intro p q Hp, apply is_contr_ordinary_cohomology, + apply is_contr_cohomology_of_is_contr_spectrum, + exact is_contr_of_is_strunc _ _ H' Hp }, + { intro r, reflexivity }, + end + + end serre end spectrum diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 83e5c09..3c1acc9 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -12,6 +12,22 @@ universe variable u AddAbGroup.struct G namespace eq + /- move to init.equiv -/ + + variables {A₀₀ A₂₀ A₀₂ A₂₂ : Type} + {f₁₀ : A₀₀ → A₂₀} + {f₀₁ : A₀₀ → A₀₂} {f₂₁ : A₂₀ → A₂₂} + {f₁₂ : A₀₂ → A₂₂} + + definition hhinverse' (f₁₀ : A₀₀ ≃ A₂₀) (f₁₂ : A₀₂ ≃ A₂₂) (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : + hsquare f₁₀⁻¹ᵉ f₁₂⁻¹ᵉ f₂₁ f₀₁ := + p⁻¹ʰᵗʸʰ + + definition hvinverse' (f₀₁ : A₀₀ ≃ A₀₂) (f₂₁ : A₂₀ ≃ A₂₂) (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : + hsquare f₁₂ f₁₀ f₀₁⁻¹ᵉ f₂₁⁻¹ᵉ := + p⁻¹ʰᵗʸᵛ + + definition transport_lemma {A : Type} {C : A → Type} {g₁ : A → A} {x y : A} (p : x = y) (f : Π⦃x⦄, C x → C (g₁ x)) (z : C x) : @@ -28,6 +44,15 @@ namespace eq end eq open eq +namespace int + + definition maxm2_eq_minus_two {n : ℤ} (H : n < 0) : maxm2 n = -2 := + begin + induction exists_eq_neg_succ_of_nat H with n p, cases p, reflexivity + end + +end int + namespace nat -- definition rec_down_le_beta_lt (P : ℕ → Type) (s : ℕ) (H0 : Πn, s ≤ n → P n) diff --git a/spectrum/trunc.hlean b/spectrum/trunc.hlean index de2efef..c58b3f9 100644 --- a/spectrum/trunc.hlean +++ b/spectrum/trunc.hlean @@ -119,6 +119,14 @@ begin intro k, apply is_trunc_lift, apply is_trunc_unit end +definition is_contr_of_is_strunc (n : ℤ) {m : ℤ} (E : spectrum) (H : is_strunc n E) + (Hmn : m < -n) : is_contr (E m) := +begin + refine transport (λn, is_trunc n (E m)) _ (H m), + apply maxm2_eq_minus_two, + exact lt_of_lt_of_le (add_lt_add_left Hmn n) (le_of_eq !add.right_inv) +end + open option definition is_strunc_add_point_spectrum {X : Type} {Y : X → spectrum} {s₀ : ℤ} (H : Πx, is_strunc s₀ (Y x)) : Π(x : X₊), is_strunc s₀ (add_point_spectrum Y x)