Weak stability data in an abstract family

This module binds the logical probes of Families.Basic to the repository's actual weak-stability and quotient-support APIs. The binding is intentionally limited to an indexed family of weak stability functions on one fixed category and one fixed heart. It is therefore an abstract model of the separable clauses of Definitions 20.5 and 21.15 of arXiv:1902.08184v4, not a construction of derived categories on geometric fibers.

The fields of WeakStabilityInFamiliesData record:

• Definition 20.5(0): a ℚ[i]-valued charge and a noetherian zero-charge torsion subcategory on every fiber;
• Definition 20.5(1), (2'), and (3') through the probes from Families.Basic;
• Definition 21.15(4) using the genuine one-form-on-the-quotient predicate from Weak.Support.Quadratic;
• Definition 21.15(5) as an explicit caller-supplied boundedness obligation.

No field asserts the existence of base changes, relative hearts, moduli spaces, or bounded families. Those remain data which a geometric client must supply. Constant and PUnit inhabitants used to test logical consistency live in the development scaffolding rather than this stable module.

def CategoryTheory.Triangulated.WeakStabilityCondition.Families.HasGaussianRationalValues {A : Type u_1} (Z : A → ℂ) : Prop

The coefficient condition denoted ℚ[i] in Definition 20.5(0): every complex value admits rational real and imaginary coefficients. This is a pointwise range predicate, not a bundled Gaussian-rational subring object.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.Families.HasGaussianRationalValues Z = ∀ (a : A), ∃ (p : ℚ) (q : ℚ), Z a = ↑p + ↑q * Complex.I

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Families.hasGaussianRationalValues_zero {A : Type u_1} : HasGaussianRationalValues fun (x : A) => 0

The zero function is Gaussian-rational-valued.

structure CategoryTheory.Triangulated.WeakStabilityCondition.Families.WeakChargeProbe (I : Type u_4) (Λ : Type u_5) : Type (max (max (u + 1) u_4) u_5)

An actual charge probe for the fixed-category model: every point chooses a fiber index and a numerical class, so the observed value is forced to be the corresponding weak charge rather than an unrelated function.

• Point : Type u

  Points of the supplied base-change test.

• topology : TopologicalSpace self.Point

  Their topology.

• fiber : self.Point → I

  Which indexed weak stability function is observed at a point.

• klass : self.Point → Λ

  Which fixed-category Grothendieck class is observed at a point.

def CategoryTheory.Triangulated.WeakStabilityCondition.Families.WeakChargeProbe.toChargeProbe {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} {t : TStructure C} (W : I → WeakStabilityFunction t) (P : WeakChargeProbe I (K₀ C)) : ChargeProbe ℂ

Forget a bound weak charge probe to its derived complex-valued probe.

Equations

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

structure CategoryTheory.Triangulated.WeakStabilityCondition.Families.WeakSemistabilityProbe (I : Type u_4) (C : Type u_5) : Type (max (max (u + 1) u_4) u_5)

A semistability probe bound to actual objects and actual weak stability functions in the fixed-category model.

• Point : Type u

  Points of the supplied base-change test.

• topology : TopologicalSpace self.Point

  Their topology.

• genericPoint : self.Point

  The distinguished generic point.

• fiber : self.Point → I

  Which weak stability function is used at each point.

• object : self.Point → C

  The fixed-category object tested at each point.

def CategoryTheory.Triangulated.WeakStabilityCondition.Families.WeakSemistabilityProbe.toGenericProbe {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} {t : TStructure C} (W : I → WeakStabilityFunction t) (P : WeakSemistabilityProbe I C) : GenericSemistabilityProbe

Forget a bound weak probe to the generic semistability locus it defines.

Equations

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

structure CategoryTheory.Triangulated.WeakStabilityCondition.Families.WeakDefinition20_5ClauseZero {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} {t : TStructure C} (W : I → WeakStabilityFunction t) : Prop

Definition 20.5(0), bound to actual weak stability functions.

• gaussianRationalCharge (i : I) : HasGaussianRationalValues ⇑(W i).Z

  Every fiber charge is defined over ℚ[i].

• zeroChargeNoetherian (i : I) : IsNoetherianTorsionSubcategory t (W i).zeroCharge

  Every zero-charge class is a noetherian torsion subcategory.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Families.WeakDefinition20_5ClauseZero.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_4} {t : TStructure C} {W : I → WeakStabilityFunction t} (h : WeakDefinition20_5ClauseZero W) (f : J → I) : WeakDefinition20_5ClauseZero fun (j : J) => W (f j)

Clause (0) is preserved by reindexing.

structure CategoryTheory.Triangulated.WeakStabilityCondition.Families.WeakQuotientQuadraticSupportData {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] {t : TStructure C} (W : WeakStabilityFunction t) (v : K₀ C →+ V) (V₀ : Submodule ℝ V) (Zlin : V →ₗ[ℝ] ℂ) (hV₀ : V₀ ≤ Zlin.ker) : Prop

The actual one-fiber charge, zero-class, and quotient-quadratic-support package.

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

  The real-linear charge realizes the weak charge.

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

  Every zero-charge class is killed in the quotient.

• quadratic : Support.HasQuadraticSupportProperty (Support.quotientCharge V₀ Zlin hV₀) (⇑V₀.mkQ '' W.semistableClasses v)

  Genuine quadratic support on the mapped semistable locus.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Families.quotientUniformQuadraticSupportData_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] [FiniteDimensional ℝ V] {v : K₀ C →+ V} {J : Type u_4} {t : TStructure C} {W : I → WeakStabilityFunction t} {V₀ : Submodule ℝ V} {Zlin : V →ₗ[ℝ] ℂ} {hV₀ : V₀ ≤ Zlin.ker} (h : WeakStabilityFunction.QuotientUniformQuadraticSupportData W v V₀ Zlin hV₀) (f : J → I) : WeakStabilityFunction.QuotientUniformQuadraticSupportData (fun (j : J) => W (f j)) v V₀ Zlin hV₀

Quotient-uniform weak support is preserved by reindexing.

structure CategoryTheory.Triangulated.WeakStabilityCondition.Families.WeakStabilityInFamiliesData {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} {JCharge JGeneric D M : Type u} {t : TStructure C} (W : I → WeakStabilityFunction t) (charge : JCharge → WeakChargeProbe I (K₀ C)) (semistable : JGeneric → WeakSemistabilityProbe I C) (dedekind : WeakDedekindHNProblem D) (V₀ : Submodule ℝ V) (Zlin : V →ₗ[ℝ] ℂ) (hV₀ : V₀ ≤ Zlin.ker) (boundedness : Moduli.BoundednessProblem M) : Prop

The separable clauses of weak stability in families which can be stated in the current abstract library. Every source clause is a named projection.

The charge and semistable probes are bound to actual weak functions via toChargeProbe and toGenericProbe; the support field is the actual quotient-uniform support package from issue #82. Relative HN and boundedness remain explicit geometric inputs.

• clauseZero : WeakDefinition20_5ClauseZero W

  Definition 20.5(0).

• definition20_5 : WeakDefinition20_5Conditions (fun (j : JCharge) => WeakChargeProbe.toChargeProbe W (charge j)) (fun (j : JGeneric) => WeakSemistabilityProbe.toGenericProbe W (semistable j)) dedekind

  Definition 20.5(1), (2'), and (3').

• uniformSupport : WeakStabilityFunction.QuotientUniformQuadraticSupportData W v V₀ Zlin hV₀

  Definition 21.15(4).

• bounded : Moduli.UniversalBoundedness boundedness

  Definition 21.15(5), retained as a geometric premise.