The splitting at a phase cutoff

Cutoff.lean cuts two classes out of the category by a number β and proves that no map runs from the first to the second. This file supplies the other half of a torsion pair: every object is an extension of an object of F β by an object of T β.

The object is cut where its own phases cross β. The phases strictly decrease, so the indices whose phase exceeds β form an initial segment 0, …, k-1; exists_crossIndex names its length k. Cutting the chain there gives

• F.chain k, filtered by restrict, whose phases are φ₀, …, φ_{k-1} — all above β;
• E / F.chain k, filtered by tailAt, whose phases are φ_k, …, φ_{n-1} — all at or below β.

The two boundary cases are not special pleading: at k = 0 the sub is ⊥ and at k = n the quotient is the cokernel of an isomorphism, so in each the missing half is zero and lands in both classes by isZero_mem_*. restrict covers k = n and tailAt covers k = 0, so no other case is needed.

hnTors_of_iso and hnFree_of_iso are here because a torsion pair asks for classes closed under isomorphism, which is AbelianHNFiltration.ofIso.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.exists_crossIndex {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) (β : ℝ) : ∃ k ≤ F.n, (∀ (j : Fin F.n), ↑j < k → β < F.phase j) ∧ ∀ (j : Fin F.n), k ≤ ↑j → F.phase j ≤ β

The crossing index. The HN phases strictly decrease, so the indices whose phase exceeds β are an initial segment; this names its length.

theorem CategoryTheory.Triangulated.StabilityFunction.hnTors_of_iso {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {β : ℝ} {E E' : A} (e : E ≅ E') (h : E ∈ Z.hnTors β) : E' ∈ Z.hnTors β

The torsion class is closed under isomorphism.

theorem CategoryTheory.Triangulated.StabilityFunction.hnFree_of_iso {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {β : ℝ} {E E' : A} (e : E ≅ E') (h : E ∈ Z.hnFree β) : E' ∈ Z.hnFree β

The torsion-free class is closed under isomorphism.

theorem CategoryTheory.Triangulated.StabilityFunction.exists_subobject_hnTors_cokernel_hnFree {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {β : ℝ} (hHN : Z.HasHNProperty) (E : A) : ∃ (T : Subobject E), Subobject.underlying.obj T ∈ Z.hnTors β ∧ Limits.cokernel T.arrow ∈ Z.hnFree β

The splitting. Every object has a subobject in T β whose cokernel is in F β, obtained by cutting an HN filtration at its crossing index.

theorem CategoryTheory.Triangulated.StabilityFunction.exists_shortExact_hnTors_hnFree {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {β : ℝ} (hHN : Z.HasHNProperty) (E : A) : ∃ (T : A) (Q : A) (i : T ⟶ E) (p : E ⟶ Q) (w : CategoryStruct.comp i p = 0), T ∈ Z.hnTors β ∧ Q ∈ Z.hnFree β ∧ { X₁ := T, X₂ := E, X₃ := Q, f := i, g := p, zero := w }.ShortExact

The splitting as a short exact sequence with the given object in the middle.