Exact mass splitting across a distinguished triangle

This file owns the cases in which Harder--Narasimhan mass is exactly additive along a distinguished triangle: when the two filtrations are phase separated, when the endpoints are cut by a gtProp/leProp boundary, and when both endpoints are semistable of a common phase. The easy triangle inequalities that follow directly from additivity are proved here too.

The hard arbitrary-left case is developed in PhaseOne and Consequences.

theorem CategoryTheory.Triangulated.stabilityMass_toReal_triangle_eq_add_of_hn_separated {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) {X E Y : C} (GX : HNFiltration C σ.slicing.P X) (GY : HNFiltration C σ.slicing.P Y) (f : X ⟶ E) (g : E ⟶ Y) (h : Y ⟶ (shiftFunctor C 1).obj X) (hT : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles) (hsep : ∀ (i : Fin GY.n) (j : Fin GX.n), GY.φ i < GX.φ j) : (stabilityMass σ E).toReal = (stabilityMass σ X).toReal + (stabilityMass σ Y).toReal

HN mass is exactly additive across a distinguished triangle when every phase of the right-hand HN filtration is strictly below every phase of the left-hand filtration. The proof peels the right filtration from its head and uses the octahedral axiom to append that factor to the left filtration.

theorem CategoryTheory.Triangulated.stabilityMass_toReal_triangle_eq_add_of_gtProp_leProp {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) {X E Y : C} (f : X ⟶ E) (g : E ⟶ Y) (h : Y ⟶ (shiftFunctor C 1).obj X) (hT : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles) (t : ℝ) (hX : Slicing.gtProp C σ.slicing t X) (hY : Slicing.leProp C σ.slicing t Y) : (stabilityMass σ E).toReal = (stabilityMass σ X).toReal + (stabilityMass σ Y).toReal

Intrinsic cutoff form of exact mass splitting. If the left endpoint has all HN phases strictly above t and the right endpoint has all phases at most t, the middle mass is the sum of the endpoint masses.

theorem CategoryTheory.Triangulated.stabilityMass_toReal_eq_heartCoh_negOne_add_zero {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) (X : C) (hgt : Slicing.gtProp C σ.slicing 0 X) (hle : Slicing.leProp C σ.slicing 2 X) : (stabilityMass σ X).toReal = (stabilityMass σ (Tilting.originalHeartCoh (Slicing.toTStructure C σ.slicing) (-1) X).obj).toReal + (stabilityMass σ (Tilting.originalHeartCoh (Slicing.toTStructure C σ.slicing) 0 X).obj).toReal

On the amplitude window with phases in (0, 2], mass is the sum of the masses of the only two possibly nonzero heart-cohomology objects.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.charge_triangle {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) (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) : σ.charge T.obj₂ = σ.charge T.obj₁ + σ.charge T.obj₃

The charge of the middle object in a distinguished triangle is the sum of the endpoint charges.

theorem CategoryTheory.Triangulated.stabilityMass_triangle_le_of_obj₂_semistable {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) (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) {φ : ℝ} (h₂ : σ.slicing.P φ T.obj₂) : (stabilityMass σ T.obj₂).toReal ≤ (stabilityMass σ T.obj₁).toReal + (stabilityMass σ T.obj₃).toReal

Mass is subadditive along a distinguished triangle whose middle object is semistable.

theorem CategoryTheory.Triangulated.stabilityMass_triangle_le_of_same_phase {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) (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (φ : ℝ) (h₁ : σ.slicing.P φ T.obj₁) (h₃ : σ.slicing.P φ T.obj₃) : (stabilityMass σ T.obj₂).toReal ≤ (stabilityMass σ T.obj₁).toReal + (stabilityMass σ T.obj₃).toReal

Mass is subadditive when both endpoints of a distinguished triangle are semistable of the same phase.

theorem CategoryTheory.Triangulated.stabilityMass_toReal_triangle_eq_add_of_same_phase {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) (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (φ : ℝ) (h₁ : σ.slicing.P φ T.obj₁) (h₃ : σ.slicing.P φ T.obj₃) : (stabilityMass σ T.obj₂).toReal = (stabilityMass σ T.obj₁).toReal + (stabilityMass σ T.obj₃).toReal

Mass is exactly additive when both endpoints of a distinguished triangle lie in one semistable slice. The middle object is in the same slice by extension closure, and all three charges lie on the same ray.

theorem CategoryTheory.Triangulated.stabilityMass_triangle_le_of_obj₁_phase_one_of_obj₃_le_one {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) (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (h₁ : σ.slicing.P 1 T.obj₁) (h₃ : Slicing.leProp C σ.slicing 1 T.obj₃) : (stabilityMass σ T.obj₂).toReal ≤ (stabilityMass σ T.obj₁).toReal + (stabilityMass σ T.obj₃).toReal

At the upper boundary of the canonical heart, a semistable left endpoint can be prepended to an arbitrary heart object without increasing mass beyond the sum of the endpoint masses.

If the right endpoint has no phase-one HN factor, the two endpoint filtrations are strictly separated. Otherwise its unique phase-one head is first combined with the left endpoint; that extension remains in P(1), and the remaining HN tail is strictly lower. This is the precise mass comparison behind the "easy to check" phase-one extension step in Ikeda's proof of Proposition 3.3.