Stable-object reduction for mass--Hom bounds

A stable object of phase φ is a nonzero simple object of the exact slice 𝒫(φ), expressed intrinsically by distinguished triangles whose three terms lie in that slice. The one missing categorical input is isolated as Slicing.HasJordanHolderFiltrations: every semistable object is a finite extension of stable objects of the same phase.

The repository's local-finiteness field controls admissible subobjects in thin interval categories, but the pinned libraries do not yet turn that well-foundedness into a categorical Jordan--Hölder filtration. Consequently the named hypothesis below is explicit; it is not a field of a stability condition and is not silently inferred from local finiteness. The missing bridge is tracked by GitHub issue #1203.

Under this hypothesis, a bound on stable targets extends first across a same-phase Jordan--Hölder filtration and then across the existing HN filtration. This is the stable-object half of Halpern--Leistner--Robotis, arXiv:2501.00710v2, Lemma 2.8.

def CategoryTheory.Triangulated.Slicing.IsStableAt {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (φ : ℝ) (E : C) : Prop

A nonzero simple object in the exact phase slice 𝒫(φ), stated without manufacturing an abelian-category instance on that slice.

Equations

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

def CategoryTheory.Triangulated.Slicing.HasJordanHolderFiltrations {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) : Prop

The explicit Jordan--Hölder input used by stable-object reduction: every semistable object is a finite extension of stable objects in its own phase slice.

Equations

• s.HasJordanHolderFiltrations = ∀ (φ : ℝ) (E : C), s.P φ E → CategoryTheory.Triangulated.ExtensionClosure (s.IsStableAt φ) E

def CategoryTheory.Triangulated.StabilityCondition.WithClassMap.HasStableMassHomBoundFor {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v₀ : K₀ C →+ Λ} (σ : WithClassMap C v₀) (A : C) : Prop

A mass--Hom bound tested only on stable target objects.

Equations

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

def CategoryTheory.Triangulated.StabilityCondition.WithClassMap.HasStableMassHomBound {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v₀ : K₀ C →+ Λ} (σ : WithClassMap C v₀) (T : ObjectProperty C) : Prop

A stable-target mass--Hom bound on a property of test objects.

Equations

• σ.HasStableMassHomBound T = ∀ (A : C), T A → σ.HasStableMassHomBoundFor A

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.HasStableMassHomBoundFor.massHom {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] [SerreFunctor.HomFinite k C] {Λ : Type u'} [AddCommGroup Λ] {v₀ : K₀ C →+ Λ} {σ : WithClassMap C v₀} {A : C} (h : σ.HasStableMassHomBoundFor A) (hJH : σ.slicing.HasJordanHolderFiltrations) : σ.HasMassHomBoundFor A

A stable-target bound extends to the full mass--Hom bound under the named Jordan--Hölder hypothesis.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.HasMassHomBoundFor.stable {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [SerreFunctor.HomFinite k C] {Λ : Type u'} [AddCommGroup Λ] {v₀ : K₀ C →+ Λ} {σ : WithClassMap C v₀} {A : C} (h : σ.HasMassHomBoundFor A) : σ.HasStableMassHomBoundFor A

A full mass--Hom bound restricts to stable targets.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.HasMassHomBoundFor.stable_iff {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] [SerreFunctor.HomFinite k C] {Λ : Type u'} [AddCommGroup Λ] {v₀ : K₀ C →+ Λ} {σ : WithClassMap C v₀} {A : C} (hJH : σ.slicing.HasJordanHolderFiltrations) : σ.HasStableMassHomBoundFor A ↔ σ.HasMassHomBoundFor A

Under Jordan--Hölder, testing a fixed source against all objects is equivalent to testing it only against stable objects.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.HasStableMassHomBound.massHom {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] [SerreFunctor.HomFinite k C] {Λ : Type u'} [AddCommGroup Λ] {v₀ : K₀ C →+ Λ} {σ : WithClassMap C v₀} {T : ObjectProperty C} (h : σ.HasStableMassHomBound T) (hJH : σ.slicing.HasJordanHolderFiltrations) : σ.HasMassHomBound T

Stable-target bounds on a test class give full mass--Hom bounds on that class under Jordan--Hölder.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.HasStableMassHomBound.triangEnvelope {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] [Pretriangulated C] [IsTriangulated C] [SerreFunctor.HomFinite k C] {Λ : Type u'} [AddCommGroup Λ] {v₀ : K₀ C →+ Λ} {σ : WithClassMap C v₀} {T : ObjectProperty C} (h : σ.HasStableMassHomBound T) (hJH : σ.slicing.HasJordanHolderFiltrations) : σ.HasMassHomBound T.triangEnvelope

The two reductions combine: stable-target bounds on generators extend to full bounds on their thick triangulated envelope.