Stable reduction of curves and stable maps

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremClassification of minimal numerical types of genus one#

Classification of minimal numerical types of genus one (Stacks, Lemma 55.6.2). Every minimal numerical type of arithmetic genus one belongs to one of the shape families of TauCeti.NumericalType.IsGenusOneMinimalShape.

TauCeti.NumericalType.IsMinimal.isGenusOneMinimalShape.{u} {T : TauCeti.NumericalType}
  (hT : T.IsMinimal) (hg : T.arithmeticGenus = 1) : T.IsGenusOneMinimalShape
Lean

Formalized in Tau Ceti as TauCeti.NumericalType.IsMinimal.isGenusOneMinimalShape.

Sources
LeanTauCeti.NumericalType.IsMinimal.isGenusOneMinimalShape

TheoremPrime torsion of a numerical type#

In a numerical type of genus g ≥ 2, every prime ℓ > 768g - 768 satisfies dim_{𝔽_ℓ} Pic(T)[ℓ] ≤ g. In particular this holds for every prime ℓ > 768g, which is Stacks, Proposition 55.7.4.

TauCeti.NumericalType.finrank_torsion_le_arithmeticGenus.{u} {T : TauCeti.NumericalType}
  (hg : 2 ≤ T.arithmeticGenus) (ℓ : ℕ) [Fact (Nat.Prime ℓ)]
  (hℓ : 768 * T.arithmeticGenus - 768 < ↑ℓ) :
  ↑(Module.finrank (ZMod ℓ) ↥(T.torsion ℓ)) ≤ T.arithmeticGenus
Lean

Formalized in Tau Ceti as TauCeti.NumericalType.finrank_torsion_le_arithmeticGenus.

Sources
LeanTauCeti.NumericalType.finrank_torsion_le_arithmeticGenus
Uses 1
Proof usesSylvester's rank inequality

TheoremA curve of genus zero with a divisor of degree one has nodal reduction#

Let C be a regular proper curve over the fraction field K of a discrete valuation ring R, with K integrally closed in K(C). If dim_K H¹(C, 𝒪_C) = 0 and some divisor on C has degree one, then C has a proper at-worst-nodal model over R; indeed C ≅ ℙ¹_K, which has the smooth proper model ℙ¹_R.

TauCeti.HasNodalReduction.of_genus_eq_zero_of_divisor_degree_eq_one.{u} {R K : Type u} [CommRing R]
  [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K]
  (C : AlgebraicGeometry.Scheme) [C.Over (AlgebraicGeometry.Spec ↧K)]
  [AlgebraicGeometry.Scheme.IsCurveOver K]
  [∀ (y : TauCeti.AlgebraicGeometry.CodimensionOnePoint C),
      IsDiscreteValuationRing ↑(C.presheaf.stalk ↑y)]
  (hk : IsIntegrallyClosedIn K ↑C.functionField)
  (hg :
    Module.finrank K
        (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology
          (TauCeti.AlgebraicGeometry.InvertibleSheaf.trivial C).obj 1) =
      0)
  {D : TauCeti.AlgebraicGeometry.SchemeWeilDivisor C}
  (hD :
    (TauCeti.AlgebraicGeometry.SchemeWeilDivisor.relativeDegree (C ↘ AlgebraicGeometry.Spec ↧K)) D =
      1) :
  TauCeti.HasNodalReduction R K C (C ↘ AlgebraicGeometry.Spec ↧K)
Lean

Formalized in Tau Ceti as TauCeti.HasNodalReduction.of_genus_eq_zero_of_divisor_degree_eq_one.

Sources
LeanTauCeti.HasNodalReduction.of_genus_eq_zero_of_divisor_degree_eq_one
Uses 6
Statement usesTauCeti.AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne
Proof usesKrull–Akizuki for Mathlib's integralClosure · Riemann's theorem · The Riemann–Roch theorem (Stichtenoth, Theorem 1.5.15), for the divisor (ω) itself · TauCeti.Ring.IsJapanese · The weak approximation theorem

TheoremAlgebraicGeometry.Scheme.exists_split_singularLocus#

All nodes of a proper nodal curve split over one finite separable field extension. For any chosen base change of the curve, its singular subscheme is the spectrum of a product of copies of the extended field, as a scheme over that field. This includes the smooth case, in which the node set is empty.

