The abstract cofiltration property

Definition 3.22 of arXiv:2607.28411v1 is geometric only in the names of its objects. Its categorical content is a chosen object G₀, a finite sequence of morphisms ending at zero, prescribed shifted finite sums as the first cone fibres, and a final cone fibre lying below a chosen t-structure bound.

CofiltrationProperty records exactly that content over an arbitrary pretriangulated category. The inputs are deliberately ordered as in the paper: the initial object, then the family of model objects, their shifts, and finally the integer bound. The multiplicities and the cofiltration itself remain existential. In a geometric instantiation these become

• G₀ = f_* O_X,
• L i the invertible sheaves Lᵢ, and
• t the standard t-structure on Dᵇ(Y).

This module does not construct any of those geometric data and makes no claim about Propositions 3.24, 3.26, or 3.27, whose pullback, tensor-product, scheme, and moduli hypotheses lie outside this abstract categorical API.

structure CategoryTheory.Triangulated.CofiltrationData {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (G₀ : C) {m : ℕ} (L : Fin m → C) (l : Fin m → ℤ) : Type (max u v)

The finite cone-by-cone data underlying the cofiltration property.

G 0 is the initial object. Each s i : G i ⟶ G (i+1) has prescribed shifted finite-biproduct fibre, and the final map lands in a zero object.

• G : Fin (m + 2) → C

  The successive objects, including the terminal zero object.

• initialIso : self.G 0 ≅ G₀

  Identification of the first object with the object being cofiltered.

• triangle : Fin (m + 1) → Pretriangulated.Triangle C

  A triangle presenting each cofiltration arrow and its cone.

• triangle_distinguished (i : Fin (m + 1)) : self.triangle i ∈ Pretriangulated.distinguishedTriangles

  Each presenting triangle is distinguished.

• triangle_obj₁ (i : Fin (m + 1)) : Nonempty ((self.triangle i).obj₁ ≅ self.G i.castSucc)

  The first vertex of each triangle is the corresponding cofiltration object.

• triangle_obj₂ (i : Fin (m + 1)) : Nonempty ((self.triangle i).obj₂ ≅ self.G i.succ)

  The second vertex is the following cofiltration object.

• multiplicity : Fin m → ℕ

  Positive multiplicity of each prescribed fibre.

• multiplicity_pos (i : Fin m) : 0 < self.multiplicity i

  The source definition requires every multiplicity to be positive.

• fibreIso (i : Fin m) : (shiftFunctor C (-1)).obj (self.triangle i.castSucc).obj₃ ≅ (shiftFunctor C (l i)).obj (⨁ fun (x : Fin (self.multiplicity i)) => L i)

  The first m shifted cone fibres have the prescribed finite-biproduct form Lᵢ^{⊕aᵢ}[lᵢ].

• terminalIsZero : Limits.IsZero (self.G ⟨m + 1, ⋯⟩)

  The last object is zero.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.CofiltrationData.remainder {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G₀ : C} {m : ℕ} {L : Fin m → C} {l : Fin m → ℤ} (F : CofiltrationData G₀ L l) : C

The final shifted cone fibre of a cofiltration.

Equations

• F.remainder = (CategoryTheory.shiftFunctor C (-1)).obj (F.triangle (Fin.last m)).obj₃

def CategoryTheory.Triangulated.CofiltrationProperty {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (G₀ : C) {m : ℕ} (L : Fin m → C) (l : Fin m → ℤ) (N : ℤ) : Prop

Abstract cofiltration property with the source paper's quantifier order: for fixed G₀, model objects L, shifts l, and bound N, there exists a finite cofiltration with positive multiplicities whose final shifted cone fibre lies in t.le (-N).

Equations

• CategoryTheory.Triangulated.CofiltrationProperty t G₀ L l N = ∃ (F : CategoryTheory.Triangulated.CofiltrationData G₀ L l), t.le (-N) F.remainder

def CategoryTheory.Triangulated.CofiltrationPropertyInfinity {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (G₀ : C) {m : ℕ} (L : Fin m → C) (l : Fin m → ℤ) : Prop

The N = infinity clause of Definition 3.22: the last cone itself is zero. This is kept separate from the integer-bounded property because the source treats infinity as an additional case, not as an integer.

Equations

• CategoryTheory.Triangulated.CofiltrationPropertyInfinity G₀ L l = ∃ (F : CategoryTheory.Triangulated.CofiltrationData G₀ L l), CategoryTheory.Limits.IsZero (F.triangle (Fin.last m)).obj₃

theorem CategoryTheory.Triangulated.CofiltrationPropertyInfinity.toCofiltrationProperty {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {G₀ : C} {m : ℕ} {L : Fin m → C} {l : Fin m → ℤ} (h : CofiltrationPropertyInfinity G₀ L l) (t : TStructure C) (N : ℤ) : CofiltrationProperty t G₀ L l N

An infinite-bound cofiltration yields the integer-bounded property for every t-structure and every bound.