The support property and its quadratic form

Kontsevich–Soibelman's support property for a central charge asks for a uniform comparison ‖v‖ ≤ C ‖Z v‖ over a distinguished set of classes. The formulation used throughout the modern literature replaces that estimate by a quadratic form Q which is nonnegative on the distinguished set and negative definite on ker Z. This file proves the two are equivalent.

What this is a theorem about

S here is an arbitrary subset of a finite-dimensional real normed space. In the intended application it is the set of classes of σ-semistable objects, but that identification needs a stability condition and is not made here: no declaration below mentions a triangulated category, a slicing, or anything else in StabilityCondition/. Every statement is linear algebra plus one compactness argument, and would hold verbatim for any other choice of S.

The intended W is ℂ; the proofs never use anything about the target beyond its norm, so it is left general.

Why the hypotheses on Q are what they are

The proofs use exactly two properties of a quadratic form: continuity and degree-two homogeneity. Both directions are therefore stated for IsHomogTwo, which is strictly weaker than being a quadratic form — see its docstring. This makes both theorems stronger and costs nothing, since every quadratic form on a finite-dimensional real space satisfies it.

Main results

• hasSupportProperty_of_isCompatible — the compactness direction.
• exists_isCompatible_of_hasSupportProperty — the explicit direction, via Q v = C² ‖Z v‖² - ‖v‖².
• hasSupportProperty_iff — the equivalence.

