Uniform support on varying fiber categories

The ordinary support adapter in Support.Semistable indexes stability conditions on one fixed triangulated category. A family in the sense of arXiv:1902.08184v4 instead has a category on every geometric fiber. This file removes that numerical fixed-category restriction: every index has its own triangulated category, Grothendieck group, class map, and slicing, while all classes land in one common real numerical space controlled by one charge and one quadratic form.

This is still an abstract fiber family. It does not provide a scheme, a relative category, or base-change functors, and it makes no openness, relative Harder--Narasimhan, or boundedness claim.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.ordinaryFiberSemistableClasses {I : Type u_1} {V : Type u_3} {C : I → Type u} [(i : I) → Category.{u_4, 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] {v : (i : I) → K₀ (C i) →+ V} (σ : (i : I) → PreStabilityCondition.WithClassMap (C i) (v i)) : I → Set V

The common numerical loci contributed by nonzero semistable objects in the actual slicing on each fiber category.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.ordinaryFiberSemistableClasses σ i = (σ i).semistableClasses

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.mem_ordinaryFiberSemistableClasses_iff {I : Type u_1} {V : Type u_3} {C : I → Type u} [(i : I) → Category.{u_4, 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] {v : (i : I) → K₀ (C i) →+ V} (σ : (i : I) → PreStabilityCondition.WithClassMap (C i) (v i)) (i : I) (x : V) : x ∈ ordinaryFiberSemistableClasses σ i ↔ ∃ (φ : ℝ) (E : C i), (σ i).slicing.P φ E ∧ ¬Limits.IsZero E ∧ x = (v i) (K₀.of (C i) E)

Membership in a fiber locus exposes the phase and the object in that fiber category which produced the common numerical class.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.class_mem_ordinaryFiberSemistableClasses {I : Type u_1} {V : Type u_3} {C : I → Type u} [(i : I) → Category.{u_4, 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] {v : (i : I) → K₀ (C i) →+ V} (σ : (i : I) → PreStabilityCondition.WithClassMap (C i) (v i)) (i : I) {φ : ℝ} {E : C i} (hP : (σ i).slicing.P φ E) (hE : ¬Limits.IsZero E) : (v i) (K₀.of (C i) E) ∈ ordinaryFiberSemistableClasses σ i

A nonzero object in a fiber slice contributes its class to that fiber's selected numerical locus.

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.OrdinaryFiberUniformQuadraticSupportData {I : Type u_1} {V : Type u_3} {C : I → Type u} [(i : I) → Category.{u_4, 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] {v : (i : I) → K₀ (C i) →+ V} (σ : (i : I) → PreStabilityCondition.WithClassMap (C i) (v i)) (Zlin : V →ₗ[ℝ] ℂ) : Prop

One real-linear charge and one genuine quadratic form controlling the actual semistable loci of an indexed family of different fiber categories.

The common space V may itself be the real quotient supplied by the Definition 21.9 comparison layer.

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

  Every fiber central charge is realized by the same charge on the common numerical space.

• quadratic : Support.HasUniformQuadraticSupportProperty Zlin (ordinaryFiberSemistableClasses σ)

  One quadratic form controls every slicing-defined fiber locus.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.OrdinaryFiberUniformQuadraticSupportData.fiber {I : Type u_1} {V : Type u_3} {C : I → Type u} [(i : I) → Category.{u_4, 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] {v : (i : I) → K₀ (C i) →+ V} {σ : (i : I) → PreStabilityCondition.WithClassMap (C i) (v i)} {Zlin : V →ₗ[ℝ] ℂ} (h : OrdinaryFiberUniformQuadraticSupportData σ Zlin) (i : I) : (σ i).QuadraticSupportData Zlin

Restrict varying-fiber uniform support to one actual fiber category.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.OrdinaryFiberUniformQuadraticSupportData.reindex {I : Type u_1} {J : Type u_2} {V : Type u_3} {C : I → Type u} [(i : I) → Category.{u_4, 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] {v : (i : I) → K₀ (C i) →+ V} {σ : (i : I) → PreStabilityCondition.WithClassMap (C i) (v i)} {Zlin : V →ₗ[ℝ] ℂ} (h : OrdinaryFiberUniformQuadraticSupportData σ Zlin) (f : J → I) : OrdinaryFiberUniformQuadraticSupportData (fun (j : J) => σ (f j)) Zlin

Reindex a varying family without changing its common charge or quadratic form.

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

One ordinary supported category gives the constant varying-fiber model. This witnesses the dependent interface without using an empty index type.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.ordinaryFiberUniformQuadraticSupportData_punit {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] {C₀ : Type u} [Category.{u_4, u} C₀] [Preadditive C₀] [Limits.HasZeroObject C₀] [HasShift C₀ ℤ] [∀ (n : ℤ), (shiftFunctor C₀ n).Additive] [Pretriangulated C₀] {v₀ : K₀ C₀ →+ V} {σ : PreStabilityCondition.WithClassMap C₀ v₀} {Zlin : V →ₗ[ℝ] ℂ} (h : σ.QuadraticSupportData Zlin) : OrdinaryFiberUniformQuadraticSupportData (fun (x : PUnit.{u_5 + 1}) => σ) Zlin

The inhabited PUnit specialization of the constant fiber family.