From ea402f56eaf63c8668313fb4c6a382d95a45f5ea Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 12 Nov 2018 18:07:05 -0500 Subject: [PATCH] finish first part of constructing gysin sequence We have a long exact sequence, we still need to show that it consists of the correct groups --- algebra/graded.hlean | 7 +++ algebra/left_module.hlean | 7 +++ algebra/submodule.hlean | 8 ++- cohomology/gysin.hlean | 107 ++++++++++++++++++++++++++------------ 4 files changed, 95 insertions(+), 34 deletions(-) diff --git a/algebra/graded.hlean b/algebra/graded.hlean index 2d222c1..a346de1 100644 --- a/algebra/graded.hlean +++ b/algebra/graded.hlean @@ -673,6 +673,13 @@ begin exact graded_hom_square f (to_right_inv (deg f) (deg f x)) idp (to_left_inv (deg f) x) idp end +definition graded_homology_isomorphism_kernel_module + (g : M₂ →gm M₃) (f : M₁ →gm M₂) (x : I) + (H : Πm, image (f ← x) m → m = 0) : graded_homology g f x ≃lm graded_kernel g x := +begin + apply quotient_module_isomorphism, intro m h, apply subtype_eq, apply H, exact h +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/left_module.hlean b/algebra/left_module.hlean index 257a620..8bbb224 100644 --- a/algebra/left_module.hlean +++ b/algebra/left_module.hlean @@ -312,6 +312,13 @@ section definition lm_constant [constructor] (M₁ M₂ : LeftModule R) : M₁ →lm M₂ := homomorphism.mk (const M₁ 0) !is_module_hom_constant + definition trivial_image_of_is_contr {R} {M₁ M₂ : LeftModule R} {φ : M₁ →lm M₂} (H : is_contr M₁) + ⦃m : M₂⦄ (hm : image φ m) : m = 0 := + begin + induction hm with m' p, induction p, + exact ap φ (@eq_of_is_contr _ H _ _) ⬝ to_respect_zero φ + end + structure isomorphism (M₁ M₂ : LeftModule R) := (to_hom : M₁ →lm M₂) (is_equiv_to_hom : is_equiv to_hom) diff --git a/algebra/submodule.hlean b/algebra/submodule.hlean index cec1193..9c95d4d 100644 --- a/algebra/submodule.hlean +++ b/algebra/submodule.hlean @@ -468,10 +468,16 @@ definition is_surjective_of_is_contr_homology_of_is_contr (ψ : M₂ →lm M₃) (H₁ : is_contr (homology ψ φ)) (H₂ : is_contr M₃) : is_surjective φ := is_surjective_of_is_contr_homology_of_constant ψ H₁ (λm, @eq_of_is_contr _ H₂ _ _) +definition homology_isomorphism_kernel_module (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) + (H : Πm, image φ m → m = 0) : homology ψ φ ≃lm kernel_module ψ := +begin + apply quotient_module_isomorphism, intro m h, apply subtype_eq, apply H, exact h +end + definition cokernel_module (φ : M₁ →lm M₂) : LeftModule R := quotient_module (image φ) -definition cokernel_module_isomorphism_homology (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) (H : Πm, ψ m = 0) : +definition homology_isomorphism_cokernel_module (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) (H : Πm, ψ m = 0) : homology ψ φ ≃lm cokernel_module φ := quotient_module_isomorphism_quotient_module (submodule_isomorphism _ H) diff --git a/cohomology/gysin.hlean b/cohomology/gysin.hlean index dfd4034..eed4574 100644 --- a/cohomology/gysin.hlean +++ b/cohomology/gysin.hlean @@ -7,22 +7,48 @@ open eq pointed is_trunc is_conn is_equiv equiv sphere fiber chain_complex left_ 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 +/- + We have maps: + d_m = d_(m-1,n+1)^n : E_(m-1,n+1)^n → E_(m+n+1,0)^n + Note that ker d_m = E_(m-1,n+1)^∞ and coker d_m = E_(m+n+1,0)^∞. + We have short exact sequences + coker d_{m-1} → D_{m+n}^∞ → ker d_m + where D^∞ is the abutment of the spectral sequence. + This comes from the spectral sequence, using the fact that coker d_{m-1} and ker d_m are the only + two nontrivial groups building up D_{m+n}^∞ (in the filtration of D_{m+n}^∞). + We can splice these SESs together to get a LES + ... E_(m+n,0)^n → D_{m+n}^∞ → E_(m-1,n+1)^n → E_(m+n+1,0)^n → D_{m+n+1}^∞ ... +-/ + +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 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) := +have deg_d_x : Π(m : ℤ), deg (convergent_spectral_sequence.d c n) ((m - 1) - 1, 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)) + refine ap (λx, x + (n+2)) !sub_sub ⬝ _, + refine add.comm4 m (- 2) n 2 ⬝ _, + refine ap (λx, x + 0) !add.comm +end, +have trivial_E : Π(r : ℕ) (p q : ℤ) (hq : q ≠ 0) (hq' : q ≠ of_nat (n+1)), + is_contr (convergent_spectral_sequence.E c r (p, q)), +begin + intros, apply is_contr_E, apply is_contr_ordinary_cohomology, esimp, + refine is_contr_equiv_closed_rev _ (unreduced_ordinary_cohomology_sphere_of_neq A hq' hq), + apply group.equiv_of_isomorphism, apply unreduced_ordinary_cohomology_isomorphism, exact e⁻¹ᵉ* +end, +have trivial_E' : Π(r : ℕ) (p q : ℤ) (hq : q > n+1), + is_contr (convergent_spectral_sequence.E c r (p, q)), +begin + intros, apply trivial_E r p q, + { intro h, subst h, apply not_lt_zero (n+1), exact lt_of_of_nat_lt_of_nat hq }, + { intro h, subst h, exact lt.irrefl _ hq } +end, +left_module.LES_of_SESs _ _ _ (λm, convergent_spectral_sequence.d c n (m - 1, n + 1)) begin intro m, fapply short_exact_mod_isomorphism, @@ -30,19 +56,19 @@ left_module.LES_of_SESs _ _ _ (λm, convergent_spectral_sequence.d c n (m - 3, n { fapply short_exact_mod_of_is_contr_submodules (convergence_0 c (n + m) (λm, neg_zero)), { exact zero_lt_succ n }, - { 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⁻¹ᵉ* }}, + { intro k Hk0 Hkn, apply trivial_E, exact λh, Hk0 (of_nat.inj h), + exact λh, Hkn (of_nat.inj h), }}, { 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 }, + convergent_spectral_sequence.α c n (n + m - 0, 0) ⬝lm + isomorphism_of_eq (ap (graded_homology _ _) _) ⬝lm + !graded_homology_isomorphism ⬝lm + homology_isomorphism_cokernel_module _ _ _, + { intros r Hr, apply trivial_E', apply of_nat_lt_of_nat_of_lt, + rewrite [zero_add], exact lt_succ_of_le Hr }, + { intros r Hr, apply is_contr_E, apply is_normal.normal2 cn, + refine lt_of_le_of_lt (le_of_eq (ap (λx : ℤ × ℤ, 0 + pr2 x) (is_normal.normal3 cn r))) _, + esimp, rewrite [-sub_eq_add_neg], apply sub_lt_of_pos, apply of_nat_lt_of_nat_of_lt, + apply succ_pos }, { exact (deg_d_x m)⁻¹ }, { intro x, apply @eq_of_is_contr, apply is_contr_E, apply is_normal.normal2 cn, @@ -51,17 +77,32 @@ left_module.LES_of_SESs _ _ _ (λm, convergent_spectral_sequence.d c n (m - 3, n 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 } + { symmetry, + refine Einf_isomorphism c (n+1) _ _ ⬝lm + convergent_spectral_sequence.α c n (n + m - (n+1), n+1) ⬝lm + graded_homology_isomorphism_kernel_module _ _ _ _ ⬝lm + isomorphism_of_eq (ap (graded_kernel _) _), + { intros r Hr, apply trivial_E', apply of_nat_lt_of_nat_of_lt, + apply lt_add_of_pos_right, apply zero_lt_succ }, + { intros r Hr, apply is_contr_E, apply is_normal.normal2 cn, + refine lt_of_le_of_lt (le_of_eq (ap (λx : ℤ × ℤ, (n+1)+pr2 x) (is_normal.normal3 cn r))) _, + esimp, rewrite [-sub_eq_add_neg], apply sub_lt_right_of_lt_add, + apply of_nat_lt_of_nat_of_lt, rewrite [zero_add], exact lt_succ_of_le Hr }, + { apply trivial_image_of_is_contr, rewrite [deg_d_inv_eq], + apply trivial_E', apply of_nat_lt_of_nat_of_lt, + apply lt_add_of_pos_right, apply zero_lt_succ }, + { refine prod_eq _ rfl, refine ap (add _) !neg_add ⬝ _, + refine add.comm4 n m (-n) (- 1) ⬝ _, + refine ap (λx, x + _) !add.right_inv ⬝ !zero_add }} end --- (λm, short_exact_mod_isomorphism --- _ --- isomorphism.rfl --- _ --- (short_exact_mod_of_is_contr_submodules --- (convergent_HDinf X _) --- (zero_lt_succ n) --- _)) +-- open fin +-- definition gysin_sequence'_zero_equiv {E B : Type*} {n : ℕ} (HB : is_conn 1 B) (f : E →* B) +-- (e : pfiber f ≃* sphere (n+1)) (A : AbGroup) (m : ℤ) : +-- gysin_sequence' HB f e A (m, 0) ≃ _ := +-- _ + + end cohomology