Perimeter comparison for Harder--Narasimhan polygons

The Harder--Narasimhan reading of the neutral perimeter comparison in Analysis/Convex/ComplexPolygonalPath/Perimeter.lean: the vertices are subobject charges, the edges are semistable-factor charges, and the path length is the mass.

Main declarations

• polygonLength_le_of_vertexHull_subset, for applications that already have containment of the two closed finite vertex polygons.
• polygonLength_le_add_norm_charge_sub_of_mono, the boundary-cut comparison along a monomorphism, and its mass_le_add_norm_cokernel_of_mono and mass_le_add_norm_of_shortExact mass forms.
• mass_eq_mass, independence of the mass of the chosen HN filtration.

Source

Ikeda, A phase limit formula and the space of stability conditions, Lemmas 3.7 and 3.8, at t = 0. Lemma 3.8 is strengthened at that parameter by not requiring the cokernel to have phase one: that hypothesis controls the exponential weight for general t and disappears when t = 0. No claim that the full ambient HN polygon is the closed HN vertex hull is used -- it is false in general; positive-angle support maxima of the ambient polygon come from HNPolygon instead.

Placement

This file is the stability adapter half of what was StabilityCondition/Metric/Mass/Subadditivity/PolygonPerimeter.lean. MO1.13 (#1324) sent the Euclidean half to its neutral owner and gave what stayed a name for its subject -- the HN polygon comparison -- rather than for the shape of its proof. The citation above travels with it unchanged.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.polygonLength_le_of_vertexHull_subset {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E E' : A} (F : AbelianHNFiltration Z E) (G : AbelianHNFiltration Z E') (hcharge : Z.charge E = Z.charge E') (hcontain : (convexHull ℝ) (Set.range F.polygonVertex) ⊆ (convexHull ℝ) (Set.range G.polygonVertex)) : F.polygonLength ≤ G.polygonLength

HN-path specialization of the finite perimeter comparison for applications which already have containment of the two closed finite vertex polygons. The monomorphism comparison below uses the more precise ambient support theorem instead of trying to derive this hypothesis from full ambient HN-polygon containment.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.polygonLength_le_add_norm_charge_sub_of_mono {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E E' : A} (F : AbelianHNFiltration Z E) (G : AbelianHNFiltration Z E') (hHN : Z.HasHNProperty) (f : E ⟶ E') [Mono f] : F.polygonLength ≤ G.polygonLength + ‖Z.charge E - Z.charge E'‖

Boundary-cut HN polygon comparison. If E ⟶ E' is monic, the HN path of E is no longer than the HN path of E' followed by the single edge from Z(E') back to Z(E).

This is the t = 0 comparison used in Ikeda's Lemma 3.8, strengthened at that parameter by not requiring the cokernel to have phase one. (That phase hypothesis controls the exponential weight for general t; it disappears when t = 0.) The final edge is allowed to lie on the positive real boundary when the cokernel does have phase one. No false claim that the full ambient HN polygon is the closed HN vertex hull is used. Instead, positive-angle support maxima of the ambient polygon are supplied by HNPolygon and the finite support-fan perimeter theorem closes the argument.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.mass_le_add_norm_cokernel_of_mono {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E E' : A} (F : AbelianHNFiltration Z E) (G : AbelianHNFiltration Z E') (hHN : Z.HasHNProperty) (f : E ⟶ E') [Mono f] : F.mass ≤ G.mass + ‖Z.charge (Limits.cokernel f)‖

Mass form of the boundary-cut comparison. The closing-edge charge is the negative of the cokernel charge, by additivity of the stability function.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.mass_le_add_norm_of_shortExact {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} (S : ShortComplex A) (hS : S.ShortExact) (F : AbelianHNFiltration Z S.X₁) (G : AbelianHNFiltration Z S.X₂) (hHN : Z.HasHNProperty) : F.mass ≤ G.mass + ‖Z.charge S.X₃‖

Short-exact-sequence form of the boundary-cut comparison.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.mass_eq_mass {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F G : AbelianHNFiltration Z E) (hHN : Z.HasHNProperty) : F.mass = G.mass

The mass of an abelian HN filtration is independent of the chosen filtration. This is the identity-monomorphism specialization of the boundary-cut comparison.