From 2913de520d4fb2c8177a8cbb7e64938291248d03 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 13 Nov 2018 19:22:07 -0500 Subject: [PATCH] finish proving that the gysin sequence consists of the correct groups --- algebra/module_chain_complex.hlean | 14 ++-- algebra/spectral_sequence.hlean | 4 ++ algebra/submodule.hlean | 44 ++++++++---- cohomology/basic.hlean | 11 ++- cohomology/gysin.hlean | 108 ++++++++++++++++++++++++----- 5 files changed, 140 insertions(+), 41 deletions(-) diff --git a/algebra/module_chain_complex.hlean b/algebra/module_chain_complex.hlean index 6c5f03e..626f915 100644 --- a/algebra/module_chain_complex.hlean +++ b/algebra/module_chain_complex.hlean @@ -14,18 +14,18 @@ structure module_chain_complex (R : Ring) (N : succ_str) : Type := (is_chain_complex : Π (n : N) (x : mod (S (S n))), hom n (hom (S n) x) = 0) -namespace module_chain_complex +namespace left_module variables {R : Ring} {N : succ_str} - definition mcc_mod [unfold 2] [coercion] (C : module_chain_complex R N) (n : N) : + definition mcc_mod [unfold 3] [coercion] (C : module_chain_complex R N) (n : N) : LeftModule R := module_chain_complex.mod C n - definition mcc_carr [unfold 2] [coercion] (C : module_chain_complex R N) (n : N) : + definition mcc_carr [unfold 3] [coercion] (C : module_chain_complex R N) (n : N) : Type := C n - definition mcc_pcarr [unfold 2] [coercion] (C : module_chain_complex R N) (n : N) : + definition mcc_pcarr [unfold 3] [coercion] (C : module_chain_complex R N) (n : N) : Set* := mcc_mod C n @@ -46,7 +46,11 @@ namespace module_chain_complex -- maybe we don't even need this? definition is_exact_at_m (C : module_chain_complex R N) (n : N) : Type := is_exact_at C n -end module_chain_complex + + definition is_exact_m (C : module_chain_complex R N) : Type := + ∀n, is_exact_at_m C n + +end left_module namespace left_module variable {R : Ring} diff --git a/algebra/spectral_sequence.hlean b/algebra/spectral_sequence.hlean index 637487d..d8cf035 100644 --- a/algebra/spectral_sequence.hlean +++ b/algebra/spectral_sequence.hlean @@ -159,6 +159,10 @@ namespace spectral_sequence variable {c} variable (nc : is_normal c) include nc + + definition deg_d_normal_pr1 (r : ℕ) : (deg_d c r).1 = r+2 := ap pr1 (normal3 nc r) + definition deg_d_normal_pr2 (r : ℕ) : (deg_d c r).2 = -(r+1) := ap pr2 (normal3 nc r) + 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 diff --git a/algebra/submodule.hlean b/algebra/submodule.hlean index 9c95d4d..a325b35 100644 --- a/algebra/submodule.hlean +++ b/algebra/submodule.hlean @@ -1,10 +1,10 @@ /- submodules and quotient modules -/ -- Authors: Floris van Doorn, Jeremy Avigad -import .left_module .quotient_group +import .left_module .quotient_group .module_chain_complex open algebra eq group sigma sigma.ops is_trunc function trunc equiv is_equiv property - +universe variable u namespace left_module /- submodules -/ variables {R : Ring} {M M₁ M₁' M₂ M₂' M₃ M₃' : LeftModule R} {m m₁ m₂ : M} @@ -484,19 +484,17 @@ quotient_module_isomorphism_quotient_module begin intro m, reflexivity end open chain_complex fin nat -definition LES_of_SESs.{u} {N : succ_str} (A B C : N → LeftModule.{_ u} R) (φ : Πn, A n →lm B n) +definition LES_of_SESs {N : succ_str} (A B C : N → LeftModule.{_ u} R) (φ : Πn, A n →lm B n) (ses : Πn : N, short_exact_mod (cokernel_module (φ (succ_str.S n))) (C n) (kernel_module (φ n))) : - chain_complex.{_ u} (stratified N 2) := + module_chain_complex.{_ _ u} R (stratified N 2) := begin - fapply chain_complex.mk, - { intro x, apply @pSet_of_LeftModule R, - induction x with n k, induction k with k H, do 3 (cases k with k; rotate 1), + fapply module_chain_complex.mk, + { intro x, induction x with n k, induction k with k H, do 3 (cases k with k; rotate 1), { /-k≥3-/ exfalso, apply lt_le_antisymm H, apply le_add_left}, { /-k=0-/ exact B n }, { /-k=1-/ exact A n }, { /-k=2-/ exact C n }}, - { intro x, apply @pmap_of_homomorphism R, - induction x with n k, induction k with k H, do 3 (cases k with k; rotate 1), + { intro x, induction x with n k, induction k with k H, do 3 (cases k with k; rotate 1), { /-k≥3-/ exfalso, apply lt_le_antisymm H, apply le_add_left}, { /-k=0-/ exact φ n }, { /-k=1-/ exact submodule_incl _ ∘lm short_exact_mod.g (ses n) }, @@ -504,14 +502,32 @@ begin { intros x m, induction x with n k, induction k with k H, do 3 (cases k with k; rotate 1), { exfalso, apply lt_le_antisymm H, apply le_add_left}, { exact (short_exact_mod.g (ses n) m).2 }, - { exact ap pr1 (is_short_exact.im_in_ker (short_exact_mod.h (ses n)) (quotient_map _ m)) }, - { exact ap (short_exact_mod.f (ses n)) (quotient_map_eq_zero _ _ (image.mk m idp)) ⬝ - to_respect_zero (short_exact_mod.f (ses n)) }} + { note h := is_short_exact.im_in_ker (short_exact_mod.h (ses n)) (quotient_map _ m), + exact ap pr1 h }, + { refine _ ⬝ to_respect_zero (short_exact_mod.f (ses n)), + rexact ap (short_exact_mod.f (ses n)) (quotient_map_eq_zero _ _ (image.mk m idp)) }} end -definition is_exact_LES_of_SESs.{u} {N : succ_str} (A B C : N → LeftModule.{_ u} R) (φ : Πn, A n →lm B n) +open prod +definition LES_of_SESs_zero {N : succ_str} {A B C : N → LeftModule.{_ u} R} (φ : Πn, A n →lm B n) + (ses : Πn : N, short_exact_mod (cokernel_module (φ (succ_str.S n))) (C n) (kernel_module (φ n))) + (n : N) : LES_of_SESs A B C φ ses (n, 0) ≃lm B n := +by reflexivity + +definition LES_of_SESs_one {N : succ_str} {A B C : N → LeftModule.{_ u} R} (φ : Πn, A n →lm B n) + (ses : Πn : N, short_exact_mod (cokernel_module (φ (succ_str.S n))) (C n) (kernel_module (φ n))) + (n : N) : LES_of_SESs A B C φ ses (n, 1) ≃lm A n := +by reflexivity + +definition LES_of_SESs_two {N : succ_str} {A B C : N → LeftModule.{_ u} R} (φ : Πn, A n →lm B n) + (ses : Πn : N, short_exact_mod (cokernel_module (φ (succ_str.S n))) (C n) (kernel_module (φ n))) + (n : N) : LES_of_SESs A B C φ ses (n, 2) ≃lm C n := +by reflexivity + +definition is_exact_LES_of_SESs {N : succ_str} {A B C : N → LeftModule.{_ u} R} + (φ : Πn, A n →lm B n) (ses : Πn : N, short_exact_mod (cokernel_module (φ (succ_str.S n))) (C n) (kernel_module (φ n))) : - is_exact (LES_of_SESs A B C φ ses) := + is_exact_m (LES_of_SESs A B C φ ses) := begin intros x m p, induction x with n k, induction k with k H, do 3 (cases k with k; rotate 1), { exfalso, apply lt_le_antisymm H, apply le_add_left}, diff --git a/cohomology/basic.hlean b/cohomology/basic.hlean index 8ee200f..fcaac45 100644 --- a/cohomology/basic.hlean +++ b/cohomology/basic.hlean @@ -395,14 +395,14 @@ definition unreduced_ordinary_cohomology_pbool_nonzero (G : AbGroup) (n : ℤ) ( 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) : +definition unreduced_ordinary_cohomology_sphere_zero (G : AbGroup.{u}) (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⁻¹)) +product_trivial_left _ _ (ordinary_cohomology_sphere_of_neq _ (λh, H (of_nat.inj 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 +unreduced_ordinary_cohomology_nonzero (sphere n) G n (λh, H (of_nat.inj h)) ⬝g ordinary_cohomology_sphere G n definition unreduced_ordinary_cohomology_sphere_of_neq (G : AbGroup) {n : ℤ} {k : ℕ} (p : n ≠ k) @@ -415,6 +415,11 @@ definition unreduced_ordinary_cohomology_sphere_of_neq_nat (G : AbGroup) {n k : (q : n ≠ 0) : is_contr (uoH^n[sphere k, G]) := unreduced_ordinary_cohomology_sphere_of_neq G (λh, p (of_nat.inj h)) (λh, q (of_nat.inj h)) +definition unreduced_ordinary_cohomology_sphere_of_gt (G : AbGroup) {n k : ℕ} (p : n > k) : + is_contr (uoH^n[sphere k, G]) := +unreduced_ordinary_cohomology_sphere_of_neq_nat + G (ne_of_gt p) (ne_of_gt (lt_of_le_of_lt (zero_le k) 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 diff --git a/cohomology/gysin.hlean b/cohomology/gysin.hlean index eed4574..f71b936 100644 --- a/cohomology/gysin.hlean +++ b/cohomology/gysin.hlean @@ -4,9 +4,10 @@ import .serre open eq pointed is_trunc is_conn is_equiv equiv sphere fiber chain_complex left_module spectrum nat - prod nat int algebra function spectral_sequence + prod nat int algebra function spectral_sequence fin group namespace cohomology +universe variable u /- We have maps: d_m = d_(m-1,n+1)^n : E_(m-1,n+1)^n → E_(m+n+1,0)^n @@ -20,8 +21,30 @@ namespace cohomology ... 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ℤ := + +definition gysin_trivial_Epage {E B : pType.{u}} {n : ℕ} (HB : is_conn 1 B) (f : E →* B) + (e : pfiber f ≃* sphere (n+1)) (A : AbGroup) (r : ℕ) (p q : ℤ) (hq : q ≠ 0) + (hq' : q ≠ of_nat (n+1)): + is_contr (convergent_spectral_sequence.E (serre_spectral_sequence_map_of_is_conn pt f + (EM_spectrum A) 0 (is_strunc_EM_spectrum A) HB) 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 + +definition gysin_trivial_Epage2 {E B : pType.{u}} {n : ℕ} (HB : is_conn 1 B) (f : E →* B) + (e : pfiber f ≃* sphere (n+1)) (A : AbGroup) (r : ℕ) (p q : ℤ) (hq : q > n+1) : + is_contr (convergent_spectral_sequence.E (serre_spectral_sequence_map_of_is_conn pt f + (EM_spectrum A) 0 (is_strunc_EM_spectrum A) HB) r (p, q)) := +begin + intros, apply gysin_trivial_Epage HB f e A 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 + +definition gysin_sequence' {E B : pType.{u}} {n : ℕ} (HB : is_conn 1 B) (f : E →* B) + (e : pfiber f ≃* sphere (n+1)) (A : AbGroup) : module_chain_complex rℤ -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 @@ -36,18 +59,10 @@ begin 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, +from gysin_trivial_Epage HB f e A, 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, +from gysin_trivial_Epage2 HB f e A, left_module.LES_of_SESs _ _ _ (λm, convergent_spectral_sequence.d c n (m - 1, n + 1)) begin intro m, @@ -96,13 +111,68 @@ left_module.LES_of_SESs _ _ _ (λm, convergent_spectral_sequence.d c n (m - 1, n refine ap (λx, x + _) !add.right_inv ⬝ !zero_add }} end --- 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) ≃ _ := --- _ - +-- set_option pp.universes true +-- print unreduced_ordinary_cohomology_sphere_zero +-- print unreduced_ordinary_cohomology_zero +-- print ordinary_cohomology_sphere_of_neq +-- set_option formatter.hide_full_terms false +definition gysin_sequence'_zero {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) ≃lm LeftModule_int_of_AbGroup (uoH^m+n+1[B, A]) := +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 +begin + refine LES_of_SESs_zero _ _ m ⬝lm _, + transitivity convergent_spectral_sequence.E c n (m+n+1, 0), + exact isomorphism_of_eq (ap (convergent_spectral_sequence.E c n) + (deg_d_normal_eq cn _ _ ⬝ prod_eq (add.comm4 m (- 1) n 2) (add.right_inv (n+1)))), + refine E_isomorphism0 _ _ _ ⬝lm + lm_iso_int.mk (unreduced_ordinary_cohomology_isomorphism_right _ _ _), + { intros r hr, apply is_contr_ordinary_cohomology, + refine is_contr_equiv_closed_rev + (equiv_of_isomorphism (cohomology_change_int _ _ _ ⬝g uoH^≃r+1[e⁻¹ᵉ*, A])) + (unreduced_ordinary_cohomology_sphere_of_neq_nat A _ _), + { exact !zero_sub ⬝ ap neg (deg_d_normal_pr2 cn r) ⬝ !neg_neg }, + { apply ne_of_lt, apply add_lt_add_right, exact hr }, + { apply succ_ne_zero }}, + { intros r hr, apply is_contr_ordinary_cohomology, + refine is_contr_equiv_closed_rev + (equiv_of_isomorphism (cohomology_change_int _ _ (!zero_add ⬝ deg_d_normal_pr2 cn r))) + (is_contr_ordinary_cohomology_of_neg _ _ _), + { rewrite [-neg_zero], apply neg_lt_neg, apply of_nat_lt_of_nat_of_lt, apply zero_lt_succ }}, + { exact uoH^≃ 0[e⁻¹ᵉ*, A] ⬝g unreduced_ordinary_cohomology_sphere_zero _ _ (succ_ne_zero n) } +end +definition gysin_sequence'_one {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, 1) ≃lm LeftModule_int_of_AbGroup (uoH^m - 1[B, A]) := +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 +begin + refine LES_of_SESs_one _ _ m ⬝lm _, + refine E_isomorphism0 _ _ _ ⬝lm + lm_iso_int.mk (unreduced_ordinary_cohomology_isomorphism_right _ _ _), + { intros r hr, apply is_contr_ordinary_cohomology, + refine is_contr_equiv_closed_rev + (equiv_of_isomorphism uoH^≃_[e⁻¹ᵉ*, A]) + (unreduced_ordinary_cohomology_sphere_of_gt _ _), + { apply lt_add_of_pos_right, apply zero_lt_succ }}, + { intros r hr, apply is_contr_ordinary_cohomology, + refine is_contr_equiv_closed_rev + (equiv_of_isomorphism (cohomology_change_int _ _ _ ⬝g uoH^≃n-r[e⁻¹ᵉ*, A])) + (unreduced_ordinary_cohomology_sphere_of_neq_nat A _ _), + { refine ap (add _) (deg_d_normal_pr2 cn r) ⬝ add_sub_comm n 1 r 1 ⬝ !add_zero ⬝ _, + symmetry, apply of_nat_sub, exact le_of_lt hr }, + { apply ne_of_lt, exact lt_of_le_of_lt (nat.sub_le n r) (lt.base n) }, + { apply ne_of_gt, exact nat.sub_pos_of_lt hr }}, + { refine uoH^≃n+1[e⁻¹ᵉ*, A] ⬝g unreduced_ordinary_cohomology_sphere _ _ (succ_ne_zero n) } +end +definition gysin_sequence'_two {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, 2) ≃lm LeftModule_int_of_AbGroup (uoH^n+m[E, A]) := +LES_of_SESs_two _ _ m end cohomology