The extremal phases of an HN filtration

This file owns the identification of the first chain step as the maximal semistable subobject of maximal phase, and the resulting formulas phiPlus_eq and phiMinus_eq for the extremal phases. These are the facts that pin an HN filtration down at both ends.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.hom_eq_zero_to_factor {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E B : A} (F : AbelianHNFiltration Z E) (hB : Z.IsSemistable B) (j : Fin F.n) (hphase : F.phase j < Z.phase B) (f : B ⟶ Limits.cokernel ((F.chain j.castSucc).ofLE (F.chain j.succ) ⋯)) : f = 0

A semistable object of phase above an HN factor has no morphisms to that factor.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.le_chain_of_semistable_phase_gt {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) {B : Subobject E} (hB : Z.IsSemistable (Subobject.underlying.obj B)) {k : ℕ} (hk : k ≤ F.n) (hphase : ∀ (j : Fin F.n), k ≤ ↑j → F.phase j < Z.phase (Subobject.underlying.obj B)) : B ≤ F.chain ⟨k, ⋯⟩

A semistable subobject whose phase is above every factor from index k onward lies in the k-th term of an HN filtration.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.eq_bot_of_semistable_phase_gt_phiPlus {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) {B : Subobject E} (hB : Z.IsSemistable (Subobject.underlying.obj B)) (hphase : F.phiPlus < Z.phase (Subobject.underlying.obj B)) : B = ⊥

A semistable subobject whose phase is above the highest HN phase is zero.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.chain_one_ne_bot {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) : F.chain ⟨1, ⋯⟩ ≠ ⊥

The first nonzero term in an HN filtration is not bottom.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.phase_chain_one {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) : Z.phase (Subobject.underlying.obj (F.chain ⟨1, ⋯⟩)) = F.phiPlus

The phase of the first nonzero term is the highest HN phase.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.chain_one_isSemistable {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) : Z.IsSemistable (Subobject.underlying.obj (F.chain ⟨1, ⋯⟩))

The first nonzero term in an HN filtration is semistable.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.phiPlus_eq {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F G : AbelianHNFiltration Z E) : F.phiPlus = G.phiPlus

The highest phase is intrinsic: any two owner HN filtrations of the same object have the same first phase.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.chain_one_eq {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F G : AbelianHNFiltration Z E) : F.chain ⟨1, ⋯⟩ = G.chain ⟨1, ⋯⟩

The first nonzero term is intrinsic: any two owner HN filtrations of the same object have the same maximally destabilizing subobject.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.semistable_phase_le_phiPlus {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) {B : Subobject E} (hB : Z.IsSemistable (Subobject.underlying.obj B)) : Z.phase (Subobject.underlying.obj B) ≤ F.phiPlus

No nonzero semistable subobject has phase above the first HN phase.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.le_chain_one_of_semistable_phase_eq_phiPlus {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) {B : Subobject E} (hB : Z.IsSemistable (Subobject.underlying.obj B)) (hphase : Z.phase (Subobject.underlying.obj B) = F.phiPlus) : B ≤ F.chain ⟨1, ⋯⟩

A semistable subobject at the highest HN phase is contained in the intrinsic first HN term.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.chain_one_maximal_semistable_phase {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) {B : Subobject E} (hB : Z.IsSemistable (Subobject.underlying.obj B)) (hphase : Z.phase (Subobject.underlying.obj B) = F.phiPlus) : B ≤ F.chain ⟨1, ⋯⟩

The first HN term contains every semistable subobject having the highest HN phase.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.hom_eq_zero_to_semistable_of_phase_lt_phiMinus {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E B : A} (F : AbelianHNFiltration Z E) (hB : Z.IsSemistable B) (hphase : Z.phase B < F.phiMinus) (f : E ⟶ B) : f = 0

Every morphism from an HN-filtered object to a semistable object whose phase is below the lowest HN phase is zero.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.phiMinus_eq {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F G : AbelianHNFiltration Z E) : F.phiMinus = G.phiMinus

The lowest phase is intrinsic: any two owner HN filtrations of the same object have the same last phase.