Quadratic support for ordinary semistable objects

This file binds the genuine quadratic-support interfaces to semistability in an actual ordinary pre-stability condition. The selected numerical locus is the set of classes of nonzero objects in a slice P(φ); callers cannot replace it by an unrelated set.

UniformQuadraticSupportData is the fixed-category numerical core of the uniform support condition in Definition 18.5, Lemma 18.6, and Definition 21.15(4) of arXiv:1902.08184v4. One real-linear charge and one quadratic form control every indexed member. Varying geometric fiber categories, the Definition 21.9 quotient, and boundedness remain separate layers.

def CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.semistableClasses {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_4} [NormedAddCommGroup V] {v : K₀ C →+ V} (σ : WithClassMap C v) : Set V

Numerical classes of nonzero ordinary semistable objects, where semistability means membership in one phase of the slicing.

Equations

• σ.semistableClasses = {x : V | ∃ (φ : ℝ) (E : C), σ.slicing.P φ E ∧ ¬CategoryTheory.Limits.IsZero E ∧ x = v (CategoryTheory.Triangulated.K₀.of C E)}

theorem CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.mem_semistableClasses_iff {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_4} [NormedAddCommGroup V] {v : K₀ C →+ V} (σ : WithClassMap C v) (x : V) : x ∈ σ.semistableClasses ↔ ∃ (φ : ℝ) (E : C), σ.slicing.P φ E ∧ ¬Limits.IsZero E ∧ x = v (K₀.of C E)

Membership in the ordinary semistable locus exposes the phase and object that produced the numerical class.

theorem CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.class_mem_semistableClasses {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_4} [NormedAddCommGroup V] {v : K₀ C →+ V} (σ : WithClassMap C v) {φ : ℝ} {E : C} (hP : σ.slicing.P φ E) (hE : ¬Limits.IsZero E) : v (K₀.of C E) ∈ σ.semistableClasses

A nonzero object in a slice contributes its class to the ordinary semistable locus.

def CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.HasSupportProperty {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_4} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ C →+ V} (σ : WithClassMap C v) (Zlin : V →ₗ[ℝ] ℂ) : Prop

The norm-bound support property for the actual ordinary semistable locus.

Equations

• σ.HasSupportProperty Zlin = CategoryTheory.Triangulated.WeakStabilityCondition.Support.HasSupportProperty Zlin σ.semistableClasses

structure CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.QuadraticSupportData {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_4} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ C →+ V} (σ : WithClassMap C v) (Zlin : V →ₗ[ℝ] ℂ) : Prop

Genuine quadratic support for one ordinary pre-stability condition, together with identification of its additive and real-linear charges.

• charge_compatible (x : V) : Zlin x = σ.Z x

  The real-linear charge realizes the pre-stability condition's central charge on the full class space.

• quadratic : WeakStabilityCondition.Support.HasQuadraticSupportProperty Zlin σ.semistableClasses

  One genuine quadratic form has the required signs on the ordinary semistable locus and the kernel of the same charge.

theorem CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.QuadraticSupportData.hasSupportProperty {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_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {v : K₀ C →+ V} {σ : WithClassMap C v} {Zlin : V →ₗ[ℝ] ℂ} (h : σ.QuadraticSupportData Zlin) : σ.HasSupportProperty Zlin

Genuine quadratic support implies the norm-bound support property on the same ordinary semistable locus.

structure CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.UniformQuadraticSupportData {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_4} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ C →+ V} (σ : I → WithClassMap C v) (Zlin : V →ₗ[ℝ] ℂ) : Prop

A single charge and a single quadratic form controlling an indexed family of ordinary pre-stability conditions on the same category and class space.

• charge_compatible (i : I) (x : V) : Zlin x = (σ i).Z x

  Every indexed central charge is the same fixed charge on classes.

• quadratic : WeakStabilityCondition.Support.HasUniformQuadraticSupportProperty Zlin fun (i : I) => (σ i).semistableClasses

  One quadratic form controls every indexed ordinary semistable locus.

theorem CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.UniformQuadraticSupportData.fiber {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_4} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ C →+ V} {σ : I → WithClassMap C v} {Zlin : V →ₗ[ℝ] ℂ} (h : UniformQuadraticSupportData σ Zlin) (i : I) : (σ i).QuadraticSupportData Zlin

Restrict a uniform ordinary support package to one index.

theorem CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.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} {J : Type u_3} {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] {v : K₀ C →+ V} {σ : I → WithClassMap C v} {Zlin : V →ₗ[ℝ] ℂ} (h : UniformQuadraticSupportData σ Zlin) (f : J → I) : UniformQuadraticSupportData (fun (j : J) => σ (f j)) Zlin

Reindex a uniformly supported ordinary family without changing its charge or quadratic form.

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

One ordinary quadratic support package gives a uniform constant family.