109.23 Contraction morphisms to 109.25 Properties of the stack…

Section109.23 Contraction morphisms#

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

Tag 0E88, a lemma

Tag 0E88 in the Stacks Project.

AlgebraicGeometry.CurveFamily.exists_isOpen_forall_isStructureContraction_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurveFamilyContractionOpen.lean, line 56.

Let S be a scheme, s ∈ S, and c : X ⟶ Y a morphism over S of families of curves. If c_{s,*}𝒪_{X_s} = 𝒪_{Y_s} and R¹c_{s,*}𝒪_{X_s} = 0, there is an open neighbourhood W of s such that for every scheme T ⟶ S landing in W and every base change c' : X_T ⟶ Y_T of c, 𝒪_{Y_T} = c'_*𝒪_{X_T} and R¹c'_*𝒪_{X_T} = 0. Taking T = W gives the statement over W, and the quantification over T is the persistence under base change.

theorem exists_isOpen_forall_isStructureContraction_baseChange
    (X Y : CurveFamily B hZ) (hb : Y.base = X.base) (c : X.total ⟶ Y.total)
    (hc : c ≫ Y.toBase ≫ eqToHom (congrArg schemeSpace hb) = X.toBase) (s : X.base.left.1)
    (hs : Space.IsStructureContraction B integerBase hZ
      (Space.structureContractionBaseChange B integerBase hZ c hc
        (schemeSpaceMap (Space.residueFieldMap B integerBase hZ X.base s
          (B.residueField_spec_contains X.base.left.property s))))) :
    ∃ W : X.base.left.1.Opens, s ∈ W ∧
      ∀ (T : BigFppfOver B integerBase hZ) (h : T ⟶ X.base),
        (∀ t, ((𝒯).map h).base t ∈ W) →
        ∀ (X' Y' : AlgebraicSpaces B integerBase hZ) (pX' : X' ⟶ X.total)
          (fX' : X' ⟶ schemeSpace T) (pY' : Y' ⟶ Y.total) (fY' : Y' ⟶ schemeSpace T)
          (c' : X' ⟶ Y'),
          IsPullback pX' fX' X.toBase (schemeSpaceMap h) →
          IsPullback pY' fY' (Y.toBase ≫ eqToHom (congrArg schemeSpace hb)) (schemeSpaceMap h) →
          c' ≫ pY' = pX' ≫ c → c' ≫ fY' = fX' →
          Space.IsStructureContraction B integerBase hZ c'
Tag 0E89, a lemma

Tag 0E89 in the Stacks Project.

AlgebraicGeometry.Space.exists_iso_near_point_of_iso_fibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ContractionUniquenessNearPoint.lean, line 415. The attribute's comment: “Families of curves are read as in AlgebraicGeometry.CurveFamily (Stacks 0D4Z): algebraic spaces X, Y₁, Y₂ with morphisms to S which are flat, proper, of finite presentation and of relative dimension at most one. The fibres over s are the fibre products along Spec κ(s) ⟶ S; the hypotheses on c₁,ₛ are read on the morphism of schemes presenting it (the fibres being schemes by Stacks 0ADD).”.

Let S be a scheme and s ∈ S a point. Let f : X ⟶ S and gᵢ : Yᵢ ⟶ S, i = 1, 2, be families of curves (algebraic spaces, flat, proper, of finite presentation and of relative dimension at most one over S) and cᵢ : X ⟶ Yᵢ morphisms over S. Let φ : Y₁,ₛ ≅ Y₂,ₛ be an isomorphism of the fibres over Spec κ(s) ⟶ S compatible with c₁,ₛ and c₂,ₛ. Suppose c₁,ₛ,* 𝒪_{Xₛ} = 𝒪_{Y₁,ₛ} and R¹c₁,ₛ,* 𝒪_{Xₛ} = 0; these are read on the morphism of schemes a₁ : F_X ⟶ F₁ which c₁,ₛ is through presentations e_X, e₁ of the fibres Xₛ and Y₁,ₛ by schemes (the fibres of a family of curves over a field are schemes, [Stacks, Tag 0ADD], AlgebraicGeometry.Space.exists_presentation_of_curveFamilyConditions_of_field). Then there are an open neighbourhood j : U ⟶ S of s and an isomorphism ψ : Y₁ ×_S U ≅ Y₂ ×_S U over U, compatible with c₁ and c₂ and with φ (through the factorisation k of Spec κ(s) ⟶ S through U).

theorem exists_iso_near_point_of_iso_fibre (S : BigFppfOver B integerBase hZ) (s : (𝒯).obj S)
    {X Y₁ Y₂ : (BigFppfOver B integerBase hZ)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B integerBase hZ X) (hY₁ : IsAlgebraicSpace B integerBase hZ Y₁)
    (hY₂ : IsAlgebraicSpace B integerBase hZ Y₂)
    (f : X ⟶ yoneda.obj S) (g₁ : Y₁ ⟶ yoneda.obj S) (g₂ : Y₂ ⟶ yoneda.obj S)
    (hfl : IsFlat B integerBase hZ f) (hpr : IsProper B integerBase hZ f)
    (hfp : IsFinitePresentation B integerBase hZ f)
    (hd : HasRelativeDimensionLE 1 B integerBase hZ f)
    (hfl₁ : IsFlat B integerBase hZ g₁) (hpr₁ : IsProper B integerBase hZ g₁)
    (hfp₁ : IsFinitePresentation B integerBase hZ g₁)
    (hd₁ : HasRelativeDimensionLE 1 B integerBase hZ g₁)
    (hfl₂ : IsFlat B integerBase hZ g₂) (hpr₂ : IsProper B integerBase hZ g₂)
    (hfp₂ : IsFinitePresentation B integerBase hZ g₂)
    (hd₂ : HasRelativeDimensionLE 1 B integerBase hZ g₂)
    (c₁ : X ⟶ Y₁) (c₂ : X ⟶ Y₂) (hc₁ : c₁ ≫ g₁ = f) (hc₂ : c₂ ≫ g₂ = f)
    {FX F₁ : BigFppfOver B integerBase hZ}
    (eX : yoneda.obj FX ≅ pullback f (yoneda.map (pointFieldMap S s)))
    (e₁ : yoneda.obj F₁ ≅ pullback g₁ (yoneda.map (pointFieldMap S s)))
    (tX : FX ⟶ pointFieldObject S s) (t₁ : F₁ ⟶ pointFieldObject S s)
    (heX : eX.hom ≫ pullback.snd f (yoneda.map (pointFieldMap S s)) = yoneda.map tX)
    (he₁ : e₁.hom ≫ pullback.snd g₁ (yoneda.map (pointFieldMap S s)) = yoneda.map t₁)
    (a₁ : FX ⟶ F₁)
    (ha₁ : yoneda.map a₁ ≫ e₁.hom =
      eX.hom ≫ pullback.map f (yoneda.map (pointFieldMap S s)) g₁
        (yoneda.map (pointFieldMap S s)) c₁ (𝟙 _) (𝟙 _) (by simp [hc₁]) (by simp))
    (h0 : IsIso (Scheme.Modules.unitToPushforwardUnit ((𝒯).map a₁)))
    (hR : IsZero (firstDirectImageStructureSheaf ((𝒯).map a₁)))
    (φ : pullback g₁ (yoneda.map (pointFieldMap S s)) ≅
      pullback g₂ (yoneda.map (pointFieldMap S s)))
    (hφ : φ.hom ≫ pullback.snd g₂ (yoneda.map (pointFieldMap S s)) =
      pullback.snd g₁ (yoneda.map (pointFieldMap S s)))
    (hφc : pullback.map f (yoneda.map (pointFieldMap S s)) g₁
        (yoneda.map (pointFieldMap S s)) c₁ (𝟙 _) (𝟙 _) (by simp [hc₁]) (by simp) ≫ φ.hom =
      pullback.map f (yoneda.map (pointFieldMap S s)) g₂
        (yoneda.map (pointFieldMap S s)) c₂ (𝟙 _) (𝟙 _) (by simp [hc₂]) (by simp)) :
    ∃ (U : BigFppfOver B integerBase hZ) (j : U ⟶ S),
      _root_.AlgebraicGeometry.IsOpenImmersion ((𝒯).map j) ∧
      s ∈ Set.range ((𝒯).map j) ∧
      ∃ (ψ : pullback g₁ (yoneda.map j) ≅ pullback g₂ (yoneda.map j))
        (k : pointFieldObject S s ⟶ U),
        ψ.hom ≫ pullback.snd g₂ (yoneda.map j) = pullback.snd g₁ (yoneda.map j) ∧
        pullback.map f (yoneda.map j) g₁ (yoneda.map j) c₁ (𝟙 _) (𝟙 _) (by simp [hc₁])
            (by simp) ≫ ψ.hom =
          pullback.map f (yoneda.map j) g₂ (yoneda.map j) c₂ (𝟙 _) (𝟙 _) (by simp [hc₂])
            (by simp) ∧
        ∃ (hk : k ≫ j = pointFieldMap S s),
          pullback.map g₁ (yoneda.map (pointFieldMap S s)) g₁ (yoneda.map j) (𝟙 _) (yoneda.map k)
              (𝟙 _) (by simp) (by rw [Category.comp_id, ← Functor.map_comp, hk]) ≫ ψ.hom =
            φ.hom ≫ pullback.map g₂ (yoneda.map (pointFieldMap S s)) g₂ (yoneda.map j) (𝟙 _)
              (yoneda.map k) (𝟙 _) (by simp)
              (by rw [Category.comp_id, ← Functor.map_comp, hk])
Tag 0E7C, a lemma

Tag 0E7C in the Stacks Project.

AlgebraicGeometry.CurveFamily.exists_elementaryEtaleNeighborhood_contraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ContractionExistenceScheme.lean, line 225.

Let F be a family of curves (Stacks 0D4Z) over a scheme S of the site, s ∈ S, X₀ the fibre of F over s (the cartesian square ι over Spec κ(s) ⟶ S; the fibre of a family of curves over a field is a scheme, Stacks 0ADD), and h₀ : X₀ ⟶ Y₀ a morphism over κ(s) to a proper scheme Y₀ over κ(s) with 𝒪_{Y₀} = h₀,*𝒪_{X₀} and R¹h₀,*𝒪_{X₀} = 0. Then there are an elementary étale neighbourhood (U, u) of (S, s), with the lift t : Spec κ(s) ⟶ U of s onto u which identifies κ(u) with κ(s), a family of curves G over U and a morphism h over U from the total space of the base change F_U to that of G whose fibre in u is isomorphic to h₀: X₀ and Y₀ are the fibres of F_U and G over t (the cartesian squares ιU and j, with ιU lying over ι), and h restricts to h₀.

theorem exists_elementaryEtaleNeighborhood_contraction {S : Scheme.{u}} (hS : B.Contains S)
    (F : CurveFamily B hZ) (hF : F.base = integerSiteObject B hZ hS) (s : S)
    {X₀ : Scheme.{u}} (hX₀ : B.Contains X₀) (pX₀ : X₀ ⟶ Spec (.of (S.residueField s)))
    (ι : yoneda.obj (integerSiteObject B hZ hX₀) ⟶ F.total.obj)
    (hι : IsPullback ι (yoneda.map (integerSiteMap B hZ hX₀
        (BigFppfSite.residueField_spec_contains B hS s) pX₀)) (F.toBaseYonedaOfEq hF)
      (yoneda.map (integerSiteMap B hZ (BigFppfSite.residueField_spec_contains B hS s) hS
        (S.fromSpecResidueField s))))
    {Y₀ : Scheme.{u}} (pY₀ : Y₀ ⟶ Spec (.of (S.residueField s))) [IsProper pY₀]
    (h₀ : X₀ ⟶ Y₀) (hh₀ : h₀ ≫ pY₀ = pX₀)
    (h0 : IsIso (C := Y₀.Modules) (Scheme.Modules.unitToPushforwardUnit h₀))
    (hR1 : IsZero (((Scheme.Modules.pushforward h₀).rightDerived 1).obj
      (SheafOfModules.unit X₀.ringCatSheaf))) :
    ∃ U : EtaleNeighborhood S s, U.IsElementary ∧
      ∃ (hU : B.Contains U.scheme) (t : Spec (.of (S.residueField s)) ⟶ U.scheme),
        t ≫ U.toBase = S.fromSpecResidueField s ∧ (∀ x, t x = U.point) ∧
        ∃ (G : CurveFamily B hZ) (hG : G.base = integerSiteObject B hZ hU)
          (h : ((F.ofBaseEq hF).pullback (integerSiteMap B hZ hU hS U.toBase)).total.obj ⟶
            G.total.obj),
          h ≫ G.toBaseYonedaOfEq hG =
            ((F.ofBaseEq hF).pullback (integerSiteMap B hZ hU hS U.toBase)).toBaseYoneda ∧
          ∃ ιU : yoneda.obj (integerSiteObject B hZ hX₀) ⟶
              ((F.ofBaseEq hF).pullback (integerSiteMap B hZ hU hS U.toBase)).total.obj,
            ιU ≫ ((F.ofBaseEq hF).pullbackHom
              (integerSiteMap B hZ hU hS U.toBase)).totalMap.hom = ι ∧
            IsPullback ιU (yoneda.map (integerSiteMap B hZ hX₀
                (BigFppfSite.residueField_spec_contains B hS s) pX₀))
              ((F.ofBaseEq hF).pullback (integerSiteMap B hZ hU hS U.toBase)).toBaseYoneda
              (yoneda.map (integerSiteMap B hZ (BigFppfSite.residueField_spec_contains B hS s)
                hU t)) ∧
            ∃ j : yoneda.obj (integerSiteObject B hZ
                (Scheme.size_lt_of_locallyOfFiniteType_of_quasiCompact pY₀
                  (BigFppfSite.residueField_spec_contains B hS s))) ⟶ G.total.obj,
              IsPullback j (yoneda.map (integerSiteMap B hZ
                  (Scheme.size_lt_of_locallyOfFiniteType_of_quasiCompact pY₀
                    (BigFppfSite.residueField_spec_contains B hS s))
                  (BigFppfSite.residueField_spec_contains B hS s) pY₀))
                (G.toBaseYonedaOfEq hG)
                (yoneda.map (integerSiteMap B hZ (BigFppfSite.residueField_spec_contains B hS s)
                  hU t)) ∧
              ιU ≫ h = yoneda.map (integerSiteMap B hZ hX₀
                (Scheme.size_lt_of_locallyOfFiniteType_of_quasiCompact pY₀
                  (BigFppfSite.residueField_spec_contains B hS s)) h₀) ≫ j
Tag 0E8A, a lemma

Tag 0E8A in the Stacks Project.

AlgebraicGeometry.CurveFamily.exists_stabilization_and_existsUnique_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PrestableStabilizationTheorem.lean, line 68. The attribute's comment: “Existence and uniqueness in one statement. X ⟶ S is a prestable family of curves whose fibres over all field-valued points have genus g ≥ 2 (HasFibresOfGenus, the genus of a prestable family, Stacks 0E6V). The factorization X ⟶ Y ⟶ S is a family of curves Y over S (same base, hb) with c ≫ g = f. Condition (1) is IsUniversalStructureContraction: for every scheme S' ⟶ S of the site and the base change c' : X' ⟶ Y', 𝒪_{Y'} ⟶ c'_*𝒪_{X'} is an isomorphism and R¹c'_*𝒪_{X'} = 0 (S' = S gives the condition for c). Condition (2) is HasStableContractionFibres, asserted at every field-valued point of S (so at every s ∈ S through Spec κ(s)): the fibre c_s satisfies the three conditions of Stacks 0E7Q, which characterize the contraction of rational tails and bridges of Section 0E7N up to unique isomorphism (exists_isStableContraction_comp_tails_bridges). Uniqueness up to unique isomorphism: for any two such cᵢ : X ⟶ Yᵢ (the targets need not be assumed stable) there is exactly one isomorphism e : Y₁ ≅ Y₂ over S with c₁ ≫ e = c₂.”.

Let X ⟶ S be a prestable family of curves of genus g ≥ 2. Then there are a stable family of curves Y ⟶ S and a morphism c : X ⟶ Y over S such that

  1. 𝒪_Y = c_*𝒪_X and R¹c_*𝒪_X = 0, and this remains true after base change by any morphism S' ⟶ S, and
  2. for every field-valued point s of S the morphism c_s : X_s ⟶ Y_s is the contraction of rational tails and bridges (it satisfies the conditions of Stacks 0E7Q characterizing it).

Moreover c is unique up to unique isomorphism: for any two morphisms cᵢ : X ⟶ Yᵢ over S to families of curves satisfying (1) and (2) there is exactly one isomorphism e : Y₁ ≅ Y₂ over S with c₁ ≫ e = c₂.

theorem exists_stabilization_and_existsUnique_iso
    {X : CurveFamily B hZ} (hX : IsPrestableCurveFamily B hZ X) {g : ℕ} (hg : 2 ≤ g)
    (hgen : X.HasFibresOfGenus g) :
    (∃ (Y : CurveFamily B hZ) (hb : Y.base = X.base) (c : X.total ⟶ Y.total),
      IsStableCurveFamily B hZ Y ∧ c ≫ Y.toBase ≫ eqToHom (congrArg schemeSpace hb) = X.toBase ∧
      X.IsUniversalStructureContraction B hZ Y hb c ∧ X.HasStableContractionFibres B hZ Y hb c) ∧
    ∀ (Y₁ Y₂ : CurveFamily B hZ) (hb₁ : Y₁.base = X.base) (hb₂ : Y₂.base = X.base)
      (c₁ : X.total ⟶ Y₁.total) (c₂ : X.total ⟶ Y₂.total),
      c₁ ≫ Y₁.toBase ≫ eqToHom (congrArg schemeSpace hb₁) = X.toBase →
      c₂ ≫ Y₂.toBase ≫ eqToHom (congrArg schemeSpace hb₂) = X.toBase →
      X.IsUniversalStructureContraction B hZ Y₁ hb₁ c₁ →
      X.IsUniversalStructureContraction B hZ Y₂ hb₂ c₂ →
      X.HasStableContractionFibres B hZ Y₁ hb₁ c₁ → X.HasStableContractionFibres B hZ Y₂ hb₂ c₂ →
      ∃! e : Y₁.total ≅ Y₂.total, c₁ ≫ e.hom = c₂ ∧
        e.hom ≫ Y₂.toBase ≫ eqToHom (congrArg schemeSpace hb₂) =
          Y₁.toBase ≫ eqToHom (congrArg schemeSpace hb₁)
Tag 0E8B, a lemma

Tag 0E8B in the Stacks Project.

AlgebraicGeometry.stabilizationMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ModuliStabilization.lean, line 103. The attribute's comment: “the stabilization morphism Curves^{prestable}_g → Mbar_g”.

For g ≥ 2, the stabilization morphism Curves^{prestable}_g ⟶ 𝓜̄_g of stacks over ℤ, a 1-morphism of categories fibred in groupoids over the big fppf site of Spec(ℤ). It sends a prestable family of curves X → S of genus g to the stable family Y → S of Stacks 0E8A (AlgebraicGeometry.stabilizationMorphism_obj).

def stabilizationMorphism (g : ℕ) (hg : 2 ≤ g) :
    curvesPrestableOfGenus B hZ g ⟶ moduliStableCurvesOfGenus B hZ g

AlgebraicGeometry.stabilizationMorphism_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ModuliStabilization.lean, line 115. The attribute's comment: “it sends a prestable family X → S of genus g to its stable model Y → S of 0E8A”.

The stabilization morphism sends a prestable family of curves X → S of genus g ≥ 2 to a stable family Y → S over the same base together with a morphism c : X → Y over S which is the stable model of Stacks 0E8A: Y is stable with fibres of genus g, 𝒪_Y = c_*𝒪_X and R¹c_*𝒪_X = 0 after every base change, and on every fibre c is the contraction of rational tails and bridges.

theorem stabilizationMorphism_obj (g : ℕ) (hg : 2 ≤ g)
    (X : (curvesPrestableOfGenus B hZ g).val.obj) :
    ∃ (h : ((stabilizationMorphism B hZ g hg).hom.obj X).obj.base = X.obj.base)
      (c : X.obj.total ⟶ ((stabilizationMorphism B hZ g hg).hom.obj X).obj.total),
      IsStableModel B hZ g (eqToHom h.symm) c
Sources
LeanAlgebraicGeometry.CurveFamily.exists_isOpen_forall_isStructureContraction_baseChange · AlgebraicGeometry.Space.exists_iso_near_point_of_iso_fibre · AlgebraicGeometry.CurveFamily.exists_elementaryEtaleNeighborhood_contraction · AlgebraicGeometry.CurveFamily.exists_stabilization_and_existsUnique_iso · AlgebraicGeometry.stabilizationMorphism · AlgebraicGeometry.stabilizationMorphism_obj

Section109.24 Stable reduction theorem#

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

Tag 0E8D, a lemma

Tag 0E8D in the Stacks Project.

Stacks.Models.hasSemistableReduction_iff_exists_isStableCurveFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PrestableStabilizationTheorem.lean, line 119. The attribute's comment: “C ⟶ Spec K is smooth, projective, a curve (IsCurve), with H⁰(C, 𝒪_C) = K and genus ≥ 2. (1) is HasSemistableReduction R c hc (Semistable Reduction, Definition 0CDH). (2), a stable family of curves over R with generic fibre C, is a stable family of curves F (Stacks 0E75) whose base is identified with Spec R (ψ), with a morphism of families of curves (a cartesian square) from the family C ⟶ Spec K to F lying over Spec K ⟶ Spec R.”.

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 C has semistable reduction (Stacks 0CDH) exactly when it is the generic fibre of a stable family of curves over R: a stable family F over Spec R with a morphism of families of curves from C ⟶ Spec K to F lying over Spec K ⟶ Spec R.

theorem hasSemistableReduction_iff_exists_isStableCurveFamily
    (B : BigFppfSite.{u}) (hZ : B.Contains integerBase) (hR : B.Contains (Spec (.of R)))
    {C : Scheme.{u}} (c : C ⟶ Spec (.of K)) [IsCurve K c] [Smooth c] (hc : IsProjective c)
    [IsIso ((Scheme.ΓSpecIso (.of K)).inv ≫ c.appTop)] (hg : 2 ≤ genus c) :
    HasSemistableReduction R c hc ↔
      ∃ (F : CurveFamily B hZ) (ψ : F.base ≅ integerSiteObject B hZ hR)
        (φ : @curveFamilyOfScheme K _ (Over.mk c) hc.isProper B hZ
          (contains_spec_of_isFractionRing hR)
          (IsCurve.topologicalKrullDim_eq_one (k := K) (f := c)).le ⟶ F),
        IsStableCurveFamily B hZ F ∧
          φ.baseMap ≫ ψ.hom = integerSiteMap B hZ (contains_spec_of_isFractionRing hR) hR
            (Spec.map (CommRingCat.ofHom (algebraMap R K)))
Tag 0E97, a lemma

Tag 0E97 in the Stacks Project.

Stacks.Models.existsUnique_isModelHom_iso_of_isStableFamilyOfSchemesOfGenus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/StableModelExistsUnique.lean, line 179.

Let R be a discrete valuation ring with fraction field K and C a smooth proper curve over K with K = H⁰(C, 𝒪_C) and genus g. If X and X' are models of C (Section 0C2R) which are stable families of genus g curves over R, then there exists a unique isomorphism of models X ≅ X'.

theorem existsUnique_isModelHom_iso_of_isStableFamilyOfSchemesOfGenus (B : BigFppfSite.{u})
    (hZ : B.Contains integerBase) (hR : B.Contains (Spec (.of R))) {C : Scheme.{u}}
    (C_to_K : C ⟶ Spec (.of K)) [IsCurve K C_to_K] [Smooth C_to_K] [IsProper C_to_K]
    [IsIso ((Scheme.ΓSpecIso (.of K)).inv ≫ C_to_K.appTop)] (g : ℕ) (_hg : genus C_to_K = g)
    {X X' : Scheme.{u}} {p : X ⟶ Spec (.of R)} {p' : X' ⟶ Spec (.of R)}
    {e : C ≅ pullback p (Spec.map (CommRingCat.ofHom (algebraMap R K)))}
    {e' : C ≅ pullback p' (Spec.map (CommRingCat.ofHom (algebraMap R K)))}
    (hX : IsModel C_to_K p e) (hX' : IsModel C_to_K p' e')
    (hst : IsStableFamilyOfSchemesOfGenus B hZ g p hR)
    (hst' : IsStableFamilyOfSchemesOfGenus B hZ g p' hR) :
    ∃! f : X ≅ X', IsModelHom p p' e e' f.hom
Tag 0E98, a theorem

Tag 0E98 in the Stacks Project.

Stacks.Models.stableReduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/StableReduction/Main.lean, line 151.

Stacks Project, Tag 0E98 (stable reduction, [DM, Corollary 2.7]). 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 and genus g ≥ 2. Let B be a big fppf site containing Spec R. Then

  1. there exist an extension of discrete valuation rings R ⊆ R' inducing a finite separable extension of fraction fields K'/K and a stable family of curves Y ⟶ Spec R' of genus g with Y_{K'} ≅ C_{K'} over K', and
  2. there exist a finite separable extension L/K and a stable family of curves Y ⟶ Spec A of genus g, where A ⊆ L is the integral closure of R in L, such that Y_L ≅ C_L over L.
theorem stableReduction (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) (B : BigFppfSite.{u})
    (hZ : B.Contains integerBase) (hR : B.Contains (Spec (.of R))) :
    (∃ (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') ∧
        ∃ (hR' : B.Contains (Spec (.of R'))) (Y : Scheme.{u}) (p : Y ⟶ Spec (.of R')),
          IsStableFamilyOfSchemesOfGenus B hZ (genus c) p hR' ∧
          Nonempty (Over.mk (pullback.snd p (Spec.map (CommRingCat.ofHom (algebraMap R' K')))) ≅
            Over.mk (pullback.snd c (Spec.map (CommRingCat.ofHom (algebraMap K K')))))) ∧
    (∃ (L : Type u) (_ : Field L) (_ : Algebra K L) (_ : Algebra R L)
      (_ : IsScalarTower R K L), FiniteDimensional K L ∧ Algebra.IsSeparable K L ∧
      ∃ (hA : B.Contains (Spec (.of (integralClosure R L)))) (Y : Scheme.{u})
        (p : Y ⟶ Spec (.of (integralClosure R L))),
        IsStableFamilyOfSchemesOfGenus B hZ (genus c) p hA ∧
        Nonempty (Over.mk (pullback.snd p
            (Spec.map (CommRingCat.ofHom (algebraMap (integralClosure R L) L)))) ≅
          Over.mk (pullback.snd c (Spec.map (CommRingCat.ofHom (algebraMap K L))))))
Sources
LeanStacks.Models.hasSemistableReduction_iff_exists_isStableCurveFamily · Stacks.Models.existsUnique_isModelHom_iso_of_isStableFamilyOfSchemesOfGenus · Stacks.Models.stableReduction

Section109.25 Properties of the stack of stable curves#

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

Tag 0E9A, a lemma

Tag 0E9A in the Stacks Project.

AlgebraicGeometry.isSeparated_moduliStableCurvesOfGenus_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ModuliStableCurvesUnconditional.lean, line 73. The attribute's comment: “g ≥ 2 (hg); 𝓜̄_g → Spec(ℤ) is separated, which is what the source says the statement means; nothing is assumed”.

Let g ≥ 2. The stack 𝓜̄_g is separated: the morphism 𝓜̄_g → Spec(ℤ) (the inclusion of the open substack of stable families of genus g into the small model of the algebraic stack Curves, followed by its structure morphism) is separated.

theorem isSeparated_moduliStableCurvesOfGenus_unconditional (g : ℕ) (hg : 2 ≤ g) :
    Stack.AlgebraicStacks.IsSeparated B integerBase hZ
      ((curvesSmallOpenSubstack B hZ
          (curvesFiberedCategory_isAlgebraicStack.{u, u + 1} B hZ)
          (isOpenCurvesLocus_isStableCurveFamilyOfGenus_unconditional B hZ g)).inclusion ≫
        Stack.structureMorphism B integerBase hZ (curvesAlgebraicStack B hZ
          (curvesFiberedCategory_isAlgebraicStack.{u, u + 1} B hZ)))
Tag 0E9B, a lemma

Tag 0E9B in the Stacks Project.

AlgebraicGeometry.compactSpace_points_moduliStableCurvesOfGenusSmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ModuliStableCurvesOfGenusQuasiCompact.lean, line 126.

Let g ≥ 2. The moduli stack 𝓜̄_g of stable curves of genus g is quasi-compact: the space of points of its small model AlgebraicGeometry.moduliStableCurvesOfGenusSmall (Stacks 04XG), with the topology of Stacks 04XL, is compact. This is quasi-compactness of an algebraic stack in the sense of Stacks 04YB (AlgebraicGeometry.Stack.IsQuasiCompactStack, which is this CompactSpace).

theorem compactSpace_points_moduliStableCurvesOfGenusSmall (g : ℕ) (hg : 2 ≤ g) :
    @CompactSpace (Stack.points B integerBase hZ (moduliStableCurvesOfGenusSmall B hZ g).val
      (moduliStableCurvesOfGenusSmall B hZ g).property)
      (Stack.pointTopology B integerBase hZ (moduliStableCurvesOfGenusSmall B hZ g))
Tag 0E9C, a theorem

Tag 0E9C in the Stacks Project.

AlgebraicGeometry.moduliStableCurves_isDeligneMumford_proper_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ModuliStableCurvesProperSmoothReduced.lean, line 335. The attribute's comment: “g ≥ 2 (hg); 𝓜̄_g is Deligne–Mumford, proper and smooth over Spec(ℤ), and 𝓜_g is an open substack of 𝓜̄_g whose points are dense in |𝓜̄_g|; nothing is assumed”.

Let g ≥ 2. The algebraic stack 𝓜̄_g is a Deligne–Mumford stack, proper and smooth over Spec(ℤ). Moreover, the locus 𝓜_g parametrizing smooth curves is a dense open substack.

Here 𝓜̄_g is the open substack of the algebraic stack of curves (Stacks 0D5A) cut out by the stable families of genus g (Stacks 0E78), and 𝓜_g the one cut out by the families smooth of relative dimension one with f_*𝒪_X = 𝒪_S universally and of genus g (Stacks 0E83); the conjuncts are: 𝓜̄_g is Deligne–Mumford, 𝓜̄_g → Spec(ℤ) is proper, it is smooth, and 𝓜_g is contained in 𝓜̄_g (so it is an open substack of 𝓜̄_g) with points dense in |𝓜̄_g|.

theorem moduliStableCurves_isDeligneMumford_proper_smooth (g : ℕ) (hg : 2 ≤ g) :
    Stack.IsDeligneMumfordStack.{u, u + 1} B integerBase hZ
        (curvesSmallOpenSubstack B hZ
          (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, u + 1} B hZ)
          (isOpenCurvesLocus_isStableCurveFamilyOfGenus_of_isStable B hZ
            (C1590Private.isOpenCurvesLocus_isStableCurveFamily B hZ)
            g)).toAlgebraicStack.val.val ∧
      Stack.AlgebraicStacks.IsProper B integerBase hZ
        ((curvesSmallOpenSubstack B hZ
            (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, u + 1} B hZ)
            (isOpenCurvesLocus_isStableCurveFamilyOfGenus_of_isStable B hZ
              (C1590Private.isOpenCurvesLocus_isStableCurveFamily B hZ) g)).inclusion ≫
          Stack.structureMorphism B integerBase hZ (curvesAlgebraicStack B hZ
            (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, u + 1} B hZ))) ∧
      IsSmoothOverIntegers B hZ
        (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, u + 1} B hZ)
        (isOpenCurvesLocus_isStableCurveFamilyOfGenus_of_isStable B hZ
          (C1590Private.isOpenCurvesLocus_isStableCurveFamily B hZ) g) ∧
      ∃ hle : (curvesSmallOpenSubstack B hZ
            (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, u + 1} B hZ)
            (isOpenCurvesLocus_isSmoothH0FamilyOfGenus_of_isStable B hZ
              (C1590Private.isOpenCurvesLocus_isStableCurveFamily B hZ) hg)).property ≤
          (curvesSmallOpenSubstack B hZ
            (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, u + 1} B hZ)
            (isOpenCurvesLocus_isStableCurveFamilyOfGenus_of_isStable B hZ
              (C1590Private.isOpenCurvesLocus_isStableCurveFamily B hZ) g)).property,
        @Dense _ (Stack.pointTopology B integerBase hZ
            (curvesSmallOpenSubstack B hZ
              (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, u + 1} B hZ)
              (isOpenCurvesLocus_isStableCurveFamilyOfGenus_of_isStable B hZ
                (C1590Private.isOpenCurvesLocus_isStableCurveFamily B hZ)
                g)).toAlgebraicStack.val)
          (Set.range (Stack.AlgebraicStacks.pointsMap B integerBase hZ
            (Stack.OpenSubstack.homOfLE B integerBase hZ
              (curvesSmallOpenSubstack B hZ
                (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, u + 1} B hZ)
                (isOpenCurvesLocus_isSmoothH0FamilyOfGenus_of_isStable B hZ
                  (C1590Private.isOpenCurvesLocus_isStableCurveFamily B hZ) hg))
              (curvesSmallOpenSubstack B hZ
                (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, u + 1} B hZ)
                (isOpenCurvesLocus_isStableCurveFamilyOfGenus_of_isStable B hZ
                  (C1590Private.isOpenCurvesLocus_isStableCurveFamily B hZ) g))
                hle)))
Sources
LeanAlgebraicGeometry.isSeparated_moduliStableCurvesOfGenus_unconditional · AlgebraicGeometry.compactSpace_points_moduliStableCurvesOfGenusSmall · AlgebraicGeometry.moduliStableCurves_isDeligneMumford_proper_smooth

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.