Slope-indexed Harder--Narasimhan filtrations for weak stability functions

HarderNarasimhan.lean stores the successive phases of an HN filtration in ℝ. That is available for a strict stability function, whose charges avoid 0, and unavailable for a weak one, whose charges do not: a skyscraper on a surface has charge exactly 0, and arg 0 = 0 is not its phase.

This file stores the successive slopes in WithTop ℝ instead, exactly as WeakStabilityCondition.WeakAbelianHNFiltration already does on the heart side. The difference from that structure is the class datum, not the indexing: this one is at abelianDatum A, with classes in K₀Ab A and subobject data in the abelian category itself, where Uniqueness/ and Cutoff.lean live. The heart structure is at heartDatum t, with classes in the ambient K₀ C. The two groups differ, so neither is an instance of the other.

The extrema are μPlus (the first, largest slope) and μMinus (the last, smallest). Note the direction: slopes decrease along the filtration and ⊤ is the largest value, so μPlus = ⊤ exactly when the first factor has charge on the real boundary.

structure CategoryTheory.Triangulated.AbelianWeakHNFiltration {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) (E : A) : Type (max u v)

A slope-indexed weak Harder--Narasimhan filtration of a nonzero object for a weak stability function on an abelian category: a strictly increasing finite chain of subobjects whose successive quotients are weak-semistable with strictly decreasing slopes in WithTop ℝ.

• n : ℕ

  Number of weak-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.

• μ : Fin self.n → WithTop ℝ

  Slopes of successive quotients, in WithTop ℝ.

• μ_anti : StrictAnti self.μ

  Successive slopes strictly decrease.

• factor_slope (j : Fin self.n) : W.slope (Limits.cokernel ((self.chain j.castSucc).ofLE (self.chain j.succ) ⋯)) = self.μ j

  The declared slope is the intrinsic slope of each quotient.

• factor_semistable (j : Fin self.n) : W.IsSemistable (Limits.cokernel ((self.chain j.castSucc).ofLE (self.chain j.succ) ⋯))

  Each successive quotient is weak-semistable.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.AbelianWeakHNFiltration.factor {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) (j : Fin F.n) : A

The j-th successive quotient.

Equations

• F.factor j = CategoryTheory.Limits.cokernel ((F.chain j.castSucc).ofLE (F.chain j.succ) ⋯)

def CategoryTheory.Triangulated.AbelianWeakHNFiltration.μPlus {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) : WithTop ℝ

The highest HN slope, at the first factor. It is ⊤ exactly when the maximal destabilizing factor has charge on the real boundary.

Equations

• F.μPlus = F.μ ⟨0, ⋯⟩

def CategoryTheory.Triangulated.AbelianWeakHNFiltration.μMinus {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) : WithTop ℝ

The lowest HN slope, at the last factor.

Equations

• F.μMinus = F.μ ⟨F.n - 1, ⋯⟩

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.μ_mem_range {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) (i : Fin F.n) : F.μMinus ≤ F.μ i ∧ F.μ i ≤ F.μPlus

Every factor slope lies between the HN extrema. The proof is the order argument of AbelianHNFiltration.phase_mem_range, unchanged: StrictAnti supplies antitone over any preorder, so nothing here is specific to ℝ.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.μMinus_le_μPlus {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) : F.μMinus ≤ F.μPlus

The lowest HN slope does not exceed the highest.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.factor_not_isZero {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) (j : Fin F.n) : ¬Limits.IsZero (F.factor j)

Every factor of an HN filtration is nonzero: a zero cokernel would make the chain step an isomorphism, contradicting strictness.

noncomputable def CategoryTheory.Triangulated.AbelianWeakHNFiltration.ofSemistable {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (hE : W.IsSemistable E) : AbelianWeakHNFiltration W E

A weak-semistable object is its own HN filtration. One factor, the object itself, so both extrema are its slope. This is what places a weak-semistable rank-zero object — slope ⊤ — in the torsion class at every finite cutoff.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.ofSemistable_μPlus {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (hE : W.IsSemistable E) : (ofSemistable hE).μPlus = W.slope E

@[simp]

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.ofSemistable_μMinus {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (hE : W.IsSemistable E) : (ofSemistable hE).μMinus = W.slope E

def CategoryTheory.Triangulated.WeakStabilityFunctionOn.HasHNProperty {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) : Prop

A weak stability function has the HN property when every nonzero object admits a slope-indexed weak HN filtration.

Equations

• W.HasHNProperty = ∀ (E : A), ¬CategoryTheory.Limits.IsZero E → Nonempty (CategoryTheory.Triangulated.AbelianWeakHNFiltration W E)

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.slope_cokernel_ofLE_congr {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) {E : A} {A₁ A₂ B₁ B₂ : Subobject E} (hA : A₁ = A₂) (hB : B₁ = B₂) {h₁ : A₁ ≤ B₁} {h₂ : A₂ ≤ B₂} : W.slope (Limits.cokernel (A₁.ofLE B₁ h₁)) = W.slope (Limits.cokernel (A₂.ofLE B₂ h₂))

Slope equality after propositionally rewriting both subobjects in a successive quotient.

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.isSemistable_cokernel_ofLE_congr {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) {E : A} {A₁ A₂ B₁ B₂ : Subobject E} (hA : A₁ = A₂) (hB : B₁ = B₂) {h₁ : A₁ ≤ B₁} {h₂ : A₂ ≤ B₂} (hs : W.IsSemistable (Limits.cokernel (A₂.ofLE B₂ h₂))) : W.IsSemistable (Limits.cokernel (A₁.ofLE B₁ h₁))

Weak semistability is preserved after propositionally rewriting both subobjects in a successive quotient.

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.slope_cokernel_mapMono_eq {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) {X Y : A} (f : X ⟶ Y) [Mono f] {S T : Subobject X} (h : S ≤ T) : W.slope (Limits.cokernel (((Subobject.map f).obj S).ofLE ((Subobject.map f).obj T) ⋯)) = W.slope (Limits.cokernel (S.ofLE T h))

Successive quotients keep their slope when a subobject chain is mapped along a monomorphism.

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.isSemistable_cokernel_mapMono_iff {A : Type u} [Category.{v, u} A] [Abelian A] (W : WeakStabilityFunctionOn (abelianDatum A)) {X Y : A} (f : X ⟶ Y) [Mono f] {S T : Subobject X} (h : S ≤ T) : W.IsSemistable (Limits.cokernel (((Subobject.map f).obj S).ofLE ((Subobject.map f).obj T) ⋯)) ↔ W.IsSemistable (Limits.cokernel (S.ofLE T h))

Successive quotients keep their weak semistability when a subobject chain is mapped along a monomorphism.