Harder--Narasimhan filtrations for weak stability functions

This file supplies the heart-level HN package needed for the weak heart--slicing correspondence of Lemma 14.4 in arXiv:1902.08184v4.

Weak HN filtrations are finite strict chains of subobjects in the abelian full heart. Their successive quotients are weak-semistable and their WithTop ℝ slopes strictly decrease. The value ⊤ incorporates the zero-charge boundary at phase 1 without assigning an argument to zero.

The main construction reads the slicing HN filtration of a heart object as a weak abelian HN filtration. It follows the ordinary heart-equivalence proof in WeakStabilityCondition/Heart/Equivalence.lean, with phase comparisons replaced by the weak phase--slope bridge proved here.

The weak abelian HN package

@[implicit_reducible]

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.instAbelianFullSubcategoryHeart_derivedAlgGeo {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} : Abelian t.heart.FullSubcategory

The abelian structure on the full heart, used for weak-slope comparisons.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.instAbelianFullSubcategoryHeart_derivedAlgGeo = t.heartFullSubcategoryAbelian

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.heartSlope {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) (E : t.heart.FullSubcategory) : WithTop ℝ

The weak slope of an object of the abelian full heart.

Equations

• W.heartSlope E = W.slope E.obj

@[reducible, inline]

abbrev CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.HeartSemistable {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) (E : t.heart.FullSubcategory) : Prop

Weak semistability for an object of the abelian full heart.

Equations

• W.HeartSemistable E = W.IsSemistable E.obj

structure CategoryTheory.Triangulated.WeakStabilityCondition.WeakAbelianHNFiltration {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) (E : t.heart.FullSubcategory) : Type (max u_1 u_3)

A Harder--Narasimhan filtration in the abelian full heart for a weak stability function. Successive slopes, rather than arguments, are stored so that a zero-charge phase-1 factor is represented honestly by ⊤.

• n : ℕ

  The number of semistable factors.

• hn : 0 < self.n

  A nonzero object has at least one factor.

• chain : Fin (self.n + 1) → Subobject E

  The chain 0 = E₀ < ... < Eₙ = E.

• chain_strictMono : StrictMono self.chain

  The chain is strict.

• chain_bot : self.chain ⟨0, ⋯⟩ = ⊥

  The first term is zero.

• chain_top : self.chain ⟨self.n, ⋯⟩ = ⊤

  The last term is the whole object.

• μ : Fin self.n → WithTop ℝ

  Slopes of successive quotients.

• μ_anti : StrictAnti self.μ

  Successive slopes strictly decrease.

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

  The stored slope is the slope of the corresponding quotient.

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

  Each successive quotient is weak-semistable.

def CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.HasHNProperty {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) : Prop

A weak stability function has the HN property when every nonzero object of its abelian full heart admits a weak abelian HN filtration.

Equations

• W.HasHNProperty = ∀ (E : t.heart.FullSubcategory), ¬CategoryTheory.Limits.IsZero E → Nonempty (CategoryTheory.Triangulated.WeakStabilityCondition.WeakAbelianHNFiltration W E)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.WeakStabilityCondition.WeakAbelianHNFiltration.factor {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} {W : WeakStabilityFunction t} {E : t.heart.FullSubcategory} (F : WeakAbelianHNFiltration W E) (j : Fin F.n) : t.heart.FullSubcategory

The j-th successive quotient of a weak abelian HN filtration.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakAbelianHNFiltration.factor_not_isZero {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} {W : WeakStabilityFunction t} {E : t.heart.FullSubcategory} (F : WeakAbelianHNFiltration W E) (j : Fin F.n) : ¬Limits.IsZero (F.factor j)

Every factor of a weak abelian HN filtration is nonzero in the full heart.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakAbelianHNFiltration.factor_obj_not_isZero {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} {W : WeakStabilityFunction t} {E : t.heart.FullSubcategory} (F : WeakAbelianHNFiltration W E) (j : Fin F.n) : ¬Limits.IsZero (F.factor j).obj

Every factor is also nonzero after forgetting from the full heart to the ambient triangulated category.

Singleton and append operations

@[implicit_reducible]

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.instAbelianFullSubcategoryHeart_derivedAlgGeo_1 {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} : Abelian t.heart.FullSubcategory

