The splitting at a weak slope cutoff

WeakCutoff.lean cuts two classes out of an abelian category by a slope μ₀ : WithTop ℝ 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 slopes cross μ₀. The slopes strictly decrease, so the indices whose slope exceeds μ₀ form an initial segment; exists_crossIndex (#789) names its length k. Cutting the chain there gives

• F.chain k, filtered by restrict (#789), whose slopes are all above μ₀;
• E / F.chain k, filtered by tailAt (WeakTail.lean), whose slopes are all at or below it.

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

What this completes

WeakTruncation.lean shipped exists_subobject_hnTors — the torsion subobject alone — and said explicitly that the torsion-free quotient was unavailable because tailAt did not port. It does now, so the honest half-statement is superseded by the full one here, and the weak TorsionPair follows in Weak/Tilting/TorsionPair/WeakStabilityFunction.lean.

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.exists_subobject_hnTors_cokernel_hnFree {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {μ₀ : WithTop ℝ} (hHN : W.HasHNProperty) (E : A) : ∃ (T : Subobject E), Subobject.underlying.obj T ∈ W.hnTors μ₀ ∧ Limits.cokernel T.arrow ∈ W.hnFree μ₀

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

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.exists_shortExact_hnTors_hnFree {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {μ₀ : WithTop ℝ} (hHN : W.HasHNProperty) (E : A) : ∃ (T : A) (Q : A) (i : T ⟶ E) (p : E ⟶ Q) (w : CategoryStruct.comp i p = 0), T ∈ W.hnTors μ₀ ∧ Q ∈ W.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.