55.14 Semistable reduction to 55.18 Semistable reduction for…

Section55.14 Semistable reduction#

Section 55.14 of the Stacks Project, Tag 0CDB. 8 tags here are carried by 29 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0CDC, an example

Tag 0CDC in the Stacks Project.

Stacks.nodalModel, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/StandardNodalModel.lean, line 106. The attribute's comment: “the scheme X = Spec A of the family A = R[x, y]/(xy - πⁿ)”.

The standard nodal model X = Spec R[x, y]/(xy - πⁿ) of exponent n, an affine scheme over S = Spec R.

public def nodalModel (R : Type u) [CommRing R] (π : R) (n : ℕ) : Scheme.{u}

Stacks.nodalModelHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/StandardNodalModel.lean, line 112. The attribute's comment: “the morphism X ⟶ S = Spec R induced by R → A = R[x, y]/(xy - πⁿ)”.

The structure morphism X ⟶ S = Spec R of the standard nodal model, the morphism of schemes induced by the ring map R → A = R[x, y]/(xy - πⁿ).

public def nodalModelHom (R : Type u) [CommRing R] (π : R) (n : ℕ) :
    nodalModel R π n ⟶ Spec (CommRingCat.of R)

Stacks.smooth_nodalModelHom_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/StandardNodalModel.lean, line 121. The attribute's comment: “if n = 0 then X → S is smooth”.

The exponent zero model is smooth over the base. For n = 0 the defining relation reads xy = 1, and X ⟶ S is smooth; no hypothesis on R or π is needed.

public theorem smooth_nodalModelHom_zero (π : R) : Smooth (nodalModelHom R π 0)

Stacks.span_nodalGen_eq_nodalModelOrigin_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/StandardNodalModel.lean, line 187. The attribute's comment: “if n = 1 then (x, y) generate the maximal ideal 𝔪 = (π, x, y)”.

At exponent one the two coordinates generate the maximal ideal of the origin. The defining relation reads π = xy, so the uniformizer already lies in (x, y) and 𝔪 = (π, x, y) = (x, y).

public theorem span_nodalGen_eq_nodalModelOrigin_one (π : R) :
    Ideal.span {nodalGen R (π ^ 1) 0, nodalGen R (π ^ 1) 1} = nodalModelOrigin R π 1

Stacks.span_nodalGen_lt_nodalModelOrigin_of_two_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/StandardNodalModel.lean, line 226. The attribute's comment: “if n > 1 then (x, y) no longer generate the maximal ideal 𝔪 = (π, x, y)”.

For exponent at least two the two coordinates no longer generate the maximal ideal of the origin. The ideal (x, y) of R[x, y]/(xy - πⁿ) is strictly smaller than 𝔪 = (π, x, y).

public theorem span_nodalGen_lt_nodalModelOrigin_of_two_le [IsDomain R] {π : R}
    (hπ : Irreducible π) {n : ℕ} (hn : 2 ≤ n) :
    Ideal.span {nodalGen R (π ^ n) 0, nodalGen R (π ^ n) 1} < nodalModelOrigin R π n

Stacks.isAtWorstNodalOfRelativeDimensionOne_nodalModelHom_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/StandardNodalModel.lean, line 313. The attribute's comment: “the exponent zero member of the family is at-worst-nodal of relative dimension one”.

The exponent zero model is at-worst-nodal of relative dimension one over the base. It is smooth of relative dimension one, and a smooth family of curves has empty relative singular subscheme.

public theorem isAtWorstNodalOfRelativeDimensionOne_nodalModelHom_zero (π : R) :
    IsAtWorstNodalOfRelativeDimensionOne (nodalModelHom R π 0)

Stacks.isAtWorstNodalOfRelativeDimensionOne_nodalModelHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/StandardNodalModel.lean, line 323. The attribute's comment: “for all n the morphism X → S is at-worst-nodal of relative dimension 1”.

Every member of the family is at-worst-nodal of relative dimension one over the base. For every exponent n the morphism X = Spec R[x, y]/(xy - πⁿ) ⟶ S = Spec R is syntomic of relative dimension one and its relative singular subscheme, cut out by the two coordinates, is unramified over S. No hypothesis on R or π is needed.

public theorem isAtWorstNodalOfRelativeDimensionOne_nodalModelHom (π : R) (n : ℕ) :
    IsAtWorstNodalOfRelativeDimensionOne (nodalModelHom R π n)

Stacks.isRegular_nodalModel_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/StandardNodalModel.lean, line 336. The attribute's comment: “if n = 1 then X is regular”. References: SGA 7 XVI (1.13), “Case 1, special case”.

The exponent one model is regular. For π a uniformizer of a discrete valuation ring the scheme Spec R[x, y]/(xy - π) is regular.

public theorem isRegular_nodalModel_one {π : R} (hπ : Irreducible π) :
    IsRegular (nodalModel R π 1)

Stacks.not_isRegular_nodalModel_of_one_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/StandardNodalModel.lean, line 343. The attribute's comment: “if n > 1 then X is not regular”.

A model of exponent greater than one is not regular. It is singular at the origin (π, x, y), where the two coordinates no longer span the maximal ideal.

public theorem not_isRegular_nodalModel_of_one_lt {π : R} (hπ : Irreducible π) {n : ℕ}
    (hn : 1 < n) : ¬ IsRegular (nodalModel R π n)

Stacks.nodalModelBlowup, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/StandardNodalModelBlowup.lean, line 157. The attribute's comment: “to ameliorate the situation in case n > 1 we consider the blowup b : X' → X of X in 𝔪: the scheme X'”.

The blowup X' of the standard nodal model X = Spec R[x, y]/(xy - πⁿ) in the ideal 𝔪 = (π, x, y) of its singular point. It is the Proj of the Rees algebra of 𝔪; that this is the blowup of the scheme X in the ideal sheaf attached to 𝔪 is Stacks.Blowup.nonempty_over_iso_blowUpToBase.

public def nodalModelBlowup (R : Type u) [CommRing R] (π : R) (n : ℕ) : Scheme.{u}

Stacks.nodalModelBlowupHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/StandardNodalModelBlowup.lean, line 163. The attribute's comment: “to ameliorate the situation in case n > 1 we consider the blowup b : X' → X of X in 𝔪: the morphism b”.

The blowup morphism b : X' ⟶ X of the standard nodal model in 𝔪 = (π, x, y).

public def nodalModelBlowupHom (R : Type u) [CommRing R] (π : R) (n : ℕ) :
    nodalModelBlowup R π n ⟶ nodalModel R π n

Stacks.iSup_opensRange_nodalModelBlowupChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/StandardNodalModelBlowup.lean, line 190. The attribute's comment: “by construction X' is covered by three affine pieces corresponding to the blowup algebras A[𝔪/π], A[𝔪/x] and A[𝔪/y]”.

By construction X' is covered by three affine pieces, the spectra of the blowup algebras A[𝔪/π], A[𝔪/x] and A[𝔪/y].

public theorem iSup_opensRange_nodalModelBlowupChart (π : R) (n : ℕ) :
    ⨆ i, (nodalModelBlowupChart R π n i).opensRange = ⊤

Stacks.isAtWorstNodalOfRelativeDimensionOne_nodalModelBlowupToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/StandardNodalModelBlowup.lean, line 390. The attribute's comment: “thus we see that X' → S is at-worst-nodal of relative dimension 1”.

X' ⟶ S is at-worst-nodal of relative dimension one. The three charts cover X', an open immersion is étale, and over S each chart is a standard nodal model: the central one with parameter π^(n-2), the two outer ones with parameter π.

