Harder--Narasimhan polygon paths for mass subadditivity #
This file supplies the algebraic path underlying the HN polygon of an object in an abelian category with a stability function. Its vertices are the charges of the subobjects in an abelian HN filtration. Consecutive edge vectors are proved to be the charges of the semistable factors, so the polygonal path length is exactly the usual sum of factor masses.
Convex-hull containment under monomorphisms, strict support of interior path vertices, and the semistable-descent/maximal-phase algebra needed for the ambient boundary theorem are proved separately below; none is hidden inside the path representation.
The planar carrier itself is not here. ComplexPolygonalPath.length, the
cross and unit-ray functionals and the supporting-hyperplane lemma say nothing
about objects or filtrations, and MO1.13 (#1324) moved them to their neutral
owner Analysis/Convex/ComplexPolygonalPath/Basic.lean, which this file
imports. What remains here is the Harder--Narasimhan reading of that carrier.
The support-completeness theorem for every positive-angle direction is stated explicitly and avoids identifying the whole ambient polygon with the closed HN vertex hull, which is false in general.
The HN polygon of an object: the convex hull of the charges of all its subobjects. This is the paper's ambient polygon; a chosen HN filtration below provides its distinguished decreasing-phase boundary path.
Equations
- Z.hnPolygon E = (convexHull ℝ) (Set.range fun (S : CategoryTheory.Subobject E) => Z.charge (CategoryTheory.Subobject.underlying.obj S))
Instances For
Every subobject charge is a point of the HN polygon.
A monomorphism induces inclusion of HN polygons: pushing a subobject forward along the monomorphism does not change its underlying object up to isomorphism, hence does not change its charge.
The tail of an HN filtration after the k-th vertex, transported to the
quotient by that vertex. Its factors are precisely the original factors at
indices k, ..., n - 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The quotient of S by S ∩ K maps canonically into E / K.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical map S / (S ∩ K) → E / K is a monomorphism.
A semistable subobject whose phase is strictly larger than every HN
factor from index k onward is contained in the k-th filtration step.
This public descent lemma is the algebraic engine behind the left boundary of
the HN polygon.
No nonzero semistable subobject has phase strictly above the first HN factor.
The object represented by the i-th successive quotient in an abelian HN
filtration.
Equations
Instances For
The charge vertices of the HN polygonal path.
Equations
- F.polygonVertex j = Z.charge (CategoryTheory.Subobject.underlying.obj (F.chain j))
Instances For
A directed edge of the distinguished HN polygonal path.
Equations
- F.polygonEdge i = F.polygonVertex i.succ - F.polygonVertex i.castSucc
Instances For
The length of the distinguished, decreasing-phase boundary path of the HN polygon.
Instances For
The abelian HN mass: the sum of the norms of the factor charges.
Instances For
A consecutive HN polygon edge is the charge of the corresponding semistable factor.
Every HN polygon edge lies in Bridgeland's semi-closed upper half-plane.
The argument of an HN polygon edge is π times the phase of its
factor.
HN polygon edges turn strictly clockwise: their arguments strictly decrease along the filtration.
Every interior HN vertex is a strict supporting point of the distinguished HN path: a continuous real-linear functional has a unique maximum there among all path vertices. This is the path-level extremality input used by HN-polygon containment arguments.
The length of the HN polygonal boundary is exactly its factor mass.
The initial HN polygon vertex is the origin.
The terminal HN polygon vertex is the charge of the filtered object.
The phase of the filtered object is at most the phase of the first HN factor.
The phase of the last HN factor is at most the phase of the filtered object.
A nonzero map from a filtration prefix to a semistable object cannot land strictly below the phase of the prefix's last factor. The proof extends zero-vanishing one HN factor at a time.
Assuming the HN property, every nonzero subobject has phase at most the first phase of a chosen HN filtration. The proof takes the first HN factor of the subobject, embeds its first filtration step into the ambient object, and applies semistable descent.
Every nonzero quotient of a filtration prefix has phase at least the phase of the prefix's last HN factor. We compose with the last semistable factor of an HN filtration of the quotient and use factor-by-factor vanishing on the prefix.
The quotient S / (S ∩ E_k) lies in the phase range of the HN tail:
its phase is at most the phase of the next factor.
A vertex which maximizes a cross-product support functional on the distinguished HN path also maximizes it against every subobject charge.
This is the support-function form of the statement that the HN path is the
left boundary of the ambient HN polygon. Unlike the stronger (and generally
false) assertion that the whole ambient polygon is the convex hull of the HN
vertices, it only controls support directions with angle in (0, π). Those
are exactly the directions used by the polygon-perimeter comparison.
The proof cuts an arbitrary subobject S at the maximizing filtration vertex
K = E_k. The quotient S / (S ∩ K) lies no higher than the next HN ray,
while K / (S ∩ K) lies no lower than the preceding HN ray. Maximality on
the two neighboring path vertices places the support ray between them, so the
two quotient contributions have opposite signs.
Every positive-angle support functional reaches its ambient HN-polygon maximum on the distinguished HN path.
Every interior HN vertex is strictly supported against the charge of
every other subobject. At the cut K = E_k, the charge difference splits as
Z(S) - Z(K) = Z(S / (S ∩ K)) - Z(K / (S ∩ K)).
The first quotient lies below the next HN ray and the second lies above the
preceding HN ray, so the cross-product functional at an intermediate angle is
strictly smaller on S.
Every interior HN path vertex is an exposed point of the full ambient HN polygon: it is the strict unique maximizer of a continuous real-linear functional over the convex hull of all subobject charges.
Every vertex of the distinguished HN path lies in the ambient HN polygon.
The norm of the total charge is bounded by the HN polygon length.
The norm of the total charge is bounded by the sum of the HN factor masses.