Bounded induction on objects with cohomology in a subcategory

Let A be an abelian category and P : ObjectProperty A a class of objects closed under isomorphism and containing zero. The canonical truncation triangles of DerivedCategory A do not leave cohomologyIn P: the cohomology of a truncation is either a cohomology object of the original complex or zero. This file proves that, and derives from it the induction principle a dévissage runs on.

Main results

• DerivedCategory.cohomologyIn_truncLT, DerivedCategory.cohomologyIn_truncGE: the canonical truncations of an object with cohomology in P have cohomology in P.
• DerivedCategory.bounded_induction: a property of objects of the derived category that holds for every single object with cohomology in P, is closed under isomorphism, and is closed under the middle term of a distinguished triangle, holds for every bounded object with cohomology in P. The induction is on the cohomological amplitude, and the step is the truncation triangle τ_{< a + 1} E ⟶ E ⟶ τ_{≥ a + 1} E.

Taking P = ⊤ gives the absolute statement: a triangulated-closed, isomorphism-closed property containing every single object holds on DerivedCategory.Bounded A.

theorem DerivedCategory.cohomologyIn_truncLT {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (P : CategoryTheory.ObjectProperty A) [P.IsClosedUnderIsomorphisms] [P.ContainsZero] {E : DerivedCategory A} (hE : cohomologyIn P E) (n : ℤ) : cohomologyIn P ((TStructure.t.truncLT n).obj E)

The cohomology of τ_{< n} E in degree i is that of E for i < n and zero otherwise, so it lies in P whenever the cohomology of E does.

theorem DerivedCategory.cohomologyIn_truncGE {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (P : CategoryTheory.ObjectProperty A) [P.IsClosedUnderIsomorphisms] [P.ContainsZero] {E : DerivedCategory A} (hE : cohomologyIn P E) (n : ℤ) : cohomologyIn P ((TStructure.t.truncGE n).obj E)

The cohomology of τ_{≥ n} E in degree i is that of E for n ≤ i and zero otherwise, so it lies in P whenever the cohomology of E does.

theorem DerivedCategory.prop_of_cohomologyIn_singleFunctor_obj {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (P : CategoryTheory.ObjectProperty A) [P.IsClosedUnderIsomorphisms] {n : ℤ} {Y : A} (h : cohomologyIn P ((singleFunctor A n).obj Y)) : P Y

The single object (singleFunctor A n).obj Y has cohomology in P exactly when Y does; only the forward direction is needed downstream.

theorem DerivedCategory.bounded_induction {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (P : CategoryTheory.ObjectProperty A) [P.IsClosedUnderIsomorphisms] [P.ContainsZero] (Q : CategoryTheory.ObjectProperty (DerivedCategory A)) (hiso : ∀ {E E' : DerivedCategory A} (a : E ≅ E'), Q E → Q E') (hsingle : ∀ (n : ℤ) (Y : A), P Y → Q ((singleFunctor A n).obj Y)) (hcone : ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, Q T.obj₁ → Q T.obj₃ → Q T.obj₂) {E : DerivedCategory A} (hE : TStructure.t.bounded E) (hP : cohomologyIn P E) : Q E

Bounded induction. Let Q be a property of objects of the derived category which is closed under isomorphism, holds for every single object (singleFunctor A n).obj Y with P Y, and holds for the middle term of a distinguished triangle whenever it holds for the outer two. Then Q holds for every bounded object whose cohomology lies in P.

The induction is on the amplitude N with E concentrated in [a, a + N]; the step splits E by the truncation triangle at a + 1, whose first term is concentrated in degree a and whose third term has amplitude N - 1.