The abelian structure on the full heart, used for weak-HN subquotients.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.instAbelianFullSubcategoryHeart_derivedAlgGeo_1 = t.heartFullSubcategoryAbelian

theorem CategoryTheory.Triangulated.WeakStabilityCondition.heartSlope_cokernel_ofLE_congr {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) {E : t.heart.FullSubcategory} {A₁ A₂ B₁ B₂ : Subobject E} (hA : A₁ = A₂) (hB : B₁ = B₂) {h₁ : A₁ ≤ B₁} {h₂ : A₂ ≤ B₂} : W.heartSlope (Limits.cokernel (A₁.ofLE B₁ h₁)) = W.heartSlope (Limits.cokernel (A₂.ofLE B₂ h₂))

theorem CategoryTheory.Triangulated.WeakStabilityCondition.heartSemistable_cokernel_ofLE_congr {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) {E : t.heart.FullSubcategory} {A₁ A₂ B₁ B₂ : Subobject E} (hA : A₁ = A₂) (hB : B₁ = B₂) {h₁ : A₁ ≤ B₁} {h₂ : A₂ ≤ B₂} (hs : W.HeartSemistable (Limits.cokernel (A₂.ofLE B₂ h₂))) : W.HeartSemistable (Limits.cokernel (A₁.ofLE B₁ h₁))

theorem CategoryTheory.Triangulated.WeakStabilityCondition.heartSlope_cokernel_mapMono_eq {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) {X Y : t.heart.FullSubcategory} (f : X ⟶ Y) [Mono f] {S T : Subobject X} (h : S ≤ T) : W.heartSlope (Limits.cokernel (((Subobject.map f).obj S).ofLE ((Subobject.map f).obj T) ⋯)) = W.heartSlope (Limits.cokernel (S.ofLE T h))

theorem CategoryTheory.Triangulated.WeakStabilityCondition.heartSemistable_cokernel_mapMono_iff {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) {X Y : t.heart.FullSubcategory} (f : X ⟶ Y) [Mono f] {S T : Subobject X} (h : S ≤ T) : W.HeartSemistable (Limits.cokernel (((Subobject.map f).obj S).ofLE ((Subobject.map f).obj T) ⋯)) ↔ W.HeartSemistable (Limits.cokernel (S.ofLE T h))

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.exists_hn_with_last_slope_of_semistable {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) {E : t.heart.FullSubcategory} (hE : ¬Limits.IsZero E) (hss : W.HeartSemistable E) : ∃ (F : WeakAbelianHNFiltration W E), F.μ ⟨F.n - 1, ⋯⟩ = W.heartSlope E

A nonzero weak-semistable heart object has the one-factor weak HN filtration.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.append_hn_filtration_of_mono {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) {X Y B : t.heart.FullSubcategory} (i : X ⟶ Y) [Mono i] (F : WeakAbelianHNFiltration W X) (eB : Limits.cokernel i ≅ B) (hB0 : ¬Limits.IsZero B) (hBss : W.HeartSemistable B) (hlast : W.heartSlope B < F.μ ⟨F.n - 1, ⋯⟩) : ∃ (G : WeakAbelianHNFiltration W Y), G.μ ⟨G.n - 1, ⋯⟩ = W.heartSlope B

Append a lower-slope semistable quotient to a weak HN filtration along a monomorphism.

HN assembly by quotient induction

@[implicit_reducible]

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.instAbelianFullSubcategoryHeart_derivedAlgGeo_2 {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} : Abelian t.heart.FullSubcategory

The abelian full heart used for quotient-inductive HN assembly.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.instAbelianFullSubcategoryHeart_derivedAlgGeo_2 = t.heartFullSubcategoryAbelian

structure CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.HNQuotientStep {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) (rank : t.heart.FullSubcategory → ℕ) (E : t.heart.FullSubcategory) : Type (max u_1 u_3)

One recursive step for constructing an HN filtration from its last semistable quotient. The kernel has smaller rank, and the quotient slope is strictly below the last slope of every HN filtration of that kernel.

The intended rank for Proposition 14.16 is the length of the original HN filtration of H⁻¹; Proposition 19.5 describes exactly this step.

• K : t.heart.FullSubcategory

  The recursive kernel.

• B : t.heart.FullSubcategory

  The last semistable quotient.

