The extremal phases are monotone along monomorphisms and epimorphisms

Uniqueness/Extrema.lean pins φ⁺ and φ⁻ down for a single object. This file compares them across a morphism:

• phiPlus_le_of_mono — a subobject cannot have a higher maximal phase than the object containing it, because its maximal destabilizing subobject is a semistable subobject of the ambient object.
• phiMinus_le_of_epi — a quotient cannot have a lower minimal phase than the object it comes from, because the composite onto the last HN factor of the quotient would be a nonzero epimorphism that φ⁻ forces to vanish.

The two together are what turn Hom-vanishing against a semistable target into Hom-vanishing against a general one: the image of a map is a quotient of the source and a subobject of the target, so its own φ⁻ and φ⁺ are trapped between theirs.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.exists_epi_to_semistable_phase_phiMinus {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) : ∃ (Q : A) (q : E ⟶ Q), Epi q ∧ Z.IsSemistable Q ∧ Z.phase Q = F.phiMinus

The last HN factor, presented as a semistable quotient of the filtered object at the lowest HN phase. The quotient map is the last chain step read through the isomorphism chain n ≅ E.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.phiPlus_le_of_mono {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {X Y : A} (F : AbelianHNFiltration Z X) (G : AbelianHNFiltration Z Y) (i : X ⟶ Y) [Mono i] : F.phiPlus ≤ G.phiPlus

φ⁺ is monotone along monomorphisms. The maximal destabilizing subobject of the source maps to a semistable subobject of the target of the same phase, and no semistable subobject exceeds φ⁺.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.phiMinus_le_of_epi {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {X Y : A} (F : AbelianHNFiltration Z X) (G : AbelianHNFiltration Z Y) (p : X ⟶ Y) [Epi p] : F.phiMinus ≤ G.phiMinus

φ⁻ is monotone along epimorphisms. A strict drop would make the composite onto the last HN factor of the target a nonzero epimorphism that hom_eq_zero_to_semistable_of_phase_lt_phiMinus forces to vanish.