Finite-type openness and relative HN consequences

This file discharges the scheme-facing openness and relative-HN interfaces from the geometric bounded-coherent base-change witness.

The finite-type condition is the standard scheme-theoretic one: a structure morphism is locally of finite type and quasi-compact. It is recorded on the actual object of Over S, not as a caller-chosen eligibility label.

The input is GeometricPreStabilityBaseChangeData, constructed from genuine bounded coherent pullback and the phase-indexed output of the owned Appendix-A inducing theorem. Its exported phase equivalence has two consequences.

• Residue-fiber phase membership is independent of the point, so each actual semistable locus is either the whole finite-type base change or empty and is Zariski open. Generic openness uses the same open locus.
• The HN filtration supplied by the slicing over a regular curve base pulls to every residue fiber. This constructs SchemeRelativeHNFiltration objectwise, including its existing length, phase, factor, and further base-change compatibility.

No openness proposition or relative-HN existence proposition is an input. The finite-type proofs are not needed after restricting the quantifiers, because the geometric phase equivalence proves the stronger all-base-change statement. This is a consequence of the deliberately strong pseudofunctorial family interface; it is not a formalization of semistable reduction, a moduli-space construction, or Theorem 22.2 of arXiv:1902.08184v4.

structure AlgebraicGeometry.Moduli.Semistability.FiniteTypeSchemeSemistableLocusIndex {S : Scheme} (F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S) : Type (max (u + 1) u_1)

A semistable-locus index whose actual structure morphism is of finite type.

• index : SchemeSemistableLocusIndex F

  The actual object, phase, and family object being tested.

• finiteType : DerivedCategory.Families.IsFiniteTypeBaseChange self.index.baseChange

  The structure morphism is locally of finite type and quasi-compact.

structure AlgebraicGeometry.Moduli.Semistability.FiniteTypeSchemeGenericSemistableLocusIndex {S : Scheme} (F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S) : Type (max (u + 1) u_1)

A generic semistable-locus index on an actual finite-type base change.

• index : SchemeGenericSemistableLocusIndex F

  The actual locus and distinguished point.

• finiteType : DerivedCategory.Families.IsFiniteTypeBaseChange self.index.index.baseChange

  The structure morphism is locally of finite type and quasi-compact.

def AlgebraicGeometry.Moduli.Semistability.finiteTypeRegularCurveEligible {S : Scheme} (T : HarderNarasimhan.RegularCurveBaseChange S) : Prop

A regular curve base change is eligible for the finite-type relative-HN statement precisely when its structure morphism is of finite type.

Equations

• AlgebraicGeometry.Moduli.Semistability.finiteTypeRegularCurveEligible T = AlgebraicGeometry.DerivedCategory.Families.IsFiniteTypeBaseChange T.baseChange

theorem AlgebraicGeometry.Moduli.Semistability.finiteTypeSchemeSemistableLocus_isOpen {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} [∀ (T : DerivedCategory.Families.SchemeBaseChange S), IsLocallyNoetherian (CategoryTheory.Over.left T)] [{T U : DerivedCategory.Families.SchemeBaseChange S} → (f : T ⟶ U) → DerivedCategory.Families.SchemeBaseChange.HasCoherentPullback f] {R : DerivedCategory.Families.BoundedCoherentDerivedRealization F} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} (h : DerivedCategory.Families.GeometricPreStabilityBaseChangeData F R classMap sigma) (j : FiniteTypeSchemeSemistableLocusIndex F) : IsOpen (schemeSemistableLocus F classMap sigma j.index)

Every semistable locus on an actual finite-type base change is Zariski open, with no openness conclusion supplied by the caller.

theorem AlgebraicGeometry.Moduli.Semistability.universalFiniteTypeSchemeSemistableOpenness {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} [∀ (T : DerivedCategory.Families.SchemeBaseChange S), IsLocallyNoetherian (CategoryTheory.Over.left T)] [{T U : DerivedCategory.Families.SchemeBaseChange S} → (f : T ⟶ U) → DerivedCategory.Families.SchemeBaseChange.HasCoherentPullback f] {R : DerivedCategory.Families.BoundedCoherentDerivedRealization F} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} (h : DerivedCategory.Families.GeometricPreStabilityBaseChangeData F R classMap sigma) : CategoryTheory.Triangulated.WeakStabilityCondition.Families.UniversalOpenness fun (j : FiniteTypeSchemeSemistableLocusIndex F) => schemeSemistableOpenProbe F classMap sigma j.index

Universal openness restricted to actual finite-type scheme base changes.

theorem AlgebraicGeometry.Moduli.Semistability.finiteTypeSchemeGenericSemistabilityProbe_isGenericallyOpen {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} [∀ (T : DerivedCategory.Families.SchemeBaseChange S), IsLocallyNoetherian (CategoryTheory.Over.left T)] [{T U : DerivedCategory.Families.SchemeBaseChange S} → (f : T ⟶ U) → DerivedCategory.Families.SchemeBaseChange.HasCoherentPullback f] {R : DerivedCategory.Families.BoundedCoherentDerivedRealization F} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} (h : DerivedCategory.Families.GeometricPreStabilityBaseChangeData F R classMap sigma) (j : FiniteTypeSchemeGenericSemistableLocusIndex F) : (schemeGenericSemistabilityProbe F classMap sigma j.index).IsGenericallyOpen

Generic openness is obtained from the same Zariski-open semistable locus, not from a separate generic-openness premise.