AlgebraicGeometry.Scheme.exists_split_singularLocus.{u} {K : Type u} [Field K]
  (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧K)]
  [AlgebraicGeometry.IsProper (X ↘ AlgebraicGeometry.Spec ↧K)]
  (hnodal :
    TauCeti.AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne (X ↘ AlgebraicGeometry.Spec ↧K)) :
  ∃ L x x_1,
    ∃ (_ : Module.Finite K L) (_ : Algebra.IsSeparable K L),
      ∃ n,
        ∀ (X' : AlgebraicGeometry.Scheme) (x_4 : X'.Over (AlgebraicGeometry.Spec ↧L)) (g : X' ⟶ X)
          (H :
            CategoryTheory.IsPullback g (X' ↘ AlgebraicGeometry.Spec ↧L)
              (X ↘ AlgebraicGeometry.Spec ↧K) (AlgebraicGeometry.Spec.algebraMap K L)),
          Nonempty
            (CategoryTheory.Over.mk
                (CategoryTheory.CategoryStruct.comp
                  (AlgebraicGeometry.Scheme.singularLocus L X').subschemeι
                  (X' ↘ AlgebraicGeometry.Spec ↧L)) ≅
              CategoryTheory.Over.mk (AlgebraicGeometry.Spec.algebraMap L (Fin n → L)))
Lean

Formalized in Tau Ceti as AlgebraicGeometry.Scheme.exists_split_singularLocus.

Sources
LeanAlgebraicGeometry.Scheme.exists_split_singularLocus
Uses 1
Statement usesTauCeti.AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne

TheoremThe universal property of a contraction#

The universal property of a contraction, for a universally closed surjective morphism, such as a proper surjective one, for which 𝒪_Y → c_* 𝒪_X is an isomorphism.

AlgebraicGeometry.Scheme.Hom.existsUnique_comp_eq_of_universallyClosed.{u}
  {X Y Z : AlgebraicGeometry.Scheme} (c : X ⟶ Y)
  (hc : ∀ (U : Y.Opens), CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.app c U)) (h : X ⟶ Z)
  (hh : Function.FactorsThrough ⇑h ⇑c) [AlgebraicGeometry.UniversallyClosed c]
  [AlgebraicGeometry.Surjective c] : ∃! g, CategoryTheory.CategoryStruct.comp c g = h
Lean

Formalized in Tau Ceti as AlgebraicGeometry.Scheme.Hom.existsUnique_comp_eq_of_universallyClosed.

Sources
LeanAlgebraicGeometry.Scheme.Hom.existsUnique_comp_eq_of_universallyClosed

DefinitionTauCeti.AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne#

Being at worst nodal of relative dimension one is the affine-local extension of the scheme-theoretic criterion over spectra.

TauCeti.AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne.{u} :
  CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme
Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne.

Sources
LeanTauCeti.AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne
Used by 2
Used byA curve of genus zero with a divisor of degree one has nodal reduction · AlgebraicGeometry.Scheme.exists_split_singularLocus

TheoremThe relative Proj is proper#

If the graded algebra A is of finite type and its degree-zero part A₀ is finite over X, then Proj_X(A) ⟶ X is proper.

CategoryTheory.CommMon.isProper_relativeProjToBase.{u} {X : AlgebraicGeometry.Scheme}
  {A : CategoryTheory.CommMon (CategoryTheory.GradedObject ℕ X.Modules)}
  [∀ (n : ℕ), SheafOfModules.IsQuasicoherent (A.X n)]
  (h :
    ∀ (U : X.Opens),
      AlgebraicGeometry.IsAffineOpen U →
        Algebra.FiniteType (↑(X.presheaf.obj (Opposite.op U)))
          (DirectSum ℕ fun n => ↑((A.X n).presheaf.obj (Opposite.op U))))
  (h₀ :
    ∀ (U : X.Opens),
      AlgebraicGeometry.IsAffineOpen U →
        Module.Finite ↑(X.presheaf.obj (Opposite.op U)) ↑((A.X 0).presheaf.obj (Opposite.op U))) :
  AlgebraicGeometry.IsProper A.relativeProjToBase
Lean

Formalized in Tau Ceti as CategoryTheory.CommMon.isProper_relativeProjToBase.

Sources
LeanCategoryTheory.CommMon.isProper_relativeProjToBase

TheoremStabilization terminates#

In the stable range 2g - 2 + n > 0, iterating stabilization steps from any graph reaches a stable graph, of the same arithmetic genus by TauCeti.DualGraph.arithmeticGenus_eq_of_reflTransGen. Termination holds because every step removes a vertex.

TauCeti.DualGraph.exists_reflTransGen_stabilizationStep_isStable.{u, v} {ι : Type v}
  (G : TauCeti.DualGraph ι) [Fintype ι]
  (hrange : 0 < 2 * ↑G.arithmeticGenus - 2 + ↑(Fintype.card ι)) :
  ∃ H, Relation.ReflTransGen TauCeti.DualGraph.StabilizationStep G H ∧ H.IsStable
Lean

Formalized in Tau Ceti as TauCeti.DualGraph.exists_reflTransGen_stabilizationStep_isStable.

Sources
LeanTauCeti.DualGraph.exists_reflTransGen_stabilizationStep_isStable

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.