Exact sequences from heart cohomology

originalHeartCohFunctor t n is homological in every degree (originalHeartCohFunctor_isHomological), so a distinguished triangle in C maps to an exact short complex in the heart of t at every n.

Main results

• originalHeartCoh_exact_of_distTriang: the degree-n short complex of a distinguished triangle is exact in the heart.
• originalHeartCoh_isZero_of_isZero: degree-zero cohomology kills zero objects.
• heart_map_originalHeartCoh: a t-exact functor carries H⁰_t(X) into the heart of the target t-structure, so degree-zero cohomology transports along it at the level of objects.

The associated connecting maps and five-term exact fragments are supplied in Cohomology.Sequence via the shift-sequence API.

theorem CategoryTheory.Triangulated.Tilting.originalHeartCoh_exact_of_distTriang {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) (n : ℤ) (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) : ((Pretriangulated.shortComplexOfDistTriangle T hT).map (originalHeartCohFunctor t n)).Exact

A distinguished triangle maps to an exact short complex under degree-n heart cohomology.

theorem CategoryTheory.Triangulated.Tilting.originalHeartCoh_isZero_of_isZero {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) {X : C} (hX : Limits.IsZero X) : Limits.IsZero ((originalHeartCohFunctor t 0).obj X)

Degree-zero heart cohomology sends zero objects to zero objects.

theorem CategoryTheory.Triangulated.Tilting.heart_map_originalHeartCoh {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (t : TStructure C) {D : Type u_1} [Category.{u_2, u_1} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {F : Functor C D} {t' : TStructure D} [F.IsTExact t t'] (X : C) : t'.heart (F.obj ((originalHeartCohFunctor t 0).obj X).obj)

A t-exact functor carries heart objects to heart objects, so it is defined on the targets of originalHeartCohFunctor.

This is the object-level statement. The natural transformation F ∘ H⁰_t ⟶ H⁰_{t'} ∘ F needs the truncation–shift API described in the module docstring and is deliberately not asserted here.