theorem AlgebraicGeometry.Moduli.Semistability.universalFiniteTypeSchemeGenericSemistabilityOpenness {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} [∀ (T : DerivedCategory.Families.SchemeBaseChange S), IsLocallyNoetherian (CategoryTheory.Over.left T)] [{T U : DerivedCategory.Families.SchemeBaseChange S} → (f : T ⟶ U) → DerivedCategory.Families.SchemeBaseChange.HasCoherentPullback f] {R : DerivedCategory.Families.BoundedCoherentDerivedRealization F} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} (h : DerivedCategory.Families.GeometricPreStabilityBaseChangeData F R classMap sigma) : CategoryTheory.Triangulated.WeakStabilityCondition.Families.UniversalGenericOpenness fun (j : FiniteTypeSchemeGenericSemistableLocusIndex F) => schemeGenericSemistabilityProbe F classMap sigma j.index

Universal generic openness on actual finite-type scheme base changes.

noncomputable def AlgebraicGeometry.Moduli.Semistability.finiteTypeSchemeRelativeHNFiltration {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} [∀ (T : DerivedCategory.Families.SchemeBaseChange S), IsLocallyNoetherian (CategoryTheory.Over.left T)] [{T U : DerivedCategory.Families.SchemeBaseChange S} → (f : T ⟶ U) → DerivedCategory.Families.SchemeBaseChange.HasCoherentPullback f] {R : DerivedCategory.Families.BoundedCoherentDerivedRealization F} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} (h : DerivedCategory.Families.GeometricPreStabilityBaseChangeData F R classMap sigma) (T : HarderNarasimhan.RegularCurveBaseChange S) : finiteTypeRegularCurveEligible T → (E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T.baseChange) → HarderNarasimhan.SchemeRelativeHNFiltration F classMap sigma E

Construct an actual relative HN filtration for one object over an eligible regular finite-type curve. The ordinary HN filtration comes from the slicing; the geometric witness constructs all residue-fiber filtrations and their compatibility.

Equations

• AlgebraicGeometry.Moduli.Semistability.finiteTypeSchemeRelativeHNFiltration h T x✝ E = AlgebraicGeometry.Moduli.HarderNarasimhan.SchemeRelativeHNFiltration.ofBaseChangeWitness ⋯.some ⋯

theorem AlgebraicGeometry.Moduli.Semistability.hasFiniteTypeSchemeRelativeHNFiltrations {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} [∀ (T : DerivedCategory.Families.SchemeBaseChange S), IsLocallyNoetherian (CategoryTheory.Over.left T)] [{T U : DerivedCategory.Families.SchemeBaseChange S} → (f : T ⟶ U) → DerivedCategory.Families.SchemeBaseChange.HasCoherentPullback f] {R : DerivedCategory.Families.BoundedCoherentDerivedRealization F} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} (h : DerivedCategory.Families.GeometricPreStabilityBaseChangeData F R classMap sigma) : HarderNarasimhan.HasSchemeRelativeHNFiltrations F classMap sigma finiteTypeRegularCurveEligible

The geometric bounded-coherent witness supplies objectwise relative HN existence on every regular finite-type curve base change.

theorem AlgebraicGeometry.Moduli.Semistability.integratesAfterFiniteTypeRegularCurveBaseChange {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} [∀ (T : DerivedCategory.Families.SchemeBaseChange S), IsLocallyNoetherian (CategoryTheory.Over.left T)] [{T U : DerivedCategory.Families.SchemeBaseChange S} → (f : T ⟶ U) → DerivedCategory.Families.SchemeBaseChange.HasCoherentPullback f] {R : DerivedCategory.Families.BoundedCoherentDerivedRealization F} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} (h : DerivedCategory.Families.GeometricPreStabilityBaseChangeData F R classMap sigma) : CategoryTheory.Triangulated.WeakStabilityCondition.Families.IntegratesAfterDedekindBaseChange (HarderNarasimhan.schemeRelativeHNProblem F classMap sigma finiteTypeRegularCurveEligible)

Consequently every regular finite-type curve base change integrates the existing object-level relative-HN problem, without accepting HasSchemeRelativeHNFiltrations as an input.

structure AlgebraicGeometry.Moduli.Semistability.FiniteTypeGeometricConsequences {S : Scheme} (F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S) {V : Type uV} [AddCommGroup V] (classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V) (sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)) : Prop

The three finite-type geometric conclusions exported together. This is an output package; none of its fields is assumed by the construction theorem below.

• semistableOpenness : CategoryTheory.Triangulated.WeakStabilityCondition.Families.UniversalOpenness fun (j : FiniteTypeSchemeSemistableLocusIndex F) => schemeSemistableOpenProbe F classMap sigma j.index

  Zariski openness of all actual finite-type semistable loci.

• genericOpenness : CategoryTheory.Triangulated.WeakStabilityCondition.Families.UniversalGenericOpenness fun (j : FiniteTypeSchemeGenericSemistableLocusIndex F) => schemeGenericSemistabilityProbe F classMap sigma j.index

  Generic openness derived from those same loci.

• relativeHN : HarderNarasimhan.HasSchemeRelativeHNFiltrations F classMap sigma finiteTypeRegularCurveEligible

  Objectwise relative HN existence on regular finite-type curves.

theorem AlgebraicGeometry.Moduli.Semistability.GeometricPreStabilityBaseChangeData.finiteTypeConsequences {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} [∀ (T : DerivedCategory.Families.SchemeBaseChange S), IsLocallyNoetherian (CategoryTheory.Over.left T)] [{T U : DerivedCategory.Families.SchemeBaseChange S} → (f : T ⟶ U) → DerivedCategory.Families.SchemeBaseChange.HasCoherentPullback f] {R : DerivedCategory.Families.BoundedCoherentDerivedRealization F} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} (h : DerivedCategory.Families.GeometricPreStabilityBaseChangeData F R classMap sigma) : FiniteTypeGeometricConsequences F classMap sigma

Construct every finite-type geometric consequence from the previously built bounded-coherent base-change input.