Genuine and uniform quadratic support for weak stability

This file binds the quadratic support interfaces to the actual classes of nonzero weak-semistable heart objects. The packages also store compatibility between the real-linear charge on the class space and the additive charge of the weak stability function; without that field a completely unrelated linear map could satisfy the numerical predicate.

UniformQuadraticSupportData is the abstract fixed-category version of the uniform clause in Definition 18.5 and Lemma 18.6 of arXiv:1902.08184v4. QuotientUniformQuadraticSupportData is the corresponding real-linear core of Definitions 21.9 and 21.15: zero-charge classes land in the killed subspace, and a single quadratic form controls all mapped semistable classes on the quotient.

The geometric boundedness clause (5) of Definition 21.15 is intentionally not part of these structures. It requires moduli functors and is outside the repository's current abstract categorical substrate.

structure CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.QuadraticSupportData {C : Type u_1} [Category.{u_4, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] {t : TStructure C} (W : WeakStabilityFunction t) (v : K₀ C →+ V) (Zlin : V →ₗ[ℝ] ℂ) : Prop

A genuine quadratic support form for one weak stability function, together with the required identification of its charge with the chosen real-linear realization.

• charge_compatible (k : K₀ C) : Zlin (v k) = W.Z k

  The linear charge realizes the weak stability charge on every class.

• quadratic : Support.HasQuadraticSupportProperty Zlin (W.semistableClasses v)

  A bundled quadratic form has the required signs on semistable classes and the kernel of the linear charge.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.QuadraticSupportData.hasSupportProperty {C : Type u_1} [Category.{u_4, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {v : K₀ C →+ V} {t : TStructure C} {W : WeakStabilityFunction t} {Zlin : V →ₗ[ℝ] ℂ} (h : W.QuadraticSupportData v Zlin) : W.HasSupportProperty v Zlin

Genuine quadratic support implies the existing norm-bound support predicate for the same semistable locus.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.QuadraticSupportData.class_eq_zero_of_zeroCharge {C : Type u_1} [Category.{u_4, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {v : K₀ C →+ V} {t : TStructure C} {W : WeakStabilityFunction t} {Zlin : V →ₗ[ℝ] ℂ} (h : W.QuadraticSupportData v Zlin) {E : C} (hE : W.zeroCharge E) : v (K₀.of C E) = 0

Under genuine support, a zero-charge heart object has zero numerical class.

structure CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.UniformQuadraticSupportData {C : Type u_1} [Category.{u_4, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {I : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] {t : TStructure C} (W : I → WeakStabilityFunction t) (v : K₀ C →+ V) (Zlin : V →ₗ[ℝ] ℂ) : Prop

A single quadratic form and a single linear charge controlling an indexed family of weak stability functions on the same heart. The quantifier order forces the form to be uniform.

• charge_compatible (i : I) (k : K₀ C) : Zlin (v k) = (W i).Z k

  Every fiber charge is the same fixed charge on classes.

• quadratic : Support.HasUniformQuadraticSupportProperty Zlin fun (i : I) => (W i).semistableClasses v

  One quadratic form controls every fiber semistable locus.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.UniformQuadraticSupportData.fiber {C : Type u_1} [Category.{u_4, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {I : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ C →+ V} {t : TStructure C} {W : I → WeakStabilityFunction t} {Zlin : V →ₗ[ℝ] ℂ} (h : UniformQuadraticSupportData W v Zlin) (i : I) : (W i).QuadraticSupportData v Zlin

Restrict a uniform weak support package to one index.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.UniformQuadraticSupportData.reindex {C : Type u_1} [Category.{u_5, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {I : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ C →+ V} {J : Type u_4} {t : TStructure C} {W : I → WeakStabilityFunction t} {Zlin : V →ₗ[ℝ] ℂ} (h : UniformQuadraticSupportData W v Zlin) (f : J → I) : UniformQuadraticSupportData (fun (j : J) => W (f j)) v Zlin

Reindex a uniform weak support package without changing its form.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.QuadraticSupportData.constant {C : Type u_1} [Category.{u_5, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ C →+ V} {t : TStructure C} {W : WeakStabilityFunction t} {Zlin : V →ₗ[ℝ] ℂ} (h : W.QuadraticSupportData v Zlin) (I : Type u_4) : UniformQuadraticSupportData (fun (x : I) => W) v Zlin

A single weak quadratic support package gives a uniform constant family.

structure CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.QuotientUniformQuadraticSupportData {C : Type u_1} [Category.{u_4, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {I : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {t : TStructure C} (W : I → WeakStabilityFunction t) (v : K₀ C →+ V) (V₀ : Submodule ℝ V) (Zlin : V →ₗ[ℝ] ℂ) (hV₀ : V₀ ≤ Zlin.ker) : Prop

Source-facing quotient support for an indexed weak family.

The original semistable classes live in V; all zero-charge classes are required to lie in V₀; and the actual quadratic form lives on V ⧸ V₀.

• charge_compatible (i : I) (k : K₀ C) : Zlin (v k) = (W i).Z k

  Every fiber charge is induced by the same charge before quotienting.

• zero_class_mem (i : I) (E : C) : (W i).zeroCharge E → v (K₀.of C E) ∈ V₀

  Every zero-charge heart class is killed by the quotient.

• quadratic : Support.HasUniformQuadraticSupportPropertyModulo V₀ Zlin hV₀ fun (i : I) => (W i).semistableClasses v

  One genuine quadratic form on the quotient controls all mapped semistable classes.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.QuotientUniformQuadraticSupportData.fiber {C : Type u_1} [Category.{u_4, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {I : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {v : K₀ C →+ V} {t : TStructure C} {W : I → WeakStabilityFunction t} {V₀ : Submodule ℝ V} {Zlin : V →ₗ[ℝ] ℂ} {hV₀ : V₀ ≤ Zlin.ker} (h : QuotientUniformQuadraticSupportData W v V₀ Zlin hV₀) (i : I) : Support.HasQuadraticSupportProperty (Support.quotientCharge V₀ Zlin hV₀) (⇑V₀.mkQ '' (W i).semistableClasses v)

Each fiber of a quotient-uniform package satisfies quadratic support on its mapped semistable locus.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakStabilityFunction.QuotientUniformQuadraticSupportData.zero_class_eq_zero {C : Type u_1} [Category.{u_4, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {I : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {v : K₀ C →+ V} {t : TStructure C} {W : I → WeakStabilityFunction t} {V₀ : Submodule ℝ V} {Zlin : V →ₗ[ℝ] ℂ} {hV₀ : V₀ ≤ Zlin.ker} (h : QuotientUniformQuadraticSupportData W v V₀ Zlin hV₀) (i : I) {E : C} (hE : (W i).zeroCharge E) : V₀.mkQ (v (K₀.of C E)) = 0

A zero-charge class is literally zero after applying the quotient map.