From 9497d7936f00a0a140bc071df48b6e094a90a0eb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sun, 15 Feb 2026 16:21:10 +0100
Subject: [PATCH 01/10] feat(Algebra/Homology/SpectralSequence): complex shapes
 for pages of spectral sequences

---
 Mathlib.lean                                  |  1 +
 .../SpectralSequence/ComplexShape.lean        | 54 +++++++++++++++++++
 2 files changed, 55 insertions(+)
 create mode 100644 Mathlib/Algebra/Homology/SpectralSequence/ComplexShape.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index cd72d6d36a5d31..479367900c845e 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -657,6 +657,7 @@ public import Mathlib.Algebra.Homology.ShortComplex.ShortExact
 public import Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
 public import Mathlib.Algebra.Homology.Single
 public import Mathlib.Algebra.Homology.SingleHomology
+public import Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
 public import Mathlib.Algebra.Homology.Square
 public import Mathlib.Algebra.Homology.TotalComplex
 public import Mathlib.Algebra.Homology.TotalComplexShift
diff --git a/Mathlib/Algebra/Homology/SpectralSequence/ComplexShape.lean b/Mathlib/Algebra/Homology/SpectralSequence/ComplexShape.lean
new file mode 100644
index 00000000000000..fdf82adb1039a1
--- /dev/null
+++ b/Mathlib/Algebra/Homology/SpectralSequence/ComplexShape.lean
@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.Algebra.Homology.ComplexShape
+
+/-!
+# Complex shapes for pages of spectral sequences
+
+In this file, we define complex shapes which correspond
+to pages of spectral sequences:
+* `ComplexShape.spectralSequenceNat`: for any `u : ℤ × ℤ`, this
+is the complex shape on `ℕ × ℕ` corresponding to differentials
+of `ComplexShape.up' u : ComplexShape (ℤ × ℤ)` with source
+and target in `ℕ × ℕ`. (With `u := (r, 1 - r)`, this will
+apply to the `r`th-page of first quadrant `E₂` cohomological
+spectral sequence).
+* `ComplexShape.spectralSequenceFin`: for any `u : ℤ × ℤ` and `l : ℕ`,
+this is a similar definition as `ComplexShape.spectralSequenceNat`
+but for `ℤ × Fin l` (identified as a subset of `ℤ × ℤ`). (This could
+be used for spectral sequences associated to a *finite* filtration.)
+
+-/
+
+@[expose] public section
+
+namespace ComplexShape
+
+/-- For `u : ℤ × ℤ`, this is the complex shape on `ℕ × ℕ`, which
+connects `a` to `b` when the equality `a + u = b` holds in `ℤ × ℤ`. -/
+def spectralSequenceNat (u : ℤ × ℤ) : ComplexShape (ℕ × ℕ) where
+  Rel a b := a.1 + u.1 = b.1 ∧ a.2 + u.2 = b.2
+  next_eq _ _ := by ext <;> lia
+  prev_eq _ _ := by ext <;> lia
+
+@[simp]
+lemma spectralSequenceNat_rel_iff (u : ℤ × ℤ) (a b : ℕ × ℕ) :
+    (spectralSequenceNat u).Rel a b ↔ a.1 + u.1 = b.1 ∧ a.2 + u.2 = b.2 := Iff.rfl
+
+/-- For `l : ℕ` and `u : ℤ × ℤ`, this is the complex shape on `ℤ × Fin l`, which
+connects `a` to `b` when the equality `a + u = b` holds in `ℤ × Fin l`. -/
+def spectralSequenceFin (l : ℕ) (u : ℤ × ℤ) : ComplexShape (ℤ × Fin l) where
+  Rel a b := a.1 + u.1 = b.1 ∧ a.2.1 + u.2 = b.2.1
+  next_eq _ _ := by ext <;> lia
+  prev_eq _ _ := by ext <;> lia
+
+@[simp]
+lemma spectralSequenceFin_rel_iff {l : ℕ} (u : ℤ × ℤ) (a b : ℤ × Fin l) :
+    (spectralSequenceFin l u).Rel a b ↔ a.1 + u.1 = b.1 ∧ a.2 + u.2 = b.2 := Iff.rfl
+
+end ComplexShape

From aa679274331720b948762dd0a8da57cb0313225a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sun, 15 Feb 2026 16:39:12 +0100
Subject: [PATCH 02/10] definition of spectral objects

---
 Mathlib.lean                                  |   1 +
 .../Homology/SpectralObject/Basic.lean        | 235 ++++++++++++++++++
 2 files changed, 236 insertions(+)
 create mode 100644 Mathlib/Algebra/Homology/SpectralObject/Basic.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index cd72d6d36a5d31..c1ed89ba5e49fb 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -657,6 +657,7 @@ public import Mathlib.Algebra.Homology.ShortComplex.ShortExact
 public import Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
 public import Mathlib.Algebra.Homology.Single
 public import Mathlib.Algebra.Homology.SingleHomology
