Scheme semistable loci

This file removes the arbitrary-set freedom from the scheme-facing openness probes. For an object over a scheme base change, its semistable locus is the set of points where the actual pullback to the residue fiber belongs to the chosen phase of the actual fiber slicing. The associated openness and generic-openness probes therefore use the Zariski topology of the scheme and that definitionally fixed locus.

FiberPreStabilityBaseChangeData is a deliberately strong named geometric hypothesis: it identifies every target slicing with the preimage slicing under pullback. Under that hypothesis, phase membership at the residue fibers is equivalent to phase membership over the base change, so the locus is either the whole scheme or empty and is therefore open. The constant categorical family supplies a concrete logically inhabited model of this implication.

No such compatibility witness is constructed here. In particular, this file does not assert exactness of arbitrary residue-field pullback, construct a geometric inducing package, prove openness for an arbitrary family, construct relative Harder--Narasimhan filtrations, or prove Theorem 22.2 of arXiv:1902.08184v4.

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

An object and a phase whose residue-fiber semistable locus is to be measured on an actual scheme base change.

• baseChange : DerivedCategory.Families.SchemeBaseChange S

  The scheme base change carrying the object.

• phase : ℝ

  The phase to test after pullback to every residue fiber.

• object : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F self.baseChange

  The object whose residue-fiber pullbacks are tested.

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

A semistable-locus index together with a distinguished point at which the generic-openness implication is tested. Geometry may require this point to be generic; that property remains an explicit responsibility of the caller.

• index : SchemeSemistableLocusIndex F

  The underlying object-and-phase index.

• genericPoint : ↥(CategoryTheory.Over.left self.index.baseChange)

  The distinguished point used by the generic-openness probe.

def AlgebraicGeometry.Moduli.Semistability.schemeSemistableLocus {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)) (j : SchemeSemistableLocusIndex F) : Set ↥(CategoryTheory.Over.left j.baseChange)

The genuine pointwise semistable locus of a family object: membership is phase membership of its actual pullback to the residue-field fiber.

Equations

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

@[simp]

theorem AlgebraicGeometry.Moduli.Semistability.mem_schemeSemistableLocus_iff {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)) (j : SchemeSemistableLocusIndex F) (x : ↥(CategoryTheory.Over.left j.baseChange)) : x ∈ schemeSemistableLocus F classMap sigma j ↔ (sigma (j.baseChange.residue x)).slicing.P j.phase ((F.pullToResidue j.baseChange x).obj j.object)

theorem AlgebraicGeometry.Moduli.Semistability.mem_schemeSemistableLocus_iff_of_baseChange {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)} (h : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData F classMap sigma) (j : SchemeSemistableLocusIndex F) (x : ↥(CategoryTheory.Over.left j.baseChange)) : x ∈ schemeSemistableLocus F classMap sigma j ↔ (sigma j.baseChange).slicing.P j.phase j.object

The geometric preimage-slicing witness identifies residue-fiber membership with phase membership of the original family object.

theorem AlgebraicGeometry.Moduli.Semistability.schemeSemistableLocus_eq_univ_of_phase {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)} (h : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData F classMap sigma) (j : SchemeSemistableLocusIndex F) (hP : (sigma j.baseChange).slicing.P j.phase j.object) : schemeSemistableLocus F classMap sigma j = Set.univ

Under the geometric preimage-slicing witness, a family object already in the chosen phase has the full scheme as its residue-fiber semistable locus.

theorem AlgebraicGeometry.Moduli.Semistability.schemeSemistableLocus_eq_empty_of_not_phase {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)} (h : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData F classMap sigma) (j : SchemeSemistableLocusIndex F) (hP : ¬(sigma j.baseChange).slicing.P j.phase j.object) : schemeSemistableLocus F classMap sigma j = ∅

Under the same witness, failure of phase membership makes the residue-fiber semistable locus empty.

theorem AlgebraicGeometry.Moduli.Semistability.schemeSemistableLocus_isOpen {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)} (h : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData F classMap sigma) (j : SchemeSemistableLocusIndex F) : IsOpen (schemeSemistableLocus F classMap sigma j)

A compatible geometric slicing family makes every actual semistable locus Zariski open. The conclusion follows from the explicit all-or-none statement, not from a caller-supplied open set.