Input conditions for stability conditions in families

This file isolates the parts of Definition 20.5 and Definition 21.15 of arXiv:1902.08184v4 which make sense without schemes, derived categories over a base, or moduli stacks. A caller supplies all geometric tests:

• ChargeProbe represents a base change together with a perfect object and the resulting pointwise charge (Definition 20.5(1));
• OpenLocusProbe represents one geometric-stability locus (Definition 20.5(2));
• GenericSemistabilityProbe represents the generic semistability test in the weak clause (2');
• DedekindHNProblem and WeakDedekindHNProblem name the witnesses demanded after every eligible essentially-finite-type Dedekind base change (clauses (3) and (3'));
• the generic BoundednessProblem interface names the moduli problems whose boundedness is required by Definition 21.15(5).

The word eligible is deliberate: this library has no scheme or base-change API, so it does not pretend to recognize Dedekind morphisms. Instantiating that predicate and the witness types is a geometric obligation of a client. These interfaces turn those obligations into separately auditable propositions; they do not prove any geometric theorem. Deliberately constant, full-locus, and proposition-only inhabitants are kept out of this stable module. Compile-only demonstrations of logical inhabitance live under DerivedAlgGeo.Development.StabilityCondition.Families.Scaffolding.

structure CategoryTheory.Triangulated.WeakStabilityCondition.Families.ChargeProbe (A : Type v) : Type (max (u + 1) v)

One universally quantified charge test. Its point type and topology are part of the supplied geometric datum.

• Point : Type u

  Points of the chosen base change.

• topology : TopologicalSpace self.Point

  The topology on those points.

• value : self.Point → A

  The charge of the chosen object on every point.

def CategoryTheory.Triangulated.WeakStabilityCondition.Families.ChargeProbe.IsLocallyConstant {A : Type v} (P : ChargeProbe A) : Prop

Definition 20.5(1) for one supplied base-change/object probe.

Equations

• P.IsLocallyConstant = IsLocallyConstant P.value

def CategoryTheory.Triangulated.WeakStabilityCondition.Families.UniversallyLocallyConstantCharge {J : Type u} {A : Type v} (P : J → ChargeProbe A) : Prop

Definition 20.5(1): every supplied base-change/object probe has locally constant charge. Universality is the outer quantifier over J.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.Families.UniversallyLocallyConstantCharge P = ∀ (j : J), (P j).IsLocallyConstant

structure CategoryTheory.Triangulated.WeakStabilityCondition.Families.OpenLocusProbe : Type (u + 1)

One supplied geometric-stability locus.

• Point : Type u

  Points of the chosen base change.

• topology : TopologicalSpace self.Point

  The topology on those points.

• locus : Set self.Point

  The points where the supplied object is geometrically stable.

def CategoryTheory.Triangulated.WeakStabilityCondition.Families.OpenLocusProbe.IsOpen (P : OpenLocusProbe) : Prop

Definition 20.5(2) for one supplied geometric-stability probe.

Equations

• P.IsOpen = IsOpen P.locus

def CategoryTheory.Triangulated.WeakStabilityCondition.Families.UniversalOpenness {J : Type u} (P : J → OpenLocusProbe) : Prop

Definition 20.5(2): geometric stability is open for every supplied base-change/object probe.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.Families.UniversalOpenness P = ∀ (j : J), (P j).IsOpen

structure CategoryTheory.Triangulated.WeakStabilityCondition.Families.GenericSemistabilityProbe : Type (u + 1)

One weak generic-semistability probe for Definition 20.5(2').

• Point : Type u

  Points of the chosen base change.

• topology : TopologicalSpace self.Point

  The topology on those points.

• genericPoint : self.Point

  The distinguished generic point.

• semistableLocus : Set self.Point

  The locus where the supplied object is semistable.

def CategoryTheory.Triangulated.WeakStabilityCondition.Families.GenericSemistabilityProbe.IsGenericallyOpen (P : GenericSemistabilityProbe) : Prop

The weak generic-openness clause for one probe: semistability at the generic point extends to an open neighbourhood of that point.

Equations

• P.IsGenericallyOpen = (P.genericPoint ∈ P.semistableLocus → ∃ (U : Set P.Point), IsOpen U ∧ P.genericPoint ∈ U ∧ U ⊆ P.semistableLocus)

def CategoryTheory.Triangulated.WeakStabilityCondition.Families.UniversalGenericOpenness {J : Type u} (P : J → GenericSemistabilityProbe) : Prop

Definition 20.5(2'): generic semistability is open for every supplied probe.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.Families.UniversalGenericOpenness P = ∀ (j : J), (P j).IsGenericallyOpen

structure CategoryTheory.Triangulated.WeakStabilityCondition.Families.DedekindHNProblem (D : Type u) : Type (max u (v + 1))

The abstract data of the ordinary HN integration problem after a proposed Dedekind base change. IsEligible is where a geometric client must encode "essentially of finite type over a Dedekind scheme".

• IsEligible : D → Prop

  Which supplied base changes are in the source's quantified class.

• HNStructure : D → Type v

  The type of relative HN structures to be constructed on a base change.

def CategoryTheory.Triangulated.WeakStabilityCondition.Families.IntegratesAfterDedekindBaseChange {D : Type u} (P : DedekindHNProblem D) : Prop

Definition 20.5(3): every eligible Dedekind base change carries a relative HN structure.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.Families.IntegratesAfterDedekindBaseChange P = ∀ (d : D), P.IsEligible d → Nonempty (P.HNStructure d)

structure CategoryTheory.Triangulated.WeakStabilityCondition.Families.WeakDedekindHNProblem (D : Type u) : Type (max u (v + 1))

The abstract weak HN integration problem of Definition 20.5(3'). The extra predicate records that the induced zero-charge torsion subcategory is noetherian after the same base change.

• IsEligible : D → Prop

  Which supplied base changes are eligible.

• HNStructure : D → Type v

  The type of induced weak HN structures.

• ZeroChargeNoetherian : D → Prop

  The noetherian zero-charge obligation on each base change.

def CategoryTheory.Triangulated.WeakStabilityCondition.Families.WeakIntegratesAfterDedekindBaseChange {D : Type u} (P : WeakDedekindHNProblem D) : Prop

Definition 20.5(3'): every eligible base change has both a weak HN structure and a noetherian zero-charge torsion subcategory.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.Families.WeakIntegratesAfterDedekindBaseChange P = ∀ (d : D), P.IsEligible d → Nonempty (P.HNStructure d) ∧ P.ZeroChargeNoetherian d

structure CategoryTheory.Triangulated.WeakStabilityCondition.Families.OrdinaryDefinition20_5Conditions {JCharge : Type u₁} {JOpen : Type u₂} {D : Type u₃} (charge : JCharge → ChargeProbe ℂ) (stable : JOpen → OpenLocusProbe) (dedekind : DedekindHNProblem D) : Prop

The three ordinary clauses of Definition 20.5, kept as separately named fields so a review can inspect their quantifier boundaries independently.

• locallyConstantCharge : UniversallyLocallyConstantCharge charge

  Definition 20.5(1).

• opennessOfGeometricStability : UniversalOpenness stable

  Definition 20.5(2).

• dedekindHN : IntegratesAfterDedekindBaseChange dedekind

  Definition 20.5(3).

structure CategoryTheory.Triangulated.WeakStabilityCondition.Families.WeakDefinition20_5Conditions {JCharge : Type u₁} {JGeneric : Type u₂} {D : Type u₃} (charge : JCharge → ChargeProbe ℂ) (semistable : JGeneric → GenericSemistabilityProbe) (dedekind : WeakDedekindHNProblem D) : Prop

The topological and relative-HN parts of the weak variant of Definition 20.5. Clause (0), which refers to an actual weak stability function, is bound to the repository's weak API in Families.Weak.

• locallyConstantCharge : UniversallyLocallyConstantCharge charge

  Definition 20.5(1).

• genericOpennessOfSemistability : UniversalGenericOpenness semistable

  Definition 20.5(2').

• dedekindWeakHN : WeakIntegratesAfterDedekindBaseChange dedekind

  Definition 20.5(3').