Documentation

DerivedAlgGeo.AlgebraicGeometry.Moduli.Semistability.LocusProbes

Scheme semistable loci as categorical openness probes #

The pointwise locus and its Zariski theorems live in Locus.lean. This file realizes the weak-family OpenLocusProbe, GenericSemistabilityProbe, and universal openness interfaces for that locus. It lives with the geometric object it is about, not below the categorical interface it implements.

source
def AlgebraicGeometry.Moduli.Semistability.schemeSemistableOpenProbe {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) :
CategoryTheory.Triangulated.WeakStabilityCondition.Families.OpenLocusProbe

The openness probe attached to the actual residue-fiber semistable locus.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def AlgebraicGeometry.Moduli.Semistability.schemeGenericSemistabilityProbe {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 : SchemeGenericSemistableLocusIndex F) :
    CategoryTheory.Triangulated.WeakStabilityCondition.Families.GenericSemistabilityProbe

    The generic-openness probe attached to the same semistable locus.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem AlgebraicGeometry.Moduli.Semistability.schemeSemistableOpenProbe_isOpen_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) :
      (schemeSemistableOpenProbe F classMap sigma j).IsOpen ↔ IsOpen (schemeSemistableLocus F classMap sigma j)
      source
      @[simp]
      theorem AlgebraicGeometry.Moduli.Semistability.schemeGenericSemistabilityProbe_isGenericallyOpen_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 : SchemeGenericSemistableLocusIndex F) :
      (schemeGenericSemistabilityProbe F classMap sigma j).IsGenericallyOpen ↔ j.genericPoint ∈ schemeSemistableLocus F classMap sigma j.index → ∃ (U : Set ↥(CategoryTheory.Over.left j.index.baseChange)), IsOpen U ∧ j.genericPoint ∈ U ∧ U ⊆ schemeSemistableLocus F classMap sigma j.index
      source
      theorem AlgebraicGeometry.Moduli.Semistability.universalSchemeSemistableOpenness_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)) :
      (CategoryTheory.Triangulated.WeakStabilityCondition.Families.UniversalOpenness fun (j : SchemeSemistableLocusIndex F) => schemeSemistableOpenProbe F classMap sigma j) ↔ ∀ (j : SchemeSemistableLocusIndex F), IsOpen (schemeSemistableLocus F classMap sigma j)
      source
      theorem AlgebraicGeometry.Moduli.Semistability.universalSchemeGenericSemistabilityOpenness_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)) :
      (CategoryTheory.Triangulated.WeakStabilityCondition.Families.UniversalGenericOpenness fun (j : SchemeGenericSemistableLocusIndex F) => schemeGenericSemistabilityProbe F classMap sigma j) ↔ ∀ (j : SchemeGenericSemistableLocusIndex F), j.genericPoint ∈ schemeSemistableLocus F classMap sigma j.index → ∃ (U : Set ↥(CategoryTheory.Over.left j.index.baseChange)), IsOpen U ∧ j.genericPoint ∈ U ∧ U ⊆ schemeSemistableLocus F classMap sigma j.index
      source
      theorem AlgebraicGeometry.Moduli.Semistability.universalSchemeSemistableOpenness {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) :
      CategoryTheory.Triangulated.WeakStabilityCondition.Families.UniversalOpenness fun (j : SchemeSemistableLocusIndex F) => schemeSemistableOpenProbe F classMap sigma j

      Geometric base-change compatibility realizes universal openness.

      source
      theorem AlgebraicGeometry.Moduli.Semistability.schemeGenericSemistabilityProbe_isGenericallyOpen {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 : SchemeGenericSemistableLocusIndex F) :
      (schemeGenericSemistabilityProbe F classMap sigma j).IsGenericallyOpen

      A Zariski-open semistable locus realizes the generic-openness probe.

      source
      theorem AlgebraicGeometry.Moduli.Semistability.universalSchemeGenericSemistabilityOpenness {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) :
      CategoryTheory.Triangulated.WeakStabilityCondition.Families.UniversalGenericOpenness fun (j : SchemeGenericSemistableLocusIndex F) => schemeGenericSemistabilityProbe F classMap sigma j

      Geometric base-change compatibility realizes universal generic openness.

      source
      theorem AlgebraicGeometry.Moduli.Semistability.universalSchemeSemistableOpenness_constant (S : Scheme) (C : Type w) [CategoryTheory.Category.{w, w} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (V : Type uV) [AddCommGroup V] (v₀ : CategoryTheory.Triangulated.K₀ C →+ V) (sigma₀ : CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap C v₀) :
      CategoryTheory.Triangulated.WeakStabilityCondition.Families.UniversalOpenness fun (j : SchemeSemistableLocusIndex (DerivedCategory.Families.SchemeTriangulatedFiberFamily.constant S C)) => schemeSemistableOpenProbe (DerivedCategory.Families.SchemeTriangulatedFiberFamily.constant S C) (fun (x : DerivedCategory.Families.SchemeBaseChange S) => v₀) (fun (x : DerivedCategory.Families.SchemeBaseChange S) => sigma₀) j

      The constant family realizes universal scheme semistable openness.

      source
      theorem AlgebraicGeometry.Moduli.Semistability.universalSchemeGenericSemistabilityOpenness_constant (S : Scheme) (C : Type w) [CategoryTheory.Category.{w, w} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (V : Type uV) [AddCommGroup V] (v₀ : CategoryTheory.Triangulated.K₀ C →+ V) (sigma₀ : CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap C v₀) :
      CategoryTheory.Triangulated.WeakStabilityCondition.Families.UniversalGenericOpenness fun (j : SchemeGenericSemistableLocusIndex (DerivedCategory.Families.SchemeTriangulatedFiberFamily.constant S C)) => schemeGenericSemistabilityProbe (DerivedCategory.Families.SchemeTriangulatedFiberFamily.constant S C) (fun (x : DerivedCategory.Families.SchemeBaseChange S) => v₀) (fun (x : DerivedCategory.Families.SchemeBaseChange S) => sigma₀) j

      The constant family realizes universal generic openness.