continue on gysin sequence

algebra/graded.hlean

@@ -17,9 +17,8 @@ variables {R : Ring} {I : AddGroup} {M M₁ M₂ M₃ : graded_module R I}
 /-
   morphisms between graded modules.
   The definition is unconventional in two ways:
-  (1) The degree is determined by an endofunction instead of a element of I (and in this case we
+  (1) The degree is determined by an endofunction instead of a element of I, which is equal to adding
-    don't need to assume that I is a group). The "standard" degree i corresponds to the endofunction
+    i on the right. This is more flexible. For example, the
-    which is addition with i on the right. However, this is more flexible. For example, the
     composition of two graded module homomorphisms φ₂ and φ₁ with degrees i₂ and i₁ has type
     M₁ i → M₂ ((i + i₁) + i₂).
     However, a homomorphism with degree i₁ + i₂ must have type
@@ -32,7 +31,6 @@ variables {R : Ring} {I : AddGroup} {M M₁ M₂ M₃ : graded_module R I}
     but as a function taking a path as argument. Specifically, for every path
     deg f i = j
     we get a function M₁ i → M₂ j.
-  (3) Note: we do assume that I is a set. This is not strictly necessary, but it simplifies things
 -/
 
 definition graded_hom_of_deg (d : I ≃ I) (M₁ M₂ : graded_module R I) : Type :=
@@ -158,11 +156,21 @@ begin
   refine cast_fn_cast_square fn _ _ !con.left_inv m
 end
 
+definition graded_hom_square (f : M₁ →gm M₂) {i₁ i₂ j₁ j₂ : I} (p : deg f i₁ = j₁) (q : deg f i₂ = j₂)
+  (r : i₁ = i₂) (s : j₁ = j₂) :
+  hsquare (f ↘ p) (f ↘ q) (homomorphism_of_eq (ap M₁ r)) (homomorphism_of_eq (ap M₂ s)) :=
+begin
+  induction p, induction q, induction r,
+  have rfl = s, from !is_set.elim, induction this,
+  exact homotopy.rfl
+end
+
 variable (I) -- for some reason Lean needs to know what I is when applying this lemma
 definition graded_hom_eq_zero {f : M₁ →gm M₂} {i j k : I} {q : deg f i = j} {p : deg f i = k}
   (m : M₁ i) (r : f ↘ q m = 0) : f ↘ p m = 0 :=
 have f ↘ p m = transport M₂ (q⁻¹ ⬝ p) (f ↘ q m), begin induction p, induction q, reflexivity end,
 this ⬝ ap (transport M₂ (q⁻¹ ⬝ p)) r ⬝ tr_eq_of_pathover (apd (λi, 0) (q⁻¹ ⬝ p))
+
 variable {I}
 
 definition graded_hom_change_image {f : M₁ →gm M₂} {i j k : I} {m : M₂ k} (p : deg f i = k)
@@ -657,6 +665,14 @@ definition graded_homology_elim {g : M₂ →gm M₃} {f : M₁ →gm M₂} (h :
   (H : compose_constant h f) : graded_homology g f →gm M :=
 graded_hom.mk (deg h) (deg_eq h) (λi, homology_elim (h i) (H _ _))
 
+definition graded_homology_isomorphism (g : M₂ →gm M₃) (f : M₁ →gm M₂) (x : I) :
+  graded_homology g f (deg f x) ≃lm homology (g (deg f x)) (f x) :=
+begin
+  refine homology_isomorphism_homology (isomorphism_of_eq (ap M₁ (left_inv (deg f) x)))
+    isomorphism.rfl isomorphism.rfl homotopy.rfl _,
+  exact graded_hom_square f (to_right_inv (deg f) (deg f x)) idp (to_left_inv (deg f) x) idp
+end
+
 definition image_of_graded_homology_intro_eq_zero {g : M₂ →gm M₃} {f : M₁ →gm M₂}
   ⦃i j : I⦄ (p : deg f i = j) (m : graded_kernel g j) (H : graded_homology_intro g f j m = 0) :
   image (f ↘ p) m.1 :=

algebra/spectral_sequence.hlean

@@ -157,25 +157,29 @@ namespace spectral_sequence
     (normal3 : Π(r : ℕ), deg_d c r = (r+2, -(r+1)))
   open is_normal
   variable {c}
-  variable (d : is_normal c)
+  variable (nc : is_normal c)
-  include d
+  include nc
   definition stable_range {n s : ℤ} {r : ℕ} (H1 : n < r + 2) (H2 : s < r + 1) :
     Einf c (n, s) ≃lm E c r (n, s) :=
   begin
     fapply Einf_isomorphism,
-    { intro r' Hr', apply is_contr_E, apply normal1 d,
+    { intro r' Hr', apply is_contr_E, apply normal1 nc,
-      refine lt_of_le_of_lt (le_of_eq (ap (λx, n - x.1) (normal3 d r'))) _,
+      refine lt_of_le_of_lt (le_of_eq (ap (λx, n - x.1) (normal3 nc r'))) _,
       apply sub_lt_left_of_lt_add,
       refine lt_of_lt_of_le H1 (le.trans _ (le_of_eq !add_zero⁻¹)),
       exact add_le_add_right (of_nat_le_of_nat_of_le Hr') 2 },
-    { intro r' Hr', apply is_contr_E, apply normal2 d,
+    { intro r' Hr', apply is_contr_E, apply normal2 nc,
-      refine lt_of_le_of_lt (le_of_eq (ap (λx, s + x.2) (normal3 d r'))) _,
+      refine lt_of_le_of_lt (le_of_eq (ap (λx, s + x.2) (normal3 nc r'))) _,
       change s - (r' + 1) < 0,
       apply sub_lt_left_of_lt_add,
       refine lt_of_lt_of_le H2 (le.trans _ (le_of_eq !add_zero⁻¹)),
       exact add_le_add_right (of_nat_le_of_nat_of_le Hr') 1 },
   end
-  omit d
+
+  definition deg_d_normal_eq (r : ℕ) (x : Z2) : deg (d c r) x = x + (r+2, -(r+1)) :=
+  deg_d_eq c r x ⬝ ap (add x) (is_normal.normal3 nc r)
+
+  omit nc
 
 
 end spectral_sequence

algebra/subgroup.hlean

@@ -7,7 +7,7 @@ Basic concepts of group theory
 -/
 import algebra.group_theory ..move_to_lib ..property
 
-open eq algebra is_trunc sigma sigma.ops prod trunc property
+open eq algebra is_trunc sigma sigma.ops prod trunc property is_equiv equiv
 
 namespace group
 
@@ -456,12 +456,8 @@ end
   open function
 
   definition subgroup_functor_fun [unfold 7] (φ : G →g H) (h : Πg, g ∈ R → φ g ∈ S)
-      (x : subgroup R) :
+      (x : subgroup R) : subgroup S :=
-    subgroup S :=
+  ⟨φ x.1, h x.1 x.2⟩
-  begin
-    induction x with g hg,
-    exact ⟨φ g, h g hg⟩
-  end
 
   definition subgroup_functor [constructor] (φ : G →g H)
     (h : Πg, g ∈ R → φ g ∈ S) : subgroup R →g subgroup S :=
@@ -510,6 +506,19 @@ end
     exact subtype_eq (p g)
   end
 
+  definition subgroup_isomorphism_subgroup [constructor] (φ : G ≃g H) (hφ : Πg, g ∈ R ↔ φ g ∈ S) :
+    subgroup R ≃g subgroup S :=
+  begin
+    apply isomorphism.mk (subgroup_functor φ (λg, iff.mp (hφ g))),
+    refine adjointify _ (subgroup_functor φ⁻¹ᵍ (λg gS, iff.mpr (hφ _) (transport S (right_inv φ g)⁻¹ gS))) _ _,
+    { refine subgroup_functor_compose _ _ _ _ ⬝hty
+             subgroup_functor_homotopy _ _ proof right_inv φ qed ⬝hty
+             subgroup_functor_gid },
+    { refine subgroup_functor_compose _ _ _ _ ⬝hty
+             subgroup_functor_homotopy _ _ proof left_inv φ qed ⬝hty
+             subgroup_functor_gid }
+  end
+
   definition subgroup_of_subgroup_incl {R S : property G} [is_subgroup G R] [is_subgroup G S]
     (H : Π (g : G), g ∈ R → g ∈ S) : subgroup R →g subgroup S
   :=

algebra/submodule.hlean

@@ -7,7 +7,7 @@ open algebra eq group sigma sigma.ops is_trunc function trunc equiv is_equiv pro
 
 namespace left_module
 /- submodules -/
-variables {R : Ring} {M M₁ M₂ M₃ : LeftModule R} {m m₁ m₂ : M}
+variables {R : Ring} {M M₁ M₁' M₂ M₂' M₃ M₃' : LeftModule R} {m m₁ m₂ : M}
 
 structure is_submodule [class] (M : LeftModule R) (S : property M) : Type :=
   (zero_mem : 0 ∈ S)
@@ -45,7 +45,7 @@ ab_subgroup_functor (smul_homomorphism M r) (λg, smul_mem S r)
 definition submodule_smul_right_distrib (r s : R) (n : submodule' S) :
   submodule_smul S (r + s) n = submodule_smul S r n + submodule_smul S s n :=
 begin
-  refine subgroup_functor_homotopy _ _ _ n ⬝ !subgroup_functor_mul⁻¹,
+  refine subgroup_functor_homotopy _ _ _ n ⬝ !subgroup_functor_mul⁻¹ᵖ,
   intro m, exact to_smul_right_distrib r s m
 end
 
@@ -135,6 +135,13 @@ definition submodule_isomorphism [constructor] (S : property M) [is_submodule M
   submodule S ≃lm M :=
 isomorphism.mk (submodule_incl S) (is_equiv_incl_of_subgroup S h)
 
+definition submodule_isomorphism_submodule [constructor] {S : property M₁} [is_submodule M₁ S]
+  {K : property M₂} [is_submodule M₂ K]
+  (φ : M₁ ≃lm M₂) (h : Π (m : M₁), m ∈ S ↔ φ m ∈ K) : submodule S ≃lm submodule K :=
+lm_isomorphism_of_group_isomorphism
+  (subgroup_isomorphism_subgroup (group_isomorphism_of_lm_isomorphism φ) h)
+  (by rexact to_respect_smul (submodule_functor φ (λg, iff.mp (h g))))
+
 /- quotient modules -/
 
 definition quotient_module' (S : property M) [is_submodule M S] : AddAbGroup :=
@@ -289,7 +296,7 @@ begin
   refine total_image.rec _, intro m, exact image.mk m (subtype_eq idp)
 end
 
-variables {ψ : M₂ →lm M₃} {φ : M₁ →lm M₂} {θ : M₁ →lm M₃}
+variables {ψ : M₂ →lm M₃} {φ : M₁ →lm M₂} {θ : M₁ →lm M₃} {ψ' : M₂' →lm M₃'} {φ' : M₁' →lm M₂'}
 
 definition image_elim [constructor] (θ : M₁ →lm M₃) (h : Π⦃g⦄, φ g = 0 → θ g = 0) :
   image_module φ →lm M₃ :=
@@ -412,6 +419,29 @@ definition homology_isomorphism [constructor] (ψ : M₂ →lm M₃) (φ : M₁
 (quotient_module_isomorphism (homology_quotient_property ψ φ)
   (eq_zero_of_mem_property_submodule_trivial (image_trivial _))) ⬝lm (kernel_module_isomorphism ψ _)
 
+definition homology_functor [constructor] (α₁ : M₁ →lm M₁') (α₂ : M₂ →lm M₂') (α₃ : M₃ →lm M₃')
+  (p : hsquare ψ ψ' α₂ α₃) (q : hsquare φ φ' α₁ α₂) : homology ψ φ →lm homology ψ' φ' :=
+begin
+  fapply quotient_module_functor,
+  { apply submodule_functor α₂, intro m pm, refine (p m)⁻¹ ⬝ ap α₃ pm ⬝ to_respect_zero α₃ },
+  { intro m pm, induction pm with m' pm',
+    refine image.mk (α₁ m') ((q m')⁻¹ ⬝ _), exact ap α₂ pm' }
+end
+
+definition homology_isomorphism_homology [constructor] (α₁ : M₁ ≃lm M₁') (α₂ : M₂ ≃lm M₂') (α₃ : M₃ ≃lm M₃')
+  (p : hsquare ψ ψ' α₂ α₃) (q : hsquare φ φ' α₁ α₂) : homology ψ φ ≃lm homology ψ' φ' :=
+begin
+  fapply quotient_module_isomorphism_quotient_module,
+  { fapply submodule_isomorphism_submodule α₂, intro m,
+    exact iff.intro (λpm, (p m)⁻¹ ⬝ ap α₃ pm ⬝ to_respect_zero α₃)
+            (λpm, inj (equiv_of_isomorphism α₃) (p m ⬝ pm ⬝ (to_respect_zero α₃)⁻¹)) },
+  { intro m, apply iff.intro,
+    { intro pm, induction pm with m' pm', refine image.mk (α₁ m') ((q m')⁻¹ ⬝ _), exact ap α₂ pm' },
+    { intro pm, induction pm with m' pm', refine image.mk (α₁⁻¹ˡᵐ m') _,
+      refine (hvinverse' (equiv_of_isomorphism α₁) (equiv_of_isomorphism α₂) q m')⁻¹ ⬝ _,
+      exact ap α₂⁻¹ˡᵐ pm' ⬝ to_left_inv (equiv_of_isomorphism α₂) m.1 }}
+end
+
 definition ker_in_im_of_is_contr_homology (ψ : M₂ →lm M₃) {φ : M₁ →lm M₂}
   (H₁ : is_contr (homology ψ φ)) {m : M₂} (p : ψ m = 0) : image φ m :=
 rel_of_is_contr_quotient_module _ H₁ ⟨m, p⟩
@@ -441,10 +471,10 @@ is_surjective_of_is_contr_homology_of_constant ψ H₁ (λm, @eq_of_is_contr _ H
 definition cokernel_module (φ : M₁ →lm M₂) : LeftModule R :=
 quotient_module (image φ)
 
-definition cokernel_module_isomorphism_homology (φ : M₁ →lm M₂) :
+definition cokernel_module_isomorphism_homology (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) (H : Πm, ψ m = 0) :
-  homology (trivial_homomorphism M₂ (trivial_LeftModule R)) φ ≃lm cokernel_module φ :=
+  homology ψ φ ≃lm cokernel_module φ :=
 quotient_module_isomorphism_quotient_module
-  (submodule_isomorphism _ (λm, idp))
+  (submodule_isomorphism _ H)
   begin intro m, reflexivity end
 
 open chain_complex fin nat

cohomology/basic.hlean

@@ -10,10 +10,10 @@ import ..spectrum.basic ..algebra.arrow_group ..algebra.product_group ..choice
        ..homotopy.fwedge ..homotopy.pushout ..homotopy.EM ..homotopy.wedge
 
 open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops equiv susp is_trunc
-     function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit pi is_conn
+     function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit pi is_conn wedge
 
 namespace cohomology
-
+universe variables u u' v w
 /- The cohomology of X with coefficients in Y is
    trunc 0 (A →* Ω[2] (Y (n+2)))
    In the file arrow_group (in algebra) we construct the group structure on this type.
@@ -287,15 +287,15 @@ definition additive_hom [constructor] {I : Type} (X : I → Type*) (Y : spectrum
   H^n[⋁X, Y] →g Πᵍ i, H^n[X i, Y] :=
 Group_pi_intro (λi, cohomology_functor (pinl i) Y n)
 
-definition additive_equiv.{u} {I : Type.{u}} (H : has_choice 0 I) (X : I → Type*) (Y : spectrum)
+definition additive_equiv {I : Type.{u}} (H : has_choice.{u (max v w)} 0 I) (X : I → pType.{v})
-  (n : ℤ) : H^n[⋁X, Y] ≃ Πᵍ i, H^n[X i, Y] :=
+  (Y : spectrum.{w}) (n : ℤ) : H^n[⋁X, Y] ≃ Πᵍ i, H^n[X i, Y] :=
 trunc_fwedge_pmap_equiv H X (Ω[2] (Y (n+2)))
 
 definition spectrum_additive {I : Type} (H : has_choice 0 I) (X : I → Type*) (Y : spectrum)
   (n : ℤ) : is_equiv (additive_hom X Y n) :=
 is_equiv_of_equiv_of_homotopy (additive_equiv H X Y n) begin intro f, induction f, reflexivity end
 
-definition cohomology_fwedge.{u} {I : Type.{u}} (H : has_choice 0 I) (X : I → Type*) (Y : spectrum)
+definition cohomology_fwedge {I : Type.{u}} (H : has_choice 0 I) (X : I → Type*) (Y : spectrum)
   (n : ℤ) : H^n[⋁X, Y] ≃g Πᵍ i, H^n[X i, Y] :=
 isomorphism.mk (additive_hom X Y n) (spectrum_additive H X Y n)
 
@@ -359,24 +359,25 @@ definition cohomology_punit (Y : spectrum) (n : ℤ) :
   is_contr (H^n[punit, Y]) :=
 @is_trunc_trunc_of_is_trunc _ _ _ !is_contr_punit_pmap
 
-definition cohomology_wedge.{u} (X X' : Type*) (Y : spectrum.{u}) (n : ℤ) :
+definition cohomology_wedge (X : pType.{u}) (X' : pType.{u'}) (Y : spectrum.{v}) (n : ℤ) :
   H^n[wedge X X', Y] ≃g H^n[X, Y] ×ag H^n[X', Y] :=
-H^≃n[(wedge_pequiv_fwedge X X')⁻¹ᵉ*, Y] ⬝g
+H^≃n[(wedge_pequiv !pequiv_plift !pequiv_plift ⬝e*
-cohomology_fwedge (has_choice_bool 0) _ _ _ ⬝g
+      wedge_pequiv_fwedge (plift.{u u'} X) (plift.{u' u} X'))⁻¹ᵉ*, Y] ⬝g
+cohomology_fwedge (has_choice_bool _) _ Y n ⬝g
 Group_pi_isomorphism_Group_pi erfl begin intro b, induction b: reflexivity end ⬝g
-(product_isomorphism_Group_pi H^n[X, Y] H^n[X', Y])⁻¹ᵍ ⬝g
+(product_isomorphism_Group_pi H^n[plift.{u u'} X, Y] H^n[plift.{u' u} X', Y])⁻¹ᵍ ⬝g
-proof !isomorphism.refl qed
+proof H^≃n[!pequiv_plift, Y] ×≃g H^≃n[!pequiv_plift, Y] qed
 
 definition cohomology_isomorphism_of_equiv {X X' : Type*} (e : X ≃ X') (Y : spectrum) (n : ℤ) :
   H^n[X', Y] ≃g H^n[X, Y] :=
 !cohomology_susp⁻¹ᵍ ⬝g H^≃n+1[susp_pequiv_of_equiv e, Y] ⬝g !cohomology_susp
 
-definition unreduced_cohomology_split (X : Type*) (Y : spectrum) (n : ℤ) :
+definition unreduced_cohomology_split (X : pType.{u}) (Y : spectrum.{v}) (n : ℤ) :
   uH^n[X, Y] ≃g H^n[X, Y] ×ag H^n[pbool, Y] :=
-cohomology_isomorphism_of_equiv (wedge.wedge_pbool_equiv_add_point X) Y n ⬝g
+cohomology_isomorphism_of_equiv (wedge_pbool_equiv_add_point X) Y n ⬝g
 cohomology_wedge X pbool Y n
 
-definition unreduced_ordinary_cohomology_nonzero (X : Type*) (G : AbGroup) (n : ℤ) (H : n ≠ 0) :
+definition unreduced_ordinary_cohomology_nonzero (X : pType.{u}) (G : AbGroup.{v}) (n : ℤ) (H : n ≠ 0) :
   uoH^n[X, G] ≃g oH^n[X, G] :=
 unreduced_cohomology_split X (EM_spectrum G) n ⬝g
 product_trivial_right _ _ (ordinary_cohomology_dimension _ _ H)
@@ -386,7 +387,7 @@ definition unreduced_ordinary_cohomology_zero (X : Type*) (G : AbGroup) :
 unreduced_cohomology_split X (EM_spectrum G) 0 ⬝g
 (!isomorphism.refl ×≃g ordinary_cohomology_pbool G)
 
-definition unreduced_ordinary_cohomology_pbool (G : AbGroup) : uoH^0[pbool, G] ≃g G ×ag G :=
+definition unreduced_ordinary_cohomology_pbool (G : AbGroup.{v}) : uoH^0[pbool, G] ≃g G ×ag G :=
 unreduced_ordinary_cohomology_zero pbool G ⬝g (ordinary_cohomology_pbool G ×≃g !isomorphism.refl)
 
 definition unreduced_ordinary_cohomology_pbool_nonzero (G : AbGroup) (n : ℤ) (H : n ≠ 0) :
@@ -447,7 +448,7 @@ end
 
 /- cohomology theory -/
 
-structure cohomology_theory.{u} : Type.{u+1} :=
+structure cohomology_theory : Type :=
   (HH : ℤ → pType.{u} → AbGroup.{u})
   (Hiso : Π(n : ℤ) {X Y : Type*} (f : X ≃* Y), HH n Y ≃g HH n X)
   (Hiso_refl : Π(n : ℤ) (X : Type*) (x : HH n X), Hiso n pequiv.rfl x = x)
@@ -465,7 +466,7 @@ structure cohomology_theory.{u} : Type.{u+1} :=
   (Hadditive : Π(n : ℤ) {I : Type.{u}} (X : I → Type*), has_choice.{u u} 0 I →
     is_equiv (Group_pi_intro (λi, Hh n (pinl i)) : HH n (⋁ X) → Πᵍ i, HH n (X i)))
 
-structure ordinary_cohomology_theory.{u} extends cohomology_theory.{u} : Type.{u+1} :=
+structure ordinary_cohomology_theory extends cohomology_theory.{u} : Type :=
  (Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (HH n (plift pbool)))
 
 attribute cohomology_theory.HH [coercion]
@@ -494,7 +495,7 @@ definition Hadditive_equiv (H : cohomology_theory) (n : ℤ) {I : Type} (X : I
   : H n (⋁ X) ≃g Πᵍ i, H n (X i) :=
 isomorphism.mk _ (Hadditive H n X H2)
 
-definition Hlift_empty.{u} (H : cohomology_theory.{u}) (n : ℤ) :
+definition Hlift_empty (H : cohomology_theory.{u}) (n : ℤ) :
   is_contr (H n (plift punit)) :=
 let P : lift empty → Type* := lift.rec empty.elim in
 let x := Hadditive H n P _ in
@@ -524,7 +525,7 @@ end
 --   refine Hadditive_equiv H n _ _ ⬝g _
 -- end
 
-definition cohomology_theory_spectrum.{u} [constructor] (Y : spectrum.{u}) : cohomology_theory.{u} :=
+definition cohomology_theory_spectrum [constructor] (Y : spectrum.{u}) : cohomology_theory.{u} :=
 cohomology_theory.mk
   (λn A, H^n[A, Y])
   (λn A B f, cohomology_isomorphism f Y n)
@@ -539,13 +540,6 @@ cohomology_theory.mk
   (λn A B f, cohomology_exact f Y n)
   (λn I A H, spectrum_additive H A Y n)
 
--- set_option pp.universes true
--- set_option pp.abbreviations false
--- print cohomology_theory_spectrum
--- print EM_spectrum
--- print has_choice_lift
--- print equiv_lift
--- print has_choice_equiv_closed
 definition ordinary_cohomology_theory_EM [constructor] (G : AbGroup) : ordinary_cohomology_theory :=
 ⦃ordinary_cohomology_theory, cohomology_theory_spectrum (EM_spectrum G), Hdimension := ordinary_cohomology_dimension_plift G ⦄
 

cohomology/gysin.hlean

@@ -4,36 +4,64 @@
 import .serre
 
 open eq pointed is_trunc is_conn is_equiv equiv sphere fiber chain_complex left_module spectrum nat
-     prod nat int algebra
+     prod nat int algebra function spectral_sequence
 
 namespace cohomology
-
+-- set_option pp.universes true
+-- print unreduced_ordinary_cohomology_sphere_of_neq_nat
+-- --set_option formatter.hide_full_terms false
+-- exit
 definition gysin_sequence' {E B : Type*} (n : ℕ) (HB : is_conn 1 B) (f : E →* B)
   (e : pfiber f ≃* sphere (n+1)) (A : AbGroup) : chain_complex +3ℤ :=
-let c := serre_spectral_sequence_map_of_is_conn pt f (EM_spectrum A) 0 (is_strunc_EM_spectrum A) HB
+let c := serre_spectral_sequence_map_of_is_conn pt f (EM_spectrum A) 0 (is_strunc_EM_spectrum A) HB in
-in
+let cn : is_normal c := !is_normal_serre_spectral_sequence_map_of_is_conn in
-left_module.LES_of_SESs _ _ _ (λm, convergent_spectral_sequence.d c n (m, n))
+let deg_d_x : Π(m : ℤ), deg (convergent_spectral_sequence.d c n) ((m+1) - 3, n + 1) = (n + m - 0, 0) :=
+begin
+  intro m, refine deg_d_normal_eq cn _ _ ⬝ _,
+  refine prod_eq _ !add.right_inv,
+  refine add.comm4 (m+1) (-3) n 2 ⬝ _,
+  exact ap (λx, x - 1) (add.comm (m + 1) n ⬝ (add.assoc n m 1)⁻¹) ⬝ !add.assoc
+end in
+left_module.LES_of_SESs _ _ _ (λm, convergent_spectral_sequence.d c n (m - 3, n + 1))
   begin
     intro m,
     fapply short_exact_mod_isomorphism,
     rotate 3,
     { fapply short_exact_mod_of_is_contr_submodules
-        (spectral_sequence.convergence_0 c (n + m) (λm, neg_zero)),
+        (convergence_0 c (n + m) (λm, neg_zero)),
       { exact zero_lt_succ n },
-      { intro k Hk0 Hkn, apply spectral_sequence.is_contr_E,
+      { intro k Hk0 Hkn, apply is_contr_E,
         apply is_contr_ordinary_cohomology,
         refine is_contr_equiv_closed_rev _
                 (unreduced_ordinary_cohomology_sphere_of_neq_nat A Hkn Hk0),
         apply group.equiv_of_isomorphism, apply unreduced_ordinary_cohomology_isomorphism,
         exact e⁻¹ᵉ* }},
+    { symmetry, refine Einf_isomorphism c (n+1) _ _ ⬝lm
+            convergent_spectral_sequence.α c n (n + m - 0, 0) ⬝lm
+            isomorphism_of_eq (ap (graded_homology _ _) _) ⬝lm
+            !graded_homology_isomorphism ⬝lm
+            cokernel_module_isomorphism_homology _ _ _,
+      { exact sorry },
+      { exact sorry },
+      { exact (deg_d_x m)⁻¹ },
+      { intro x, apply @eq_of_is_contr, apply is_contr_E,
+        apply is_normal.normal2 cn,
+        refine lt_of_le_of_lt (@le_of_eq ℤ _ _ _ (ap (pr2 ∘ deg (convergent_spectral_sequence.d c n))
+          (deg_d_x m) ⬝ ap pr2 (deg_d_normal_eq cn _ _))) _,
+        refine lt_of_le_of_lt (le_of_eq (zero_add (-(n+1)))) _,
+        apply neg_neg_of_pos, apply of_nat_succ_pos }},
+    { reflexivity },
+    { exact sorry }
   end
+
 --   (λm, short_exact_mod_isomorphism
 --     _
 --     isomorphism.rfl
 --     _
 --     (short_exact_mod_of_is_contr_submodules
---       (convergent_spectral_sequence.HDinf X _)
+--       (convergent_HDinf X _)
 --       (zero_lt_succ n)
 --       _))
 
+
 end cohomology

cohomology/serre.hlean

@@ -371,7 +371,7 @@ section serre
     begin intro n, apply unreduced_cohomology_isomorphism, exact !sigma_fiber_equiv⁻¹ᵉ end
   qed
 
-  definition serre_spectral_sequence_map_of_is_conn (H2 : is_conn 1 B) :
+  definition serre_spectral_sequence_map_of_is_conn' (H2 : is_conn 1 B) :
     convergent_spectral_sequence_g (λp q, uoH^p[B, uH^q[fiber f b₀, Y]]) (λn, uH^n[X, Y]) :=
   begin
     apply convergent_spectral_sequence_of_exact_couple (serre_convergence_map_of_is_conn b₀ f Y s₀ H H2),
@@ -379,6 +379,27 @@ section serre
     { reflexivity }
   end
 
+  definition serre_spectral_sequence_map_of_is_conn (H2 : is_conn 1 B) :
+    convergent_spectral_sequence_g (λp q, uoH^p[B, uH^q[fiber f b₀, Y]]) (λn, uH^n[X, Y]) :=
+  ⦃convergent_spectral_sequence,
+    deg_d := λ(r : ℕ), (r + 2, -(r + 1)),
+    lb    := λx, -s₀,
+    serre_spectral_sequence_map_of_is_conn' b₀ f Y s₀ H H2⦄
+
+  omit H
+  definition is_normal_serre_spectral_sequence_map_of_is_conn (H' : is_strunc 0 Y)
+    (H2 : is_conn 1 B) :
+    spectral_sequence.is_normal (serre_spectral_sequence_map_of_is_conn b₀ f Y 0 H' H2) :=
+  begin
+    apply spectral_sequence.is_normal.mk,
+    { intro p q Hp, exact is_contr_ordinary_cohomology_of_neg _ _ Hp },
+    { intro p q Hp, apply is_contr_ordinary_cohomology,
+      apply is_contr_cohomology_of_is_contr_spectrum,
+      exact is_contr_of_is_strunc _ _ H' Hp },
+    { intro r, reflexivity },
+  end
+
+
 end serre
 
 end spectrum

move_to_lib.hlean

@@ -12,6 +12,22 @@ universe variable u
   AddAbGroup.struct G
 
 namespace eq
+  /- move to init.equiv -/
+
+  variables {A₀₀ A₂₀ A₀₂ A₂₂ : Type}
+            {f₁₀ : A₀₀ → A₂₀}
+            {f₀₁ : A₀₀ → A₀₂} {f₂₁ : A₂₀ → A₂₂}
+            {f₁₂ : A₀₂ → A₂₂}
+
+  definition hhinverse' (f₁₀ : A₀₀ ≃ A₂₀) (f₁₂ : A₀₂ ≃ A₂₂) (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) :
+    hsquare f₁₀⁻¹ᵉ f₁₂⁻¹ᵉ f₂₁ f₀₁ :=
+  p⁻¹ʰᵗʸʰ
+
+  definition hvinverse' (f₀₁ : A₀₀ ≃ A₀₂) (f₂₁ : A₂₀ ≃ A₂₂) (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) :
+    hsquare f₁₂ f₁₀ f₀₁⁻¹ᵉ f₂₁⁻¹ᵉ :=
+  p⁻¹ʰᵗʸᵛ
+
+
 
   definition transport_lemma {A : Type} {C : A → Type} {g₁ : A → A}
     {x y : A} (p : x = y) (f : Π⦃x⦄, C x → C (g₁ x)) (z : C x) :
@@ -28,6 +44,15 @@ namespace eq
 
 end eq open eq
 
+namespace int
+
+  definition maxm2_eq_minus_two {n : ℤ} (H : n < 0) : maxm2 n = -2 :=
+  begin
+    induction exists_eq_neg_succ_of_nat H with n p, cases p, reflexivity
+  end
+
+end int
+
 namespace nat
 
 --   definition rec_down_le_beta_lt (P : ℕ → Type) (s : ℕ) (H0 : Πn, s ≤ n → P n)

spectrum/trunc.hlean

@@ -119,6 +119,14 @@ begin
   intro k, apply is_trunc_lift, apply is_trunc_unit
 end
 
+definition is_contr_of_is_strunc (n : ℤ) {m : ℤ} (E : spectrum) (H : is_strunc n E)
+  (Hmn : m < -n) : is_contr (E m) :=
+begin
+  refine transport (λn, is_trunc n (E m)) _ (H m),
+  apply maxm2_eq_minus_two,
+  exact lt_of_lt_of_le (add_lt_add_left Hmn n) (le_of_eq !add.right_inv)
+end
+
 open option
 definition is_strunc_add_point_spectrum {X : Type} {Y : X → spectrum} {s₀ : ℤ}
   (H : Πx, is_strunc s₀ (Y x)) : Π(x : X₊), is_strunc s₀ (add_point_spectrum Y x)