Stability over a field and the good-moduli input chain

This file records Definition 8.17 and the implication chain used in Theorem 8.23 of arXiv:2607.28411v1. Definition817Conditions specializes the existing canonical OrdinaryDeformationInputConditions root to the actual semistable classes of the fiber slicings. Its four conditions are uniform quotient support, openness, relative HN structures after the specified Dedekind base changes, and boundedness.

The external HLR and BLMNPS results used by the paper are named proposition types. Assembly theorems consume them as hypotheses; no structure carries a good-moduli conclusion, and this file does not manufacture a moduli space. The semistable variant used by Lemma 8.22 is a second abbreviation of the same root with semistable probes substituted for stable probes.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.Definition817Conditions {I : Type u_1} {JOpen : Type u_2} {D : Type u_3} {M : Type u_4} {V : Type u_5} {C : I → Type u} [(i : I) → Category.{u_6, 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} (σ : (i : I) → PreStabilityCondition.WithClassMap (C i) (v i)) (V₀ : Submodule ℝ V) (Zlin : V →ₗ[ℝ] ℂ) (hV₀ : V₀ ≤ Zlin.ker) (openLoci : JOpen → Families.OpenLocusProbe) (dedekind : Families.DedekindHNProblem D) (boundedness : Moduli.BoundednessProblem M) : Prop

The four clauses of PF4 Definition 8.17 as a specialization of the canonical deformation-input root. The support locus is definitionally the set of classes of actual nonzero semistable objects in each fiber. The zero-charge subspace and its containment proof stay explicit, as required by the repository's quotient-support interface.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.Lemma822SemistableConditions {I : Type u_1} {JOpen : Type u_2} {D : Type u_3} {M : Type u_4} {V : Type u_5} {C : I → Type u} [(i : I) → Category.{u_6, 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} (σ : (i : I) → PreStabilityCondition.WithClassMap (C i) (v i)) (V₀ : Submodule ℝ V) (Zlin : V →ₗ[ℝ] ℂ) (hV₀ : V₀ ≤ Zlin.ker) (semistableLoci : JOpen → Families.OpenLocusProbe) (dedekind : Families.DedekindHNProblem D) (semistableBoundedness : Moduli.BoundednessProblem M) : Prop

The (ii')/(iv') semistable variant used in PF4 Lemma 8.22. It is the same canonical four-condition interface; only the caller's openness and boundedness probes now describe semistable objects.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.HLRTheorem235OneToTwo {J : Type u_6} (dimension : J → ℕ) (mass : J → ℝ) (boundedMassAndPhase : Prop) : Prop

HLR Theorem 2.35, implication (1) → (2), in the exact direction used in PF4 Theorem 8.23.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.HLRProposition238 {JOpen : Type u_2} (boundedMassAndPhase : Prop) (semistableLoci : JOpen → Families.OpenLocusProbe) : Prop

HLR Proposition 2.38 as used to obtain semistable openness from the bounded-mass-and-phase condition.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.BLMNPSTheorems187And57 {D : Type u_3} (boundedMassAndPhase : Prop) (dedekind : Families.DedekindHNProblem D) : Prop

BLMNPS Theorems 18.7 and 5.7, together with HLR Proposition 2.38, in the direction used to construct relative HN structures.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.HLRProposition241 {M : Type u_4} (boundedMassAndPhase : Prop) (semistableBoundedness : Moduli.BoundednessProblem M) : Prop

The boundedness implication extracted from the proof of HLR Proposition 2.41, producing the semistable form of clause (iv').

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.PF4Lemma822 {I : Type u_1} {JOpen : Type u_2} {D : Type u_3} {M : Type u_4} {V : Type u_5} {C : I → Type u} [(i : I) → Category.{u_6, 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} {σ : (i : I) → PreStabilityCondition.WithClassMap (C i) (v i)} (V₀ : Submodule ℝ V) {Zlin : V →ₗ[ℝ] ℂ} (hV₀ : V₀ ≤ Zlin.ker) (semistableLoci : JOpen → Families.OpenLocusProbe) (stableLoci : JOpen → Families.OpenLocusProbe) (dedekind : Families.DedekindHNProblem D) (semistableBoundedness stableBoundedness : Moduli.BoundednessProblem M) : Prop

PF4 Lemma 8.22, kept as an explicit implication from its semistable hypotheses to Definition 8.17.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.BLMNPSTheorem2124 {I : Type u_1} {JOpen : Type u_2} {D : Type u_3} {M : Type u_4} {V : Type u_5} {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} (k : Type u_6) [Field k] {σ : (i : I) → PreStabilityCondition.WithClassMap (C i) (v i)} (V₀ : Submodule ℝ V) {Zlin : V →ₗ[ℝ] ℂ} (hV₀ : V₀ ≤ Zlin.ker) (stableLoci : JOpen → Families.OpenLocusProbe) (dedekind : Families.DedekindHNProblem D) (stableBoundedness : Moduli.BoundednessProblem M) (ProperGoodModuli : Prop) : Prop

BLMNPS Theorem 21.24 in the characteristic-zero direction used in PF4 Theorem 8.23. ProperGoodModuli is a caller-supplied proposition because the repository does not yet define good moduli spaces.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.lemma822SemistableConditions_of_massHom {I : Type u_1} {JOpen : Type u_2} {D : Type u_3} {M : Type u_4} {V : Type u_5} {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} {J : Type u_6} {dimension : J → ℕ} {mass : J → ℝ} {boundedMassAndPhase : Prop} {σ : (i : I) → PreStabilityCondition.WithClassMap (C i) (v i)} {V₀ : Submodule ℝ V} {Zlin : V →ₗ[ℝ] ℂ} {hV₀ : V₀ ≤ Zlin.ker} {semistableLoci : JOpen → Families.OpenLocusProbe} {dedekind : Families.DedekindHNProblem D} {semistableBoundedness : Moduli.BoundednessProblem M} (hSupport : Support.HasUniformQuadraticSupportPropertyModulo V₀ Zlin hV₀ (ordinaryFiberSemistableClasses σ)) (h84 : StabilityCondition.WithClassMap.UniformMassHomBound dimension mass) (h235 : HLRTheorem235OneToTwo dimension mass boundedMassAndPhase) (h238 : HLRProposition238 boundedMassAndPhase semistableLoci) (hHN : BLMNPSTheorems187And57 boundedMassAndPhase dedekind) (h241 : HLRProposition241 boundedMassAndPhase semistableBoundedness) : Lemma822SemistableConditions σ V₀ Zlin hV₀ semistableLoci dedekind semistableBoundedness

Assemble the semistable four-condition input of PF4 Lemma 8.22 from the mass--Hom estimate and the named HLR/BLMNPS implications.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.theorem823_definition817 {I : Type u_1} {JOpen : Type u_2} {D : Type u_3} {M : Type u_4} {V : Type u_5} {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} {J : Type u_6} {dimension : J → ℕ} {mass : J → ℝ} {boundedMassAndPhase : Prop} {σ : (i : I) → PreStabilityCondition.WithClassMap (C i) (v i)} {V₀ : Submodule ℝ V} {Zlin : V →ₗ[ℝ] ℂ} {hV₀ : V₀ ≤ Zlin.ker} {semistableLoci : JOpen → Families.OpenLocusProbe} {stableLoci : JOpen → Families.OpenLocusProbe} {dedekind : Families.DedekindHNProblem D} {semistableBoundedness stableBoundedness : Moduli.BoundednessProblem M} (hSupport : Support.HasUniformQuadraticSupportPropertyModulo V₀ Zlin hV₀ (ordinaryFiberSemistableClasses σ)) (h84 : StabilityCondition.WithClassMap.UniformMassHomBound dimension mass) (h235 : HLRTheorem235OneToTwo dimension mass boundedMassAndPhase) (h238 : HLRProposition238 boundedMassAndPhase semistableLoci) (hHN : BLMNPSTheorems187And57 boundedMassAndPhase dedekind) (h241 : HLRProposition241 boundedMassAndPhase semistableBoundedness) (h822 : PF4Lemma822 V₀ hV₀ semistableLoci stableLoci dedekind semistableBoundedness stableBoundedness) : Definition817Conditions σ V₀ Zlin hV₀ stableLoci dedekind stableBoundedness

PF4 Theorem 8.23 up to Definition 8.17: the mass--Hom estimate feeds the named HLR/BLMNPS chain, and PF4 Lemma 8.22 upgrades the semistable clauses.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.theorem823_properGoodModuli {I : Type u_1} {JOpen : Type u_2} {D : Type u_3} {M : Type u_4} {V : Type u_5} {C : I → Type u} [(i : I) → Category.{u_8, 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} (k : Type u_6) [Field k] [CharZero k] {J : Type u_7} {dimension : J → ℕ} {mass : J → ℝ} {boundedMassAndPhase ProperGoodModuli : Prop} {σ : (i : I) → PreStabilityCondition.WithClassMap (C i) (v i)} {V₀ : Submodule ℝ V} {Zlin : V →ₗ[ℝ] ℂ} {hV₀ : V₀ ≤ Zlin.ker} {semistableLoci : JOpen → Families.OpenLocusProbe} {stableLoci : JOpen → Families.OpenLocusProbe} {dedekind : Families.DedekindHNProblem D} {semistableBoundedness stableBoundedness : Moduli.BoundednessProblem M} (hSupport : Support.HasUniformQuadraticSupportPropertyModulo V₀ Zlin hV₀ (ordinaryFiberSemistableClasses σ)) (h84 : StabilityCondition.WithClassMap.UniformMassHomBound dimension mass) (h235 : HLRTheorem235OneToTwo dimension mass boundedMassAndPhase) (h238 : HLRProposition238 boundedMassAndPhase semistableLoci) (hHN : BLMNPSTheorems187And57 boundedMassAndPhase dedekind) (h241 : HLRProposition241 boundedMassAndPhase semistableBoundedness) (h822 : PF4Lemma822 V₀ hV₀ semistableLoci stableLoci dedekind semistableBoundedness stableBoundedness) (h2124 : BLMNPSTheorem2124 k V₀ hV₀ stableLoci dedekind stableBoundedness ProperGoodModuli) : ProperGoodModuli

The final characteristic-zero good-moduli conclusion of PF4 Theorem 8.23, conditional on the named BLMNPS Theorem 21.24 implication. The field and its characteristic-zero instance remain explicit.