Algebraic stability conditions and mass--Hom bounds

An algebraic stability condition has a finite-length heart with finitely many simple objects. The categorical content needed here is recorded operationally: the slicing has Jordan--Hölder filtrations and its stable objects form finitely many shift-orbits. This avoids identifying the repository's free lattice of simple charges with a categorical Grothendieck group before the missing Jordan--Hölder bridge is constructed (GitHub issue #1203).

With the properness input HomFiniteBounded, a fixed source has only finitely many nonzero shifted Hom-spaces into each simple representative. Summing those dimensions and dividing by the finitely many positive simple masses gives a stable-target bound; the stable-object reduction then gives the global mass--Hom bound. This is the algebraic base case in Halpern--Leistner--Robotis, arXiv:2501.00710v2, Example 2.9.

This proof deliberately does not use the tempting estimate dim Hom(Sⱼ⟦m⟧, F) ≤ length(F): finite length controls morphisms in the heart, not arbitrary shifted Ext groups. Finite Ext-amplitude is therefore kept visible as HomFiniteBounded and all shifted Hom dimensions are summed before the finite family of simple representatives is used.

The numerical lemma exists_common_positive_functional isolates the other finite-heart estimate: finitely many charges in the semi-closed upper half plane admit one strictly positive real linear functional, with a uniform positive lower bound. Its functional (x,y) ↦ y - δx is the unnormalised form of taking real part after rotation; normalising does not affect strict positivity.

No geometry is imported, and no stability condition is manufactured from the finite-lattice charge model. In particular, the concrete Kᵇ(FGModuleCat k) properness witness does not by itself supply a heart, slicing, or stability condition. The nondegenerate concrete stability witness is tracked separately by GitHub issue #1206.

def CategoryTheory.Triangulated.WeakStabilityCondition.FiniteLength.tiltedImaginaryPart (δ : ℝ) (z : ℂ) : ℝ

The real functional used to tilt the boundary ray of the semi-closed upper half plane into an open half plane.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.FiniteLength.tiltedImaginaryPart δ z = z.im - δ * z.re

theorem CategoryTheory.Triangulated.WeakStabilityCondition.FiniteLength.exists_common_positive_functional {ι : Type u_1} [Fintype ι] [Nonempty ι] (z : ι → ℂ) (hz : ∀ (i : ι), z i ∈ semiClosedUpperHalfPlane) : ∃ (δ : ℝ) (c : ℝ), 0 < δ ∧ 0 < c ∧ ∀ (i : ι), c ≤ tiltedImaginaryPart δ (z i)

Finitely many vectors in the semi-closed upper half plane admit a common strictly positive direction and a uniform positive lower bound.

The direction is the real functional z.im - δ * z.re, with δ > 0. It is the dot product with (-δ, 1); division by its positive norm gives the equivalent unit-direction formulation.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.FiniteLength.exists_common_unit_direction {ι : Type u_1} [Fintype ι] [Nonempty ι] (z : ι → ℂ) (hz : ∀ (i : ι), z i ∈ semiClosedUpperHalfPlane) : ∃ (u : ℂ) (c : ℝ), ‖u‖ = 1 ∧ 0 < c ∧ ∀ (i : ι), c ≤ (z i * (starRingEnd ℂ) u).re

Unit-vector form of exists_common_positive_functional: after one rotation, the real parts of a finite family of upper-half-plane vectors have a uniform positive lower bound.

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

The literal finite-heart part of algebraicity: every object of the canonical heart is Artinian and Noetherian, and a finite list exhausts its simple objects up to isomorphism.

Equations

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

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

The currently explicit categorical bridge from a finite-length heart to the slicing: same-phase Jordan--Hölder filtrations exist, and stable objects are shifts of finitely many representatives. Deriving this bridge from HasFiniteLengthHeart is the missing Jordan--Hölder lane (#1203).

Equations

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

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

An algebraic stability condition, with the unresolved heart-to-slicing Jordan--Hölder bridge kept explicit rather than inferred from local finiteness.

Equations

• σ.IsAlgebraic = (σ.HasFiniteLengthHeart ∧ σ.HasFiniteStableOrbits)

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.IsAlgebraic.hasJordanHolder {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v₀ : K₀ C →+ Λ} {σ : WithClassMap C v₀} (h : σ.IsAlgebraic) : σ.slicing.HasJordanHolderFiltrations

An algebraic stability condition has the explicit Jordan--Hölder input required by stable-object reduction.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.IsAlgebraic.exists_classicalGenerator {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v₀ : K₀ C →+ Λ} {σ : WithClassMap C v₀} (h : σ.IsAlgebraic) : ∃ (n : ℕ) (S : Fin n → C), (∀ (i : Fin n), ∃ (φ : ℝ), σ.slicing.IsStableAt φ (S i)) ∧ ObjectProperty.IsClassicalTriangulatedGenerator fun (E : C) => ∃ (i : Fin n), Nonempty (E ≅ S i)

The finite stable representatives of a nonzero algebraic stability condition classically generate the ambient triangulated category. This is assembled from the explicit Jordan--Hölder bridge and the slicing's HN towers.

noncomputable def CategoryTheory.Triangulated.StabilityCondition.WithClassMap.IsAlgebraic.totalShiftedHomRank {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [HasShift C ℤ] (A B : C) : ℕ

The total dimension of all shifted Hom-spaces from A to B.

Equations

• CategoryTheory.Triangulated.StabilityCondition.WithClassMap.IsAlgebraic.totalShiftedHomRank A B = ∑ᶠ (m : ℤ), Module.finrank k (A ⟶ (CategoryTheory.shiftFunctor C m).obj B)

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.IsAlgebraic.hasGlobalMassHomBound {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] [HomFiniteBounded k C] {Λ : Type u'} [AddCommGroup Λ] {v₀ : K₀ C →+ Λ} {σ : WithClassMap C v₀} (h : σ.IsAlgebraic) : σ.HasGlobalMassHomBound

An algebraic stability condition on a proper category has a mass--Hom bound. Properness is the explicit HomFiniteBounded hypothesis; it is not inferred from finite length of the heart.