Uniqueness and finiteness of Harder--Narasimhan mass

This file develops choice-free mass for a bare slicing and additive charge.

The categorical input is a head--tail decomposition. Octahedral induction turns an HN tower into a distinguished triangle

  F₀ ⟶ E ⟶ E_{< φ₀} ⟶ F₀[1]

whose third object carries the tail HN filtration. For two filtrations with nonzero first factors, the first phases agree. The t-structure induced by the phase-shifted slicing then identifies the two head--tail triangles. Induction on the total filtration length, deleting zero first factors when necessary, proves equality of all finite mass sums.

The induction never consults the compatibility ray of the stability condition: it runs on the slicing and on an additive charge alone. It is therefore stated for a bare carrier (s : Slicing C, Z : K₀ C →+ ℂ) — classCharge, HNFiltration.classMass, Slicing.classMass. The strong Bridgeland wrappers live downstream in StabilityCondition/Metric/Mass/Uniqueness.lean; the weak parent imports only this carrier-level theorem.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.classCharge {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (Z : K₀ C →+ ℂ) (E : C) : ℂ

An additive charge on the class lattice, evaluated on the K₀ class of an object. This is PreStabilityCondition.WithClassMap.charge with the charge decoupled from any prestability structure, so the mass-uniqueness induction in this file can serve any carrier providing a slicing and a charge — in particular the weak stability conditions of §14, whose closed compatibility ray cannot inhabit WithClassMap.

Equations

• CategoryTheory.Triangulated.classCharge Z E = Z (CategoryTheory.Triangulated.K₀.of C E)

noncomputable def CategoryTheory.Triangulated.HNFiltration.classMass {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (Z : K₀ C →+ ℂ) {P : ℝ → ObjectProperty C} {E : C} (F : HNFiltration C P E) : ENNReal

The finite mass sum of one HN filtration, for a bare additive charge. HNFiltration.mass is definitionally this at Z = σ.Z.comp v, because charge is an abbreviation for Z ∘ classOf.

Equations

• CategoryTheory.Triangulated.HNFiltration.classMass Z F = ∑ i : Fin F.n, ENNReal.ofReal ‖CategoryTheory.Triangulated.classCharge Z (F.factor i)‖

noncomputable def CategoryTheory.Triangulated.Slicing.classMass {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (Z : K₀ C →+ ℂ) (E : C) : ENNReal

The choice-free mass envelope of an object, for a slicing and a bare additive charge. stabilityMass is definitionally this at (σ.slicing, σ.Z.comp v).

Equations

• s.classMass Z E = ⨆ (F : CategoryTheory.Triangulated.HNFiltration C s.P E), CategoryTheory.Triangulated.HNFiltration.classMass Z F

theorem CategoryTheory.Triangulated.HNFiltration.classMass_eq_zero_of_isZero {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {s : Slicing C} (Z : K₀ C →+ ℂ) {E : C} (F : HNFiltration C s.P E) (hE : Limits.IsZero E) : classMass Z F = 0

Every HN filtration of a zero object has zero mass. This also rules out spurious positive mass coming from a nontrivial tower of a zero object.

theorem CategoryTheory.Triangulated.HNFiltration.classMass_eq_classMass {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {s : Slicing C} (Z : K₀ C →+ ℂ) {E : C} (F G : HNFiltration C s.P E) : classMass Z F = classMass Z G

HN mass is independent of the chosen HN filtration.

theorem CategoryTheory.Triangulated.Slicing.classMass_eq_classMass {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) (Z : K₀ C →+ ℂ) {E : C} (F : HNFiltration C s.P E) : s.classMass Z E = HNFiltration.classMass Z F

The choice-free mass envelope is the mass sum of every HN filtration.

theorem CategoryTheory.Triangulated.Slicing.classMass_ne_top {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) (Z : K₀ C →+ ℂ) (E : C) : s.classMass Z E ≠ ⊤

The ordinary HN mass is always finite.

theorem CategoryTheory.Triangulated.Slicing.classMass_lt_top {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) (Z : K₀ C →+ ℂ) (E : C) : s.classMass Z E < ⊤

theorem CategoryTheory.Triangulated.Slicing.classMass_toReal_eq_sum {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) (Z : K₀ C →+ ℂ) {E : C} (F : HNFiltration C s.P E) : (s.classMass Z E).toReal = ∑ i : Fin F.n, ‖classCharge Z (F.factor i)‖

Real-valued form of the mass identification: this is the literal finite sum of the norms of the HN-factor charges.

theorem CategoryTheory.Triangulated.Slicing.classMass_eq_ofReal_norm_classCharge {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) (Z : K₀ C →+ ℂ) {E : C} {φ : ℝ} (hP : s.P φ E) : s.classMass Z E = ENNReal.ofReal ‖classCharge Z E‖

A semistable object's mass is the norm of its charge, in ℝ≥0∞.

The toReal form is stabilityMass_toReal_eq_norm_charge; this is the un-truncated statement, which is what an additive splitting argument needs.

theorem CategoryTheory.Triangulated.Slicing.exists_headTail_classMass {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) (Z : K₀ C →+ ℂ) {E : C} (F : HNFiltration C s.P E) (hn : 0 < F.n) : ∃ (Y : C) (G : HNFiltration C s.P Y) (f : F.factor ⟨0, hn⟩ ⟶ E) (g : E ⟶ Y) (h : Y ⟶ (shiftFunctor C 1).obj (F.factor ⟨0, hn⟩)), Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles ∧ s.classMass Z E = s.classMass Z (F.factor ⟨0, hn⟩) + s.classMass Z Y ∧ G.n = F.n - 1

Public head/tail split of the mass, stated entirely in stabilityMass.

exists_headTail is private and phrased with the private factorMass; this is the form downstream files can use. The head is the top HN factor, the tail is HN-filtered with one fewer factor, and the mass splits additively across the distinguished triangle joining them.

theorem CategoryTheory.Triangulated.HNFiltration.exists_headTail_classMass {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] (s : Slicing C) (Z : K₀ C →+ ℂ) {E : C} (F : HNFiltration C s.P E) (hn : 0 < F.n) : ∃ (Y : C) (G : HNFiltration C s.P Y) (f : F.factor ⟨0, hn⟩ ⟶ E) (g : E ⟶ Y) (h : Y ⟶ (shiftFunctor C 1).obj (F.factor ⟨0, hn⟩)), Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles ∧ (s.classMass Z E).toReal = ‖classCharge Z (F.factor ⟨0, hn⟩)‖ + (s.classMass Z Y).toReal ∧ G.n = F.n - 1 ∧ ∀ (j : Fin G.n), ∃ (i : Fin F.n), ↑i = ↑j + 1 ∧ G.φ j = F.φ i

Split off the highest-phase HN factor, preserving both the mass identity and the indexing of every phase in the tail.

This is the public form used by inductive mass arguments: unlike Slicing.exists_headTail_classMass, it retains the phase correspondence needed to re-establish strict HN separation after an octahedral step.