Harder--Narasimhan filtrations for owner stability functions #

This file owns the finite subobject-chain data attached to an abelian stability function. Existence is kept as an explicit property of a stability function; uniqueness and construction criteria build on this representation.

source

structure CategoryTheory.Triangulated.AbelianHNFiltration {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) (E : A) :

Type (max u v)

A Harder--Narasimhan filtration of a nonzero object for an abelian stability function. It is a strictly increasing finite chain of subobjects whose successive quotients are semistable with strictly decreasing phases.

n : ℕ
Number of semistable factors.
nonempty : 0 < self.n
An HN filtration has at least one factor.
chain : Fin (self.n + 1) → Subobject E
The chain from zero to the whole object.
chain_strictMono : StrictMono self.chain
The chain is strictly increasing.
chain_bot : self.chain ⟨0, ⋯⟩ = ⊥
The initial term is zero.
chain_top : self.chain ⟨self.n, ⋯⟩ = ⊤
The final term is the whole object.
phase : Fin self.n → ℝ
Phases of successive quotients.
phase_strictAnti : StrictAnti self.phase
Successive phases strictly decrease.
factor_phase (j : Fin self.n) : Z.phase (Limits.cokernel ((self.chain j.castSucc).ofLE (self.chain j.succ) ⋯)) = self.phase j
The declared phase is the intrinsic phase of each quotient.
factor_semistable (j : Fin self.n) : Z.IsSemistable (Limits.cokernel ((self.chain j.castSucc).ofLE (self.chain j.succ) ⋯))
Each successive quotient is semistable.