• i : self.K ⟶ E

  Kernel inclusion.

• mono_i : Mono self.i

  The inclusion is monic.

• cokernelIso : Limits.cokernel self.i ≅ self.B

  Identification of its cokernel with the chosen quotient.

• kernel_not_isZero : ¬Limits.IsZero self.K

  The kernel is nonzero.

• quotient_not_isZero : ¬Limits.IsZero self.B

  The quotient is nonzero.

• quotient_semistable : W.HeartSemistable self.B

  The quotient is weak semistable.

• rank_lt : rank self.K < rank E

  The recursive measure decreases.

• slope_lt_last (F : WeakAbelianHNFiltration W self.K) : W.heartSlope self.B < F.μ ⟨F.n - 1, ⋯⟩

  The quotient belongs after every factor of the recursive HN filtration.

def CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.HasHNQuotientInduction {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) (rank : t.heart.FullSubcategory → ℕ) : Prop

Quotient-induction data for all nonzero objects: each is already semistable, or admits a rank-decreasing last-quotient step.

Equations

• W.HasHNQuotientInduction rank = ∀ (E : t.heart.FullSubcategory), ¬CategoryTheory.Limits.IsZero E → W.HeartSemistable E ∨ Nonempty (W.HNQuotientStep rank E)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.hasHNProperty_of_quotientInduction {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {t : TStructure C} (W : WeakStabilityFunction t) (rank : t.heart.FullSubcategory → ℕ) (hstep : W.HasHNQuotientInduction rank) : W.HasHNProperty

Rank-decreasing semistable quotients assemble to the weak HN property.

This is the formal recursion used implicitly in Proposition 14.16 and explicitly in Proposition 19.5.

Phase--slope comparison for the induced weak heart function

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.charge_im_pos_of_mem_P_phi_lt_one {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WeakPreStabilityCondition v) {phi : ℝ} (hphi : phi ∈ Set.Ioo 0 1) (E : C) (hP : σ.slicing.P phi E) (hE : ¬Limits.IsZero E) : 0 < (σ.weakStabilityFunctionOnHeart.charge E).im

A nonzero slicing-semistable heart object below phase 1 has positive imaginary charge.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.charge_arg_eq_pi_mul_of_mem_P_phi_lt_one {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WeakPreStabilityCondition v) {phi : ℝ} (hphi : phi ∈ Set.Ioo 0 1) (E : C) (hP : σ.slicing.P phi E) (hE : ¬Limits.IsZero E) : (σ.weakStabilityFunctionOnHeart.charge E).arg = Real.pi * phi

Below phase 1, compatibility identifies the argument of the induced weak heart charge with π * phi.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.slope_eq_top_of_mem_P_one {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WeakPreStabilityCondition v) (E : C) (hP : σ.slicing.P 1 E) (hE : ¬Limits.IsZero E) : σ.weakStabilityFunctionOnHeart.slope E = ⊤

A nonzero phase-1 object has weak slope +∞, including when its charge vanishes.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.slope_lt_of_mem_P_of_phase_lt {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WeakPreStabilityCondition v) {phi₁ phi₂ : ℝ} (hphi₁ : phi₁ ∈ Set.Ioc 0 1) (hphi₂ : phi₂ ∈ Set.Ioc 0 1) (hphi : phi₁ < phi₂) (E₁ E₂ : C) (hP₁ : σ.slicing.P phi₁ E₁) (hP₂ : σ.slicing.P phi₂ E₂) (hE₁ : ¬Limits.IsZero E₁) (hE₂ : ¬Limits.IsZero E₂) : σ.weakStabilityFunctionOnHeart.slope E₁ < σ.weakStabilityFunctionOnHeart.slope E₂

On nonzero slicing-semistable objects in (0,1], strict phase order is strict weak-slope order. The upper endpoint is the ⊤ boundary.

Slicing HN filtrations induce weak abelian HN filtrations

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.weakStabilityFunctionOnHeart_hasHN {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u_2} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WeakPreStabilityCondition v) : σ.weakStabilityFunctionOnHeart.HasHNProperty

The weak stability function induced on the slicing heart has the Harder--Narasimhan property. Zero factors in an ambient slicing tower are discarded; every remaining factor becomes a successive quotient in the abelian full heart.