Head/tail decompositions of HN filtrations

This file splits the highest-phase factor from an owner HN filtration. The tail has one fewer factor, and its phase indexing is identified with the remaining phase indexing of the original filtration.

The construction is purely triangulated. In particular, it does not depend on a central charge or mass; those structures consume this decomposition but are not prerequisites for it.

theorem CategoryTheory.Triangulated.HNFiltration.exists_headTailFiltration (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} {E : C} (F : HNFiltration C s.P E) (hn : 0 < F.n) : ∃ (Y : C) (G : HNFiltration C s.P Y) (f : F.factor ⟨0, hn⟩ ⟶ E) (g : E ⟶ Y) (h : Y ⟶ (shiftFunctor C 1).obj (F.factor ⟨0, hn⟩)), Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles ∧ G.n = F.n - 1 ∧ ∀ (j : Fin G.n), ∃ (i : Fin F.n), ↑i = ↑j + 1 ∧ G.φ j = F.φ i

Split an HN filtration into its highest-phase factor and an HN-filtered tail. The tail has one fewer factor, and factor j of the tail has the phase of factor j + 1 of the original filtration.