Degree-zero homology and the canonical heart truncation

Mathlib's degree-zero homology object, embedded by the single functor, is isomorphic to the pure degree-zero truncation of any derived object. The comparison is pointwise and requires no boundedness hypothesis.

Main definitions

This file introduces no carrier, class, or instance.

Main results

• DerivedCategory.singleH0TruncIso identifies the single object on degree-zero homology with the nested t-structure truncation.

Implementation notes

The heart equivalence first identifies the truncation with a single object. The long exact homology sequence shows that both truncation maps induce isomorphisms on degree-zero homology, identifying that object with Mathlib's homology object.

References

Mathlib's DerivedCategory.HomologySequence.exact₁, DerivedCategory.HomologySequence.exact₂, DerivedCategory.HomologySequence.exact₃, and DerivedCategory.singleFunctorCompHomologyFunctorIso at the pinned revision.

Tags

derived category, heart, t-structure, homology, truncation

noncomputable def DerivedCategory.singleH0TruncIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (M : DerivedCategory C) : (singleFunctor C 0).obj ((homologyFunctor C 0).obj M) ≅ (TStructure.t.truncGE 0).obj ((TStructure.t.truncLT 1).obj M)

The single complex on Mathlib's degree-zero homology object is pointwise isomorphic to the pure degree-zero t-structure truncation. The comparison uses homology exactness for the two truncation triangles, rather than definitional equality of the objects.

Equations

• DerivedCategory.singleH0TruncIso C M = (DerivedCategory.singleFunctor C 0).mapIso (DerivedCategory.h0HeartObjectIsoHomology✝ C M).symm ≪≫ DerivedCategory.h0HeartTruncIso✝ C M