From c19192fbe52208f78d34e869af000fb0e4aea128 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 3 Oct 2018 17:14:37 -0400 Subject: [PATCH] fix error with numerals in integers --- algebra/exact_couple.hlean | 17 +++++++++-------- algebra/ring.hlean | 16 ++++++++++++---- algebra/spectral_sequence.hlean | 6 +++--- cohomology/serre.hlean | 16 ++++++++++++++++ homotopy/EMRing.hlean | 6 +++--- 5 files changed, 43 insertions(+), 18 deletions(-) diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean index 32833e1..1d4321c 100644 --- a/algebra/exact_couple.hlean +++ b/algebra/exact_couple.hlean @@ -5,7 +5,7 @@ -- Author: Floris van Doorn -import .graded ..spectrum.basic .product_group +import .graded ..spectrum.basic .product_group .ring open algebra is_trunc left_module is_equiv equiv eq function nat sigma set_quotient group left_module @@ -535,7 +535,8 @@ namespace exact_couple open int group prod convergence_theorem prod.ops - definition Z2 [constructor] : AddAbGroup := agℤ ×aa agℤ + local attribute [coercion] AddAbGroup_of_Ring + definition Z2 [constructor] : AddAbGroup := rℤ ×aa 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)} := @@ -722,7 +723,7 @@ namespace spectrum definition i_sequence : D_sequence →gm D_sequence := begin - fapply graded_hom.mk, exact (prod_equiv_prod erfl (add_right_action (- (1 : ℤ)))), + fapply graded_hom.mk, exact (prod_equiv_prod erfl (add_right_action (- 1))), { intro i, exact pair_eq !add_zero⁻¹ idp }, intro v, apply lm_hom_int.mk, esimp, @@ -730,7 +731,7 @@ namespace spectrum end definition deg_j_seq_inv [constructor] : I ≃ I := - prod_equiv_prod (add_right_action (1 : ℤ)) (add_right_action (- (1 : ℤ))) + prod_equiv_prod (add_right_action 1) (add_right_action (- 1)) definition fn_j_sequence [unfold 3] (x : I) : D_sequence (deg_j_seq_inv x) →lm E_sequence x := @@ -759,7 +760,7 @@ namespace spectrum intro y, induction x with n s, induction y with m t, refine equiv_rect !pair_eq_pair_equiv⁻¹ᵉ _ _, intro pq, esimp at pq, induction pq with p q, - revert t q, refine eq.rec_equiv (add_right_action (-(1 : ℤ))) _, + revert t q, refine eq.rec_equiv (add_right_action (- 1)) _, induction p using eq.rec_symm, apply is_exact_homotopy homotopy.rfl, { symmetry, exact graded_hom_mk_out_destruct deg_j_seq_inv⁻¹ᵉ (λi, idp) fn_j_sequence }, @@ -789,7 +790,7 @@ namespace spectrum open int parameters (ub : ℤ → ℤ) (lb : ℤ → ℤ) - (Aub : Π(s n : ℤ), s ≥ ub n + (1 : ℤ) → is_equiv (πₛ→[n] (f s))) + (Aub : Π(s n : ℤ), s ≥ ub n + 1 → is_equiv (πₛ→[n] (f s))) (Alb : Π(s n : ℤ), s ≤ lb n → is_contr (πₛ[n] (A s))) definition B : I → ℕ @@ -799,7 +800,7 @@ namespace spectrum | (n, s) := max0 (ub n - s) definition B'' : I → ℕ - | (n, s) := max0 (max (ub n + (1 : ℤ) - s) (ub (n+(1 : ℤ)) + (1 : ℤ) - s)) + | (n, s) := max0 (max (ub n + 1 - s) (ub (n+1) + 1 - s)) lemma iterate_deg_i (n s : ℤ) (m : ℕ) : (deg i_sequence)^[m] (n, s) = (n, s - m) := begin @@ -862,7 +863,7 @@ namespace spectrum { intro n, change max0 (ub n - ub n) = 0, exact ap max0 (sub_self (ub n)) }, { intro ns, reflexivity }, { intro n, reflexivity }, - { intro r, exact (-(1 : ℤ), r + (1 : ℤ)) }, + { intro r, exact (- 1, r + 1) }, { intro r, refine !convergence_theorem.deg_dr ⬝ _, refine ap (deg j_sequence) !iterate_deg_i_inv ⬝ _, exact prod_eq idp !zero_add } diff --git a/algebra/ring.hlean b/algebra/ring.hlean index be89caf..97ee0f6 100644 --- a/algebra/ring.hlean +++ b/algebra/ring.hlean @@ -5,14 +5,22 @@ import algebra.ring .direct_sum ..heq ..move_to_lib open algebra group eq is_trunc sigma namespace algebra -definition AbGroup_of_Ring [constructor] (R : Ring) : AbGroup := -AbGroup.mk R (add_ab_group_of_ring R) +definition AddAbGroup_of_Ring [constructor] (R : Ring) : AddAbGroup := +AddAbGroup.mk R (add_ab_group_of_ring R) -definition ring_AbGroup_of_Ring [instance] (R : Ring) : ring (AbGroup_of_Ring R) := +definition AddGroup_of_Ring [constructor] (R : Ring) : AddGroup := +AddGroup.mk R (add_group_of_add_ab_group R) + +definition ring_AddAbGroup_of_Ring [instance] (R : Ring) : ring (AddAbGroup_of_Ring R) := Ring.struct R +/- we give the following instance very high priority, otherwise type class inference would sometimes find the additive structure of R as the group structure. -/ +definition monoid_AddAbGroup_of_Ring [instance] [priority 3000] [constructor] (R : Ring) : + monoid (Group_of_AbGroup (AddAbGroup_of_Ring R)) := +@monoid_of_ring _ (Ring.struct R) + definition ring_right_action [constructor] {R : Ring} (r : R) : - AbGroup_of_Ring R →g AbGroup_of_Ring R := + AddAbGroup_of_Ring R →a AddAbGroup_of_Ring R := homomorphism.mk (λs, s * r) (λs s', !right_distrib) definition ring_of_ab_group [constructor] (G : Type) [ab_group G] (m : G → G → G) (o : G) diff --git a/algebra/spectral_sequence.hlean b/algebra/spectral_sequence.hlean index 9a33df5..cc0dda3 100644 --- a/algebra/spectral_sequence.hlean +++ b/algebra/spectral_sequence.hlean @@ -36,7 +36,7 @@ convergent_spectral_sequence (λn s, LeftModule_int_of_AbGroup (E' n s)) definition convergent_spectral_sequence_of_exact_couple {R : Ring} {E' : agℤ → agℤ → LeftModule R} {Dinf : agℤ → LeftModule R} (c : convergent_exact_couple E' Dinf) - (st_eq : Πn, (st c n).1 + (st c n).2 = n) (deg_i_eq : deg (i (X c)) 0 = (-(1 : ℤ), (1 : ℤ))) : + (st_eq : Πn, (st c n).1 + (st c n).2 = n) (deg_i_eq : deg (i (X c)) 0 = (- 1, 1)) : convergent_spectral_sequence E' Dinf := convergent_spectral_sequence.mk (λr, E (page (X c) r)) (λr, d (page (X c) r)) (deg_d c) (deg_d_eq0 c) @@ -49,8 +49,8 @@ convergent_spectral_sequence (λn s, LeftModule_int_of_AbGroup (E' n s)) induction p with p IH, { exact !prod.eta⁻¹ ⬝ prod_eq (eq_sub_of_add_eq (ap (add _) !zero_add ⬝ st_eq n)) (zero_add (st c n).2)⁻¹ }, - { assert H1 : Π(a : ℤ), n - (p + a) - (1 : ℤ) = n - (succ p + a), - exact λa, !sub_add_eq_sub_sub⁻¹ ⬝ ap (sub n) (add_comm_middle p a (1 : ℤ) ⬝ proof idp qed), + { assert H1 : Π(a : ℤ), n - (p + a) - 1 = n - (succ p + a), + exact λa, !sub_add_eq_sub_sub⁻¹ ⬝ ap (sub n) (add_comm_middle p a 1 ⬝ proof idp qed), assert H2 : Π(a : ℤ), p + a + 1 = succ p + a, exact λa, add_comm_middle p a 1, refine ap (deg (i (X c))) IH ⬝ !deg_eq ⬝ ap (add _) deg_i_eq ⬝ prod_eq !H1 !H2 } diff --git a/cohomology/serre.hlean b/cohomology/serre.hlean index 6059149..e6c6ab4 100644 --- a/cohomology/serre.hlean +++ b/cohomology/serre.hlean @@ -232,6 +232,22 @@ section atiyah_hirzebruch { reflexivity } end +/- + to unfold a field of atiyah_hirzebruch_spectral_sequence: + esimp [atiyah_hirzebruch_spectral_sequence, convergent_spectral_sequence_of_exact_couple, + atiyah_hirzebruch_convergence, convergent_exact_couple_g_isomorphism, + convergent_exact_couple_isomorphism, convergent_exact_couple_reindex, + atiyah_hirzebruch_convergence2, convergent_exact_couple_negate_abutment, + atiyah_hirzebruch_convergence1, convergent_exact_couple_sequence], + +-/ + definition AHSS_deg_d (r : ℕ) : + convergent_spectral_sequence.deg_d atiyah_hirzebruch_spectral_sequence r = + (r + 2, -(r + 1)) := + begin + reflexivity + end + end atiyah_hirzebruch section unreduced_atiyah_hirzebruch diff --git a/homotopy/EMRing.hlean b/homotopy/EMRing.hlean index 9093f1c..b85a7d4 100644 --- a/homotopy/EMRing.hlean +++ b/homotopy/EMRing.hlean @@ -8,10 +8,10 @@ namespace EM definition EM1product_adj {R : Ring} : - EM1 (AbGroup_of_Ring R) →* ppmap (EM1 (AbGroup_of_Ring R)) (EMadd1 (AbGroup_of_Ring R) 1) := + EM1 (AddGroup_of_Ring R) →* ppmap (EM1 (AddGroup_of_Ring R)) (EMadd1 (AddAbGroup_of_Ring R) 1) := begin - have is_trunc 1 (ppmap (EM1 (AbGroup_of_Ring R)) (EMadd1 (AbGroup_of_Ring R) 1)), - from is_trunc_pmap_of_is_conn _ _ _ _ _ _ (le.refl 2) !is_trunc_EMadd1, + have is_trunc 1 (ppmap (EM1 (AddGroup_of_Ring R)) (EMadd1 (AddAbGroup_of_Ring R) 1)), + from is_trunc_pmap_of_is_conn _ _ !is_conn_EM1 _ _ _ (le.refl 2) !is_trunc_EMadd1, apply EM1_pmap, fapply inf_homomorphism.mk, { intro r, refine pfunext _ _, exact !loop_EM2⁻¹ᵉ* ∘* EM1_functor (ring_right_action r), }, { intro r r', exact sorry }