[Merged by Bors] - feat(Algebra/Homology/SpectralObject): first quadrant spectral objects

Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean

@@ -359,6 +359,91 @@ instance {l : ℕ} (E : SpectralObject C (Fin (l + 1))) :
     have := isIso_homOfLE this
     apply E.isZero_H_map_mk₁_of_isIso
 
+section
+
+variable (Y : SpectralObject C EInt)
+
+/-- The conditions on a spectral object indexed by `EInt` which allow
+to obtain a (convergent) first quadrant `E₂` cohomological spectral sequence. -/
+class IsFirstQuadrant : Prop where
+  isZero₁ (i j : EInt) (hij : i ≤ j) (hj : j ≤ (0 : ℤ)) (n : ℤ) :
+    IsZero ((Y.H n).obj (mk₁ (homOfLE hij)))
+  isZero₂ (i j : EInt) (hij : i ≤ j) (n : ℤ) (hi : n < i) :
+    IsZero ((Y.H n).obj (mk₁ (homOfLE hij)))
+
+variable [Y.IsFirstQuadrant]
+
+lemma isZero₁_of_isFirstQuadrant (i j : EInt) (hij : i ≤ j) (hj : j ≤ (0 : ℤ)) (n : ℤ) :
+    IsZero ((Y.H n).obj (mk₁ (homOfLE hij))) :=
+  IsFirstQuadrant.isZero₁ i j hij  hj n
+
+lemma isZero₂_of_isFirstQuadrant (i j : EInt) (hij : i ≤ j) (n : ℤ) (hi : n < i) :
+    IsZero ((Y.H n).obj (mk₁ (homOfLE hij))) :=
+  IsFirstQuadrant.isZero₂ i j hij n hi
+
+instance : Y.HasSpectralSequence coreE₂CohomologicalNat where
+  isZero_H_obj_mk₁_i₀_le := by
+    rintro r _ ⟨p, q⟩ hpq n rfl rfl hr
+    apply isZero₁_of_isFirstQuadrant
+    simp only [coreE₂CohomologicalNat_i₀, WithBotTop.coe_le_coe]
+    by_contra!
+    obtain ⟨p', hp'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ p + r by lia)
+    obtain ⟨q', hq'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ q + 1 - r by lia)
+    exact hpq ⟨p', q'⟩ (by constructor <;> lia)
+  isZero_H_obj_mk₁_i₃_le := by
+    rintro r _ ⟨p, q⟩ hpq n rfl rfl hr
+    apply isZero₂_of_isFirstQuadrant
+    simp only [coreE₂CohomologicalNat_deg, coreE₂CohomologicalNat_i₃, WithBotTop.coe_lt_coe]
+    by_contra!
+    obtain ⟨p', hp'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ p - r by lia)
+    obtain ⟨q', hq'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ q - 1 + r by lia)
+    exact hpq ⟨p', q'⟩ (by constructor <;> lia)
+
+end
+
+section
+
+variable (Y : SpectralObject C EInt)
+
+/-- The conditions on a spectral object indexed by `EInt` which allow
+to obtain a (convergent) third quadrant `E₂` cohomological spectral sequence,
+or a (convergent) first quadrant `E₂` *homological* spectral sequence -/
+class IsThirdQuadrant where
+  isZero₁ (i j : EInt) (hij : i ≤ j) (hi : (0 : ℤ) < i) (n : ℤ) :
+    IsZero ((Y.H n).obj (mk₁ (homOfLE hij)))
+  isZero₂ (i j : EInt) (hij : i ≤ j) (n : ℤ) (hj : j ≤ n) :
+    IsZero ((Y.H n).obj (mk₁ (homOfLE hij)))
+
+variable [Y.IsThirdQuadrant]
+
+lemma isZero₁_of_isThirdQuadrant (i j : EInt) (hij : i ≤ j) (hi : (0 : ℤ) < i) (n : ℤ) :
+    IsZero ((Y.H n).obj (mk₁ (homOfLE hij))) :=
+  IsThirdQuadrant.isZero₁ i j hij hi n
+
+lemma isZero₂_of_isThirdQuadrant (i j : EInt) (hij : i ≤ j) (n : ℤ) (hj : j ≤ n) :
+    IsZero ((Y.H n).obj (mk₁ (homOfLE hij))) :=
+  IsThirdQuadrant.isZero₂ i j hij n hj
+
+instance : Y.HasSpectralSequence coreE₂HomologicalNat where
+  isZero_H_obj_mk₁_i₀_le := by
+    rintro r _ ⟨p, q⟩ hpq n rfl rfl hr
+    apply isZero₂_of_isThirdQuadrant
+    simp only [coreE₂HomologicalNat_i₀, coreE₂HomologicalNat_deg, WithBotTop.coe_le_coe]
+    by_contra!
+    obtain ⟨p', hp'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ p - r by lia)
+    obtain ⟨q', hq'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ q + r - 1 by lia)
+    exact hpq ⟨p', q'⟩ (by constructor <;> lia)
+  isZero_H_obj_mk₁_i₃_le := by
+    rintro r _ ⟨p, q⟩ hpq n rfl rfl hr
+    apply isZero₁_of_isThirdQuadrant
+    simp only [coreE₂HomologicalNat_i₃, WithBotTop.coe_lt_coe]
+    by_contra!
+    obtain ⟨p', hp'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ p + r by lia)
+    obtain ⟨q', hq'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ q + 1 - r by lia)
+    exact hpq ⟨p', q'⟩ (by constructor <;> lia)
+
+end
+
 end SpectralObject
 
 end Abelian