Harder--Narasimhan mass

For an HN filtration F of E, its mass is the finite sum

  ∑ i, ‖Z(F.factor i)‖.

WeakStabilityCondition/Foundation/Slicing/IntrinsicPhases.lean proves that the extreme phases of an HN filtration are intrinsic, but nothing exposes uniqueness of the complete HN filtration. Defining the mass using Classical.choice (s.hn_exists E) would therefore make its transport law depend on an arbitrary, non-functorial choice. We first take the supremum of the masses of all HN filtrations. This is choice-free and lives naturally in ℝ≥0∞.

WeakStabilityCondition/StabilityCondition/Metric/Mass/Uniqueness.lean subsequently proves that every term in this supremum is equal, identifying stabilityMass with the usual finite Bridgeland mass.

noncomputable def CategoryTheory.Triangulated.HNFiltration.mass {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) {E : C} (F : HNFiltration C σ.slicing.P E) : ENNReal

The finite mass sum attached to one HN filtration.

Stated over StabilityCondition.WithClassMap for uniformity with the rest of the §8 track, but note that the mass API never projects locallyFinite: Bridgeland §5 defines m_σ from the slicing and the charge alone. The parent field is not a class, so Lean generates no coercion and dropping it would require .toWithClassMap at every positional call site — hence this comment rather than a weakening. [IsTriangulated C] is genuinely needed downstream, for someOctahedron in HNMassUniqueness.

Equations

• CategoryTheory.Triangulated.HNFiltration.mass σ F = ∑ i : Fin F.n, ENNReal.ofReal ‖σ.charge (F.factor i)‖

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.charge_ne_zero_of_semistable {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WithClassMap C v) (φ : ℝ) (E : C) (hP : σ.slicing.P φ E) (hE : ¬Limits.IsZero E) : σ.charge E ≠ 0

A nonzero semistable object has nonzero charge.

theorem CategoryTheory.Triangulated.HNFiltration.mass_pos {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) {E : C} (F : HNFiltration C σ.slicing.P E) (hE : ¬Limits.IsZero E) : 0 < mass σ F

Every HN filtration of a nonzero object has strictly positive finite-sum mass.

@[simp]

theorem CategoryTheory.Triangulated.HNFiltration.mass_ofIso {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) {E E' : C} (F : HNFiltration C σ.slicing.P E) (e : E ≅ E') : mass σ (ofIso C F e) = mass σ F

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

The choice-free HN mass envelope of an object. Downstream, stabilityMass_eq_mass identifies it with the mass of every HN filtration.

Equations

• CategoryTheory.Triangulated.stabilityMass σ E = ⨆ (F : CategoryTheory.Triangulated.HNFiltration C σ.slicing.P E), CategoryTheory.Triangulated.HNFiltration.mass σ F

theorem CategoryTheory.Triangulated.stabilityMass_pos {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) {E : C} (hE : ¬Limits.IsZero E) : 0 < stabilityMass σ E

The mass envelope is positive on every nonzero object.

theorem CategoryTheory.Triangulated.stabilityMass_congr {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) {E E' : C} (e : E ≅ E') : stabilityMass σ E = stabilityMass σ E'

The mass envelope depends on an object only up to isomorphism.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair.act_charge {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (a : AutPair v) (σ : StabilityCondition.WithClassMap C v) (E : C) : (a.act σ).charge E = σ.charge (a.Φ.e.inverse.obj E)

The charge of an acted stability condition is the original charge of the inverse-image object.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair.mass_map_inverse {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (a : AutPair v) (σ : StabilityCondition.WithClassMap C v) {E : C} (F : HNFiltration C (a.act σ).slicing.P E) : HNFiltration.mass σ (F.mapF a.Φ.e.inverse ⋯) = HNFiltration.mass (a.act σ) F

Mapping an HN filtration backward through the equivalence preserves its finite mass sum.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair.mass_map_functor {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (a : AutPair v) (σ : StabilityCondition.WithClassMap C v) {E : C} (F : HNFiltration C σ.slicing.P E) : HNFiltration.mass (a.act σ) (F.mapF a.Φ.e.functor ⋯) = HNFiltration.mass σ F

Mapping an HN filtration forward through the equivalence preserves its finite mass sum.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair.act_stabilityMass {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (a : AutPair v) (σ : StabilityCondition.WithClassMap C v) (E : C) : stabilityMass (a.act σ) E = stabilityMass σ (a.Φ.e.inverse.obj E)

Transport by a compatible autoequivalence replaces an object by its inverse image and leaves the mass envelope unchanged.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair.act_stabilityMass_functor_obj {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (a : AutPair v) (σ : StabilityCondition.WithClassMap C v) (E : C) : stabilityMass (a.act σ) (a.Φ.e.functor.obj E) = stabilityMass σ E

Objectwise form of mass invariance, with the object moved forward.