Heart cohomology commutes with shifts

The truncation--shift comparisons assemble into the natural isomorphism

H^n_t ≅ [n] ⋙ H^0_t.

This is the functorial bridge from degree-zero heart cohomology to every cohomological degree.

noncomputable def CategoryTheory.Triangulated.Tilting.originalHeartCohUnderlyingShiftNatIso {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (t : TStructure C) (n : ℤ) : (t.truncGELE n n).comp (shiftFunctor C n) ≅ (shiftFunctor C n).comp ((t.truncGELE 0 0).comp (shiftFunctor C 0))

The ambient-functor comparison underlying originalHeartCohShiftNatIso.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Triangulated.Tilting.originalHeartCohShiftNatIso {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 : ℤ) : originalHeartCohFunctor t n ≅ (shiftFunctor C n).comp (originalHeartCohFunctor t 0)

Degree-n heart cohomology is naturally degree-zero heart cohomology after shifting the input by n.

Equations

• One or more equations did not get rendered due to their size.