From acae548d3a5b910442db99af5a73540795da6745 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 26 Sep 2018 19:53:23 +0200 Subject: [PATCH] some cleanup, and add a todo list --- algebra/product_group.hlean | 9 ++++++++ algebra/spectral_sequence.hlean | 40 ++++++++++++++++----------------- cohomology/serre.hlean | 1 - move_to_lib.hlean | 4 ++++ 4 files changed, 33 insertions(+), 21 deletions(-) diff --git a/algebra/product_group.hlean b/algebra/product_group.hlean index 6e1d966..ad61754 100644 --- a/algebra/product_group.hlean +++ b/algebra/product_group.hlean @@ -58,8 +58,17 @@ namespace group definition ab_product [constructor] (G G' : AbGroup) : AbGroup := AbGroup.mk _ (ab_group_prod G G') + definition add_product [constructor] (G G' : AddGroup) : AddGroup := + group.product G G' + + definition add_ab_product [constructor] (G G' : AddAbGroup) : AddAbGroup := + group.ab_product G G' + infix ` ×g `:60 := group.product infix ` ×ag `:60 := group.ab_product + infix ` ×a `:60 := group.add_product + infix ` ×aa `:60 := group.add_ab_product + definition product_inl [constructor] (G H : Group) : G →g G ×g H := homomorphism.mk (λx, (x, one)) (λx y, prod_eq !refl !one_mul⁻¹) diff --git a/algebra/spectral_sequence.hlean b/algebra/spectral_sequence.hlean index c092132..f0702e8 100644 --- a/algebra/spectral_sequence.hlean +++ b/algebra/spectral_sequence.hlean @@ -592,17 +592,8 @@ namespace left_module open int group prod convergence_theorem prod.ops - definition Z2 [constructor] : AddAbGroup := agℤ ×ag agℤ + definition Z2 [constructor] : AddAbGroup := agℤ ×aa agℤ - -- set_option pp.coercions true - -- set_option pp.binder_types true - - -- todo: move - definition AddAbGroup.struct2 [instance] (G : AddAbGroup) : - add_ab_group (algebra._trans_of_Group_of_AbGroup_2 G) := - AddAbGroup.struct G - - /- TODO: redefine/generalize converges_to so that it supports the usual indexing on ℤ × ℤ -/ structure converges_to.{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) @@ -614,16 +605,6 @@ 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)) - structure converging_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) - (α : Π(n : ℕ) (x : Z2), E (n+1) x ≃lm graded_homology (d n) (d n) x) - (e : Π(n : ℕ) (x : Z2), E 0 x ≃lm E' x.1 x.2) - (s₀ : Z2 → ℕ) - (f : Π{n : ℕ} {x : Z2} (h : s₀ x ≤ n), E (s₀ x) x ≃lm E n x) - (HDinf : Π(n : agℤ), is_built_from (Dinf n) (λ(k : ℕ), (λx, E (s₀ x) x) (k, n - k))) - infix ` ⟹ `:25 := converges_to definition converges_to_g [reducible] (E' : agℤ → agℤ → AbGroup) (Dinf : agℤ → AbGroup) : Type := @@ -757,6 +738,25 @@ namespace left_module converges_to_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) + (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) + (α : Π(n : ℕ) (x : Z2), E (n+1) x ≃lm graded_homology (d n) (d n) x) + (e : Π(n : ℕ) (x : Z2), E 0 x ≃lm E' x.1 x.2) + (s₀ : Z2 → ℕ) + (f : Π{n : ℕ} {x : Z2} (h : s₀ x ≤ n), E (s₀ x) x ≃lm E n x) + (lb : ℤ → ℤ) + (HDinf : Π(n : agℤ), is_built_from (Dinf n) (λ(k : ℕ), (λx, E (s₀ x) x) (k + lb n, n - (k + lb n)))) + + /- + 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 (with the additional hypothesis that the degree of i is (1, -1) or something) + - redefine `⟹` to be a converging spectral sequence + -/ + end left_module open left_module namespace pointed diff --git a/cohomology/serre.hlean b/cohomology/serre.hlean index 625b1d7..441a540 100644 --- a/cohomology/serre.hlean +++ b/cohomology/serre.hlean @@ -296,7 +296,6 @@ section serre begin intro n, apply unreduced_cohomology_isomorphism, exact !sigma_fiber_equiv⁻¹ᵉ end qed - end serre diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 63e94e6..282f919 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -7,6 +7,10 @@ open eq nat int susp pointed sigma is_equiv equiv fiber algebra trunc pi group universe variable u + definition AddAbGroup.struct2 [instance] (G : AddAbGroup) : + add_ab_group (algebra._trans_of_Group_of_AbGroup_2 G) := + AddAbGroup.struct G + namespace eq definition transport_lemma {A : Type} {C : A → Type} {g₁ : A → A}