The tail filtration and uniqueness of length

This file owns the induction step: removing the first factor of a nontrivial HN filtration and pushing the remaining chain to the quotient by its first nonzero term, together with the length bookkeeping that makes the number of factors an invariant of the object.

noncomputable def CategoryTheory.Triangulated.AbelianHNFiltration.tailAt {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) (k : ℕ) (hk : k < F.n) : AbelianHNFiltration Z (Limits.cokernel (F.chain ⟨k, ⋯⟩).arrow)

Cut an HN filtration above an index: push the chain from index k onward down to the quotient by the k-th term. The factors are the original factors k, …, n-1, so the phases are the original phases from k on.

The chain index is written k + j rather than j + k so that the successor step is definitionally (k + j) + 1, which is what factor_phase and factor_semistable of the original filtration are stated at.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Triangulated.AbelianHNFiltration.tailAt_n {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) (k : ℕ) (hk : k < F.n) : (F.tailAt k hk).n = F.n - k

@[simp]

theorem CategoryTheory.Triangulated.AbelianHNFiltration.tailAt_phase {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) (k : ℕ) (hk : k < F.n) (j : ℕ) (hj : j < F.n - k) : (F.tailAt k hk).phase ⟨j, hj⟩ = F.phase ⟨k + j, ⋯⟩

theorem CategoryTheory.Triangulated.AbelianHNFiltration.tailAt_phiPlus {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) (k : ℕ) (hk : k < F.n) : (F.tailAt k hk).phiPlus = F.phase ⟨k, hk⟩

The highest phase of a tail is the phase at the index it was cut at.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.tailAt_phiMinus {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) (k : ℕ) (hk : k < F.n) : (F.tailAt k hk).phiMinus = F.phiMinus

A tail ends where the filtration it was cut from ends.

noncomputable def CategoryTheory.Triangulated.AbelianHNFiltration.tail {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) (hn : 2 ≤ F.n) : AbelianHNFiltration Z (Limits.cokernel (F.chain ⟨1, ⋯⟩).arrow)

Remove the first factor of a nontrivial HN filtration and push the remaining chain to the quotient by its first nonzero term.

Equations

• F.tail hn = F.tailAt 1 ⋯

@[simp]

theorem CategoryTheory.Triangulated.AbelianHNFiltration.tail_n {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) (hn : 2 ≤ F.n) : (F.tail hn).n = F.n - 1

theorem CategoryTheory.Triangulated.AbelianHNFiltration.transport_n {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E₁ E₂ : A} (h : E₁ = E₂) (F : AbelianHNFiltration Z E₁) : (h ▸ F).n = F.n

Transporting an owner HN filtration along equality of its ambient objects preserves the number of factors.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.n_eq {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (hE : ¬Limits.IsZero E) (hFinite : ∀ (X : A), Finite (Subobject X)) (F G : AbelianHNFiltration Z E) : F.n = G.n

Owner HN filtrations have a unique length when every object has a finite subobject lattice. The proof recursively removes the intrinsic first HN term and descends to its strictly smaller quotient subobject lattice.