diff --git a/algebra/spectral_sequence.hlean b/algebra/spectral_sequence.hlean index d1af0f8..c092132 100644 --- a/algebra/spectral_sequence.hlean +++ b/algebra/spectral_sequence.hlean @@ -292,7 +292,8 @@ namespace left_module structure is_bounded {R : Ring} {I : AddAbGroup} (X : exact_couple R I) : Type := mk' :: (B B' : I → ℕ) (Dub : Π⦃x y⦄ ⦃s : ℕ⦄, (deg (i X))^[s] x = y → B x ≤ s → is_contr (D X y)) - (Dlb : Π⦃x y z⦄ ⦃s : ℕ⦄ (p : deg (i X) x = y), (deg (i X))^[s] y = z → B' z ≤ s → is_surjective (i X ↘ p)) + (Dlb : Π⦃x y z⦄ ⦃s : ℕ⦄ (p : deg (i X) x = y), (deg (i X))^[s] y = z → B' z ≤ s → + is_surjective (i X ↘ p)) (Elb : Π⦃x y⦄ ⦃s : ℕ⦄, (deg (i X))⁻¹ᵉ^[s] x = y → B x ≤ s → is_contr (E X y)) /- Note: Elb proves Dlb for some bound B', but we want tight control over when B' = 0 -/ @@ -495,22 +496,22 @@ namespace left_module parameters (x : I) - definition r (n : ℕ) : ℕ := + definition rb (n : ℕ) : ℕ := max (max (B (deg (j X) (deg (k X) x)) + n + 1) (B3 ((deg (i X))^[n] x))) (max (B' (deg (k X) ((deg (i X))^[n] x))) (max (B' (deg (k X) ((deg (i X))^[n+1] x))) (B ((deg (j X))⁻¹ ((deg (i X))^[n] x))))) - lemma rb0 (n : ℕ) : r n ≥ n + 1 := + lemma rb0 (n : ℕ) : rb n ≥ n + 1 := ge.trans !le_max_left (ge.trans !le_max_left !le_add_left) - lemma rb1 (n : ℕ) : B (deg (j X) (deg (k X) x)) ≤ r n - (n + 1) := + lemma rb1 (n : ℕ) : B (deg (j X) (deg (k X) x)) ≤ rb n - (n + 1) := nat.le_sub_of_add_le (le.trans !le_max_left !le_max_left) - lemma rb2 (n : ℕ) : B3 ((deg (i X))^[n] x) ≤ r n := + lemma rb2 (n : ℕ) : B3 ((deg (i X))^[n] x) ≤ rb n := le.trans !le_max_right !le_max_left - lemma rb3 (n : ℕ) : B' (deg (k X) ((deg (i X))^[n] x)) ≤ r n := + lemma rb3 (n : ℕ) : B' (deg (k X) ((deg (i X))^[n] x)) ≤ rb n := le.trans !le_max_left !le_max_right - lemma rb4 (n : ℕ) : B' (deg (k X) ((deg (i X))^[n+1] x)) ≤ r n := + lemma rb4 (n : ℕ) : B' (deg (k X) ((deg (i X))^[n+1] x)) ≤ rb n := le.trans (le.trans !le_max_left !le_max_right) !le_max_right - lemma rb5 (n : ℕ) : B ((deg (j X))⁻¹ ((deg (i X))^[n] x)) ≤ r n := + lemma rb5 (n : ℕ) : B ((deg (j X))⁻¹ ((deg (i X))^[n] x)) ≤ rb n := le.trans (le.trans !le_max_right !le_max_right) !le_max_right definition Einfdiag : graded_module R ℕ := @@ -520,24 +521,24 @@ namespace left_module λn, Dinf (deg (k X) ((deg (i X))^[n] x)) definition short_exact_mod_page_r (n : ℕ) : short_exact_mod - (E (page (r n)) ((deg (i X))^[n] x)) - (D (page (r n)) (deg (k (page (r n))) ((deg (i X))^[n] x))) - (D (page (r n)) (deg (i (page (r n))) (deg (k (page (r n))) ((deg (i X))^[n] x)))) := + (E (page (rb n)) ((deg (i X))^[n] x)) + (D (page (rb n)) (deg (k (page (rb n))) ((deg (i X))^[n] x))) + (D (page (rb n)) (deg (i (page (rb n))) (deg (k (page (rb n))) ((deg (i X))^[n] x)))) := begin fapply short_exact_mod_of_is_exact, - { exact j (page (r n)) ← ((deg (i X))^[n] x) }, - { exact k (page (r n)) ((deg (i X))^[n] x) }, - { exact i (page (r n)) (deg (k (page (r n))) ((deg (i X))^[n] x)) }, - { exact j (page (r n)) _ }, + { exact j (page (rb n)) ← ((deg (i X))^[n] x) }, + { exact k (page (rb n)) ((deg (i X))^[n] x) }, + { exact i (page (rb n)) (deg (k (page (rb n))) ((deg (i X))^[n] x)) }, + { exact j (page (rb n)) _ }, { apply is_contr_D, refine Dub !deg_j_inv⁻¹ (rb5 n) }, { apply is_contr_E, refine Elb _ (rb1 n), refine !deg_iterate_ij_commute ⬝ _, refine ap (deg (j X)) _ ⬝ !deg_j⁻¹, - refine iterate_sub _ !rb0 _ ⬝ _, apply ap (_^[r n]), + refine iterate_sub _ !rb0 _ ⬝ _, apply ap (_^[rb n]), exact ap (deg (i X)) (!deg_iterate_ik_commute ⬝ !deg_k⁻¹) ⬝ !deg_i⁻¹ }, - { apply jk (page (r n)) }, - { apply ki (page (r n)) }, - { apply ij (page (r n)) } + { apply jk (page (rb n)) }, + { apply ki (page (rb n)) }, + { apply ij (page (rb n)) } end definition short_exact_mod_infpage (n : ℕ) : @@ -573,6 +574,20 @@ namespace left_module (λs, Dinfdiag_stable) end + + definition deg_d_reindex {R : Ring} {I J : AddAbGroup} + (e : AddGroup_of_AddAbGroup J ≃g AddGroup_of_AddAbGroup I) (X : exact_couple R I) + (r : ℕ) : deg (d (page (exact_couple_reindex e X) r)) ~ + e⁻¹ᵍ ∘ deg (d (page X r)) ∘ e := + begin + intro x, refine !deg_d ⬝ _ ⬝ ap e⁻¹ᵍ !deg_d⁻¹, + apply ap (e⁻¹ᵍ ∘ deg (j X)), + note z := @iterate_hsquare _ _ (deg (i (exact_couple_reindex e X)))⁻¹ᵉ (deg (i X))⁻¹ᵉ e + (λx, proof to_right_inv (group.equiv_of_isomorphism e) _ qed)⁻¹ʰᵗʸʰ r, + refine z _ ⬝ _, apply ap ((deg (i X))⁻¹ᵉ^[r]), + exact to_right_inv (group.equiv_of_isomorphism e) _ + end + end convergence_theorem open int group prod convergence_theorem prod.ops @@ -592,12 +607,12 @@ namespace left_module (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) - (s₀ : agℤ → agℤ) - (HB : Π(n : agℤ), is_bounded.B' HH (deg (k X) (n, s₀ n)) = 0) + (s₁ : agℤ → agℤ) (s₂ : agℤ → agℤ) + (HB : Π(n : agℤ), is_bounded.B' HH (deg (k X) (s₁ n, s₂ n)) = 0) (e : Π(x : Z2), exact_couple.E X x ≃lm E' x.1 x.2) - (f : Π(n : agℤ), exact_couple.D X (deg (k X) (n, s₀ n)) ≃lm Dinf n) + (f : Π(n : agℤ), exact_couple.D X (deg (k X) (s₁ n, s₂ n)) ≃lm Dinf n) (deg_d1 : ℕ → agℤ) (deg_d2 : ℕ → agℤ) - (deg_d_eq : Π(r : ℕ) (n s : agℤ), deg (d (page X r)) (n, s) = (n, s) + (deg_d1 r, deg_d2 r)) + (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)} := @@ -622,9 +637,14 @@ namespace left_module local abbreviation X := X c local abbreviation i := i X local abbreviation HH := HH c - local abbreviation s₀ := s₀ c - local abbreviation Dinfdiag (n : agℤ) (k : ℕ) := Dinfdiag HH (n, s₀ n) k - local abbreviation Einfdiag (n : agℤ) (k : ℕ) := Einfdiag HH (n, s₀ n) k + local abbreviation s₁ := s₁ c + local abbreviation s₂ := s₂ c + local abbreviation Dinfdiag (n : agℤ) (k : ℕ) := Dinfdiag HH (s₁ n, s₂ n) k + local abbreviation Einfdiag (n : agℤ) (k : ℕ) := Einfdiag HH (s₁ n, s₂ n) k + + definition deg_d_eq (r : ℕ) (n s : agℤ) : + (deg (d (page X r))) (n, s) = (n + deg_d1 c r, s + deg_d2 c r) := + !deg_eq ⬝ ap (λx, _ + x) (deg_d_eq0 c r) definition deg_d_inv_eq (r : ℕ) (n s : agℤ) : (deg (d (page X r)))⁻¹ᵉ (n, s) = (n - deg_d1 c r, s - deg_d2 c r) := @@ -632,16 +652,38 @@ namespace left_module definition converges_to_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₀ (HB c) + converges_to.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 n s, deg_d_eq c r n s) + (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) := + begin + fapply converges_to.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, + refine to_right_inv (group.equiv_of_isomorphism i) _ ⬝ _, + apply ap (deg (k X)), exact ap i !prod.eta ⬝ to_right_inv (group.equiv_of_isomorphism i) _ }, + { intro x, induction x with p q, exact e c (i (p, q)) }, + { intro n, refine _ ⬝lm f c n, refine isomorphism_of_eq (ap (D X) _), + refine to_right_inv (group.equiv_of_isomorphism i) _ ⬝ _, + apply ap (deg (k X)), exact ap i !prod.eta ⬝ to_right_inv (group.equiv_of_isomorphism i) _ }, + { exact λn, (i⁻¹ᵍ (deg_d1 c n, deg_d2 c n)).1 }, + { exact λn, (i⁻¹ᵍ (deg_d1 c n, deg_d2 c n)).2 }, + { 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 + omit c /- definition converges_to_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₀ + converges_to.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-/ @@ -651,17 +693,17 @@ namespace left_module (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) - (λn, -s₀ (-n)) + (λ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) := - is_built_from_isomorphism_left (f c n) (is_built_from_infpage HH (n, s₀ n) (HB c 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ℤ) - (H : Π(n : agℤ) (l : ℕ), is_contr (E' ((deg i)^[l] (n, s₀ n)).1 ((deg i)^[l] (n, s₀ n)).2)) : + (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 assert H2 : Π(l : ℕ), is_contr (Einfdiag n l), @@ -669,13 +711,13 @@ namespace left_module refine is_trunc_equiv_closed_rev -2 (equiv_of_isomorphism (e c _)) (H n l) }, assert H3 : is_contr (Dinfdiag n 0), { fapply nat.rec_down (λk, is_contr (Dinfdiag n k)), - { exact is_bounded.B HH (deg (k X) (n, s₀ n)) }, + { exact is_bounded.B HH (deg (k X) (s₁ n, s₂ n)) }, { apply Dinfdiag_stable, reflexivity }, { intro l H, - exact is_contr_middle_of_short_exact_mod (short_exact_mod_infpage HH (n, s₀ n) l) + exact is_contr_middle_of_short_exact_mod (short_exact_mod_infpage HH (s₁ n, s₂ n) l) (H2 l) H }}, refine is_trunc_equiv_closed _ _ H3, - exact equiv_of_isomorphism (Dinfdiag0 HH (n, s₀ n) (HB c n) ⬝lm f c n) + 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) := @@ -686,7 +728,7 @@ namespace left_module (H2 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X (n + deg_d1 c r, s + deg_d2 c r))) : E (page X r₂) (n, s) ≃lm E (page X r₁) (n, s) := E_isomorphism' X H (λr Hr₁ Hr₂, transport (is_contr ∘ E X) (deg_d_inv_eq r n s)⁻¹ᵖ (H1 Hr₁ Hr₂)) - (λr Hr₁ Hr₂, transport (is_contr ∘ E X) (deg_d_eq c r n s)⁻¹ᵖ (H2 Hr₁ Hr₂)) + (λr Hr₁ Hr₂, transport (is_contr ∘ E X) (deg_d_eq r n s)⁻¹ᵖ (H2 Hr₁ Hr₂)) definition E_isomorphism0 {r : ℕ} {n s : agℤ} (H1 : Πr, is_contr (E X (n - deg_d1 c r, s - deg_d2 c r))) @@ -699,7 +741,7 @@ namespace left_module (H2 : Π⦃r⦄, r₁ ≤ r → is_contr (E X (n + deg_d1 c r, s + deg_d2 c r))) : Einf HH (n, s) ≃lm E (page X r₁) (n, s) := Einf_isomorphism' HH r₁ (λr Hr₁, transport (is_contr ∘ E X) (deg_d_inv_eq r n s)⁻¹ᵖ (H1 Hr₁)) - (λr Hr₁, transport (is_contr ∘ E X) (deg_d_eq c r n s)⁻¹ᵖ (H2 Hr₁)) + (λr Hr₁, transport (is_contr ∘ E X) (deg_d_eq r n s)⁻¹ᵖ (H2 Hr₁)) definition Einf_isomorphism0 {n s : agℤ} (H1 : Π⦃r⦄, is_contr (E X (n - deg_d1 c r, s - deg_d2 c r))) @@ -921,15 +963,16 @@ namespace spectrum fapply converges_to.mk, { exact exact_couple_sequence }, { exact is_bounded_sequence }, + { exact id }, { exact ub }, { 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 : ℤ) }, { intro r, exact r + (1 : ℤ) }, - { intro r n s, refine !convergence_theorem.deg_d ⬝ _, + { intro r, refine !convergence_theorem.deg_d ⬝ _, refine ap (deg j_sequence) !iterate_deg_i_inv ⬝ _, - exact prod_eq idp (!add.assoc ⬝ ap (λx, s + (r + x)) !neg_neg) }, + exact prod_eq idp !zero_add } end end diff --git a/cohomology/serre.hlean b/cohomology/serre.hlean index 8e271df..625b1d7 100644 --- a/cohomology/serre.hlean +++ b/cohomology/serre.hlean @@ -1,7 +1,7 @@ import ..algebra.spectral_sequence ..spectrum.trunc .basic open eq spectrum trunc is_trunc pointed int EM algebra left_module fiber lift equiv is_equiv - cohomology group sigma unit is_conn + cohomology group sigma unit is_conn prod set_option pp.binder_types true /- Eilenberg MacLane spaces are the fibers of the Postnikov system of a type -/ @@ -171,14 +171,14 @@ section atiyah_hirzebruch definition is_bounded_atiyah_hirzebruch : is_bounded atiyah_hirzebruch_exact_couple := is_bounded_sequence _ (λn, s₀) (λn, n - 1) atiyah_hirzebruch_lb atiyah_hirzebruch_ub - definition atiyah_hirzebruch_convergence' : + 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 - definition atiyah_hirzebruch_convergence : + 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_convergence' + converges_to_g_isomorphism atiyah_hirzebruch_convergence1 begin intro n s, refine _ ⬝g (parametrized_cohomology_isomorphism_shomotopy_group_spi _ idp)⁻¹ᵍ, @@ -194,11 +194,32 @@ section atiyah_hirzebruch exact ppi_pequiv_right (λx, ptrunc_pequiv (maxm2 (s₀ + k)) (Y x k)), end --- set_option pp.metavar_args true --- definition atiyah_reindexed : (λp q, opH^p[(x : X), πₛ[q] (Y x)]) ⟹ᵍ (λn, pH^n[(x : X), Y x]) --- := --- converges_to_reindex atiyah_hirzebruch_convergence (λp q, -(p - q)) (λp q, q) (λp q, by reflexivity) --- (λn, -n) (λn, by reflexivity) + open prod.ops + definition atiyah_hirzebruch_base_change [constructor] : agℤ ×ag agℤ ≃g agℤ ×ag agℤ := + begin + fapply group.isomorphism.mk, + { fapply group.homomorphism.mk, exact (λpq, (-(pq.1 + pq.2), -pq.2)), + intro pq pq', + induction pq with p q, induction pq' with p' q', esimp, + exact prod_eq (ap neg !add.comm4 ⬝ !neg_add) !neg_add }, + { fapply adjointify, + { exact (λns, (ns.2 - ns.1, -ns.2)) }, + { intro ns, esimp, + exact prod_eq (ap neg (!add.comm ⬝ !neg_add_cancel_left) ⬝ !neg_neg) !neg_neg }, + { intro pq, esimp, + exact prod_eq (ap (λx, _ + x) !neg_neg ⬝ !add.comm ⬝ !add_neg_cancel_right) !neg_neg }} + end + + definition atiyah_hirzebruch_convergence : + (λ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), + intro p q, + apply parametrized_cohomology_change_int, + esimp, + refine !neg_neg_sub_neg ⬝ !add_neg_cancel_right + end end atiyah_hirzebruch @@ -206,11 +227,11 @@ section unreduced_atiyah_hirzebruch definition unreduced_atiyah_hirzebruch_convergence {X : Type} (Y : X → spectrum) (s₀ : ℤ) (H : Πx, is_strunc s₀ (Y x)) : - (λn s, uopH^-(n-s)[(x : X), πₛ[s] (Y x)]) ⟹ᵍ (λn, upH^-n[(x : X), Y x]) := + (λp q, uopH^p[(x : X), πₛ[-q] (Y x)]) ⟹ᵍ (λn, upH^-n[(x : X), Y x]) := converges_to_g_isomorphism (@atiyah_hirzebruch_convergence X₊ (add_point_spectrum Y) s₀ (is_strunc_add_point_spectrum H)) begin - intro n s, refine _ ⬝g !uopH_isomorphism_opH⁻¹ᵍ, + intro p q, refine _ ⬝g !uopH_isomorphism_opH⁻¹ᵍ, apply ordinary_parametrized_cohomology_isomorphism_right, intro x, apply shomotopy_group_add_point_spectrum @@ -227,17 +248,17 @@ section serre include H definition serre_convergence : - (λn s, uopH^-(n-s)[(b : B), uH^-s[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 (unreduced_atiyah_hirzebruch_convergence (λx, sp_ucotensor (F x) Y) s₀ (λx, is_strunc_sp_ucotensor s₀ (F x) H)) begin - intro n s, - refine unreduced_ordinary_parametrized_cohomology_isomorphism_right _ (-(n-s)), + intro p q, + refine unreduced_ordinary_parametrized_cohomology_isomorphism_right _ p, intro x, - exact (unreduced_cohomology_isomorphism_shomotopy_group_sp_ucotensor _ _ idp)⁻¹ᵍ + exact (unreduced_cohomology_isomorphism_shomotopy_group_sp_ucotensor _ _ !neg_neg)⁻¹ᵍ end begin intro n, @@ -249,29 +270,29 @@ section serre qed definition serre_convergence_map : - (λn s, uopH^-(n-s)[(b : B), uH^-s[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 (serre_convergence (fiber f) Y s₀ H) - begin intro n s, reflexivity end + 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) : - (λn s, uoH^-(n-s)[B, uH^-s[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 (serre_convergence F Y s₀ H) - begin intro n s, exact @uopH_isomorphism_uoH_of_is_conn (pointed.MK B b₀) _ _ H2 end + 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) : - (λn s, uoH^-(n-s)[B, uH^-s[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 (serre_convergence_of_is_conn b₀ (fiber f) Y s₀ H H2) - begin intro n s, reflexivity end + begin intro p q, reflexivity end begin intro n, apply unreduced_cohomology_isomorphism, exact !sigma_fiber_equiv⁻¹ᵉ end qed