Documentation

DerivedAlgGeo.CategoryTheory.Triangulated.StabilityCondition.Families.Ordinary

Ordinary stability-in-families interface #

This file combines the three ordinary clauses of Definition 20.5 with the uniform support and boundedness clauses (4)--(5) of Definition 21.15 of arXiv:1902.08184v4. It is the top-level ordinary abstract family package.

The index types stand for geometric base-change, object, fiber, and numerical moduli tests supplied by a client. The library neither constructs nor recognizes those geometric objects. The support field, by contrast, is the genuine quotient-uniform quadratic support predicate already implemented in the support subsystem. Vacuous-probe inhabitants -- constant-true predicates and full-locus witnesses -- are development scaffolding, not part of this stable interface; constant-family reindexings that consume a genuine support datum remain stable API.

source
structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.OrdinaryStabilityInFamiliesData {JCharge : Type u_1} {JOpen : Type u_2} {D : Type u_3} {I : Type u_4} {M : Type u_5} {V : Type u_6} {W : Type u_7} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (charge : JCharge → Families.ChargeProbe ℂ) (stable : JOpen → Families.OpenLocusProbe) (dedekind : Families.DedekindHNProblem D) (V₀ : Submodule ℝ V) (Z : V →ₗ[ℝ] W) (hV₀ : V₀ ≤ Z.ker) (semistableClasses : I → Set V) (boundedness : Moduli.BoundednessProblem M) :
Prop

The five separately auditable ordinary family conditions: Definition 20.5(1)--(3) followed by Definition 21.15(4)--(5).

Instances For
    source
    structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.OrdinaryDeformationInputConditions {JOpen : Type u_2} {D : Type u_3} {I : Type u_4} {M : Type u_5} {V : Type u_6} {W : Type u_7} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (stable : JOpen → Families.OpenLocusProbe) (dedekind : Families.DedekindHNProblem D) (V₀ : Submodule ℝ V) (Z : V →ₗ[ℝ] W) (hV₀ : V₀ ≤ Z.ker) (semistableClasses : I → Set V) (boundedness : Moduli.BoundednessProblem M) :
    Prop

    The geometric and numerical input conditions used by deformation arguments: openness, relative HN integration, uniform quotient support, and boundedness. The theorem consuming these inputs is deliberately not named or indexed here.

    Instances For