def CategoryTheory.Triangulated.WeakStabilityCondition.Support.HasSupportProperty {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (Z : V →ₗ[ℝ] W) (S : Set V) : Prop

The support property: a uniform linear comparison of the norm of a class with the norm of its charge, over the distinguished set S.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.Support.HasSupportProperty Z S = ∃ (C : ℝ), 0 < C ∧ ∀ v ∈ S, ‖v‖ ≤ C * ‖Z v‖

structure CategoryTheory.Triangulated.WeakStabilityCondition.Support.IsHomogTwo {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (Q : V → ℝ) : Prop

The two properties of a quadratic form that the equivalence below actually uses: continuity and homogeneity of degree two.

This is deliberately weaker than being a quadratic form. Continuity plus Q (a • v) = a² Q v does not imply bilinearity: Q (x, y) = |x * y| on ℝ² satisfies both and is not a quadratic form. Stating the hypothesis this way makes both directions stronger theorems and costs nothing, because every quadratic form on a finite-dimensional real space satisfies it.

• continuous : Continuous Q

  Q is continuous

• smul (a : ℝ) (v : V) : Q (a • v) = a ^ 2 * Q v

  Q is homogeneous of degree two

structure CategoryTheory.Triangulated.WeakStabilityCondition.Support.IsCompatible {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (Z : V →ₗ[ℝ] W) (S : Set V) (Q : V → ℝ) : Prop

Compatibility of a form with the pair (Z, S): nonnegative on S, and negative definite on ker Z.

• nonneg_of_mem (v : V) : v ∈ S → 0 ≤ Q v

  Q is nonnegative on the distinguished set

• neg_of_ker (v : V) : Z v = 0 → v ≠ 0 → Q v < 0

  Q is negative definite on the kernel of the charge

def CategoryTheory.Triangulated.WeakStabilityCondition.Support.slice {V : Type u_1} [NormedAddCommGroup V] (Q : V → ℝ) : Set V

The compact slice the argument runs on: the unit sphere cut by Q ≥ 0.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.Support.slice Q = Metric.sphere 0 1 ∩ {v : V | 0 ≤ Q v}

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.isCompact_slice {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {Q : V → ℝ} (hQ : IsHomogTwo Q) : IsCompact (slice Q)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.norm_inv_smul_mem_slice {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {Q : V → ℝ} (hQ : IsHomogTwo Q) {v : V} (hv : v ≠ 0) (hQv : 0 ≤ Q v) : ‖v‖⁻¹ • v ∈ slice Q

Normalising a nonzero vector on which Q is nonnegative lands in the slice. This is the only place degree-two homogeneity is used.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.hasSupportProperty_of_isCompatible {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {Z : V →ₗ[ℝ] W} {S : Set V} {Q : V → ℝ} (hQ : IsHomogTwo Q) (hc : IsCompatible Z S Q) : HasSupportProperty Z S

The support property follows from a compatible form.

The slice is compact and Z does not vanish on it, so ‖Z ·‖ attains a positive minimum there; the comparison constant is its reciprocal.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.exists_isCompatible_of_hasSupportProperty {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {Z : V →ₗ[ℝ] W} {S : Set V} (h : HasSupportProperty Z S) : ∃ (Q : V → ℝ), IsHomogTwo Q ∧ IsCompatible Z S Q

A compatible form follows from the support property.

The witness is explicit: Q v = C² ‖Z v‖² - ‖v‖². On S it is nonnegative by squaring the support estimate, and on ker Z it is -‖v‖².

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.hasSupportProperty_iff {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {Z : V →ₗ[ℝ] W} {S : Set V} : HasSupportProperty Z S ↔ ∃ (Q : V → ℝ), IsHomogTwo Q ∧ IsCompatible Z S Q

The support property is exactly the existence of a compatible form.

This is the Kontsevich–Soibelman reformulation, at the level of the numerical data it is a statement about.

Elementary consequences

Both are immediate from the definition and are stated because they are the sanity checks a reader will want: the property is monotone in S, and it forces the charge to be injective on the span of S in the strong pointwise sense.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.HasSupportProperty.mono {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {Z : V →ₗ[ℝ] W} {S S' : Set V} (h : HasSupportProperty Z S) (hS : S' ⊆ S) : HasSupportProperty Z S'

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.HasSupportProperty.eq_zero_of_charge_eq_zero {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {Z : V →ₗ[ℝ] W} {S : Set V} (h : HasSupportProperty Z S) {v : V} (hv : v ∈ S) (hZ : Z v = 0) : v = 0

A class in S with vanishing charge is zero.

Stability under perturbation of the charge

The support property is an open condition on Z. That is what makes it the right hypothesis for a deformation argument: a charge that has it keeps it under any sufficiently small change, so the property propagates along a path rather than having to be re-established at every point.

None of this uses compactness, the quadratic form, or finite-dimensionality — only the triangle inequality and one division — so all three are stated with FiniteDimensional omitted. The topological statement at the end is the only one that needs a norm on the space of charges, and it is a corollary of the other two rather than a separate argument.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.hasSupportProperty_of_norm_sub_le {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {Z : V →ₗ[ℝ] W} {S : Set V} {Z' : V →ₗ[ℝ] W} {C ε : ℝ} (hC : 0 < C) (hb : ∀ v ∈ S, ‖v‖ ≤ C * ‖Z v‖) (hε : ∀ (v : V), ‖Z' v - Z v‖ ≤ ε * ‖v‖) (hCε : C * ε < 1) : HasSupportProperty Z' S

The support property survives a small perturbation of the charge.

Both the constant and the closeness bound are explicit, because the admissible size of the perturbation depends on C: an estimate that is only barely true tolerates only a barely nonzero change. The perturbed constant is C / (1 - Cε), which degrades to +∞ exactly as Cε → 1.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.HasSupportProperty.exists_tolerance {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {Z : V →ₗ[ℝ] W} {S : Set V} (h : HasSupportProperty Z S) : ∃ (ε : ℝ), 0 < ε ∧ ∀ (Z' : V →ₗ[ℝ] W), (∀ (v : V), ‖Z' v - Z v‖ ≤ ε * ‖v‖) → HasSupportProperty Z' S

Openness, stated without a topology on the space of charges.

Every charge with the support property admits a positive tolerance inside which every other charge still has it. isOpen_hasSupportProperty is this made topological; this form is separated out because it needs no norm on the space of maps and so applies to plain linear maps.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.isOpen_hasSupportProperty {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (S : Set V) : IsOpen {Z : V →L[ℝ] W | HasSupportProperty (↑Z) S}

The charges with the support property form an open set.

S is fixed and the charges are topologized by the operator norm. This is the IsOpen form of HasSupportProperty.exists_tolerance; the mathematical content is entirely in that lemma, and the only step here is le_opNorm.