Image factorisations in owner slicing hearts

This module combines the repository-owned phase-bound API with the ForMathlib abelian-heart bridge. It places the image of a nonzero morphism in the two overlapping phase windows used by the small-gap Hom-vanishing argument.

theorem CategoryTheory.Triangulated.Slicing.exists_heart_image_factorisation_windows (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) {a l u : ℝ} (hau : a < u) (hua : u ≤ a + 1) (hla : l < a + 1) {δ : ℝ} (hδ : 0 < δ) {E F : C} (hEheart : (toTStructure C (phaseShift C s a)).heart E) (hFheart : (toTStructure C (phaseShift C s a)).heart F) (hE_lower : ∀ (hE : ¬Limits.IsZero E), l < phiMinus C s E hE) (hE_upper : ∀ (hE : ¬Limits.IsZero E), phiPlus C s E hE < u) (hF_lower : ∀ (hF : ¬Limits.IsZero F), l < phiMinus C s F hF) (hF_upper : ∀ (hF : ¬Limits.IsZero F), phiPlus C s F hF < u) {f : E ⟶ F} (hf : f ≠ 0) : let t := toTStructure C (phaseShift C s a); ∃ (I : t.heart.FullSubcategory) (K : t.heart.FullSubcategory) (Q : t.heart.FullSubcategory) (p : { obj := E, property := hEheart } ⟶ I) (i : I ⟶ { obj := F, property := hFheart }) (k : K ⟶ { obj := E, property := hEheart }) (q : { obj := F, property := hFheart } ⟶ Q) (δp : I.obj ⟶ (shiftFunctor C 1).obj K.obj) (δi : Q.obj ⟶ (shiftFunctor C 1).obj I.obj), CategoryStruct.comp p i = ObjectProperty.homMk 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 ∧ ¬Limits.IsZero I.obj ∧ intervalProp C s a u K.obj ∧ intervalProp C s a u I.obj ∧ intervalProp C s l (a + 1) I.obj ∧ intervalProp C s l (a + 1 + δ) Q.obj

A nonzero morphism inside a shifted slicing heart has a nonzero abelian image. If the source is bounded below by l and the target is bounded above by u, that image belongs to both overlapping old phase intervals (a,u) and (l,a+1).