diff --git a/Mathlib.lean b/Mathlib.lean
index cd72d6d36a5d31..f6bb772c65c28e 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -657,6 +657,8 @@ 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.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/Basic.lean b/Mathlib/Algebra/Homology/SpectralObject/Basic.lean
new file mode 100644
index 00000000000000..ac796f96615664
--- /dev/null
+++ b/Mathlib/Algebra/Homology/SpectralObject/Basic.lean
@@ -0,0 +1,235 @@
+/-
+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.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
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