public theorem isAtWorstNodalOfRelativeDimensionOne_nodalModelBlowupToBase
    (hπ : π ≠ 0) (hn : 2 ≤ n) :
    IsAtWorstNodalOfRelativeDimensionOne (nodalModelBlowupToBase R π n)

Stacks.exists_isOpenImmersion_nodalModel_sub_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/StandardNodalModelBlowup.lean, line 443. The attribute's comment: “X' is regular, except for one point which has an affine open neighbourhood exactly as above but with n replaced by n - 2: that neighbourhood, as the standard nodal model of exponent n - 2 over S”.

The one point at which X' can fail to be regular has an affine open neighbourhood exactly as the original situation, with n replaced by n - 2. The central chart A[𝔪/π] is an affine open of X' which, over S, is the standard nodal model of exponent n - 2; the two outer charts are regular by Stacks.isRegular_spec_nodalXChart and Stacks.isRegular_spec_nodalYChart.

public theorem exists_isOpenImmersion_nodalModel_sub_two (hπ : π ≠ 0) (hn : 2 ≤ n) :
    ∃ j : nodalModel R π (n - 2) ⟶ nodalModelBlowup R π n,
      IsOpenImmersion j ∧ j ≫ nodalModelBlowupToBase R π n = nodalModelHom R π (n - 2) ∧
        Set.range j.base = Set.range (nodalModelBlowupChart R π n 0).base

Stacks.isRegular_nodalModelBlowup_of_le_three, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/StandardNodalModelBlowup.lean, line 516. The attribute's comment: “using induction on n: for 2 ≤ n ≤ 3 the sequence of blowing ups in closed points X_{⌊n/2⌋} → … → X₁ → X₀ = X is the single blowup b : X' → X, and X_{⌊n/2⌋} = X' is regular”.

For 2 ≤ n ≤ 3 the single blowup already resolves the singularity: X' is regular. The exponent drop n ↦ n - 2 of the central chart lands on 0 or 1, where the standard nodal model is regular, and the two outer charts are regular for every n ≥ 2. Since ⌊n/2⌋ = 1 for these n, the chain of blowing ups in closed points of [Stacks, Tag 0CDC] is here the single blowup b : X' ⟶ X, and X' ⟶ S is at-worst-nodal of relative dimension one by Stacks.isAtWorstNodalOfRelativeDimensionOne_nodalModelBlowupToBase.

public theorem isRegular_nodalModelBlowup_of_le_three {π : R} (hπ : Irreducible π) {n : ℕ}
    (h2 : 2 ≤ n) (h3 : n ≤ 3) : IsRegular (nodalModelBlowup R π n)

Stacks.exists_pointBlowupChainOfLength_nodalModel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/StandardNodalModelResolution.lean, line 330. The attribute's comment: “using induction on n we conclude that there is a sequence of blowing ups in closed points X_{⌊n/2⌋} → … → X₁ → X₀ = X such that X_{⌊n/2⌋} → S is at-worst-nodal of relative dimension 1 and X_{⌊n/2⌋} is regular”.

Stacks Project, Tag 0CDC. Using induction on n there is a sequence of blowups at closed points 

X_{⌊n/2⌋} → … → X₁ → X₀ = X
of the standard nodal model X = Spec R[x, y]/(xy - πⁿ) over S = Spec R such that X_{⌊n/2⌋} → S is at-worst-nodal of relative dimension one and X_{⌊n/2⌋} is regular.

public theorem exists_pointBlowupChainOfLength_nodalModel {π : R} (hπ : Irreducible π) (n : ℕ) :
    ∃ (Y : Scheme.{u}) (g : Y ⟶ nodalModel R π n),
      PointBlowupChainOfLength (nodalModel R π n) Set.univ (n / 2) Y g ∧
      IsAtWorstNodalOfRelativeDimensionOne (g ≫ nodalModelHom R π n) ∧ IsRegular Y

Stacks.nodalXChart_equiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NodalChart/Blowup.lean, line 386. The attribute's comment: “the algebra A[𝔪/x] has generators x, u = π/x subject to the relation xu - π”.

The x-chart of the blowup of the standard nodal model. For n ≥ 2 the affine blowup algebra A[𝔪/x] of A = R[x, y]/(xy - πⁿ) at x, where 𝔪 = (π, x, y), is R[x, u]/(xu - π), the identification carrying x to x and y to u·π^(n-1).

public theorem nodalXChart_equiv [IsDomain R] [UniqueFactorizationMonoid R]
    (hπ : π ≠ 0) (hn : 2 ≤ n) :
    ∃ e : ↥(nodalXChart π n S) ≃+* nodalChartRing R π,
      (∀ r : R, e (algebraMap (nodalChartRing R (π ^ n)) ↥(nodalXChart π n S)
          (algebraMap R (nodalChartRing R (π ^ n)) r))
        = algebraMap R (nodalChartRing R π) r) ∧
      e (algebraMap (nodalChartRing R (π ^ n)) ↥(nodalXChart π n S) (nodalGen R (π ^ n) 0))
        = nodalGen R π 0 ∧
      e (algebraMap (nodalChartRing R (π ^ n)) ↥(nodalXChart π n S) (nodalGen R (π ^ n) 1))
        = nodalGen R π 1 * algebraMap R (nodalChartRing R π) (π ^ (n - 1))

Stacks.nodalCentralChart_equiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NodalChart/Blowup.lean, line 585. The attribute's comment: “the algebra A[𝔪/π] has generators x' = x/π and y' = y/π with x'y' = π^(n-2), so this part of X' is the spectrum of R[x', y']/(x'y' - π^(n-2))”.

The central chart of the blowup of the standard nodal model, and the drop n ↦ n - 2. For n ≥ 2 the affine blowup algebra A[𝔪/π] of A = R[x, y]/(xy - πⁿ) at π, where 𝔪 = (π, x, y), is again a standard nodal model, with the exponent lowered by two: R[x', y']/(x'y' - π^(n-2)), the identification carrying x to πx' and y to πy'.

public theorem nodalCentralChart_equiv [IsDomain R] [UniqueFactorizationMonoid R]
    (hπ : π ≠ 0) (hn : 2 ≤ n) :
    ∃ e : ↥(nodalCentralChart π n S) ≃+* nodalChartRing R (π ^ (n - 2)),
      (∀ r : R, e (algebraMap (nodalChartRing R (π ^ n)) ↥(nodalCentralChart π n S)
          (algebraMap R (nodalChartRing R (π ^ n)) r))
        = algebraMap R (nodalChartRing R (π ^ (n - 2))) r) ∧
      (∀ i : Fin 2,
        e (algebraMap (nodalChartRing R (π ^ n)) ↥(nodalCentralChart π n S)
            (nodalGen R (π ^ n) i))
          = algebraMap R (nodalChartRing R (π ^ (n - 2))) π *
              nodalGen R (π ^ (n - 2)) i)

Stacks.nodalYChart_equiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NodalChart/Blowup.lean, line 771. The attribute's comment: “by symmetry the case of the algebra A[𝔪/y] is the same as the case of A[𝔪/x]”.

The y-chart of the blowup of the standard nodal model. For n ≥ 2 the affine blowup algebra A[𝔪/y] of A = R[x, y]/(xy - πⁿ) at y, where 𝔪 = (π, x, y), is R[y, v]/(yv - π), the identification carrying y to y and x to v·π^(n-1).

