Named inequality targets and the heart short-exact bridge

This file owns the statement-level interface of the subadditivity milestone -- the Prop-valued named targets -- together with the bridge between a short exact sequence in the canonical heart and the distinguished triangle it generates. It converts an abelian Harder--Narasimhan filtration into an ambient tower of the same mass and proves the phase-one boundary-heart inequality.

Definitions of the targets are kept above their proofs so that a consumer may depend on the statement without the proof's import surface.

def CategoryTheory.Triangulated.StabilityMassBoundaryHeartInequality {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 →+ Λ} : Prop

The first major mass-triangle milestone, in its phase-one boundary-heart form. For a short exact sequence 0 ⟶ A ⟶ B ⟶ C ⟶ 0 in the canonical heart with C ∈ P(1), the mass of A is at most the combined mass of B and C.

This is a named proof target, not an installed premise.

Equations

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

def CategoryTheory.Triangulated.StabilityMassSemistableLeftTriangleInequality {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 →+ Λ} : Prop

The second paper-level mass-triangle milestone: subadditivity for a distinguished triangle whose first object is semistable.

Equations

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

theorem CategoryTheory.Triangulated.stabilityMassTriangleInequality_of_semistable_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 →+ Λ} (hsemistable : StabilityMassSemistableLeftTriangleInequality) : StabilityMassTriangleInequality

The arbitrary-left octahedral milestone. Once the triangle inequality is known for semistable first objects, split an HN filtration of the first object into its head and tail. The octahedron produces one semistable-left triangle and a shorter arbitrary-left triangle, so induction proves the unrestricted statement.

def CategoryTheory.Triangulated.StabilityMassHeartShortExactInequality {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 →+ Λ} : Prop

The first remaining polygonal milestone: mass subadditivity for every short exact sequence in the canonical heart P((0, 1]).

Equations

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

theorem CategoryTheory.Triangulated.heartShortExact_exists_distinguished_triangle {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) (S : ShortComplex (Slicing.toTStructure C σ.slicing).heart.FullSubcategory) (hS : S.ShortExact) : ∃ (δ : S.X₃.obj ⟶ (shiftFunctor C 1).obj S.X₁.obj), Pretriangulated.Triangle.mk S.f.hom S.g.hom δ ∈ Pretriangulated.distinguishedTriangles

A short exact sequence in the canonical heart is induced by a distinguished triangle on its underlying ambient objects.

theorem CategoryTheory.Triangulated.phaseOne_endpoints_of_heart_shortExact {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) (S : ShortComplex (Slicing.toTStructure C σ.slicing).heart.FullSubcategory) (hS : S.ShortExact) (h₂ : σ.slicing.P 1 S.X₂.obj) : σ.slicing.P 1 S.X₁.obj ∧ σ.slicing.P 1 S.X₃.obj

In a short exact sequence in the canonical heart, if the middle object lies on the phase-one boundary ray, then both endpoint objects do as well. This is the boundary-specific kernel/image closure used in the six-term cohomology argument; it does not assert the false general closure of P(φ) under arbitrary heart subobjects.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.mass_eq_stabilityMass_toReal {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 : (Slicing.toTStructure C σ.slicing).heart.FullSubcategory} (F : AbelianHNFiltration σ.observableStabilityFunctionOnHeart E) : F.mass = (stabilityMass σ E.obj).toReal

An abelian HN filtration in the canonical heart is also an ambient HN filtration after replacing each short exact successive quotient by its distinguished triangle. Consequently its factor-norm mass is exactly the ambient stabilityMass.

theorem CategoryTheory.Triangulated.stabilityMassBoundaryHeartInequality {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 →+ Λ} : StabilityMassBoundaryHeartInequality

The phase-one boundary-heart mass inequality. The nonzero case is the boundary-cut comparison for abelian HN polygons, transported to ambient mass by AbelianHNFiltration.mass_eq_stabilityMass_toReal; the zero source case is handled directly.