From 96e11300edec09a063c1d0f2d594e4c3b25b5921 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sat, 29 Sep 2018 12:07:54 +0200 Subject: [PATCH] fix indexing of abutment in spectral sequences --- algebra/spectral_sequence.hlean | 52 +++++++++++++++++---------------- cohomology/serre.hlean | 38 ++++++++++++------------ 2 files changed, 46 insertions(+), 44 deletions(-) diff --git a/algebra/spectral_sequence.hlean b/algebra/spectral_sequence.hlean index 39bad5d..3803eb0 100644 --- a/algebra/spectral_sequence.hlean +++ b/algebra/spectral_sequence.hlean @@ -594,7 +594,7 @@ namespace left_module definition Z2 [constructor] : AddAbGroup := agℤ ×aa agℤ - structure converges_to.{u v w} {R : Ring} (E' : agℤ → agℤ → LeftModule.{u v} 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)} := (X : exact_couple.{u 0 w v} R Z2) (HH : is_bounded X) @@ -605,15 +605,15 @@ namespace left_module (deg_d1 : ℕ → agℤ) (deg_d2 : ℕ → agℤ) (deg_d_eq0 : Π(r : ℕ), deg (d (page X r)) 0 = (deg_d1 r, deg_d2 r)) - infix ` ⟹ `:25 := converges_to + infix ` ⟹ `:25 := convergent_exact_couple - definition converges_to_g [reducible] (E' : agℤ → agℤ → AbGroup) (Dinf : agℤ → AbGroup) : Type := + definition convergent_exact_couple_g [reducible] (E' : agℤ → agℤ → AbGroup) (Dinf : agℤ → AbGroup) : Type := (λn s, LeftModule_int_of_AbGroup (E' n s)) ⟹ (λn, LeftModule_int_of_AbGroup (Dinf n)) - infix ` ⟹ᵍ `:25 := converges_to_g + infix ` ⟹ᵍ `:25 := convergent_exact_couple_g section - open converges_to + open convergent_exact_couple parameters {R : Ring} {E' : agℤ → agℤ → LeftModule R} {Dinf : agℤ → LeftModule R} (c : E' ⟹ Dinf) local abbreviation X := X c local abbreviation i := i X @@ -631,19 +631,18 @@ namespace left_module (deg (d (page X r)))⁻¹ᵉ (n, s) = (n - deg_d1 c r, s - deg_d2 c r) := inv_eq_of_eq (!deg_d_eq ⬝ prod_eq !sub_add_cancel !sub_add_cancel)⁻¹ - definition converges_to_isomorphism {E'' : agℤ → agℤ → LeftModule R} {Dinf' : graded_module R agℤ} + definition convergent_exact_couple_isomorphism {E'' : agℤ → agℤ → LeftModule R} {Dinf' : graded_module R agℤ} (e' : Πn s, E' n s ≃lm E'' n s) (f' : Πn, Dinf n ≃lm Dinf' n) : E'' ⟹ Dinf' := - converges_to.mk X HH s₁ s₂ (HB c) + convergent_exact_couple.mk X HH s₁ s₂ (HB c) begin intro x, induction x with n s, exact e c (n, s) ⬝lm e' n s end (λn, f c n ⬝lm f' n) (deg_d1 c) (deg_d2 c) (λr, deg_d_eq0 c r) - include c - definition converges_to_reindex (i : agℤ ×ag agℤ ≃g agℤ ×ag agℤ) : - (λp q, E' (i (p, q)).1 (i (p, q)).2) ⟹ (λn, Dinf n) := + definition convergent_exact_couple_reindex (i : agℤ ×ag agℤ ≃g agℤ ×ag agℤ) : + (λp q, E' (i (p, q)).1 (i (p, q)).2) ⟹ Dinf := begin - fapply converges_to.mk (exact_couple_reindex i X) (is_bounded_reindex i HH), + fapply convergent_exact_couple.mk (exact_couple_reindex i X) (is_bounded_reindex i HH), { exact λn, (i⁻¹ᵍ (s₁ n, s₂ n)).1 }, { exact λn, (i⁻¹ᵍ (s₁ n, s₂ n)).2 }, { intro n, refine ap (B' HH) _ ⬝ HB c n, @@ -658,32 +657,36 @@ namespace left_module { intro r, esimp, refine !deg_d_reindex ⬝ ap i⁻¹ᵍ (ap (deg (d _)) (group.to_respect_zero i) ⬝ deg_d_eq0 c r) ⬝ !prod.eta⁻¹ } end + + definition convergent_exact_couple_negate_inf : E' ⟹ (λn, Dinf (-n)) := + convergent_exact_couple.mk X HH (s₁ ∘ neg) (s₂ ∘ neg) (λn, HB c (-n)) (e c) (λn, f c (-n)) + (deg_d1 c) (deg_d2 c) (deg_d_eq0 c) omit c -/- definition converges_to_reindex {E'' : agℤ → agℤ → LeftModule R} {Dinf' : graded_module R agℤ} +/- definition convergent_exact_couple_reindex {E'' : agℤ → agℤ → LeftModule R} {Dinf' : graded_module R agℤ} (i : agℤ ×g agℤ ≃ agℤ × agℤ) (e' : Πp q, E' p q ≃lm E'' (i (p, q)).1 (i (p, q)).2) (i2 : agℤ ≃ agℤ) (f' : Πn, Dinf n ≃lm Dinf' (i2 n)) : (λp q, E'' p q) ⟹ λn, Dinf' n := - converges_to.mk (exact_couple_reindex i X) (is_bounded_reindex i HH) s₁ s₂ + convergent_exact_couple.mk (exact_couple_reindex i X) (is_bounded_reindex i HH) s₁ s₂ sorry --(λn, ap (B' HH) (to_right_inv i _ ⬝ begin end) ⬝ HB c n) sorry --begin intro x, induction x with p q, exact e c (p, q) ⬝lm e' p q end sorry-/ -/- definition converges_to_reindex_neg {E'' : agℤ → agℤ → LeftModule R} {Dinf' : graded_module R agℤ} +/- definition convergent_exact_couple_reindex_neg {E'' : agℤ → agℤ → LeftModule R} {Dinf' : graded_module R agℤ} (e' : Πp q, E' p q ≃lm E'' (-p) (-q)) (f' : Πn, Dinf n ≃lm Dinf' (-n)) : (λp q, E'' p q) ⟹ λn, Dinf' n := - converges_to.mk (exact_couple_reindex (equiv_neg ×≃ equiv_neg) X) (is_bounded_reindex _ HH) + convergent_exact_couple.mk (exact_couple_reindex (equiv_neg ×≃ equiv_neg) X) (is_bounded_reindex _ HH) (λn, -s₂ (-n)) (λn, ap (B' HH) (begin esimp, end) ⬝ HB c n) sorry --begin intro x, induction x with p q, exact e c (p, q) ⬝lm e' p q end sorry-/ - definition is_built_from_of_converges_to (n : ℤ) : is_built_from (Dinf n) (Einfdiag n) := + definition is_built_from_of_convergent_exact_couple (n : ℤ) : is_built_from (Dinf n) (Einfdiag n) := is_built_from_isomorphism_left (f c n) (is_built_from_infpage HH (s₁ n, s₂ n) (HB c n)) /- TODO: reprove this using is_built_of -/ - theorem is_contr_converges_to_precise (n : agℤ) + theorem is_contr_convergent_exact_couple_precise (n : agℤ) (H : Π(n : agℤ) (l : ℕ), is_contr (E' ((deg i)^[l] (s₁ n, s₂ n)).1 ((deg i)^[l] (s₁ n, s₂ n)).2)) : is_contr (Dinf n) := begin @@ -701,8 +704,8 @@ namespace left_module exact equiv_of_isomorphism (Dinfdiag0 HH (s₁ n, s₂ n) (HB c n) ⬝lm f c n) end - theorem is_contr_converges_to (n : agℤ) (H : Π(n s : agℤ), is_contr (E' n s)) : is_contr (Dinf n) := - is_contr_converges_to_precise n (λn s, !H) + theorem is_contr_convergent_exact_couple (n : agℤ) (H : Π(n s : agℤ), 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₂) (H1 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X (n - deg_d1 c r, s - deg_d2 c r))) @@ -733,12 +736,12 @@ namespace left_module end variables {E' : agℤ → agℤ → AbGroup} {Dinf : agℤ → AbGroup} (c : E' ⟹ᵍ Dinf) - definition converges_to_g_isomorphism {E'' : agℤ → agℤ → AbGroup} {Dinf' : agℤ → AbGroup} + definition convergent_exact_couple_g_isomorphism {E'' : agℤ → agℤ → AbGroup} {Dinf' : agℤ → AbGroup} (e' : Πn s, E' n s ≃g E'' n s) (f' : Πn, Dinf n ≃g Dinf' n) : E'' ⟹ᵍ Dinf' := - converges_to_isomorphism c (λn s, lm_iso_int.mk (e' n s)) (λn, lm_iso_int.mk (f' n)) + convergent_exact_couple_isomorphism c (λn s, lm_iso_int.mk (e' n s)) (λn, lm_iso_int.mk (f' n)) - structure converging_spectral_sequence.{u v w} {R : Ring} (E' : agℤ → agℤ → LeftModule.{u v} R) + 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)} := (E : ℕ → graded_module.{u 0 v} R Z2) (d : Π(n : ℕ), E n →gm E n) @@ -751,7 +754,6 @@ namespace left_module /- todo: - - rename "converges_to" to converging_exact_couple - double-check the definition of converging_spectral_sequence - construct converging spectral sequence from a converging exact couple, - This requires the additional hypothesis that the degree of i is (-1, 1), which is true by reflexivity for the spectral sequences we construct @@ -959,9 +961,9 @@ namespace spectrum -- refine !add.assoc ⬝ ap (add s) !add.comm ⬝ !add.assoc⁻¹, -- end - definition converges_to_sequence : (λn s, πₛ[n] (sfiber (f s))) ⟹ᵍ (λn, πₛ[n] (A (ub n))) := + definition convergent_exact_couple_sequence : (λn s, πₛ[n] (sfiber (f s))) ⟹ᵍ (λn, πₛ[n] (A (ub n))) := begin - fapply converges_to.mk, + fapply convergent_exact_couple.mk, { exact exact_couple_sequence }, { exact is_bounded_sequence }, { exact id }, diff --git a/cohomology/serre.hlean b/cohomology/serre.hlean index 79ac456..b4ccb97 100644 --- a/cohomology/serre.hlean +++ b/cohomology/serre.hlean @@ -174,11 +174,11 @@ section atiyah_hirzebruch definition atiyah_hirzebruch_convergence1 : (λn s, πₛ[n] (sfiber (spi_compose_left (λx, postnikov_smap (Y x) s)))) ⟹ᵍ (λn, πₛ[n] (spi X (λx, strunc s₀ (Y x)))) := - converges_to_sequence _ (λn, s₀) (λn, n - 1) atiyah_hirzebruch_lb atiyah_hirzebruch_ub + convergent_exact_couple_sequence _ (λn, s₀) (λn, n - 1) atiyah_hirzebruch_lb atiyah_hirzebruch_ub definition atiyah_hirzebruch_convergence2 : - (λn s, opH^-(n-s)[(x : X), πₛ[s] (Y x)]) ⟹ᵍ (λn, pH^-n[(x : X), Y x]) := - converges_to_g_isomorphism atiyah_hirzebruch_convergence1 + (λn s, opH^-(n-s)[(x : X), πₛ[s] (Y x)]) ⟹ᵍ (λn, pH^n[(x : X), Y x]) := + convergent_exact_couple_g_isomorphism (convergent_exact_couple_negate_inf atiyah_hirzebruch_convergence1) begin intro n s, refine _ ⬝g (parametrized_cohomology_isomorphism_shomotopy_group_spi _ idp)⁻¹ᵍ, @@ -189,7 +189,7 @@ section atiyah_hirzebruch end begin intro n, - refine _ ⬝g (parametrized_cohomology_isomorphism_shomotopy_group_spi _ idp)⁻¹ᵍ, + refine _ ⬝g (parametrized_cohomology_isomorphism_shomotopy_group_spi _ !neg_neg)⁻¹ᵍ, apply shomotopy_group_isomorphism_of_pequiv, intro k, exact ppi_pequiv_right (λx, ptrunc_pequiv (maxm2 (s₀ + k)) (Y x k)), end @@ -211,10 +211,10 @@ section atiyah_hirzebruch end definition atiyah_hirzebruch_convergence : - (λp q, opH^p[(x : X), πₛ[-q] (Y x)]) ⟹ᵍ (λn, pH^-n[(x : X), Y x]) := + (λp q, opH^p[(x : X), πₛ[-q] (Y x)]) ⟹ᵍ (λn, pH^n[(x : X), Y x]) := begin - note z := converges_to_reindex atiyah_hirzebruch_convergence2 atiyah_hirzebruch_base_change, - refine converges_to_g_isomorphism z _ (λn, by reflexivity), + note z := convergent_exact_couple_reindex atiyah_hirzebruch_convergence2 atiyah_hirzebruch_base_change, + refine convergent_exact_couple_g_isomorphism z _ (by intro n; reflexivity), intro p q, apply parametrized_cohomology_change_int, esimp, @@ -227,8 +227,8 @@ section unreduced_atiyah_hirzebruch definition unreduced_atiyah_hirzebruch_convergence {X : Type} (Y : X → spectrum) (s₀ : ℤ) (H : Πx, is_strunc s₀ (Y x)) : - (λp q, uopH^p[(x : X), πₛ[-q] (Y x)]) ⟹ᵍ (λn, upH^-n[(x : X), Y x]) := -converges_to_g_isomorphism + (λp q, uopH^p[(x : X), πₛ[-q] (Y x)]) ⟹ᵍ (λn, upH^n[(x : X), Y x]) := +convergent_exact_couple_g_isomorphism (@atiyah_hirzebruch_convergence X₊ (add_point_spectrum Y) s₀ (is_strunc_add_point_spectrum H)) begin intro p q, refine _ ⬝g !uopH_isomorphism_opH⁻¹ᵍ, @@ -248,9 +248,9 @@ section serre include H definition serre_convergence : - (λp q, uopH^p[(b : B), uH^q[F b, Y]]) ⟹ᵍ (λn, uH^-n[Σ(b : B), F b, Y]) := + (λp q, uopH^p[(b : B), uH^q[F b, Y]]) ⟹ᵍ (λn, uH^n[Σ(b : B), F b, Y]) := proof - converges_to_g_isomorphism + convergent_exact_couple_g_isomorphism (unreduced_atiyah_hirzebruch_convergence (λx, sp_ucotensor (F x) Y) s₀ (λx, is_strunc_sp_ucotensor s₀ (F x) H)) @@ -262,35 +262,35 @@ section serre end begin intro n, - refine unreduced_parametrized_cohomology_isomorphism_shomotopy_group_supi _ idp ⬝g _, - refine _ ⬝g (unreduced_cohomology_isomorphism_shomotopy_group_sp_ucotensor _ _ idp)⁻¹ᵍ, + refine unreduced_parametrized_cohomology_isomorphism_shomotopy_group_supi _ !neg_neg ⬝g _, + refine _ ⬝g (unreduced_cohomology_isomorphism_shomotopy_group_sp_ucotensor _ _ !neg_neg)⁻¹ᵍ, apply shomotopy_group_isomorphism_of_pequiv, intro k, exact (sigma_pumap F (Y k))⁻¹ᵉ* end qed definition serre_convergence_map : - (λp q, uopH^p[(b : B), uH^q[fiber f b, Y]]) ⟹ᵍ (λn, uH^-n[X, Y]) := + (λp q, uopH^p[(b : B), uH^q[fiber f b, Y]]) ⟹ᵍ (λn, uH^n[X, Y]) := proof - converges_to_g_isomorphism + convergent_exact_couple_g_isomorphism (serre_convergence (fiber f) Y s₀ H) begin intro p q, reflexivity end begin intro n, apply unreduced_cohomology_isomorphism, exact !sigma_fiber_equiv⁻¹ᵉ end qed definition serre_convergence_of_is_conn (H2 : is_conn 1 B) : - (λp q, uoH^p[B, uH^q[F b₀, Y]]) ⟹ᵍ (λn, uH^-n[Σ(b : B), F b, Y]) := + (λp q, uoH^p[B, uH^q[F b₀, Y]]) ⟹ᵍ (λn, uH^n[Σ(b : B), F b, Y]) := proof - converges_to_g_isomorphism + convergent_exact_couple_g_isomorphism (serre_convergence F Y s₀ H) begin intro p q, exact @uopH_isomorphism_uoH_of_is_conn (pointed.MK B b₀) _ _ H2 end begin intro n, reflexivity end qed definition serre_convergence_map_of_is_conn (H2 : is_conn 1 B) : - (λp q, uoH^p[B, uH^q[fiber f b₀, Y]]) ⟹ᵍ (λn, uH^-n[X, Y]) := + (λp q, uoH^p[B, uH^q[fiber f b₀, Y]]) ⟹ᵍ (λn, uH^n[X, Y]) := proof - converges_to_g_isomorphism + convergent_exact_couple_g_isomorphism (serre_convergence_of_is_conn b₀ (fiber f) Y s₀ H H2) begin intro p q, reflexivity end begin intro n, apply unreduced_cohomology_isomorphism, exact !sigma_fiber_equiv⁻¹ᵉ end