public theorem nodalYChart_equiv [IsDomain R] [UniqueFactorizationMonoid R]
    (hπ : π ≠ 0) (hn : 2 ≤ n) :
    ∃ e : ↥(nodalYChart π n S) ≃+* nodalChartRing R π,
      (∀ r : R, e (algebraMap (nodalChartRing R (π ^ n)) ↥(nodalYChart π n S)
          (algebraMap R (nodalChartRing R (π ^ n)) r))
        = algebraMap R (nodalChartRing R π) r) ∧
      e (algebraMap (nodalChartRing R (π ^ n)) ↥(nodalYChart π n S) (nodalGen R (π ^ n) 1))
        = nodalGen R π 0 ∧
      e (algebraMap (nodalChartRing R (π ^ n)) ↥(nodalYChart π n S) (nodalGen R (π ^ n) 0))
        = nodalGen R π 1 * algebraMap R (nodalChartRing R π) (π ^ (n - 1))

Stacks.isRegular_spec_nodalXChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NodalChart/Regularity.lean, line 555. The attribute's comment: “the x-chart of X' is regular”.

The x-chart of the blowup of the standard nodal model is regular. It is the exponent one model R[x, u]/(xu - π), by Stacks.nodalXChart_equiv.

public theorem isRegular_spec_nodalXChart {π : R} (hπ : Irreducible π) {n : ℕ} (hn : 2 ≤ n)
    (S : Type u) [CommRing S] [Algebra (nodalChartRing R (π ^ n)) S]
    [IsLocalization.Away (nodalGen R (π ^ n) 0) S] [Algebra R S]
    [IsScalarTower R (nodalChartRing R (π ^ n)) S] :
    IsRegular (Spec (CommRingCat.of ↥(nodalXChart π n S)))

Stacks.isRegular_spec_nodalYChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NodalChart/Regularity.lean, line 565. The attribute's comment: “the y-chart of X' is regular”.

The y-chart of the blowup of the standard nodal model is regular.

public theorem isRegular_spec_nodalYChart {π : R} (hπ : Irreducible π) {n : ℕ} (hn : 2 ≤ n)
    (S : Type u) [CommRing S] [Algebra (nodalChartRing R (π ^ n)) S]
    [IsLocalization.Away (nodalGen R (π ^ n) 1) S] [Algebra R S]
    [IsScalarTower R (nodalChartRing R (π ^ n)) S] :
    IsRegular (Spec (CommRingCat.of ↥(nodalYChart π n S)))
Tag 0CDD, a lemma

Tag 0CDD in the Stacks Project.

Stacks.Models.exists_etale_nodalChart_pow_uniformizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/Models/SemistableNodalChart.lean, line 453. The attribute's comment: “the TRANSLATION STEP ONLY, with the etale local structure carried as a hypothesis. CARRIED HYPOTHESES, each inherited and not discharged here: hCBY : Stacks.NodalEtaleLocalStructure.NodalChartNeighbourhood f x is the EXISTENCE half of [Stacks, Tag 0CBY] -- an etale neighbourhood U of x, an affine etale neighbourhood Spec B of its image, a parameter h of B and an etale U -> Spec B[x,y]/(xy-h) over Spec B -- which is the CHART form of the tag and is still not proved in this repository. [Stacks, Tag 0CBY] ITSELF IS PROVED: Stacks.NodalEtaleLocalStructure.nonempty_standardNodalDiagram_of_isAtWorstNodal at StacksFrontier/AlgebraicGeometry/Curves/NodalEtaleLocalStructureAssembly.lean proves the tag's own statement, with no hypothesis beyond the tag's, in the DIAGRAM form Stacks.NodalEtaleLocalStructure.StandardNodalDiagram -- etale U -> X, etale V -> S, etale U -> W and a cartesian square presenting W as a base change of the standard nodal family. What separates that from hCBY is not the existence but the PACKAGING: the chart form asks for the base V to be AFFINE, say Spec B, and for an actual parameter h in B, so passing from the diagram to the chart means shrinking V to an affine open and reading the local model off Stacks.NodalEtaleLocalStructure.chartIsoOfIsPullback, which is a step nobody has taken. _hf : IsAtWorstNodalOfRelativeDimensionOne f is the tag's own hypothesis; it appears in the statement for faithfulness but is NOT consumed, because the whole use of nodality in the source proof is to produce hCBY. WHAT IS PROVED HERE, and is exactly what the source calls the translation: the affine etale base Spec B is shrunk to a discrete valuation ring R' with R -> R' etale and R ⊆ R' an extension of discrete valuation rings in the sense of [Stacks, Tag 09E4] (exists_isDiscreteValuationRing_localizationAtPrime_of_etale, the route of [Stacks, Tag 0AP2]); the chart is base changed along B -> R' and is again a nodal chart (isPullback_specMap_nodalChartMap); and the resulting parameter is normalised to 0 or a power of a uniformizer by rescaling a coordinate by a unit (exists_pow_irreducible_nodalChartRing_algEquiv). The SMOOTH case of the source proof, which routes through [Stacks, Tag 054L] instead of 0CBY, is not covered by this statement: see the module documentation”.

Stacks 0CDD. Let R be a discrete valuation ring, let f : X ⟶ Spec R be at-worst-nodal of relative dimension one, and let x be a point of the special fibre. Then there is an étale extension R ⊆ R' of discrete valuation rings, a scheme U with étale morphisms U ⟶ X and U ⟶ Spec A over Spec R', and a point x' of U above x, with

A = R'[u, v]/(uv) or A = R'[u, v]/(uv - π ^ n)

for a uniformizer π of R' and n ≥ 0; the two cases are the vanishing and the nonvanishing of the parameter h, which is a power of a uniformizer in the second case.

The étale local structure in chart form over an arbitrary affine étale base is carried as the hypothesis hCBY; everything else — shrinking that base to a discrete valuation ring and normalising the parameter — is proved here.

