michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

reindex the AHSS and SSS

Browse source 
Now the 2nd page is the correct indexing.
This commit is contained in:
Floris van Doorn 2018-09-26 13:12:33 +02:00
parent 4d3053daff
commit f9ce395b1c
2 changed files with 124 additions and 60 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

121
algebra/spectral_sequence.hlean
View file

@ -292,7 +292,8 @@ namespace left_module
structure is_bounded {R : Ring} {I : AddAbGroup} (X : exact_couple R I) : Type := structure is_bounded {R : Ring} {I : AddAbGroup} (X : exact_couple R I) : Type :=
mk' :: (B B' : I → ℕ) mk' :: (B B' : I → ℕ)
(Dub : Π⦃x y⦄ ⦃s : ℕ⦄, (deg (i X))^[s] x = y → B x ≤ s → is_contr (D X y)) (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)) (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 -/ /- 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) 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 (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] x)))
(max (B' (deg (k X) ((deg (i X))^[n+1] x))) (B ((deg (j 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) 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) 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 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 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 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 le.trans (le.trans !le_max_right !le_max_right) !le_max_right
definition Einfdiag : graded_module R ℕ := definition Einfdiag : graded_module R ℕ :=
@ -520,24 +521,24 @@ namespace left_module
λn, Dinf (deg (k X) ((deg (i X))^[n] x)) λn, Dinf (deg (k X) ((deg (i X))^[n] x))
definition short_exact_mod_page_r (n : ℕ) : short_exact_mod definition short_exact_mod_page_r (n : ℕ) : short_exact_mod
(E (page (r n)) ((deg (i X))^[n] x)) (E (page (rb n)) ((deg (i X))^[n] x))
(D (page (r n)) (deg (k (page (r n))) ((deg (i X))^[n] x))) (D (page (rb n)) (deg (k (page (rb 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)))) := (D (page (rb n)) (deg (i (page (rb n))) (deg (k (page (rb n))) ((deg (i X))^[n] x)))) :=
begin begin
fapply short_exact_mod_of_is_exact, fapply short_exact_mod_of_is_exact,
{ exact j (page (r n)) ← ((deg (i X))^[n] x) }, { exact j (page (rb n)) ← ((deg (i X))^[n] x) },
{ exact k (page (r n)) ((deg (i X))^[n] x) }, { exact k (page (rb n)) ((deg (i X))^[n] x) },
{ exact i (page (r n)) (deg (k (page (r n))) ((deg (i X))^[n] x)) }, { exact i (page (rb n)) (deg (k (page (rb n))) ((deg (i X))^[n] x)) },
{ exact j (page (r n)) _ }, { exact j (page (rb n)) _ },
{ apply is_contr_D, refine Dub !deg_j_inv⁻¹ (rb5 n) }, { apply is_contr_D, refine Dub !deg_j_inv⁻¹ (rb5 n) },
{ apply is_contr_E, refine Elb _ (rb1 n), { apply is_contr_E, refine Elb _ (rb1 n),
refine !deg_iterate_ij_commute ⬝ _, refine !deg_iterate_ij_commute ⬝ _,
refine ap (deg (j X)) _ ⬝ !deg_j⁻¹, 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⁻¹ }, exact ap (deg (i X)) (!deg_iterate_ik_commute ⬝ !deg_k⁻¹) ⬝ !deg_i⁻¹ },
{ apply jk (page (r n)) }, { apply jk (page (rb n)) },
{ apply ki (page (r n)) }, { apply ki (page (rb n)) },
{ apply ij (page (r n)) } { apply ij (page (rb n)) }
end end
definition short_exact_mod_infpage (n : ℕ) : definition short_exact_mod_infpage (n : ℕ) :
@ -573,6 +574,20 @@ namespace left_module
(λs, Dinfdiag_stable) (λs, Dinfdiag_stable)
end 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 end convergence_theorem
open int group prod convergence_theorem prod.ops 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)} := (Dinf : agℤ → LeftModule.{u w} R) : Type.{max u (v+1) (w+1)} :=
(X : exact_couple.{u 0 w v} R Z2) (X : exact_couple.{u 0 w v} R Z2)
(HH : is_bounded X) (HH : is_bounded X)
(s₀ : agℤ → agℤ) (s₁ : agℤ → agℤ) (s₂ : agℤ → agℤ)
(HB : Π(n : agℤ), is_bounded.B' HH (deg (k X) (n, s₀ n)) = 0) (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) (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_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) 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)} := (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 X := X c
local abbreviation i := i X local abbreviation i := i X
local abbreviation HH := HH c local abbreviation HH := HH c
local abbreviation s₀ := s₀ c local abbreviation s₁ := s₁ c
local abbreviation Dinfdiag (n : agℤ) (k : ℕ) := Dinfdiag HH (n, s₀ n) k local abbreviation s₂ := s₂ c
local abbreviation Einfdiag (n : agℤ) (k : ℕ) := Einfdiag HH (n, s₀ n) k 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ℤ) : 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) := (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ℤ} 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' := (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 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) (λ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ℤ} /- 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) (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)) : (i2 : agℤ ≃ agℤ) (f' : Πn, Dinf n ≃lm Dinf' (i2 n)) :
(λp q, E'' p q) ⟹ λn, Dinf' 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 --(λ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 --begin intro x, induction x with p q, exact e c (p, q) ⬝lm e' p q end
sorry-/ sorry-/
@ -651,17 +693,17 @@ namespace left_module
(f' : Πn, Dinf n ≃lm Dinf' (-n)) : (f' : Πn, Dinf n ≃lm Dinf' (-n)) :
(λp q, E'' p q) ⟹ λn, 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) 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) (λ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 --begin intro x, induction x with p q, exact e c (p, q) ⬝lm e' p q end
sorry-/ sorry-/
definition is_built_from_of_converges_to (n : ℤ) : is_built_from (Dinf n) (Einfdiag n) := 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 -/ /- TODO: reprove this using is_built_of -/
theorem is_contr_converges_to_precise (n : agℤ) 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) := is_contr (Dinf n) :=
begin begin
assert H2 : Π(l : ℕ), is_contr (Einfdiag n l), 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) }, refine is_trunc_equiv_closed_rev -2 (equiv_of_isomorphism (e c _)) (H n l) },
assert H3 : is_contr (Dinfdiag n 0), assert H3 : is_contr (Dinfdiag n 0),
{ fapply nat.rec_down (λk, is_contr (Dinfdiag n k)), { 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 }, { apply Dinfdiag_stable, reflexivity },
{ intro l H, { 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 }}, (H2 l) H }},
refine is_trunc_equiv_closed _ _ H3, 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 end
theorem is_contr_converges_to (n : agℤ) (H : Π(n s : agℤ), is_contr (E' n s)) : is_contr (Dinf n) := 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))) : (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 (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₂)) 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ℤ} definition E_isomorphism0 {r : ℕ} {n s : agℤ}
(H1 : Πr, is_contr (E X (n - deg_d1 c r, s - deg_d2 c r))) (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))) : (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 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₁)) 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ℤ} definition Einf_isomorphism0 {n s : agℤ}
(H1 : Π⦃r⦄, is_contr (E X (n - deg_d1 c r, s - deg_d2 c r))) (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, fapply converges_to.mk,
{ exact exact_couple_sequence }, { exact exact_couple_sequence },
{ exact is_bounded_sequence }, { exact is_bounded_sequence },
{ exact id },
{ exact ub }, { exact ub },
{ intro n, change max0 (ub n - ub n) = 0, exact ap max0 (sub_self (ub n)) }, { intro n, change max0 (ub n - ub n) = 0, exact ap max0 (sub_self (ub n)) },
{ intro ns, reflexivity }, { intro ns, reflexivity },
{ intro n, reflexivity }, { intro n, reflexivity },
{ intro r, exact - (1 : ℤ) }, { intro r, exact - (1 : ℤ) },
{ intro r, exact r + (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 ⬝ _, 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
end end

63
cohomology/serre.hlean
View file

@ -1,7 +1,7 @@
import ..algebra.spectral_sequence ..spectrum.trunc .basic import ..algebra.spectral_sequence ..spectrum.trunc .basic
open eq spectrum trunc is_trunc pointed int EM algebra left_module fiber lift equiv is_equiv 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 set_option pp.binder_types true
/- Eilenberg MacLane spaces are the fibers of the Postnikov system of a type -/ /- 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 := 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 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 s, πₛ[n] (sfiber (spi_compose_left (λx, postnikov_smap (Y x) s)))) ⟹ᵍ
(λn, πₛ[n] (spi X (λx, strunc s₀ (Y x)))) := (λn, πₛ[n] (spi X (λx, strunc s₀ (Y x)))) :=
converges_to_sequence _ (λn, s₀) (λn, n - 1) atiyah_hirzebruch_lb atiyah_hirzebruch_ub 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]) := (λ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 begin
intro n s, intro n s,
refine _ ⬝g (parametrized_cohomology_isomorphism_shomotopy_group_spi _ idp)⁻¹ᵍ, 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)), exact ppi_pequiv_right (λx, ptrunc_pequiv (maxm2 (s₀ + k)) (Y x k)),
end end
-- set_option pp.metavar_args true open prod.ops
-- definition atiyah_reindexed : (λp q, opH^p[(x : X), πₛ[q] (Y x)]) ⟹ᵍ (λn, pH^n[(x : X), Y x]) definition atiyah_hirzebruch_base_change [constructor] : agℤ ×ag agℤ ≃g agℤ ×ag agℤ :=
-- := begin
-- converges_to_reindex atiyah_hirzebruch_convergence (λp q, -(p - q)) (λp q, q) (λp q, by reflexivity) fapply group.isomorphism.mk,
-- (λn, -n) (λn, by reflexivity) { 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 end atiyah_hirzebruch
@ -206,11 +227,11 @@ section unreduced_atiyah_hirzebruch
definition unreduced_atiyah_hirzebruch_convergence {X : Type} (Y : X → spectrum) (s₀ : ℤ) definition unreduced_atiyah_hirzebruch_convergence {X : Type} (Y : X → spectrum) (s₀ : ℤ)
(H : Πx, is_strunc s₀ (Y x)) : (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 converges_to_g_isomorphism
(@atiyah_hirzebruch_convergence X₊ (add_point_spectrum Y) s₀ (is_strunc_add_point_spectrum H)) (@atiyah_hirzebruch_convergence X₊ (add_point_spectrum Y) s₀ (is_strunc_add_point_spectrum H))
begin begin
intro n s, refine _ ⬝g !uopH_isomorphism_opH⁻¹ᵍ, intro p q, refine _ ⬝g !uopH_isomorphism_opH⁻¹ᵍ,
apply ordinary_parametrized_cohomology_isomorphism_right, apply ordinary_parametrized_cohomology_isomorphism_right,
intro x, intro x,
apply shomotopy_group_add_point_spectrum apply shomotopy_group_add_point_spectrum
@ -227,17 +248,17 @@ section serre
include H include H
definition serre_convergence : 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 proof
converges_to_g_isomorphism converges_to_g_isomorphism
(unreduced_atiyah_hirzebruch_convergence (unreduced_atiyah_hirzebruch_convergence
(λx, sp_ucotensor (F x) Y) s₀ (λx, sp_ucotensor (F x) Y) s₀
(λx, is_strunc_sp_ucotensor s₀ (F x) H)) (λx, is_strunc_sp_ucotensor s₀ (F x) H))
begin begin
intro n s, intro p q,
refine unreduced_ordinary_parametrized_cohomology_isomorphism_right _ (-(n-s)), refine unreduced_ordinary_parametrized_cohomology_isomorphism_right _ p,
intro x, intro x,
exact (unreduced_cohomology_isomorphism_shomotopy_group_sp_ucotensor _ _ idp)⁻¹ᵍ exact (unreduced_cohomology_isomorphism_shomotopy_group_sp_ucotensor _ _ !neg_neg)⁻¹ᵍ
end end
begin begin
intro n, intro n,
@ -249,29 +270,29 @@ section serre
qed qed
definition serre_convergence_map : 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 proof
converges_to_g_isomorphism converges_to_g_isomorphism
(serre_convergence (fiber f) Y s₀ H) (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 begin intro n, apply unreduced_cohomology_isomorphism, exact !sigma_fiber_equiv⁻¹ᵉ end
qed qed
definition serre_convergence_of_is_conn (H2 : is_conn 1 B) : 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 proof
converges_to_g_isomorphism converges_to_g_isomorphism
(serre_convergence F Y s₀ H) (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 begin intro n, reflexivity end
qed qed
definition serre_convergence_map_of_is_conn (H2 : is_conn 1 B) : 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 proof
converges_to_g_isomorphism converges_to_g_isomorphism
(serre_convergence_of_is_conn b₀ (fiber f) Y s₀ H H2) (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 begin intro n, apply unreduced_cohomology_isomorphism, exact !sigma_fiber_equiv⁻¹ᵉ end
qed qed