The ordinary families interface on actual fiber categories

OrdinaryStabilityInFamiliesData keeps its semistable loci abstract so that the five source clauses can be audited independently of category theory. The adapter in this file removes that freedom: its support locus is definitionally the set of classes of nonzero objects in phases of actual slicings on a family of possibly different triangulated categories.

The geometric inputs remain honest premises. In particular, this file does not construct a scheme, a relative category, base-change functors, relative Harder--Narasimhan structures, or bounded moduli spaces.

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.OrdinaryFiberStabilityInFamiliesData {JCharge : Type u_1} {JOpen : Type u_2} {D : Type u_3} {I : Type u_4} {M : Type u_5} {V : Type u_6} {C : I → Type u} [(i : I) → Category.{u_7, u} (C i)] [(i : I) → Preadditive (C i)] [∀ (i : I), Limits.HasZeroObject (C i)] [(i : I) → HasShift (C i) ℤ] [∀ (i : I) (n : ℤ), (shiftFunctor (C i) n).Additive] [(i : I) → Pretriangulated (C i)] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {v : (i : I) → K₀ (C i) →+ V} (charge : JCharge → Families.ChargeProbe ℂ) (stable : JOpen → Families.OpenLocusProbe) (dedekind : Families.DedekindHNProblem D) (V₀ : Submodule ℝ V) (Z : V →ₗ[ℝ] ℂ) (hV₀ : V₀ ≤ Z.ker) (σ : (i : I) → PreStabilityCondition.WithClassMap (C i) (v i)) (boundedness : Moduli.BoundednessProblem M) : Prop

The five ordinary stability-in-families clauses with the support locus bound to actual slicings on the fiber categories.

The charge, stable, dedekind, and boundedness parameters are still client-supplied geometric probes. The numerical support parameter is not: it is forced to be ordinaryFiberSemistableClasses σ.

• definition20_5 : Families.OrdinaryDefinition20_5Conditions charge stable dedekind

  Definition 20.5(1)--(3), still expressed through explicit client probes.

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

  The one real-linear charge on the common class space realizes the central charge of every fiber pre-stability condition.

• uniformSupport : Support.HasUniformQuadraticSupportPropertyModulo V₀ Z hV₀ (ordinaryFiberSemistableClasses σ)

  Definition 21.15(4), on the quotient, for the actual slicing-defined semistable classes of every fiber.

• bounded : Moduli.UniversalBoundedness boundedness

  Definition 21.15(5), retained as the caller's geometric boundedness obligation.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.OrdinaryFiberStabilityInFamiliesData.toOrdinaryStabilityInFamiliesData {JCharge : Type u_1} {JOpen : Type u_2} {D : Type u_3} {I : Type u_4} {M : Type u_5} {V : Type u_6} {C : I → Type u} [(i : I) → Category.{u_10, u} (C i)] [(i : I) → Preadditive (C i)] [∀ (i : I), Limits.HasZeroObject (C i)] [(i : I) → HasShift (C i) ℤ] [∀ (i : I) (n : ℤ), (shiftFunctor (C i) n).Additive] [(i : I) → Pretriangulated (C i)] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {v : (i : I) → K₀ (C i) →+ V} {charge : JCharge → Families.ChargeProbe ℂ} {stable : JOpen → Families.OpenLocusProbe} {dedekind : Families.DedekindHNProblem D} {V₀ : Submodule ℝ V} {Z : V →ₗ[ℝ] ℂ} {hV₀ : V₀ ≤ Z.ker} {σ : (i : I) → PreStabilityCondition.WithClassMap (C i) (v i)} {boundedness : Moduli.BoundednessProblem M} (h : OrdinaryFiberStabilityInFamiliesData charge stable dedekind V₀ Z hV₀ σ boundedness) : OrdinaryStabilityInFamiliesData charge stable dedekind V₀ Z hV₀ (ordinaryFiberSemistableClasses σ) boundedness