public theorem exists_etale_nodalChart_pow_uniformizer
    {R : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of R))
    (_hf : IsAtWorstNodalOfRelativeDimensionOne f)
    (x : X) (hx : f.base x = IsLocalRing.closedPoint R)
    (hCBY : NodalChartNeighbourhood f x) :
    ∃ (R' : Type u) (_ : CommRing R') (_ : IsDomain R')
      (_ : IsDiscreteValuationRing R') (_ : Algebra R R')
      (_ : IsDiscreteValuationRing.IsExtension R R') (_ : Algebra.Etale R R') (h : R'),
      (h = 0 ∨ ∃ (π : R') (n : ℕ), Irreducible π ∧ h = π ^ n) ∧
        ∃ (U : Scheme.{u}) (g : U ⟶ X) (j : U ⟶ Spec (.of (nodalChartRing R' h))) (x' : U),
          Etale g ∧ Etale j ∧ g.base x' = x ∧
            g ≫ f = j ≫
              Spec.map (CommRingCat.ofHom (algebraMap R' (nodalChartRing R' h))) ≫
                Spec.map (CommRingCat.ofHom (algebraMap R R'))

Stacks.Models.exists_etale_nodalChart_pow_uniformizer_of_isAtWorstNodal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/Models/SemistableNodalChartOfNodal.lean, line 313.

Stacks 0CDD. Let R be a discrete valuation ring, let f : X ⟶ Spec R be at-worst-nodal of relative dimension one, and let x be a point of the special fibre. Then there is an étale extension R ⊆ R' of discrete valuation rings, a scheme U with étale morphisms U ⟶ X and U ⟶ Spec A over Spec R', and a point x' of U above x, with

A = R'[u, v]/(uv) or A = R'[u, v]/(uv - π ^ n)

for a uniformizer π of R' and n ≥ 0; the two cases are the vanishing and the nonvanishing of the parameter h, which is a power of a uniformizer in the second case.

The étale local structure in chart form is Stacks.NodalEtaleLocalStructure.nonempty_nodalChartNeighbourhood_of_isAtWorstNodal (Tag 0CBY at a singular point of the fibre, Tag 054L at a smooth one), and the translation into the statement of the tag is Stacks.Models.exists_etale_nodalChart_pow_uniformizer.

public theorem exists_etale_nodalChart_pow_uniformizer_of_isAtWorstNodal
    {R : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of R))
    (hf : IsAtWorstNodalOfRelativeDimensionOne f)
    (x : X) (hx : f.base x = IsLocalRing.closedPoint R) :
    ∃ (R' : Type u) (_ : CommRing R') (_ : IsDomain R')
      (_ : IsDiscreteValuationRing R') (_ : Algebra R R')
      (_ : IsDiscreteValuationRing.IsExtension R R') (_ : Algebra.Etale R R') (h : R'),
      (h = 0 ∨ ∃ (π : R') (n : ℕ), Irreducible π ∧ h = π ^ n) ∧
        ∃ (U : Scheme.{u}) (g : U ⟶ X)
          (j : U ⟶ Spec (.of (nodalChartRing R' h))) (x' : U),
          Etale g ∧ Etale j ∧ g.base x' = x ∧
            g ≫ f = j ≫
              Spec.map (CommRingCat.ofHom (algebraMap R' (nodalChartRing R' h))) ≫
                Spec.map (CommRingCat.ofHom (algebraMap R R'))
Tag 0CDE, a lemma

Tag 0CDE in the Stacks Project.

Stacks.SemistableReduction.exists_nodalBlowupChain_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/NodalResolution.lean, line 542.

Stacks Project, Tag 0CDE. Let R be a discrete valuation ring and let X be a quasi-compact scheme which is at-worst-nodal of relative dimension one over R, with smooth generic fibre. Then there is a finite sequence X_m ⟶ ⋯ ⟶ X_1 ⟶ X_0 = X such that 1. each X_{i+1} ⟶ X_i is the blowing up of X_i in a closed point at which X_i is singular, 2. each X_i ⟶ Spec R is at-worst-nodal of relative dimension one, and 3. X_m is regular.

The sequence is Stacks.SemistableReduction.NodalBlowupChain f Y h with h : Y ⟶ X its composite, which records (1) and (2) at every step, and (3) is IsRegular Y. The generic fibre is the fibre of f over the generic point ⊥ of Spec R.

public theorem exists_nodalBlowupChain_isRegular {X : Scheme.{u}} [CompactSpace X]
    (f : X ⟶ Spec (.of R)) (hf : IsAtWorstNodalOfRelativeDimensionOne f)
    (hsmooth : Smooth (f.fiberToSpecResidueField (⊥ : PrimeSpectrum R))) :
    ∃ (Y : Scheme.{u}) (h : Y ⟶ X), NodalBlowupChain f Y h ∧ IsRegular Y
Tag 0CDF, a lemma

Tag 0CDF in the Stacks Project.

AlgebraicGeometry.isAtWorstNodalOfRelativeDimensionOne_of_isContractionOfExceptionalCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NodalContraction/Nodal.lean, line 50.

Stacks Project, Tag 0CDF. Let R be a discrete valuation ring and let f : X ⟶ Spec R be at-worst-nodal of relative dimension one. Let b : X ⟶ X' be the contraction of an exceptional curve E ⊆ X of the first kind, presented by its ideal sheaf D and an isomorphism e : 𝐏¹_κ ≅ E. Then X' is at-worst-nodal of relative dimension one over R: there is a morphism f' : X' ⟶ Spec R with b ≫ f' = f, and it is at-worst-nodal of relative dimension one.

Away from the contracted point b is an isomorphism, so the only issue is a neighbourhood of that point. The closed fibre of f is reduced, so the uniformizer of R vanishes to order one along E and therefore lies in the maximal ideal at the contracted point but not in its square. The local ring there being regular of dimension two, the local ring of the closed fibre is regular of dimension one; its residue field is geometrically reduced over the residue field of R because the closed fibre of f is. Hence the closed fibre of f' is smooth at the contracted point, and with flatness so is f'; a morphism smooth of relative dimension one is at-worst-nodal of relative dimension one.

public theorem isAtWorstNodalOfRelativeDimensionOne_of_isContractionOfExceptionalCurve
    {R : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    {X X' : Scheme.{u}} (D : X.IdealSheafData) (κ : Type u) [Field κ]
    (e : projectiveLineProj κ ≅ D.subscheme)
    (hE : D.IsExceptionalCurveOfFirstKind κ e)
    (b : X ⟶ X') (hb : IsContractionOfExceptionalCurve D b)
    (f : X ⟶ Spec (CommRingCat.of R))
    (hf : IsAtWorstNodalOfRelativeDimensionOne f) :
    ∃ f' : X' ⟶ Spec (CommRingCat.of R),
      b ≫ f' = f ∧ IsAtWorstNodalOfRelativeDimensionOne f'
Tag 0CDG, a lemma

Tag 0CDG in the Stacks Project.

Stacks.Models.tfae_hasSemistableReduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/Models/SemistableReduction/ReductionTypes.lean, line 139.

Stacks Project, Tag 0CDG. Let R be a discrete valuation ring with fraction field K and let C be a smooth projective curve over K with H⁰(C, 𝒪_C) = K. The following are equivalent: 1. there exists a proper model of C which is at-worst-nodal of relative dimension one over R, 2. there exists a minimal model of C which is at-worst-nodal of relative dimension one over R, and 3. any minimal model of C is at-worst-nodal of relative dimension one over R.

Condition (1) is the base's Stacks.Models.HasSemistableReduction, the definition of semistable reduction ([Stacks, Tag 0CDH]); minimal models are Stacks.Models.IsMinimalModel ([Stacks, Tag 0C2V]).

public theorem tfae_hasSemistableReduction {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
    [IsCurve K c] [Smooth c] (hc : IsProjective c)
    [IsIso ((Scheme.ΓSpecIso (.of K)).inv ≫ c.appTop)] :
    List.TFAE [HasSemistableReduction R c hc,
      ∃ (X : Scheme.{u}) (p : X ⟶ Spec (.of R))
        (e : C ≅ pullback p (Spec.map (CommRingCat.ofHom (algebraMap R K)))),
        IsMinimalModel c p e ∧ IsAtWorstNodalOfRelativeDimensionOne p,
      ∀ (X : Scheme.{u}) (p : X ⟶ Spec (.of R))
        (e : C ≅ pullback p (Spec.map (CommRingCat.ofHom (algebraMap R K)))),
        IsMinimalModel c p e → IsAtWorstNodalOfRelativeDimensionOne p]
Tag 0CDH, a definition

Tag 0CDH in the Stacks Project.

Stacks.Models.HasSemistableReduction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/Models/Reduction.lean, line 70. The attribute's comment: “existence of a proper model of the curve that is at-worst-nodal of relative dimension one”.

Stacks Project, Tag 0CDH. A smooth projective curve C over the fraction field K of a discrete valuation ring R, with H⁰(C, 𝒪_C) = K, has semistable reduction if there is a proper model X ⟶ Spec R of C which is at-worst-nodal of relative dimension one.

def HasSemistableReduction {C : Scheme.{u}} (C_to_K : C ⟶ Spec (.of K))
    [IsCurve K C_to_K] [Smooth C_to_K] (_ : IsProjective C_to_K)
    [IsIso ((Scheme.ΓSpecIso (.of K)).inv ≫ C_to_K.appTop)] : Prop
Tag 0CDI, a lemma

Tag 0CDI in the Stacks Project.

Stacks.Models.tfae_hasGoodReduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/Models/SemistableReduction/ReductionTypes.lean, line 170.

Stacks Project, Tag 0CDI. Let R be a discrete valuation ring with fraction field K and let C be a smooth projective curve over K with H⁰(C, 𝒪_C) = K. The following are equivalent: 1. there exists a proper smooth model for C, 2. there exists a minimal model for C which is smooth over R, 3. any minimal model is smooth over R.

Condition (1) is the base's Stacks.Models.HasGoodReduction, the definition of good reduction ([Stacks, Tag 0CDJ]). A smooth proper model is minimal: its special fibre is connected ([Stacks, Tag 0C62]) and smooth, hence irreducible, so its numerical type is minimal ([Stacks, Tag 0CA6]).

public theorem tfae_hasGoodReduction {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
    [IsCurve K c] [Smooth c] (hc : IsProjective c)
    [IsIso ((Scheme.ΓSpecIso (.of K)).inv ≫ c.appTop)] :
    List.TFAE [HasGoodReduction R c hc,
      ∃ (X : Scheme.{u}) (p : X ⟶ Spec (.of R))
        (e : C ≅ pullback p (Spec.map (CommRingCat.ofHom (algebraMap R K)))),
        IsMinimalModel c p e ∧ Smooth p,
      ∀ (X : Scheme.{u}) (p : X ⟶ Spec (.of R))
        (e : C ≅ pullback p (Spec.map (CommRingCat.ofHom (algebraMap R K)))),
        IsMinimalModel c p e → Smooth p]
Tag 0CDJ, a definition

Tag 0CDJ in the Stacks Project.

Stacks.Models.HasGoodReduction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/Models/Reduction.lean, line 81. The attribute's comment: “existence of a proper smooth model of the curve”.

Stacks Project, Tag 0CDJ. A smooth projective curve C over the fraction field K of a discrete valuation ring R, with H⁰(C, 𝒪_C) = K, has good reduction if there is a proper model X ⟶ Spec R of C which is smooth over R.

def HasGoodReduction {C : Scheme.{u}} (C_to_K : C ⟶ Spec (.of K))
    [IsCurve K C_to_K] [Smooth C_to_K] (_ : IsProjective C_to_K)
    [IsIso ((Scheme.ΓSpecIso (.of K)).inv ≫ C_to_K.appTop)] : Prop
Sources
LeanStacks.nodalModel · Stacks.nodalModelHom · Stacks.smooth_nodalModelHom_zero · Stacks.span_nodalGen_eq_nodalModelOrigin_one · Stacks.span_nodalGen_lt_nodalModelOrigin_of_two_le · Stacks.isAtWorstNodalOfRelativeDimensionOne_nodalModelHom_zero · Stacks.isAtWorstNodalOfRelativeDimensionOne_nodalModelHom · Stacks.isRegular_nodalModel_one

Section55.15 Semistable reduction in genus zero#

Section 55.15 of the Stacks Project, Tag 0CDK. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0CDL, an example

Tag 0CDL in the Stacks Project.

Stacks.Models.RealConicModel.realConic_example, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/Models/RealConicExample.lean, line 339.

Stacks Project, Tag 0CDL. Let R = ℝ[[π]] with fraction field K, let X = V(T₁² + T₂² - πT₀²) ⊆ ℙ²_R and let C = V(T₁² + T₂² - πT₀²) ⊆ ℙ²_K be its generic fibre. 1. The base change of X to ℂ[[π]] is the scheme V(T₁T₂ - πT₀²) of [Stacks, Tag 0CA0]. 2. X is regular, and its special fibre is irreducible yet singular. 3. X is a minimal model of C, and the unique one: every minimal model of C is isomorphic to X as a model. 4. C has genus 0 and does not have good reduction over R: an extension of R is needed even in genus 0.

theorem realConic_example :
    IsPullback (splitMap PowerSeries.X (algebraMap (PowerSeries ℝ) (PowerSeries ℂ))
        iPowerSeries_sq two_mul_halfPowerSeries
        (GenusZero.isHomogeneous_conicEquation (PowerSeries.X : PowerSeries ℂ))
        (by rw [algebraMap_powerSeries_X]; rfl) ≫
        PlaneCurveModel.mapMap (equation PowerSeries.X) (isHomogeneous_equation _)
          (algebraMap (PowerSeries ℝ) (PowerSeries ℂ)))
      (GenusZero.conicToSpec (PowerSeries.X : PowerSeries ℂ))
      (toSpec (PowerSeries.X : PowerSeries ℝ))
      (Spec.map (CommRingCat.ofHom (algebraMap (PowerSeries ℝ) (PowerSeries ℂ)))) ∧
    IsRegular (scheme (PowerSeries.X : PowerSeries ℝ)) ∧
    IrreducibleSpace (specialFiber (PowerSeries.X : PowerSeries ℝ)
      (IsLocalRing.ResidueField (PowerSeries ℝ))) ∧
    ¬ IsRegular (specialFiber (PowerSeries.X : PowerSeries ℝ)
      (IsLocalRing.ResidueField (PowerSeries ℝ))) ∧
    IsMinimalModel (toSpec (algebraMap (PowerSeries ℝ) K PowerSeries.X))
      (toSpec (PowerSeries.X : PowerSeries ℝ)) (genericFiberIso K PowerSeries.X) ∧
    (∀ (Y : Scheme.{0}) (pY : Y ⟶ Spec (.of (PowerSeries ℝ)))
      (eY : scheme (algebraMap (PowerSeries ℝ) K PowerSeries.X) ≅
        pullback pY (Spec.map (CommRingCat.ofHom (algebraMap (PowerSeries ℝ) K)))),
      IsMinimalModel (toSpec (algebraMap (PowerSeries ℝ) K PowerSeries.X)) pY eY →
        ∃ φ : scheme (PowerSeries.X : PowerSeries ℝ) ≅ Y,
          φ.hom ≫ pY = toSpec (PowerSeries.X : PowerSeries ℝ) ∧
          (genericFiberIso K PowerSeries.X).hom ≫
              pullback.fst (toSpec (PowerSeries.X : PowerSeries ℝ))
                (Spec.map (CommRingCat.ofHom (algebraMap (PowerSeries ℝ) K))) ≫ φ.hom =
            eY.hom ≫
              pullback.fst pY (Spec.map (CommRingCat.ofHom (algebraMap (PowerSeries ℝ) K)))) ∧
    genus (toSpec (algebraMap (PowerSeries ℝ) K PowerSeries.X)) = 0 ∧
    ¬ HasGoodReduction (PowerSeries ℝ) (toSpec (algebraMap (PowerSeries ℝ) K PowerSeries.X))
      (isProjective_toSpec_powerSeries K)
Sources
LeanStacks.Models.RealConicModel.realConic_example

Section55.16 Semistable reduction in genus one#

Section 55.16 of the Stacks Project, Tag 0CEG. 1 tag here is carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0CEH, an example

Tag 0CEH in the Stacks Project.

Stacks.CyclicCover.finite_flat_pushforward_coverMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/CyclicCover/UnboundedRamification.lean, line 84. The attribute's comment: “p : X → Z_R is finite and flat, and p_O_X = Sym(L_R)/(φ - π) = O ⊕ L_R ⊕ … ⊕ L_R^{⊗ n-1}; X is built from φ : L^{⊗ n} ≅ O_Z through Symⁿ L ≅ L^{⊗ n}”.

p : X ⟶ Z_R is finite flat, with p_* 𝒪_X = ⨁_{i < n} L_R^{⊗ i}, the direct sum of the pullbacks to Z_R of the tensor powers of L.

theorem finite_flat_pushforward_coverMap (hn : 1 ≤ n) :
    IsFinite (coverMap f (symPowTrivialization f φ) (PowerSeries k) PowerSeries.X) ∧
      Flat (coverMap f (symPowTrivialization f φ) (PowerSeries k) PowerSeries.X) ∧
      Nonempty ((⨁ fun i : Fin n => (Scheme.Modules.pullback (baseChangeFst f (PowerSeries k))).obj
          (tensorPow L i)) ≅
        (Scheme.Modules.pushforward
          (coverMap f (symPowTrivialization f φ) (PowerSeries k) PowerSeries.X)).obj
          (SheafOfModules.unit _))

Stacks.CyclicCover.nonempty_coverMapArrowIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/CyclicCover/UnboundedRamification.lean, line 106. The attribute's comment: “p⁻¹(U_R) = Spec((A ⊗_k R)[x]/(xⁿ - π f)) for U = Spec A trivializing L by s, with f = φ(s^{⊗ n}) a unit”.

The local description of p: over an affine open U = Spec A of Z on which L is trivialized by s, with f = φ(s^{⊗ n}) a unit of A, p⁻¹(U_R) = Spec (A ⊗_k R)[x]/(xⁿ - π f) over U_R = Spec (A ⊗_k R).

theorem nonempty_coverMapArrowIso (U : Z.affineOpens)
    (b : Module.Basis PUnit.{u + 1} Γ(Z, U.1) Γ(L, U.1)) :
    letI := (sectionsStructure f U.1).hom.toAlgebra
    let fU : Γ(Z, U.1) := φ.hom.app U.1 ((symPowIsoTensorPower f L n).hom.app U.1 (basisPow f U b))
    IsUnit fU ∧
      Nonempty (Arrow.mk (coverMap f (symPowTrivialization f φ) (PowerSeries k)
          PowerSeries.X ∣_ baseChangeOpen f (PowerSeries k) U.1) ≅
        Arrow.mk (Spec.map (CommRingCat.ofHom (algebraMap (Γ(Z, U.1) ⊗[k] PowerSeries k)
          (chartRing k n fU (PowerSeries.X : PowerSeries k))))))

Stacks.CyclicCover.finite_etale_genericFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/CyclicCover/UnboundedRamification.lean, line 123. The attribute's comment: “the morphism X_K → Z_K of generic fibres is finite étale”.

The morphism of generic fibres X_K ⟶ Z_K is finite étale.

theorem finite_etale_genericFibre (hnk : IsUnit (n : k)) :
    IsFinite (coverMapBaseChange f (symPowTrivialization f φ) (PowerSeries.X : PowerSeries k)
        (powerSeriesToLaurent k)) ∧
      Etale (coverMapBaseChange f (symPowTrivialization f φ) (PowerSeries.X : PowerSeries k)
        (powerSeriesToLaurent k))

Stacks.CyclicCover.globalSections_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/CyclicCover/UnboundedRamification.lean, line 172. The attribute's comment: “H^0(X, O_X) = R and H^0(X_K, O_{X_K}) = K”.

H⁰(X, 𝒪_X) = R and H⁰(X_K, 𝒪_{X_K}) = K.

theorem globalSections_cover (hn : 1 ≤ n)
    (hord : addOrderOf
      (Stacks.SheafOfModules.picardClass Z.presheaf (structureIsSheaf Z.toRingedSpace) L ‹_›) = n) :
    Function.Bijective
        (coverSnd f (symPowTrivialization f φ) (PowerSeries k) PowerSeries.X).appTop ∧
      Function.Bijective (pullback.snd
        (coverSnd f (symPowTrivialization f φ) (PowerSeries k) PowerSeries.X)
        (Spec.map (CommRingCat.ofHom (powerSeriesToLaurent k).toRingHom))).appTop

Stacks.CyclicCover.genus_genericFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/CyclicCover/UnboundedRamification.lean, line 185. The attribute's comment: “the genus of X_K is n(g - 1) + 1, in particular 1 if Z has genus 1”.

The genus of X_K is n(g - 1) + 1; in particular it is 1 when Z has genus 1.

theorem genus_genericFibre (hn : 1 ≤ n)
    (hord : addOrderOf
      (Stacks.SheafOfModules.picardClass Z.presheaf (structureIsSheaf Z.toRingedSpace) L ‹_›) = n) :
    (genus (pullback.snd
        (coverSnd f (symPowTrivialization f φ) (PowerSeries k) PowerSeries.X)
        (Spec.map (CommRingCat.ofHom (powerSeriesToLaurent k).toRingHom))) : ℤ) =
        n * (genus f - 1) + 1 ∧
      (genus f = 1 → genus (pullback.snd
        (coverSnd f (symPowTrivialization f φ) (PowerSeries k) PowerSeries.X)
        (Spec.map (CommRingCat.ofHom (powerSeriesToLaurent k).toRingHom))) = 1)

Stacks.CyclicCover.isRegular_model, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/CyclicCover/UnboundedRamification.lean, line 204. The attribute's comment: “the scheme X is regular”.

The scheme X is regular.

theorem isRegular_model [Smooth f] (hnk : IsUnit (n : k)) :
    IsRegular (cover f (symPowTrivialization f φ) (PowerSeries k) PowerSeries.X)

Stacks.CyclicCover.specialFibre_eq_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/CyclicCover/UnboundedRamification.lean, line 212. The attribute's comment: “the special fibre X_k is n times the reduced special fibre (X_k)_red as an effective Cartier divisor”.

The special fibre X_k is n times the reduced special fibre as an effective Cartier divisor: π 𝒪_X and its radical are invertible ideals, and π 𝒪_X = (rad(π 𝒪_X))ⁿ.

theorem specialFibre_eq_pow [Smooth f] (hnk : IsUnit (n : k)) :
    Stacks.Divisors.IsEffectiveCartierDivisor (specialFibreIdeal f (symPowTrivialization f φ)) ∧
      Stacks.Divisors.IsEffectiveCartierDivisor
        (specialFibreIdeal f (symPowTrivialization f φ)).radical ∧
      specialFibreIdeal f (symPowTrivialization f φ) =
        (specialFibreIdeal f (symPowTrivialization f φ)).radical ^ n

Stacks.CyclicCover.ramification_of_semistable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/CyclicCover/UnboundedRamification.lean, line 229. The attribute's comment: “any finite extension K'/K over which X_K attains semistable reduction has ramification index at least n: v_{R'}(π) is a positive multiple of n, for R' the integral closure of R in K'”.

Any finite extension K'/K over which X_K attains semistable reduction has ramification index at least n: the valuation v_{R'}(π) of π in the integral closure R' of R in K' is a positive multiple of n.

theorem ramification_of_semistable [IsAlgClosed k] [IsProper f] [Nonempty Z] (hn : 1 ≤ n)
    (K' : Type u) [Field K'] [Algebra (LaurentSeries k) K']
    [FiniteDimensional (LaurentSeries k) K'] [Algebra (PowerSeries k) K']
    [IsScalarTower (PowerSeries k) (LaurentSeries k) K'] :
    haveI := isDiscreteValuationRing_integralClosure (PowerSeries k) (LaurentSeries k) K'
    haveI := _root_.isFractionRing_integralClosure (PowerSeries k) (LaurentSeries k) K'
    (∃ (Y : Scheme.{u}) (q : Y ⟶ Spec (.of (integralClosure (PowerSeries k) K')))
      (e : pullback (coverSnd f (symPowTrivialization f φ) (PowerSeries k) PowerSeries.X)
          (Spec.map (CommRingCat.ofHom (algebraMap (PowerSeries k) K'))) ≅
        pullback q (Spec.map (CommRingCat.ofHom
          (algebraMap (integralClosure (PowerSeries k) K') K')))),
      Stacks.Models.IsModel (pullback.snd _ _) q e ∧ IsProper q ∧
        IsAtWorstNodalOfRelativeDimensionOne q) →
    ∃ m : ℕ, 0 < m ∧ IsDiscreteValuationRing.addVal (integralClosure (PowerSeries k) K')
      (algebraMap (PowerSeries k) (integralClosure (PowerSeries k) K') PowerSeries.X) =
        (n * m : ℕ)

Stacks.CyclicCover.no_universal_bound, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/CyclicCover/UnboundedRamification.lean, line 317. The attribute's comment: “there is no universal bound for the degree of an extension over which a genus 1 curve attains semistable reduction: for every B there is a curve X_K over K = k((π)) with H⁰(X_K, O) = K and genus 1 such that every finite K'/K over which X_K attains semistable reduction has [K' : K] > B”.

There is no universal bound on the degree of an extension over which a genus one curve attains semistable reduction. For every B there is a curve X_K over K = k((π)) with H⁰(X_K, 𝒪) = K and genus 1, namely the generic fibre of the cyclic cover of a genus one curve Z by an invertible module of prime order ℓ > B, such that every finite extension K'/K over which X_K attains semistable reduction has [K' : K] > B.

theorem no_universal_bound (k : Type u) [Field k] [IsAlgClosed k] (B : ℕ) :
    ∃ (Z : Scheme.{u}) (f : Z ⟶ Spec (.of k)) (_ : IsCurve k f) (_ : IsProjectiveVariety k f)
      (_ : Smooth f) (L : Z.Modules)
      (_ : SheafOfModules.IsInvertible Z.sheaf.obj Z.ringCatSheaf.property L) (n : ℕ)
      (φ : tensorPow L n ≅ SheafOfModules.unit Z.ringCatSheaf),
      genus (pullback.snd (coverSnd f (symPowTrivialization f φ) (PowerSeries k) PowerSeries.X)
        (Spec.map (CommRingCat.ofHom (powerSeriesToLaurent k).toRingHom))) = 1 ∧
      Function.Bijective (pullback.snd (coverSnd f (symPowTrivialization f φ) (PowerSeries k)
        PowerSeries.X) (Spec.map (CommRingCat.ofHom (powerSeriesToLaurent k).toRingHom))).appTop ∧
      ∀ (K' : Type u) [Field K'] [Algebra (LaurentSeries k) K']
        [FiniteDimensional (LaurentSeries k) K'] [Algebra (PowerSeries k) K']
        [IsScalarTower (PowerSeries k) (LaurentSeries k) K'],
        haveI := isDiscreteValuationRing_integralClosure (PowerSeries k) (LaurentSeries k) K'
        haveI := _root_.isFractionRing_integralClosure (PowerSeries k) (LaurentSeries k) K'
        (∃ (Y : Scheme.{u}) (q : Y ⟶ Spec (.of (integralClosure (PowerSeries k) K')))
          (e : pullback (coverSnd f (symPowTrivialization f φ) (PowerSeries k) PowerSeries.X)
              (Spec.map (CommRingCat.ofHom (algebraMap (PowerSeries k) K'))) ≅
            pullback q (Spec.map (CommRingCat.ofHom
              (algebraMap (integralClosure (PowerSeries k) K') K')))),
          Stacks.Models.IsModel (pullback.snd _ _) q e ∧ IsProper q ∧
            IsAtWorstNodalOfRelativeDimensionOne q) →
        B < Module.finrank (LaurentSeries k) K'
Sources
LeanStacks.CyclicCover.finite_flat_pushforward_coverMap · Stacks.CyclicCover.nonempty_coverMapArrowIso · Stacks.CyclicCover.finite_etale_genericFibre · Stacks.CyclicCover.globalSections_cover · Stacks.CyclicCover.genus_genericFibre · Stacks.CyclicCover.isRegular_model · Stacks.CyclicCover.specialFibre_eq_pow · Stacks.CyclicCover.ramification_of_semistable

Section55.18 Semistable reduction for curves#

Section 55.18 of the Stacks Project, Tag 0CDM. 2 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0CEJ, an equation

Tag 0CEJ in the Stacks Project.

AlgebraicGeometry.SemistableReduction.semistableReductionDegreeBound, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/Curves.lean, line 37.

The genus-dependent degree bound used in the semistable reduction theorem. Here ℓ is the second prime strictly greater than 768 * g.

public noncomputable def semistableReductionDegreeBound (g : ℕ) : ℕ
Tag 0CDN, a theorem

Tag 0CDN in the Stacks Project.

Stacks.Models.semistableReduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/Models/SemistableReduction/Unconditional.lean, line 81.

Stacks Project, Tag 0CDN. Let R be a discrete valuation ring with fraction field K and C a smooth projective curve over K with H⁰(C, 𝒪_C) = K. Then there is an extension of discrete valuation rings R ⊆ R' inducing a finite separable extension K'/K of fraction fields such that C_{K'} has semistable reduction over R'. More precisely:

  1. if the genus of C is zero, there is a separable K'/K of degree 2 with C_{K'} ≅ 𝐏¹_{K'}, and C_{K'} is the generic fibre of the smooth projective 𝐏¹_{R'} over the integral closure R' of R in K';
  2. if the genus of C is one, there is a finite separable K'/K such that C_{K'} has semistable reduction over R'_𝔪 for every maximal ideal 𝔪 of the integral closure R' of R in K', and the special fibre of the minimal model of C_{K'} over R'_𝔪 is a smooth genus one curve or a cycle of rational curves;
  3. if the genus g of C is at least two, there is a finite separable K'/K of degree at most B_g such that C_{K'} has semistable reduction over R'_𝔪 for every maximal ideal 𝔪 of the integral closure R' of R in K'.
theorem semistableReduction
    (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K]
    [IsFractionRing R K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K)) [IsCurve K c] [Smooth c]
    (hproj : IsProjective c) [IsIso ((Scheme.ΓSpecIso (.of K)).inv ≫ c.appTop)] :
    haveI : IsProper c := hproj.isProper
    (∃ (K' : Type u) (_ : Field K') (_ : Algebra K K') (_ : Algebra R K')
      (_ : IsScalarTower R K K'), FiniteDimensional K K' ∧ Algebra.IsSeparable K K' ∧
      ∃ (R' : Type u) (_ : CommRing R') (_ : IsDomain R') (_ : IsDiscreteValuationRing R')
        (_ : Algebra R' K') (_ : IsFractionRing R' K') (_ : Algebra R R')
        (_ : IsScalarTower R R' K'), IsLocalHom (algebraMap R R') ∧
        HasSemistableReduction R'
          (pullback.snd c (Spec.map (CommRingCat.ofHom (algebraMap K K'))))
          (hproj.pullback_snd _)) ∧
    (genus c = 0 →
      ∃ (K' : Type u) (_ : Field K') (_ : Algebra K K') (_ : Algebra R K')
        (_ : IsScalarTower R K K'),
        FiniteDimensional K K' ∧ Algebra.IsSeparable K K' ∧ Module.finrank K K' = 2 ∧
        Nonempty (Over.mk (pullback.snd c (Spec.map (CommRingCat.ofHom (algebraMap K K')))) ≅
          Over.mk (projectiveSpaceOver 1 (Spec (.of K')) ↘ Spec (.of K'))) ∧
        IsFractionRing (integralClosure R K') K' ∧
        Smooth (projectiveSpaceOver 1 (Spec (.of (integralClosure R K'))) ↘
          Spec (.of (integralClosure R K'))) ∧
        IsProjective (projectiveSpaceOver 1 (Spec (.of (integralClosure R K'))) ↘
          Spec (.of (integralClosure R K'))) ∧
        Nonempty (Over.mk (pullback.snd c (Spec.map (CommRingCat.ofHom (algebraMap K K')))) ≅
          Over.mk (pullback.snd (C := Scheme.{u})
            (projectiveSpaceOver 1 (Spec (.of (integralClosure R K'))) ↘
              Spec (.of (integralClosure R K')))
            (Spec.map (CommRingCat.ofHom (algebraMap (integralClosure R K') K')))))) ∧
    (genus c = 1 →
      ∃ (K' : Type u) (_ : Field K') (_ : Algebra K K') (_ : Algebra R K')
        (_ : IsScalarTower R K K'), FiniteDimensional K K' ∧ Algebra.IsSeparable K K' ∧
        HasSemistableReductionAtMaximalIdeals R K'
          (pullback.snd c (Spec.map (CommRingCat.ofHom (algebraMap K K'))))
          (hproj.pullback_snd _) ∧
        HasGenusOneMinimalFibresAtMaximalIdeals R K'
          (pullback.snd c (Spec.map (CommRingCat.ofHom (algebraMap K K'))))) ∧
    (2 ≤ genus c →
      ∃ (K' : Type u) (_ : Field K') (_ : Algebra K K') (_ : Algebra R K')
        (_ : IsScalarTower R K K'), FiniteDimensional K K' ∧ Algebra.IsSeparable K K' ∧
        Module.finrank K K' ≤
          AlgebraicGeometry.SemistableReduction.semistableReductionDegreeBound (genus c) ∧
        HasSemistableReductionAtMaximalIdeals R K'
          (pullback.snd c (Spec.map (CommRingCat.ofHom (algebraMap K K'))))
          (hproj.pullback_snd _))

Stacks.Models.exists_genusOne_semistableReduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/Models/SemistableReduction/Unconditional.lean, line 146. The attribute's comment: “(2), genus one”.

Stacks Project, Tag 0CDN (2), genus one. Let R be a discrete valuation ring with fraction field K and C a smooth projective curve of genus one over K with H⁰(C, 𝒪_C) = K. Then there is a finite separable extension K'/K such that C_{K'} has semistable reduction over R'_𝔪 for every maximal ideal 𝔪 of the integral closure R' of R in K', and the special fibre of the minimal model of C_{K'} over R'_𝔪 is a smooth genus one curve or a cycle of rational curves.

theorem exists_genusOne_semistableReduction
    (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K]
    [IsFractionRing R K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K)) [IsCurve K c] [Smooth c]
    (hproj : IsProjective c) [IsIso ((Scheme.ΓSpecIso (.of K)).inv ≫ c.appTop)]
    (hg : genus c = 1) :
    haveI : IsProper c := hproj.isProper
    ∃ (K' : Type u) (_ : Field K') (_ : Algebra K K') (_ : Algebra R K')
      (_ : IsScalarTower R K K'), FiniteDimensional K K' ∧ Algebra.IsSeparable K K' ∧
      HasSemistableReductionAtMaximalIdeals R K'
        (pullback.snd c (Spec.map (CommRingCat.ofHom (algebraMap K K'))))
        (hproj.pullback_snd _) ∧
      HasGenusOneMinimalFibresAtMaximalIdeals R K'
        (pullback.snd c (Spec.map (CommRingCat.ofHom (algebraMap K K'))))

Stacks.Models.exists_hasSemistableReductionAtMaximalIdeals_of_two_le_genus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/Models/SemistableReduction/Unconditional.lean, line 167. The attribute's comment: “(3), genus at least two”.

Stacks Project, Tag 0CDN (3), genus at least two. Let R be a discrete valuation ring with fraction field K and C a smooth projective curve over K with H⁰(C, 𝒪_C) = K, of genus g ≥ 2. Then there is a finite separable extension K'/K of degree at most B_g such that C_{K'} has semistable reduction over R'_𝔪 for every maximal ideal 𝔪 of the integral closure R' of R in K'.

theorem exists_hasSemistableReductionAtMaximalIdeals_of_two_le_genus
    (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K]
    [IsFractionRing R K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K)) [IsCurve K c] [Smooth c]
    (hproj : IsProjective c) [IsIso ((Scheme.ΓSpecIso (.of K)).inv ≫ c.appTop)]
    (hg : 2 ≤ genus c) :
    haveI : IsProper c := hproj.isProper
    ∃ (K' : Type u) (_ : Field K') (_ : Algebra K K') (_ : Algebra R K')
      (_ : IsScalarTower R K K'), FiniteDimensional K K' ∧ Algebra.IsSeparable K K' ∧
      Module.finrank K K' ≤ AlgebraicGeometry.SemistableReduction.semistableReductionDegreeBound
        (genus c) ∧
      HasSemistableReductionAtMaximalIdeals R K'
        (pullback.snd c (Spec.map (CommRingCat.ofHom (algebraMap K K'))))
        (hproj.pullback_snd _)

AlgebraicGeometry.SemistableReduction.genusZero_splitting, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SemistableReduction/GenusZeroSplitting.lean, line 287. The attribute's comment: “(1), genus zero”.

Stacks Project, Tag 0CDN, part (1). Let R be a discrete valuation ring with fraction field K and C a smooth projective curve over K with H⁰(C, 𝒪_C) = K. If the genus of C is zero, then there exists a separable extension K'/K of degree 2 such that C_{K'} ≅ 𝐏¹_{K'}, and hence C_{K'} is isomorphic to the generic fibre of the smooth projective scheme 𝐏¹_{R'} over the integral closure R' of R in K' (whose fraction field is K').

The extension K' is returned with an R-algebra structure compatible with K ⟶ K', the integral closure is integralClosure R K', and the generic fibre is the base change of 𝐏¹_{R'} ⟶ Spec R' along Spec K' ⟶ Spec R'; both isomorphisms are over K'.

theorem genusZero_splitting (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    [Field K] [Algebra R K] [IsFractionRing R K] {C : Scheme.{u}} (c : C ⟶ Spec (.of K))
    [IsCurve K c] [Smooth c] (hc : IsProjective c)
    [IsIso ((Scheme.ΓSpecIso (.of K)).inv ≫ c.appTop)] (hgenus : genus c = 0) :
    ∃ (K' : Type u) (_ : Field K') (_ : Algebra K K') (_ : Algebra R K')
      (_ : IsScalarTower R K K'),
      FiniteDimensional K K' ∧ Algebra.IsSeparable K K' ∧ Module.finrank K K' = 2 ∧
      Nonempty (Over.mk (pullback.snd c (Spec.map (CommRingCat.ofHom (algebraMap K K')))) ≅
        Over.mk (projectiveSpaceOver 1 (Spec (.of K')) ↘ Spec (.of K'))) ∧
      IsFractionRing (integralClosure R K') K' ∧
      Smooth (projectiveSpaceOver 1 (Spec (.of (integralClosure R K'))) ↘
        Spec (.of (integralClosure R K'))) ∧
      IsProjective (projectiveSpaceOver 1 (Spec (.of (integralClosure R K'))) ↘
        Spec (.of (integralClosure R K'))) ∧
      Nonempty (Over.mk (pullback.snd c (Spec.map (CommRingCat.ofHom (algebraMap K K')))) ≅
        Over.mk (pullback.snd (C := Scheme.{u})
          (projectiveSpaceOver 1 (Spec (.of (integralClosure R K'))) ↘
            Spec (.of (integralClosure R K')))
          (Spec.map (CommRingCat.ofHom (algebraMap (integralClosure R K') K')))))
Sources
LeanAlgebraicGeometry.SemistableReduction.semistableReductionDegreeBound · Stacks.Models.semistableReduction · Stacks.Models.exists_genusOne_semistableReduction · Stacks.Models.exists_hasSemistableReductionAtMaximalIdeals_of_two_le_genus · AlgebraicGeometry.SemistableReduction.genusZero_splitting

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.