Ordinary stability conditions on a categorical family

This file joins the five-clause ordinary stability-in-families interface to one contravariant family of triangulated categories. The resulting package contains both the existing source-clause data and compatibility of its actual fiber pre-stability conditions under the categorical pullback functors.

This remains an abstract adapter. It does not construct a family of schemes, derived pullback, the required preimage/HN witnesses from geometry, relative Harder--Narasimhan structures, openness, boundedness, or a moduli space, and it does not assert a deformation-theoretic conclusion.

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.CategoricalOrdinaryFiberStabilityInFamiliesData {B : Type u} [Category.{v, u} B] {JCharge : Type u_1} {JOpen : Type u_2} {D : Type u_3} {M : Type u_4} (F : Families.TriangulatedFiberFamily) {V : Type uV} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (classMap : (b : B) → K₀ (F.Fiber b) →+ V) (sigma : (b : B) → PreStabilityCondition.WithClassMap (F.Fiber b) (classMap b)) (charge : JCharge → Families.ChargeProbe ℂ) (stable : JOpen → Families.OpenLocusProbe) (dedekind : Families.DedekindHNProblem D) (V₀ : Submodule ℝ V) (Z : V →ₗ[ℝ] ℂ) (hV₀ : V₀ ≤ Z.ker) (boundedness : Moduli.BoundednessProblem M) : Prop

The five ordinary stability-in-families clauses on the fibers of one categorical family, together with compatibility under its pullbacks.

• ordinary : OrdinaryFiberStabilityInFamiliesData charge stable dedekind V₀ Z hV₀ sigma boundedness

  The existing five-clause interface, with support bound to actual fiber slicings.

• baseChange : FiberPreStabilityBaseChangeData F classMap sigma

  The same fiber conditions are compatible with every categorical pullback.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.CategoricalOrdinaryFiberStabilityInFamiliesData.toDeformationInputConditions {B : Type u} [Category.{v, u} B] {JCharge : Type u_1} {JOpen : Type u_2} {D : Type u_3} {M : Type u_4} {F : Families.TriangulatedFiberFamily} {V : Type uV} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {classMap : (b : B) → K₀ (F.Fiber b) →+ V} {sigma : (b : B) → PreStabilityCondition.WithClassMap (F.Fiber b) (classMap b)} {charge : JCharge → Families.ChargeProbe ℂ} {stable : JOpen → Families.OpenLocusProbe} {dedekind : Families.DedekindHNProblem D} {V₀ : Submodule ℝ V} {Z : V →ₗ[ℝ] ℂ} {hV₀ : V₀ ≤ Z.ker} {boundedness : Moduli.BoundednessProblem M} (h : CategoricalOrdinaryFiberStabilityInFamiliesData F classMap sigma charge stable dedekind V₀ Z hV₀ boundedness) : OrdinaryDeformationInputConditions stable dedekind V₀ Z hV₀ (ordinaryFiberSemistableClasses sigma) boundedness

Project the geometric and numerical conditions used by deformation arguments. This proves no geometric or analytic conclusion.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.CategoricalOrdinaryFiberStabilityInFamiliesData.class_mem_semistableClasses_pull {B : Type u} [Category.{v, u} B] {JCharge : Type u_1} {JOpen : Type u_2} {D : Type u_3} {M : Type u_4} {F : Families.TriangulatedFiberFamily} {V : Type uV} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {classMap : (b : B) → K₀ (F.Fiber b) →+ V} {sigma : (b : B) → PreStabilityCondition.WithClassMap (F.Fiber b) (classMap b)} {charge : JCharge → Families.ChargeProbe ℂ} {stable : JOpen → Families.OpenLocusProbe} {dedekind : Families.DedekindHNProblem D} {V₀ : Submodule ℝ V} {Z : V →ₗ[ℝ] ℂ} {hV₀ : V₀ ≤ Z.ker} {boundedness : Moduli.BoundednessProblem M} (h : CategoricalOrdinaryFiberStabilityInFamiliesData F classMap sigma charge stable dedekind V₀ Z hV₀ boundedness) {s t : B} (f : s ⟶ t) {phi : ℝ} {E : F.Fiber t} (hP : (sigma t).slicing.P phi E) (hE : ¬Limits.IsZero ((F.pull f).obj E)) : (classMap t) (K₀.of (F.Fiber t) E) ∈ ordinaryFiberSemistableClasses sigma s

The actual slicing-defined semistable locus is stable under a pullback which does not annihilate the chosen object.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.CategoricalOrdinaryFiberStabilityInFamiliesData.commonCharge_pull {B : Type u} [Category.{v, u} B] {JCharge : Type u_1} {JOpen : Type u_2} {D : Type u_3} {M : Type u_4} {F : Families.TriangulatedFiberFamily} {V : Type uV} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {classMap : (b : B) → K₀ (F.Fiber b) →+ V} {sigma : (b : B) → PreStabilityCondition.WithClassMap (F.Fiber b) (classMap b)} {charge : JCharge → Families.ChargeProbe ℂ} {stable : JOpen → Families.OpenLocusProbe} {dedekind : Families.DedekindHNProblem D} {V₀ : Submodule ℝ V} {Z : V →ₗ[ℝ] ℂ} {hV₀ : V₀ ≤ Z.ker} {boundedness : Moduli.BoundednessProblem M} (h : CategoricalOrdinaryFiberStabilityInFamiliesData F classMap sigma charge stable dedekind V₀ Z hV₀ boundedness) {s t : B} (f : s ⟶ t) (E : F.Fiber t) : Z ((classMap s) (K₀.of (F.Fiber s) ((F.pull f).obj E))) = (sigma t).charge E

The common real-linear charge evaluates the preserved object class as the fiber central charge on either side of pullback.