Forget that the support loci came from actual fiber slicings and recover the existing five-clause abstract package.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.OrdinaryFiberStabilityInFamiliesData.toDeformationInputConditions {JCharge : Type u_1} {JOpen : Type u_2} {D : Type u_3} {I : Type u_4} {M : Type u_5} {V : Type u_6} {C : I → Type u} [(i : I) → Category.{u_10, u} (C i)] [(i : I) → Preadditive (C i)] [∀ (i : I), Limits.HasZeroObject (C i)] [(i : I) → HasShift (C i) ℤ] [∀ (i : I) (n : ℤ), (shiftFunctor (C i) n).Additive] [(i : I) → Pretriangulated (C i)] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {v : (i : I) → K₀ (C i) →+ V} {charge : JCharge → Families.ChargeProbe ℂ} {stable : JOpen → Families.OpenLocusProbe} {dedekind : Families.DedekindHNProblem D} {V₀ : Submodule ℝ V} {Z : V →ₗ[ℝ] ℂ} {hV₀ : V₀ ≤ Z.ker} {σ : (i : I) → PreStabilityCondition.WithClassMap (C i) (v i)} {boundedness : Moduli.BoundednessProblem M} (h : OrdinaryFiberStabilityInFamiliesData charge stable dedekind V₀ Z hV₀ σ boundedness) : OrdinaryDeformationInputConditions stable dedekind V₀ Z hV₀ (ordinaryFiberSemistableClasses σ) boundedness

Project the geometric and numerical conditions used by deformation arguments. This does not produce a geometric or analytic conclusion.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.OrdinaryFiberStabilityInFamiliesData.fiberSupport {JCharge : Type u_1} {JOpen : Type u_2} {D : Type u_3} {I : Type u_4} {M : Type u_5} {V : Type u_6} {C : I → Type u} [(i : I) → Category.{u_10, u} (C i)] [(i : I) → Preadditive (C i)] [∀ (i : I), Limits.HasZeroObject (C i)] [(i : I) → HasShift (C i) ℤ] [∀ (i : I) (n : ℤ), (shiftFunctor (C i) n).Additive] [(i : I) → Pretriangulated (C i)] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {v : (i : I) → K₀ (C i) →+ V} {charge : JCharge → Families.ChargeProbe ℂ} {stable : JOpen → Families.OpenLocusProbe} {dedekind : Families.DedekindHNProblem D} {V₀ : Submodule ℝ V} {Z : V →ₗ[ℝ] ℂ} {hV₀ : V₀ ≤ Z.ker} {σ : (i : I) → PreStabilityCondition.WithClassMap (C i) (v i)} {boundedness : Moduli.BoundednessProblem M} (h : OrdinaryFiberStabilityInFamiliesData charge stable dedekind V₀ Z hV₀ σ boundedness) (i : I) : Support.HasQuadraticSupportProperty (Support.quotientCharge V₀ Z hV₀) (⇑V₀.mkQ '' ordinaryFiberSemistableClasses σ i)

The quotient-uniform support field specializes to genuine quadratic support for the actual semistable locus of each fiber.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.OrdinaryFiberStabilityInFamiliesData.quotientCharge_mkQ {JCharge : Type u_1} {JOpen : Type u_2} {D : Type u_3} {I : Type u_4} {M : Type u_5} {V : Type u_6} {C : I → Type u} [(i : I) → Category.{u_10, u} (C i)] [(i : I) → Preadditive (C i)] [∀ (i : I), Limits.HasZeroObject (C i)] [(i : I) → HasShift (C i) ℤ] [∀ (i : I) (n : ℤ), (shiftFunctor (C i) n).Additive] [(i : I) → Pretriangulated (C i)] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {v : (i : I) → K₀ (C i) →+ V} {charge : JCharge → Families.ChargeProbe ℂ} {stable : JOpen → Families.OpenLocusProbe} {dedekind : Families.DedekindHNProblem D} {V₀ : Submodule ℝ V} {Z : V →ₗ[ℝ] ℂ} {hV₀ : V₀ ≤ Z.ker} {σ : (i : I) → PreStabilityCondition.WithClassMap (C i) (v i)} {boundedness : Moduli.BoundednessProblem M} (h : OrdinaryFiberStabilityInFamiliesData charge stable dedekind V₀ Z hV₀ σ boundedness) (i : I) (x : V) : (Support.quotientCharge V₀ Z hV₀) (V₀.mkQ x) = (σ i).Z x

On every original fiber class, the descended common charge agrees with the central charge stored by that fiber's pre-stability condition.