Homologicality of original-heart cohomology

For any t-structure t, degree-zero heart cohomology sends distinguished triangles to exact short complexes in t.heart.FullSubcategory. The proof is independent of stability functions and Harder--Narasimhan data.

The argument first uses the alternative normal form τ≤0(τ≥0 X) for H⁰_t(X). On a distinguished triangle contained in D^{≤0}, this normal form sends the second arrow to a cokernel. An octahedral truncation then reduces a triangle with nonpositive source to that case. Finally, splitting an arbitrary source at degree one compares it with the nonpositive-source triangle by isomorphisms on the first two terms and a monomorphism on the third.

The alternative degree-zero normal form

Exactness on nonpositive triangles

Reduction to a nonpositive source

The strictly positive source

Unconditional homologicality

@[reducible, inline]

abbrev CategoryTheory.Triangulated.Tilting.OriginalHeartCohomologyIsHomological {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) (n : ℤ) : Prop

The proposition that degree-n original-heart cohomology is homological.

Equations

• CategoryTheory.Triangulated.Tilting.OriginalHeartCohomologyIsHomological t n = (CategoryTheory.Triangulated.Tilting.originalHeartCohFunctor t n).IsHomological

instance CategoryTheory.Triangulated.Tilting.originalHeartCohFunctor_isHomological {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) (n : ℤ) : (originalHeartCohFunctor t n).IsHomological

Heart cohomology in every degree sends distinguished triangles to exact short complexes in the heart.