Weak stability: the definitions of §14 #
Definitions 14.1–14.3 of arXiv:1902.08184v4, on the abstract layer, together with the embedding of ordinary stability into the weak structure.
What "weak" changes and nothing else: at integer phases the central
charge of a nonzero semistable object may lie on the closed ray
ℝ_{≥0}·e^{iπφ} — in particular it may vanish — while at non-integer phases
the open-ray condition of an ordinary prestability condition is kept. On a
heart, the values land in ℍ ⊔ ℝ_{≤0} rather than ℍ ⊔ ℝ_{<0}. The objects
of charge zero form the subcategory A⁰ of Definition 14.3, whose closure
properties under subobjects, quotients and extensions are proved here from
K₀ additivity and elementary half-plane arithmetic.
Phrasing choices, stated for the reviewer #
- The heart is carried inside
Cast.heart, followingWeakStabilityCondition/Tilting/TorsionPair/Heart.lean. The pinned Mathlib does supplyt.heartFullSubcategoryAbelian; triangle-form subobject data is retained here because it stays in the ambient category where the charge and slicing live.TStructure.heartFullSubcategory_shortExact_of_distTriangidentifies those heart triangles with short exact sequences in the abelian heart. - The paper's
K(A)is replaced by the ambientK₀ C, on which this library's charges already live; the positivity conditions quantify over heart objects only. The comparisonK(A) ≅ K(D)for a bounded t-structure is not available at the pin and is not assumed — nothing here needs it. - Slopes take values in
WithTop ℝ, withμ = +∞exactly when the charge has vanishing imaginary part, as in Definition 14.2. - No binding to any statement of the paper is claimed. These declarations
are candidates for the §14 coordinates of the coverage map; promotion past
targetis a separate, evidence-gated act (#111).
Definition 14.1: weak prestability conditions #
The weak parent data has the compatibility ray closed at integer phases and open elsewhere. Ordinary prestability extends this structure downstream, so the weak layer does not import its stronger child.
A weak prestability condition with respect to a class map v : K₀ C →+ Λ
(Definition 14.1): a slicing and a central charge on Λ such that a nonzero
semistable object of phase φ has charge on the ray ℝ_{>0}·e^{iπφ} when
φ ∉ ℤ, and on the closed ray ℝ_{≥0}·e^{iπφ} — so possibly zero — when
φ ∈ ℤ.
- slicing : Slicing C
The underlying slicing.
The central charge on the class lattice
Λ.- compat' (φ : ℝ) (E : C) : self.slicing.P φ E → ¬Limits.IsZero E → ∃ (m : ℝ), 0 ≤ m ∧ ((∀ (n : ℤ), φ ≠ ↑n) → 0 < m) ∧ self.Z (v (K₀.of C E)) = ↑m * Complex.exp (↑(Real.pi * φ) * Complex.I)
Compatibility: nonnegative radius always, positive off the integers.
Instances For
Definition 14.2: weak stability functions on a heart #
A weak stability function on the heart of t (Definition 14.2): an
additive charge whose value on every nonzero heart object lies in
ℍ ⊔ ℝ_{≤0} = {z : 0 < Im z} ∪ {z : Im z = 0 ∧ Re z ≤ 0}.
This is WeakStabilityFunctionOn at heartDatum t — the ambient
instantiation of the one charge-positivity structure — not a structure of
its own. The half-plane it used to write out by hand is
closedUpperHalfPlane, and the two agree definitionally. Z keeps its name
as a field and upper keeps its name and argument shape as a theorem below,
so consumers are unaffected.
Equations
Instances For
An ordinary stability function on the heart of t: values on nonzero
heart objects lie in ℍ ⊔ ℝ_{<0}, the strict form. Carried here so the
embedding into the weak structure is a theorem rather than prose.
This is StabilityFunctionOn at heartDatum t, at
semiClosedUpperHalfPlane. The strict-implies-weak embedding is
StabilityFunctionOn.toWeak, proved once for every class datum rather than
once here.
Equations
Instances For
Values on nonzero heart objects lie in ℍ ⊔ ℝ_{≤0} — the defining
positivity, in the curried argument shape consumers use. Formerly a structure
field; now the datum's positivity condition, unfolded.
Values on nonzero heart objects lie in ℍ ⊔ ℝ_{<0} — the strict form,
in the curried argument shape consumers use.
Ordinary stability functions are weak stability functions:
ℝ_{<0} ⊆ ℝ_{≤0}, same charge.
The inclusion is StabilityFunctionOn.toWeak, proved once for every class
datum. This wrapper preserves the name and signature the §14 lane uses.
Instances For
The charge of an object: Z evaluated at its K₀ class.
Equations
- W.charge E = W.Z (CategoryTheory.Triangulated.K₀.of C E)
Instances For
Charges are additive on distinguished triangles, by the defining relation
of K₀.
charge_triangle, specialised to an explicit Triangle.mk so the
projections are already reduced.
The charge of a zero object vanishes.
The slope of Definition 14.2: -Re Z(E)/Im Z(E) when Im Z(E) > 0, and
+∞ otherwise.
Instances For
The charge is invariant under isomorphism of ambient objects.
The weak slope is invariant under isomorphism of ambient objects.
Z-semistability (Definition 14.2): every subobject has slope at most
the slope of the corresponding quotient. Subobject data is a distinguished
triangle with all three vertices in the heart — for heart objects that is a
short exact sequence — and both ends are required nonzero, matching the
paper's quantification over proper nonzero subobjects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Z-stability: every proper nonzero subobject has slope strictly smaller
than the corresponding nonzero quotient. This is the strict counterpart of
IsSemistable, expressed using the same ambient distinguished triangles.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A weak-stable object is weak-semistable.
Weak semistability is invariant under isomorphism of ambient heart objects.
Isomorphism-invariant reformulation of weak semistability.
Weak stability is invariant under isomorphism of ambient heart objects.
Isomorphism-invariant reformulation of weak stability.
Definition 14.3: the zero-charge subcategory #
The zero-charge subcategory A⁰ (Definition 14.3): heart objects of
vanishing charge.
Instances For
The half-plane splitting behind every closure property of A⁰: two
values in ℍ ⊔ ℝ_{≤0} summing to zero are each zero. Stated on a pair of
heart objects, zero objects allowed.
A⁰ is closed under subobjects (in the triangle phrasing): the left
vertex of a heart short exact sequence with zero-charge middle has zero
charge.
A⁰ is closed under quotients: the right vertex, dually.
A⁰ is closed under extensions: charges add on triangles.