Cohomology in a weak Serre subcategory cuts out a triangulated subcategory

Let A be an abelian category and P : ObjectProperty A a weak Serre subcategory — closed under kernels, cokernels and extensions, and containing the zero object. This file proves that

cohomologyIn P := fun E ↦ ∀ n, P (Hⁿ E)

is a triangulated subcategory of DerivedCategory A, so that (cohomologyIn P).FullSubcategory inherits a pretriangulated structure from Mathlib's ObjectProperty.instPretriangulatedFullSubcategory, with the inclusion triangulated.

The one mathematical input

Closure under cones is the only field with content, and it is exactly the five-term statement of Abelian/WeakSerre.lean applied to the long exact homology sequence. For a distinguished triangle X₁ ⟶ X₂ ⟶ X₃ ⟶ X₁⟦1⟧ the sequence

Hⁿ⁻¹X₃ ⟶ HⁿX₁ ⟶ HⁿX₂ ⟶ HⁿX₃ ⟶ Hⁿ⁺¹X₁

is exact at its three inner spots, and if X₁ and X₃ have all cohomology in P then the four outer terms are in P. This is why a weak Serre subcategory suffices and no closure under subobjects or quotients is needed: the two extra terms of the five-term sequence pay for exactly that gap.

Why this is not in Mathlib

Mathlib has the three closure classes and the long exact sequence, and it has ObjectProperty.IsTriangulated, but nothing connects them. The t-structure route (DerivedCategory.TStructure) answers a different question — boundedness, not cohomological support in a subcategory.

Main results

• DerivedCategory.cohomologyIn — the object property.
• DerivedCategory.cohomologyIn_isTriangulated — it is a triangulated subcategory, hence Pretriangulated on the full subcategory and the inclusion is triangulated.

def DerivedCategory.cohomologyIn {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (P : CategoryTheory.ObjectProperty A) : CategoryTheory.ObjectProperty (DerivedCategory A)

The objects of DerivedCategory A all of whose cohomology objects satisfy P. For P quasi-coherence on a scheme this is the honest Dqc(X).

Equations

• DerivedCategory.cohomologyIn P E = ∀ (n : ℤ), P ((DerivedCategory.homologyFunctor A n).obj E)

theorem DerivedCategory.mem_cohomologyIn_iff {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (P : CategoryTheory.ObjectProperty A) (E : DerivedCategory A) : cohomologyIn P E ↔ ∀ (n : ℤ), P ((homologyFunctor A n).obj E)

instance DerivedCategory.instIsClosedUnderIsomorphismsCohomologyIn {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (P : CategoryTheory.ObjectProperty A) [P.IsClosedUnderIsomorphisms] : (cohomologyIn P).IsClosedUnderIsomorphisms

instance DerivedCategory.instContainsZeroCohomologyInOfIsClosedUnderIsomorphisms {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (P : CategoryTheory.ObjectProperty A) [P.ContainsZero] [P.IsClosedUnderIsomorphisms] : (cohomologyIn P).ContainsZero

instance DerivedCategory.instIsStableUnderShiftCohomologyInIntOfIsClosedUnderIsomorphisms {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (P : CategoryTheory.ObjectProperty A) [P.IsClosedUnderIsomorphisms] : (cohomologyIn P).IsStableUnderShift ℤ

instance DerivedCategory.cohomologyIn_isTriangulatedClosed₂ {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (P : CategoryTheory.ObjectProperty A) [P.IsClosedUnderKernels] [P.IsClosedUnderCokernels] [P.IsClosedUnderExtensions] [P.IsClosedUnderIsomorphisms] : (cohomologyIn P).IsTriangulatedClosed₂

Closure under cones: the only field of IsTriangulated with content.

The long exact homology sequence of the distinguished triangle supplies the three exactness hypotheses of ObjectProperty.prop_X₃_of_exact₅, and the four outer terms come from X₁ and X₃ in adjacent degrees.

instance DerivedCategory.cohomologyIn_isTriangulated {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (P : CategoryTheory.ObjectProperty A) [P.IsClosedUnderKernels] [P.IsClosedUnderCokernels] [P.IsClosedUnderExtensions] [P.IsClosedUnderIsomorphisms] [P.ContainsZero] : (cohomologyIn P).IsTriangulated

cohomologyIn P is a triangulated subcategory when P is a weak Serre subcategory containing zero.

Two consequences come for free from Mathlib: (cohomologyIn P).FullSubcategory is Pretriangulated (and IsTriangulated when DerivedCategory A is), and (cohomologyIn P).ι is a triangulated functor.

theorem DerivedCategory.cohomologyIn_coproduct {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] {n : ℤ} (P : CategoryTheory.ObjectProperty A) {ι : Type t} [P.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete ι)] (E : ι → DerivedCategory A) [CategoryTheory.Limits.HasCoproduct E] (hpres : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ι) (homologyFunctor A n)) (hE : ∀ (i : ι), cohomologyIn P (E i)) : P ((homologyFunctor A n).obj (∐ E))

Closure under a coproduct that cohomology preserves.

The two hypotheses are stated for the one indexing type at hand rather than as instances on A: they hold by instance search when A has exact coproducts of that shape (DerivedCategory.hasCoproductsOfShape and DerivedCategory.homologyFunctor_preservesCoproductsOfShape in DerivedCategory/Coproducts.lean), and a consumer with a different source for them passes it here.

Given them, the argument is one step: Hⁿ(∐ Eᵢ) is a colimit of the Hⁿ(Eᵢ), each of which is in P, so P's own closure under ι-indexed colimits applies.

theorem DerivedCategory.cohomologyIn_prop_coproduct {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (P : CategoryTheory.ObjectProperty A) {ι : Type t} [P.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete ι)] (E : ι → DerivedCategory A) [CategoryTheory.Limits.HasCoproduct E] (hpres : ∀ (n : ℤ), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ι) (homologyFunctor A n)) (hE : ∀ (i : ι), cohomologyIn P (E i)) : cohomologyIn P (∐ E)

cohomologyIn P is closed under a coproduct preserved by every Hⁿ.

theorem DerivedCategory.cohomologyIn_isClosedUnderColimitsOfShape_discrete {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (P : CategoryTheory.ObjectProperty A) {ι : Type t} [P.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete ι)] [P.IsClosedUnderIsomorphisms] [CategoryTheory.Limits.HasCoproductsOfShape ι (DerivedCategory A)] (hpres : ∀ (n : ℤ), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ι) (homologyFunctor A n)) : (cohomologyIn P).IsClosedUnderColimitsOfShape (CategoryTheory.Discrete ι)

cohomologyIn P is closed under coproducts of shape ι as an ObjectProperty, so that Mathlib's full-subcategory machinery applies: (cohomologyIn P).FullSubcategory has coproducts of shape ι and (cohomologyIn P).ι creates and preserves them (Limits.hasColimitsOfShape_of_closedUnderColimits, Limits.createsColimitsOfShapeFullSubcategoryInclusion).

The hypothesis hpres is stated rather than assumed as an instance for the same reason as in cohomologyIn_prop_coproduct. A colimit of shape Discrete ι of a diagram p.diag is a coproduct of the family i ↦ p.diag.obj ⟨i⟩ up to the isomorphism Discrete.natIsoFunctor, and cohomologyIn_prop_coproduct applies degreewise.