Image factorisations in triangulated hearts

This Apache-2.0 ForMathlib bridge exposes the two distinguished triangles attached to the canonical image factorisation of a morphism in a t-structure heart. It is derived from Mathlib's abelian-heart instance and its existing epi-to-triangle theorem.

theorem CategoryTheory.Triangulated.TStructure.exists_distinguished_triangle_of_heart_mono {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {H : Type u} [Category.{v, u} H] [Preadditive H] (t : TStructure C) [hHeart : t.Heart H] {X Y : H} (i : X ⟶ Y) [Mono i] : ∃ (Q : H) (q : Y ⟶ Q) (δ : t.ιHeart.obj Q ⟶ (shiftFunctor C 1).obj (t.ιHeart.obj X)), Pretriangulated.Triangle.mk (t.ιHeart.map i) (t.ιHeart.map q) δ ∈ Pretriangulated.distinguishedTriangles

A monomorphism in any presentation of a t-structure heart completes to a distinguished triangle whose third vertex is again in that heart.

theorem CategoryTheory.Triangulated.TStructure.exists_distinguished_triangle_of_heart_epi {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {H : Type u} [Category.{v, u} H] [Preadditive H] (t : TStructure C) [hHeart : t.Heart H] {X Y : H} (p : X ⟶ Y) [Epi p] : ∃ (K : H) (i : K ⟶ X) (δ : t.ιHeart.obj Y ⟶ (shiftFunctor C 1).obj (t.ιHeart.obj K)), Pretriangulated.Triangle.mk (t.ιHeart.map i) (t.ιHeart.map p) δ ∈ Pretriangulated.distinguishedTriangles

An epimorphism in any presentation of a t-structure heart completes to a distinguished triangle whose first vertex is again in that heart.

theorem CategoryTheory.Triangulated.TStructure.exists_image_factorisation_epi_triangle {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 Y : t.heart.FullSubcategory} (f : X ⟶ Y) : ∃ (I : t.heart.FullSubcategory) (K : t.heart.FullSubcategory) (p : X ⟶ I) (i : I ⟶ Y) (k : K ⟶ X) (δp : I.obj ⟶ (shiftFunctor C 1).obj K.obj), CategoryStruct.comp p i = f ∧ Mono i ∧ Pretriangulated.Triangle.mk k.hom p.hom δp ∈ Pretriangulated.distinguishedTriangles

The canonical image factorisation of a heart morphism supplies its image, epimorphic projection, monomorphic inclusion, and the distinguished kernel triangle of that projection in the ambient triangulated category.

theorem CategoryTheory.Triangulated.TStructure.exists_image_factorisation_triangles {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 Y : t.heart.FullSubcategory} (f : X ⟶ Y) : ∃ (I : t.heart.FullSubcategory) (K : t.heart.FullSubcategory) (Q : t.heart.FullSubcategory) (p : X ⟶ I) (i : I ⟶ Y) (k : K ⟶ X) (q : Y ⟶ Q) (δp : I.obj ⟶ (shiftFunctor C 1).obj K.obj) (δi : Q.obj ⟶ (shiftFunctor C 1).obj I.obj), CategoryStruct.comp p i = f ∧ Epi p ∧ Mono i ∧ Pretriangulated.Triangle.mk k.hom p.hom δp ∈ Pretriangulated.distinguishedTriangles ∧ Pretriangulated.Triangle.mk i.hom q.hom δi ∈ Pretriangulated.distinguishedTriangles

The canonical image factorisation of a heart morphism is represented in the ambient triangulated category by distinguished triangles on both sides of the image. Thus the epimorphism onto the image has a kernel in the heart, and the monomorphism from the image has a cokernel in the heart.