+public import Mathlib.Algebra.Homology.SpectralObject.Basic
 public import Mathlib.Algebra.Homology.Square
 public import Mathlib.Algebra.Homology.TotalComplex
 public import Mathlib.Algebra.Homology.TotalComplexShift
diff --git a/Mathlib/Algebra/Homology/SpectralObject/Basic.lean b/Mathlib/Algebra/Homology/SpectralObject/Basic.lean
new file mode 100644
index 00000000000000..dc327d0a3c3c5b
--- /dev/null
+++ b/Mathlib/Algebra/Homology/SpectralObject/Basic.lean
@@ -0,0 +1,235 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.Algebra.Homology.ExactSequence
+public import Mathlib.CategoryTheory.ComposableArrows.One
+public import Mathlib.CategoryTheory.ComposableArrows.Two
+
+/-!
+# Spectral objects in abelian categories
+
+In this file, we introduce the category `SpectralObject C ι` of spectral
+objects in an abelian category `C` indexed by the category `ι`.
+
+## References
+* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*, II.4][verdier1996]
+
+-/
+
+@[expose] public section
+
+namespace CategoryTheory
+
+open Category Limits
+
+namespace Abelian
+
+variable (C ι : Type*) [Category C] [Category ι] [Abelian C]
+
+open ComposableArrows
+
+/-- A spectral object in an abelian category category `C` indexed by a category ``
+consists of a functor `H : ComposableArrows ι 1 ⥤ C`, and a
+functorial long exact sequence
+`⋯ ⟶ (H n₀).obj (mk₁ f) ⟶ (H n₀).obj (mk₁ (f ≫ g)) ⟶ (H n₀).obj (mk₁ g) ⟶ (H n₁).obj (mk₁ f) ⟶ ⋯`
+when `n₀ + 1 = n₁` and `f` and `g` are composable morphisms in `ι`. (This will be
+shortened as `H^n₀(f) ⟶ H^n₀(f ≫ g) ⟶ H^n₀(g) ⟶ H^n₁(f)` in the documentation.) -/
+structure SpectralObject where
+  /-- A sequence of functors from `ComposableArrows ι 1` to the abelian category.
+  The image of `mk₁ f` will be referred to as `H^n(f)` in the documentation. -/
+  H (n : ℤ) : ComposableArrows ι 1 ⥤ C
+  /-- The connecting homomorphism of the spectral object. (Use `δ` instead.) -/
+  δ' (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) :
+    functorArrows ι 1 2 2 ⋙ H n₀ ⟶ functorArrows ι 0 1 2 ⋙ H n₁
+  exact₁' (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (D : ComposableArrows ι 2) :
+    (mk₂ ((δ' n₀ n₁ h).app D) ((H n₁).map ((mapFunctorArrows ι 0 1 0 2 2).app D))).Exact
+  exact₂' (n : ℤ) (D : ComposableArrows ι 2) :
+    (mk₂ ((H n).map ((mapFunctorArrows ι 0 1 0 2 2).app D))
+      ((H n).map ((mapFunctorArrows ι 0 2 1 2 2).app D))).Exact
+  exact₃' (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (D : ComposableArrows ι 2) :
+    (mk₂ ((H n₀).map ((mapFunctorArrows ι 0 2 1 2 2).app D)) ((δ' n₀ n₁ h).app D)).Exact
+
+namespace SpectralObject
+
+variable {C ι} (X : SpectralObject C ι)
+
+section
+
+variable (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k)
+
+/-- The connecting homomorphism of the spectral object. -/
+def δ : (X.H n₀).obj (mk₁ g) ⟶ (X.H n₁).obj (mk₁ f) :=
+  (X.δ' n₀ n₁ hn₁).app (mk₂ f g)
+
+@[reassoc]
+lemma δ_naturality {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k')
+    (α : mk₁ f ⟶ mk₁ f') (β : mk₁ g ⟶ mk₁ g') (hαβ : α.app 1 = β.app 0 := by cat_disch) :
+    (X.H n₀).map β ≫ X.δ n₀ n₁ hn₁ f' g' = X.δ n₀ n₁ hn₁ f g ≫ (X.H n₁).map α := by
+  have h := (X.δ' n₀ n₁ hn₁).naturality
+    (homMk₂ (α.app 0) (α.app 1) (β.app 1) (naturality' α 0 1)
+      (by simpa only [hαβ] using naturality' β 0 1) : mk₂ f g ⟶ mk₂ f' g')
+  dsimp at h
+  convert h <;> cat_disch
+
+end
+
+section
+
+variable (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k)
+  (fg : i ⟶ k) (h : f ≫ g = fg)
+
+@[reassoc (attr := simp)]
+lemma zero₁ :
+    X.δ n₀ n₁ hn₁ f g ≫ (X.H n₁).map (twoδ₂Toδ₁ f g fg h) = 0 := by
+  subst h
+  exact (X.exact₁' n₀ n₁ hn₁ (mk₂ f g)).zero 0
+
+@[reassoc (attr := simp)]
+lemma zero₂ (fg : i ⟶ k) (h : f ≫ g = fg) :
+    (X.H n₀).map (twoδ₂Toδ₁ f g fg h) ≫ (X.H n₀).map (twoδ₁Toδ₀ f g fg h) = 0 := by
+  subst h
+  exact (X.exact₂' n₀ (mk₂ f g)).zero 0
+
+@[reassoc (attr := simp)]
+lemma zero₃ :
+    (X.H n₀).map (twoδ₁Toδ₀ f g fg h) ≫ X.δ n₀ n₁ hn₁ f g = 0 := by
+  subst h
+  exact (X.exact₃' n₀ n₁ hn₁ (mk₂ f g)).zero 0
+
+/-- The (exact) short complex `H^n₀(g) ⟶ H^n₁(f) ⟶ H^n₁(fg)` of a
+spectral object, when `f ≫ g = fg` and `n₀ + 1 = n₁`. -/
+@[simps]
+def sc₁ : ShortComplex C :=
+  ShortComplex.mk _ _ (X.zero₁ n₀ n₁ hn₁ f g fg h)
+
+/-- The (exact) short complex `H^n₀(f) ⟶ H^n₀(fg) ⟶ H^n₀(g)` of a
+spectral object, when `f ≫ g = fg`. -/
+@[simps]
+def sc₂ : ShortComplex C :=
+  ShortComplex.mk _ _ (X.zero₂ n₀ f g fg h)
+
+/-- The (exact) short complex `H^n₀(fg) ⟶ H^n₀(g) ⟶ H^n₁(f)`
+of a spectral object, when `f ≫ g = fg` and `n₀ + 1 = n₁`. -/
+@[simps]
+def sc₃ : ShortComplex C :=
+  ShortComplex.mk _ _ (X.zero₃ n₀ n₁ hn₁ f g fg h)
+
+lemma exact₁ : (X.sc₁ n₀ n₁ hn₁ f g fg h).Exact := by
+  subst h
+  exact (X.exact₁' n₀ n₁ hn₁ (mk₂ f g)).exact 0
+
+lemma exact₂ : (X.sc₂ n₀ f g fg h).Exact := by
+  subst h
+  exact (X.exact₂' n₀ (mk₂ f g)).exact 0
+
+lemma exact₃ : (X.sc₃ n₀ n₁ hn₁ f g fg h).Exact := by
+  subst h
+  exact ((X.exact₃' n₀ n₁ hn₁ (mk₂ f g))).exact 0
+
+/-- The (exact) sequence
+`H^n₀(f) ⟶ H^n₀(fg) ⟶ H^n₀(g) ⟶ H^n₁(f) ⟶ H^n₁(fg) ⟶ H^n₁(g)`
+of a spectral object, when `f ≫ g = fg` and `n₀ + 1 = n₁`. -/
+abbrev composableArrows₅ : ComposableArrows C 5 :=
+  mk₅ ((X.H n₀).map (twoδ₂Toδ₁ f g fg h)) ((X.H n₀).map (twoδ₁Toδ₀ f g fg h))
+    (X.δ n₀ n₁ hn₁ f g) ((X.H n₁).map (twoδ₂Toδ₁ f g fg h))
+    ((X.H n₁).map (twoδ₁Toδ₀ f g fg h))
+
+lemma composableArrows₅_exact :
+    (X.composableArrows₅ n₀ n₁ hn₁ f g fg h).Exact :=
+  exact_of_δ₀ (X.exact₂ n₀ _ _ _ h).exact_toComposableArrows
+    (exact_of_δ₀ (X.exact₃ n₀ n₁ hn₁ _ _ _ h).exact_toComposableArrows
+      (exact_of_δ₀ (X.exact₁ n₀ n₁ hn₁ _ _ _ h).exact_toComposableArrows
+        ((X.exact₂ n₁ _ _ _ h).exact_toComposableArrows)))
+
+end
+
+@[reassoc (attr := simp)]
+lemma δ_δ (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂)
+    {i j k l : ι} (f : i ⟶ j) (g : j ⟶ k) (h : k ⟶ l) :
+    X.δ n₀ n₁ hn₁ g h ≫ X.δ n₁ n₂ hn₂ f g = 0 := by
+  have eq := X.δ_naturality n₁ n₂ hn₂ f g f (g ≫ h) (𝟙 _) (twoδ₂Toδ₁ g h _ rfl)
+  rw [Functor.map_id, comp_id] at eq
+  rw [← eq, X.zero₁_assoc n₀ n₁ hn₁ g h _ rfl, zero_comp]
+
+/-- The type of morphisms between spectral objects in abelian categories. -/
+@[ext]
+structure Hom (X' : SpectralObject C ι) where
+  /-- The natural transformation that is part of a morphism between spectral objects. -/
+  hom (n : ℤ) : X.H n ⟶ X'.H n
+  comm (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) :
+    X.δ n₀ n₁ hn₁ f g ≫ (hom n₁).app (mk₁ f) =
+    (hom n₀).app (mk₁ g) ≫ X'.δ n₀ n₁ hn₁ f g := by cat_disch
+
+attribute [reassoc (attr := simp)] Hom.comm
+
+@[simps]
+instance : Category (SpectralObject C ι) where
+  Hom := Hom
+  id X := { hom _ := 𝟙 _ }
+  comp f g := { hom n := f.hom n ≫ g.hom n }
+
+attribute [simp] id_hom
+attribute [reassoc, simp] comp_hom
+
+lemma isZero_H_map_mk₁_of_isIso (n : ℤ) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) [IsIso f] :
+    IsZero ((X.H n).obj (mk₁ f)) := by
+  let φ := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) (by simp) ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀)
+  have : IsIso φ := by
+    rw [isIso_iff₁]
+    constructor <;> dsimp <;> infer_instance
+  rw [IsZero.iff_id_eq_zero]
+  rw [← cancel_mono ((X.H n).map φ), Category.id_comp, zero_comp,
+    ← X.zero₂ n f (inv f) (𝟙 _) (by simp), ← Functor.map_comp]
+
+section
+
+variable (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i₀ i₁ i₂ : ι}
+  (f : i₀ ⟶ i₁) (g : i₁ ⟶ i₂) (fg : i₀ ⟶ i₂) (hfg : f ≫ g = fg)
+  (h₁ : IsZero ((X.H n₀).obj (mk₁ f))) (h₂ : IsZero ((X.H n₁).obj (mk₁ f)))
+
+include h₁ in
+lemma mono_H_map_twoδ₁Toδ₀ : Mono ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg)) :=
+  (X.exact₂ n₀ f g fg hfg).mono_g (h₁.eq_of_src _ _)
+
+include h₂ hn₁ in
+lemma epi_H_map_twoδ₁Toδ₀ : Epi ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg)) :=
+  (X.exact₃ n₀ n₁ hn₁ f g fg hfg).epi_f (h₂.eq_of_tgt _ _)
+
+include h₁ h₂ hn₁ in
+lemma isIso_H_map_twoδ₁Toδ₀ : IsIso ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg)) := by
+  have := X.mono_H_map_twoδ₁Toδ₀ n₀ f g fg hfg h₁
+  have := X.epi_H_map_twoδ₁Toδ₀ n₀ n₁ hn₁ f g fg hfg h₂
+  apply isIso_of_mono_of_epi
+
+end
+
+section
+
+variable {ι' : Type*} [Preorder ι'] (X' : SpectralObject C ι')
+  (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) (i₀ i₁ i₂ : ι') (h₀₁ : i₀ ≤ i₁) (h₁₂ : i₁ ≤ i₂)
+  (h₁ : IsZero ((X'.H n₀).obj (mk₁ (homOfLE h₀₁))))
+  (h₂ : IsZero ((X'.H n₁).obj (mk₁ (homOfLE h₀₁))))
+
+include h₁ in
+lemma mono_H_map_twoδ₁Toδ₀' : Mono ((X'.H n₀).map (twoδ₁Toδ₀' i₀ i₁ i₂ h₀₁ h₁₂)) :=
+  X'.mono_H_map_twoδ₁Toδ₀ _ _ _ _ _ h₁
+
+include h₂ hn₁ in
+lemma epi_H_map_twoδ₁Toδ₀' : Epi ((X'.H n₀).map (twoδ₁Toδ₀' i₀ i₁ i₂ h₀₁ h₁₂)) :=
+  X'.epi_H_map_twoδ₁Toδ₀ _ _ hn₁ _ _ _ _ h₂
+
+include h₁ h₂ hn₁ in
+lemma isIso_H_map_twoδ₁Toδ₀' : IsIso ((X'.H n₀).map (twoδ₁Toδ₀' i₀ i₁ i₂ h₀₁ h₁₂)) :=
+  X'.isIso_H_map_twoδ₁Toδ₀ _ _ hn₁ _ _ _ _ h₁ h₂
+
+end
+
+end SpectralObject
+
+end Abelian
+
+end CategoryTheory

From 3d2a747ba8003dd7a692fa6f78139365d5ccf94a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sun, 15 Feb 2026 16:46:07 +0100
Subject: [PATCH 03/10] year

---
 Mathlib/Algebra/Homology/SpectralObject/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Homology/SpectralObject/Basic.lean b/Mathlib/Algebra/Homology/SpectralObject/Basic.lean
index dc327d0a3c3c5b..ac796f96615664 100644
--- a/Mathlib/Algebra/Homology/SpectralObject/Basic.lean
+++ b/Mathlib/Algebra/Homology/SpectralObject/Basic.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2024 Joël Riou. All rights reserved.
+Copyright (c) 2026 Joël Riou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/

From 7a1e13e5dd4873097cf549b31fab8948335b48e6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sun, 15 Feb 2026 16:46:37 +0100
Subject: [PATCH 04/10] year

---
 Mathlib/Algebra/Homology/SpectralSequence/ComplexShape.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Homology/SpectralSequence/ComplexShape.lean b/Mathlib/Algebra/Homology/SpectralSequence/ComplexShape.lean
index fdf82adb1039a1..aeb6a6dba6b71e 100644
--- a/Mathlib/Algebra/Homology/SpectralSequence/ComplexShape.lean
+++ b/Mathlib/Algebra/Homology/SpectralSequence/ComplexShape.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2025 Joël Riou. All rights reserved.
+Copyright (c) 2026 Joël Riou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/

From 0ca9c304c9ea74193041b524d856c576b8823b65 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sun, 15 Feb 2026 18:05:53 +0100
Subject: [PATCH 05/10] SpectralSequenceMkData

---
 Mathlib.lean                                  |   1 +
 .../SpectralObject/HasSpectralSequence.lean   | 156 ++++++++++++++++++
 2 files changed, 157 insertions(+)
 create mode 100644 Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index c1ed89ba5e49fb..f6bb772c65c28e 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -658,6 +658,7 @@ public import Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
 public import Mathlib.Algebra.Homology.Single
 public import Mathlib.Algebra.Homology.SingleHomology
 public import Mathlib.Algebra.Homology.SpectralObject.Basic
+public import Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
 public import Mathlib.Algebra.Homology.Square
 public import Mathlib.Algebra.Homology.TotalComplex
 public import Mathlib.Algebra.Homology.TotalComplexShift
diff --git a/Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean b/Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean
new file mode 100644
index 00000000000000..27a22b40cd48e2
--- /dev/null
+++ b/Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean
@@ -0,0 +1,156 @@
+/-
+Copyright (c) 2026 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.Algebra.Homology.ComplexShape
+public import Mathlib.Algebra.Homology.SpectralObject.Basic
+public import Mathlib.Order.WithBotTop
+
+/-!
+# Shapes of spectral sequences obtained from a spectral object
+
+This file prepares for the construction of the spectral sequence
+of a spectral object in an abelian category which shall be conducted
+in the file `Mathlib/Algebra/Homology/SpectralObject/SpectralSequence.lean` (TODO).
+
+In this file, we introduce a structure `SpectralSequenceMkData` which
+contains a recipe for the construction of the pages of the spectral sequence.
+For example, from a spectral object `X` indexed by `EInt` the definition
+`mkDataE₂Cohomological` will allow to construct an `E₂` cohomological
+spectral sequence such that the object on position `(p, q)` on the `r`th
+page is `E^{p + q}(q - r + 2 ≤ q ≤ q + 1 ≤ q + r - 1)`.
+The data (and properties) in the structure `SpectralSequenceMkData` shall allow
+to define the pages and the differentials directly from the `SpectralObject` API (TODO).
+
+-/
+
+/-!
+# The spectral sequence of a spectral object
+
+-/
+
+@[expose] public section
+
+namespace CategoryTheory
+
+open Category Limits ComposableArrows
+
+namespace Abelian
+
+namespace SpectralObject
+
+variable {C ι κ : Type*} [Category C] [Abelian C] [Preorder ι]
+  {c : ℤ → ComplexShape κ} {r₀ : ℤ}
+
+variable (ι c r₀) in
+/-- This data is a recipe in order to produce a spectral sequence starting on
+page `r₀` (where the `r`th page is of shape `c r`) from a spectral object
+indexed by `ι`. The object on page `r` at the position `pq : κ` shall be
+`E^(deg pq)(i₀ ≤ i₁ ≤ i₂ ≤ i₃)`, where `i₀ ≤ i₁ ≤ i₂ ≤ i₃` are elements in the
+index type `ι` of the spectral object and `deg pq : ℤ` is a cohomological degree.
+The indices `i₀` and `i₃` depend on `r` and `pq`, but `i₁`, `i₂` only depend on `pq`.
+Various conditions are added in order to construct the differentials on the pages
+and show that the homology of a page identifies to the next page; in certain
+cases, additional conditions may be required on the spectral object. -/
+structure SpectralSequenceMkData where
+  /-- The cohomological degree of objects in the pages -/
+  deg : κ → ℤ
+  /-- The zeroth index -/
+  i₀ (r : ℤ) (pq : κ) (hr : r₀ ≤ r := by lia) : ι
+  /-- The first index -/
+  i₁ (pq : κ) : ι
+  /-- The second index -/
+  i₂ (pq : κ) : ι
+  /-- The third index -/
+  i₃ (r : ℤ) (pq : κ) (hr : r₀ ≤ r := by lia) : ι
+  le₀₁ (r : ℤ) (pq : κ) (hr : r₀ ≤ r := by lia) : i₀ r pq ≤ i₁ pq
+  le₁₂ (pq : κ) : i₁ pq ≤ i₂ pq
+  le₂₃ (r : ℤ) (pq : κ) (hr : r₀ ≤ r := by lia) : i₂ pq ≤ i₃ r pq
+  hc (r : ℤ) (pq pq' : κ) (hpq : (c r).Rel pq pq') (hr : r₀ ≤ r := by lia) : deg pq + 1 = deg pq'
+  hc₀₂ (r : ℤ) (pq pq' : κ) (hpq : (c r).Rel pq pq') (hr : r₀ ≤ r := by lia) : i₀ r pq = i₂ pq'
+  hc₁₃ (r : ℤ) (pq pq' : κ) (hpq : (c r).Rel pq pq') (hr : r₀ ≤ r := by lia) : i₁ pq = i₃ r pq'
+  antitone_i₀ (r r' : ℤ) (pq : κ) (hr : r₀ ≤ r := by lia) (hrr' : r ≤ r' := by lia) :
+      i₀ r' pq ≤ i₀ r pq
+  monotone_i₃ (r r' : ℤ) (pq : κ) (hr : r₀ ≤ r := by lia) (hrr' : r ≤ r' := by lia) :
+      i₃ r pq ≤ i₃ r' pq
+  i₀_prev (r r' : ℤ) (pq pq' : κ) (hpq : (c r).Rel pq pq') (hrr' : r + 1 = r' := by lia)
+      (hr : r₀ ≤ r := by lia) :
+      i₀ r' pq = i₁ pq'
+  i₃_next (r r' : ℤ) (pq pq' : κ) (hpq : (c r).Rel pq pq') (hrr' : r + 1 = r' := by lia)
+      (hr : r₀ ≤ r := by lia) :
+      i₃ r' pq' = i₂ pq
+
+namespace SpectralSequenceMkData
+
+variable (data : SpectralSequenceMkData ι c r₀)
+
+lemma i₀_le (r r' : ℤ) (pq : κ) (hrr' : r + 1 = r' := by lia) (hr : r₀ ≤ r := by lia) :
+    data.i₀ r' pq ≤ data.i₀ r pq :=
+  data.antitone_i₀ r r' pq
+
+lemma i₃_le (r r' : ℤ) (pq : κ) (hrr' : r + 1 = r' := by lia) (hr : r₀ ≤ r := by lia) :
+    data.i₃ r pq ≤ data.i₃ r' pq :=
+  data.monotone_i₃ r r' pq
+
+lemma le₀'₀ {r r' : ℤ} (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq' : κ)
+    {i₀' i₀ : ι} (hi₀' : i₀' = data.i₀ r' pq') (hi₀ : i₀ = data.i₀ r pq') :
+    i₀' ≤ i₀ := by
+  rw [hi₀', hi₀]
+  exact data.antitone_i₀ r r' pq'
+
+lemma le₀₁' (r : ℤ) (hr : r₀ ≤ r) (pq' : κ) {i₀ i₁ : ι}
+    (hi₀ : i₀ = data.i₀ r pq')
+    (hi₁ : i₁ = data.i₁ pq') :
+    i₀ ≤ i₁ := by
+  have := data.le₀₁ r pq'
+  simpa only [hi₀, hi₁] using data.le₀₁ r pq'
+
+lemma le₁₂' (pq' : κ) {i₁ i₂ : ι} (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') :
+    i₁ ≤ i₂ := by
+  simpa only [hi₁, hi₂] using data.le₁₂ pq'
+
+lemma le₂₃' (r : ℤ) (hr : r₀ ≤ r) (pq' : κ)
+    {i₂ i₃ : ι}
+    (hi₂ : i₂ = data.i₂ pq')
+    (hi₃ : i₃ = data.i₃ r pq') :
+    i₂ ≤ i₃ := by
+  simpa only [hi₂, hi₃] using data.le₂₃ r pq'
+
+lemma le₃₃' {r r' : ℤ} (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq' : κ)
+    {i₃ i₃' : ι}
+    (hi₃ : i₃ = data.i₃ r pq')
+    (hi₃' : i₃' = data.i₃ r' pq') :
+    i₃ ≤ i₃' := by
+  simpa only [hi₃, hi₃'] using data.monotone_i₃ r r' pq'
+
+end SpectralSequenceMkData
+
+/-- The data which allows to construct an `E₂`-cohomological spectral sequence
+indexed by `ℤ × ℤ` from a spectral object indexed by `EInt`. -/
+@[simps!]
+def mkDataE₂Cohomological :
+    SpectralSequenceMkData EInt (fun r ↦ ComplexShape.up' (⟨r, 1 - r⟩ : ℤ × ℤ)) 2 where
+  deg pq := pq.1 + pq.2
+  i₀ r pq hr := (pq.2 - r + 2 :)
+  i₁ pq := pq.2
+  i₂ pq := (pq.2 + 1 :)
+  i₃ r pq hr := (pq.2 + r - 1 :)
+  le₀₁ r pq hr := by simp; lia
+  le₁₂ pq := by simp
+  le₂₃ r pq hr := by simp; lia
+  hc := by rintro r pq _ rfl _; dsimp; lia
+  hc₀₂ := by rintro r pq hr rfl _; simp; lia
+  hc₁₃ := by rintro r pq hr rfl _; simp; lia
+  antitone_i₀ r r' pq hr hrr' := by simp; lia
+  monotone_i₃ r r' pq hr hrr' := by simp; lia
+  i₀_prev := by rintro r r' hr pq rfl _ _; dsimp; lia
+  i₃_next := by rintro r r' hr pq rfl _ _; dsimp; lia
+
+end SpectralObject
+
+end Abelian
+
+end CategoryTheory

From a1f4a5528463fe9d92054cd7ed6bd522054044b5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sun, 15 Feb 2026 18:26:53 +0100
Subject: [PATCH 06/10] feat(Order/Fin): lemmas about Fin.clamp

---
 Mathlib.lean                 |  1 +
 Mathlib/Order/Fin/Clamp.lean | 29 +++++++++++++++++++++++++++++
 2 files changed, 30 insertions(+)
 create mode 100644 Mathlib/Order/Fin/Clamp.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index cd72d6d36a5d31..4ba5892a13215b 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5658,6 +5658,7 @@ public import Mathlib.Order.Filter.Ultrafilter.Basic
 public import Mathlib.Order.Filter.Ultrafilter.Defs
 public import Mathlib.Order.Filter.ZeroAndBoundedAtFilter
 public import Mathlib.Order.Fin.Basic
+public import Mathlib.Order.Fin.Clamp
 public import Mathlib.Order.Fin.Finset
 public import Mathlib.Order.Fin.SuccAboveOrderIso
 public import Mathlib.Order.Fin.Tuple
diff --git a/Mathlib/Order/Fin/Clamp.lean b/Mathlib/Order/Fin/Clamp.lean
new file mode 100644
index 00000000000000..6db65d84f3a361
--- /dev/null
+++ b/Mathlib/Order/Fin/Clamp.lean
@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2026 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Batteries.Data.Fin.Lemmas
+public import Mathlib.Order.Fin.Basic
+public import Mathlib.Order.MinMax
+
+/-!
+# Lemmas about `Fin.clamp`
+
+-/
+
+namespace Fin
+
+lemma Fin.clamp_mono {m : ℕ} : Monotone (fun n ↦ Fin.clamp n m) := by
+  intro a b h
+  rw [Fin.le_iff_val_le_val]
+  exact min_le_min_right m h
+
+lemma Fin.clamp_eq_last (n m : ℕ) (hnm : m ≤ n) :
+    Fin.clamp n m = Fin.last _ := by
+  ext
+  simpa
+
+end Fin

From e590fc20d263a6291575dca319442726854c81a7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sun, 15 Feb 2026 18:27:40 +0100
Subject: [PATCH 07/10] better syntax

---
 Mathlib/Order/Fin/Clamp.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Order/Fin/Clamp.lean b/Mathlib/Order/Fin/Clamp.lean
index 6db65d84f3a361..05bb73927bcfe0 100644
--- a/Mathlib/Order/Fin/Clamp.lean
+++ b/Mathlib/Order/Fin/Clamp.lean
@@ -16,13 +16,13 @@ public import Mathlib.Order.MinMax
 
 namespace Fin
 
-lemma Fin.clamp_mono {m : ℕ} : Monotone (fun n ↦ Fin.clamp n m) := by
+lemma clamp_mono {m : ℕ} : Monotone (fun n ↦ clamp n m) := by
   intro a b h
-  rw [Fin.le_iff_val_le_val]
+  rw [le_iff_val_le_val]
   exact min_le_min_right m h
 
-lemma Fin.clamp_eq_last (n m : ℕ) (hnm : m ≤ n) :
-    Fin.clamp n m = Fin.last _ := by
+lemma clamp_eq_last (n m : ℕ) (hnm : m ≤ n) :
+    clamp n m = last _ := by
   ext
   simpa
 

From 0b9f94c81a88488121403641b7d4614a5d344b93 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sun, 15 Feb 2026 18:30:36 +0100
Subject: [PATCH 08/10] fix

---
 Mathlib/Order/Fin/Clamp.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Order/Fin/Clamp.lean b/Mathlib/Order/Fin/Clamp.lean
index 05bb73927bcfe0..cbe5cfd1ab8208 100644
--- a/Mathlib/Order/Fin/Clamp.lean
+++ b/Mathlib/Order/Fin/Clamp.lean
@@ -16,12 +16,12 @@ public import Mathlib.Order.MinMax
 
 namespace Fin
 
-lemma clamp_mono {m : ℕ} : Monotone (fun n ↦ clamp n m) := by
+public lemma clamp_mono {m : ℕ} : Monotone (fun n ↦ clamp n m) := by
   intro a b h
   rw [le_iff_val_le_val]
   exact min_le_min_right m h
 
-lemma clamp_eq_last (n m : ℕ) (hnm : m ≤ n) :
+public lemma clamp_eq_last (n m : ℕ) (hnm : m ≤ n) :
     clamp n m = last _ := by
   ext
   simpa

From 400682f4df3c753fc01ecf9d3b95955ccb94b69e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sun, 15 Feb 2026 18:33:08 +0100
Subject: [PATCH 09/10] fix

---
 .../Homology/SpectralObject/HasSpectralSequence.lean     | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean b/Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean
index c76f8b8497d4d5..0f06cad8c66f2a 100644
--- a/Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean
+++ b/Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Homology.SpectralObject.Basic
 public import Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
+public import Mathlib.Order.Fin.Clamp
 public import Mathlib.Order.WithBotTop
 
 /-!
@@ -229,8 +230,7 @@ def mkDataE₂CohomologicalFin (l : ℕ) :
     rintro r r' ⟨a, ⟨a', _⟩⟩ hr hrr'
     dsimp
     rw [Fin.mk_le_mk]
-    apply Fin.clamp_le_clamp
-    lia
+    exact Fin.clamp_mono (by lia)
   i₀_prev := by
     rintro r r' ⟨a, ⟨a', _⟩⟩ ⟨b, ⟨b', _⟩⟩ ⟨h₁, h₂⟩ hrr' hr
     ext
@@ -334,11 +334,6 @@ instance (E : SpectralObject C EInt) : E.HasSpectralSequence mkDataE₂Cohomolog
     exfalso
     exact hpq (pq - (r, 1-r)) (by simp)
 
-lemma _root_.Fin.clamp_eq_last (n m : ℕ) (hnm : m ≤ n) :
-    Fin.clamp n m = Fin.last _ := by
-  ext
-  simpa
-
 instance {l : ℕ} (E : SpectralObject C (Fin (l + 1))) :
     E.HasSpectralSequence (mkDataE₂CohomologicalFin l) where
   isZero_H_obj_mk₁_i₀_le r r' pq hpq n hn hrr' hr := by

From 604a59222b9a8f8aea864bc60525d1108fcbc1c0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sun, 15 Feb 2026 18:36:57 +0100
Subject: [PATCH 10/10] first quadrant

---
 .../SpectralObject/HasSpectralSequence.lean   | 93 +++++++++++++++++++
 1 file changed, 93 insertions(+)

diff --git a/Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean b/Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean
index 0f06cad8c66f2a..07bcb9f64f75c6 100644
--- a/Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean
+++ b/Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean
@@ -368,6 +368,99 @@ 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 mkDataE₂CohomologicalNat where
+  isZero_H_obj_mk₁_i₀_le := by
+    rintro r _ ⟨p, q⟩ hpq n rfl rfl hr
+    apply isZero₁_of_isFirstQuadrant
+    dsimp
+    simp only [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)
+    simp only [ComplexShape.spectralSequenceNat_rel_iff] at hpq
+    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
+    dsimp
+    simp only [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)
+    simp only [ComplexShape.spectralSequenceNat_rel_iff] at hpq
+    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 mkDataE₂HomologicalNat where
+  isZero_H_obj_mk₁_i₀_le := by
+    rintro r _ ⟨p, q⟩ hpq n rfl rfl hr
+    apply isZero₂_of_isThirdQuadrant
+    dsimp
+    simp only [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)
+    simp only [ComplexShape.spectralSequenceNat_rel_iff] at hpq
+    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
+    dsimp
+    simp only [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)
+    simp only [ComplexShape.spectralSequenceNat_rel_iff] at hpq
+    exact hpq ⟨p', q'⟩ (by constructor <;> lia)
+
+end
+
 end SpectralObject
 
 end Abelian