Full support from mass--Hom bounds

This file formalizes the categorical core of Cheng's full-support argument (arXiv:2608.14540v1, Theorem 2.1). A finite family of test objects supplies Euler probes on the real numerical class space. If those probes separate classes and a finite Ext-window controls every probe on semistable objects, then a mass--Hom bound produces one genuine Kontsevich--Soibelman quadratic support form.

The Ext-window is deliberately an explicit hypothesis. Its geometric proof uses phase vanishing and Grothendieck--Serre duality with a dualizing complex; none of that geometry is manufactured in this categorical layer.

structure CategoryTheory.Triangulated.StabilityCondition.WithClassMap.EulerProbeFamily {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] [Pretriangulated C] [HomFiniteBounded k C] {V : Type u'} [NormedAddCommGroup V] [NormedSpace ℝ V] {v₀ : K₀ C →+ V} {ι : Type u_1} (A : ι → C) (probe : ι → V →ₗ[ℝ] ℝ) : Prop

A finite collection of test objects whose Euler pairings extend to real-linear functionals separating the full real numerical class space.

The realizes field is the precise bridge to the Hom-built Euler form. The extension and separation are input: this file does not infer either from a presentation of the numerical Grothendieck group.

• realizes (i : ι) (x : K₀ C) : (probe i) (v₀ x) = ↑(((chiK₀ k C) (K₀.of C (A i))) x)

  The real probe extends χ(Aᵢ,-) along the chosen class map.

• separates (x : V) : (∀ (i : ι), (probe i) x = 0) → x = 0

  The finite family of extended Euler probes separates all real classes.

structure CategoryTheory.Triangulated.StabilityCondition.WithClassMap.SemistableExtWindow {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u'} [NormedAddCommGroup V] {v₀ : K₀ C →+ V} {ι : Type u_1} (s : WithClassMap C v₀) (T : ObjectProperty C) (A : ι → C) : Type u_1

The finite Ext-window needed in Cheng's argument.

For each Euler test A i, shifts i lists the only shifted tests needed to bound its Euler pairing on a semistable object. The shifted tests are required to lie in the mass--Hom test class T. The final field is exactly the triangle-inequality estimate furnished geometrically by phase vanishing and Serre duality; it remains explicit until those geometric bridges exist.

• shifts : ι → Finset ℤ

  The finite set of relevant Ext-degrees for each Euler test.

• shifted_mem (i : ι) (j : ℤ) : j ∈ self.shifts i → T ((shiftFunctor C (-j)).obj (A i))

  Every shifted source occurring in the window belongs to the test class.

• euler_abs_le (i : ι) (P : ℝ) (F : C) : s.slicing.P P F → |↑(chiHom k C (A i) F)| ≤ ∑ j ∈ self.shifts i, ↑(Module.finrank k ((shiftFunctor C (-j)).obj (A i) ⟶ F))

  On semistables, the absolute Euler pairing is bounded by the Hom-dimensions in the declared finite window.

def CategoryTheory.Triangulated.StabilityCondition.WithClassMap.FullSupport.probeQuadratic {V : Type u'} [NormedAddCommGroup V] [NormedSpace ℝ V] {ι : Type u_1} [Fintype ι] (probe : ι → V →ₗ[ℝ] ℝ) : QuadraticForm ℝ V

The sum-of-squares quadratic form attached to a finite family of real linear probes.

Equations

• CategoryTheory.Triangulated.StabilityCondition.WithClassMap.FullSupport.probeQuadratic probe = ∑ i : ι, QuadraticMap.linMulLin (probe i) (probe i)

@[simp]

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.FullSupport.probeQuadratic_apply {V : Type u'} [NormedAddCommGroup V] [NormedSpace ℝ V] {ι : Type u_1} [Fintype ι] (probe : ι → V →ₗ[ℝ] ℝ) (x : V) : (probeQuadratic probe) x = ∑ i : ι, (probe i) x ^ 2

def CategoryTheory.Triangulated.StabilityCondition.WithClassMap.FullSupport.chargeQuadratic {V : Type u'} [NormedAddCommGroup V] [NormedSpace ℝ V] (Z : V →ₗ[ℝ] ℂ) : QuadraticForm ℝ V

The quadratic form x ↦ ‖Zx‖², written algebraically using the real and imaginary coordinate functionals of the complex charge.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.FullSupport.chargeQuadratic_apply {V : Type u'} [NormedAddCommGroup V] [NormedSpace ℝ V] (Z : V →ₗ[ℝ] ℂ) (x : V) : (chargeQuadratic Z) x = ‖Z x‖ ^ 2

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.FullSupport.hasQuadraticSupportProperty_of_finite_probes {V : Type u'} [NormedAddCommGroup V] [NormedSpace ℝ V] {ι : Type u_1} [Fintype ι] (Z : V →ₗ[ℝ] ℂ) (S : Set V) (probe : ι → V →ₗ[ℝ] ℝ) (hsep : ∀ (x : V), (∀ (i : ι), (probe i) x = 0) → x = 0) (B : ι → ℝ) (hB : ∀ (i : ι), 0 ≤ B i) (hbound : ∀ x ∈ S, ∀ (i : ι), |(probe i) x| ≤ B i * ‖Z x‖) : WeakStabilityCondition.Support.HasQuadraticSupportProperty Z S

Finite separating probes with uniform linear charge bounds produce a genuine quadratic support form.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.HasMassHomBound.quadraticSupportData {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)] [Pretriangulated C] [IsTriangulated C] [SerreFunctor.HomFinite k C] [HomFiniteBounded k C] {V : Type u'} [NormedAddCommGroup V] [NormedSpace ℝ V] {v₀ : K₀ C →+ V} {ι : Type u_1} [Fintype ι] (s : WithClassMap C v₀) (T : ObjectProperty C) (hs : s.HasMassHomBound T) (A : ι → C) (probe : ι → V →ₗ[ℝ] ℝ) (hprobe : EulerProbeFamily A probe) (hwindow : s.SemistableExtWindow T A) (Zlin : V →ₗ[ℝ] ℂ) (hZ : ∀ (x : V), Zlin x = s.Z x) : s.QuadraticSupportData Zlin

Cheng's categorical full-support argument: a mass--Hom bound, finitely many separating Euler probes, and an explicit semistable Ext-window imply genuine quadratic support on the full real numerical class space.