Bridgeland specializations of mass uniqueness

The choice-free mass theorem is owned by the weak parent and is stated for a bare slicing and additive charge. This file supplies the stronger Bridgeland wrappers, including positivity consequences that fail for weak stability.

theorem CategoryTheory.Triangulated.HNFiltration.mass_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] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) {E : C} (F : HNFiltration C σ.slicing.P E) (hE : Limits.IsZero E) : mass σ F = 0

Every HN filtration of a zero object has zero mass.

theorem CategoryTheory.Triangulated.HNFiltration.mass_eq_mass {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 →+ Λ} (σ : StabilityCondition.WithClassMap C v) {E : C} (F G : HNFiltration C σ.slicing.P E) : mass σ F = mass σ G

HN mass is independent of the chosen HN filtration.

theorem CategoryTheory.Triangulated.stabilityMass_eq_mass {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 →+ Λ} (σ : StabilityCondition.WithClassMap C v) {E : C} (F : HNFiltration C σ.slicing.P E) : stabilityMass σ E = HNFiltration.mass σ F

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

theorem CategoryTheory.Triangulated.stabilityMass_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] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) (E : C) : stabilityMass σ E ≠ ⊤

The ordinary HN mass is always finite.

theorem CategoryTheory.Triangulated.stabilityMass_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] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) (E : C) : stabilityMass σ E < ⊤

theorem CategoryTheory.Triangulated.stabilityMass_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] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : StabilityCondition.WithClassMap C v) {E : C} (F : HNFiltration C σ.slicing.P E) : (stabilityMass σ E).toReal = ∑ i : Fin F.n, ‖σ.charge (F.factor i)‖

Real-valued form of the mass identification.

theorem CategoryTheory.Triangulated.stabilityMass_eq_ofReal_norm_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 →+ Λ} (σ : StabilityCondition.WithClassMap C v) {E : C} {φ : ℝ} (hP : σ.slicing.P φ E) : stabilityMass σ E = ENNReal.ofReal ‖σ.charge E‖

A semistable object's mass is the norm of its charge.

theorem CategoryTheory.Triangulated.exists_headTail_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 →+ Λ} (σ : StabilityCondition.WithClassMap C v) {E : C} (F : HNFiltration C σ.slicing.P E) (hn : 0 < F.n) : ∃ (Y : C) (G : HNFiltration C σ.slicing.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 ∧ stabilityMass σ E = stabilityMass σ (F.factor ⟨0, hn⟩) + stabilityMass σ Y ∧ G.n = F.n - 1

Split off the highest-phase HN factor and retain the mass identity.

theorem CategoryTheory.Triangulated.HNFiltration.exists_headTail_mass {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 →+ Λ} (σ : StabilityCondition.WithClassMap C v) {E : C} (F : HNFiltration C σ.slicing.P E) (hn : 0 < F.n) : ∃ (Y : C) (G : HNFiltration C σ.slicing.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 ∧ (stabilityMass σ E).toReal = ‖σ.charge (F.factor ⟨0, hn⟩)‖ + (stabilityMass σ 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 while retaining phase indices.

@[simp]

theorem CategoryTheory.Triangulated.stabilityMass_eq_zero_iff {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 →+ Λ} (σ : StabilityCondition.WithClassMap C v) (E : C) : stabilityMass σ E = 0 ↔ Limits.IsZero E

Mass vanishes exactly on zero objects.

theorem CategoryTheory.Triangulated.stabilityMass_toReal_pos {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 →+ Λ} (σ : StabilityCondition.WithClassMap C v) {E : C} (hE : ¬Limits.IsZero E) : 0 < (stabilityMass σ E).toReal

The real-valued mass coordinate is strictly positive on nonzero objects.