Genuine quadratic forms for the support property

The basic support layer is intentionally stated for continuous degree-two homogeneous functions. The source definitions in §§18 and 21 of arXiv:1902.08184v4 instead quantify over an actual quadratic form. This file supplies that stronger, bundled interface and proves that it implies the existing norm estimate.

No converse is asserted here. Over an arbitrary normed real vector space the explicit witness built from the norm in Support.Basic need not be a quadratic form. That asymmetry is deliberate and remains visible in the API.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.quadraticForm_isHomogTwo {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (Q : QuadraticForm ℝ V) : IsHomogTwo ⇑Q

Every quadratic form on a finite-dimensional real normed space is a continuous degree-two homogeneous function.

Continuity is obtained from the polar bilinear form. Finite dimensionality is used precisely to turn that algebraic bilinear map into a continuous one.

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

Compatibility with a genuine quadratic form: nonnegative on the selected classes and negative definite on the kernel of the charge.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.HasQuadraticSupportProperty.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 : HasQuadraticSupportProperty Z S) : HasSupportProperty Z S

A genuine quadratic support form yields the norm-bound formulation of the support property.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Support.HasQuadraticSupportProperty.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 : HasQuadraticSupportProperty Z S) (hS : S' ⊆ S) : HasQuadraticSupportProperty Z S'

The genuine quadratic predicate is monotone in the selected locus.