109.3 The stack of curves to 109.22 Stable curves

Section109.3 The stack of curves #

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

Tag 0DMK, a lemma

Tag 0DMK in the Stacks Project.

AlgebraicGeometry.relativeCurvesMorphismsEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesMorphismsFromSpace.lean, line 324. The attribute's comment: “the identification of Mor_B(T, B-Curves) with Mor(T, Curves)”.

Stacks 0DMK, the identification Mor_B(T, B-Curves) = Mor(T, Curves). For a morphism f : T → A of algebraic spaces, the category of morphisms over (Sch/A) from T to the stack A-Curves is equivalent to the category of morphisms over the big fppf site from T to the stack of curves, by forgetting the morphisms of the bases to A.

def relativeCurvesMorphismsEquivalence {T A : AlgebraicSpaces B integerBase hZ} (f : T ⟶ A) :
    (schemesOverSpaceBasedOver B hZ f ⥤ᵇ curvesOverSpaceBased B hZ A) ≌
      (schemesOverSpaceBased B hZ T ⥤ᵇ (curvesFiberedCategory B hZ).val)

AlgebraicGeometry.curvesMorphismsEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesMorphismsFromSpace.lean, line 428. The attribute's comment: “Mor(T, Curves) is the category of families of curves over the algebraic space T”.

Stacks 0DMK, Mor(T, Curves) is the category of families of curves over T. For an algebraic space T, the category of morphisms over the big fppf site from T (read as the category (Sch/T) of schemes with a morphism to T) to the stack of curves is equivalent to the category of families of curves over T: morphisms of algebraic spaces X ⟶ T which are flat, proper, of finite presentation and of relative dimension at most one, with the isomorphisms over T as morphisms. A family X ⟶ T corresponds to the morphism sending U ⟶ T to the family of curves U ×_T X ⟶ U.

noncomputable def curvesMorphismsEquivalence (T : AlgebraicSpaces B integerBase hZ) :
    (schemesOverSpaceBased B hZ T ⥤ᵇ (curvesFiberedCategory B hZ).val) ≌
      CurveFamilyOnSpace B integerBase hZ T

AlgebraicGeometry.relativeCurvesMorphismsCurveFamilyEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesMorphismsFromSpace.lean, line 442. The attribute's comment: “Mor_B(T, B-Curves) = Mor(T, Curves) is the category of families of curves over T”.

Stacks 0DMK. For a morphism f : T ⟶ A of algebraic spaces, the category Mor_A(T, A-Curves) of morphisms over (Sch/A) from T to the stack A-Curves is equivalent to Mor(T, Curves) (AlgebraicGeometry.relativeCurvesMorphismsEquivalence), and both are the category of families of curves over T.

noncomputable def relativeCurvesMorphismsCurveFamilyEquivalence
    {T A : AlgebraicSpaces B integerBase hZ} (f : T ⟶ A) :
    (schemesOverSpaceBasedOver B hZ f ⥤ᵇ curvesOverSpaceBased B hZ A) ≌
      CurveFamilyOnSpace B integerBase hZ T

Sources

LeanAlgebraicGeometry.relativeCurvesMorphismsEquivalence · AlgebraicGeometry.curvesMorphismsEquivalence · AlgebraicGeometry.relativeCurvesMorphismsCurveFamilyEquivalence

Section109.4 The stack of polarized curves #

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

Tag 0DPY, the section

Tag 0DPY in the Stacks Project.

AlgebraicGeometry.polarizedCurvesSquareUnconditional, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedCurvesStack.lean, line 47. The attribute's comment: “the 2-fibre product square defining PolarizedCurves”.

The 2-fibre product square defining the stack of polarized curves: the cospan is the forgetful 1-morphism 𝒫olarized ⟶ 𝒮paces'_{fp, flat, proper} of Stacks 0D3Y and the inclusion 𝒞urves ⟶ 𝒮paces'_{fp, flat, proper} of Stacks 0D50, and the apex is the canonical 2-fibre product of Stacks 0040.

def polarizedCurvesSquareUnconditional :
    Bicategory.TwoCommSq
      (polarizedToCartesianProperFlatHom B hZ
        (polarizedProjection_comp_schemeOverIntegers_isFiberedInGroupoids B))
      (curvesToCartesianProperFlatHom B hZ)

AlgebraicGeometry.polarizedCurves, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedCurvesStack.lean, line 58. The attribute's comment: “PolarizedCurves, the apex of the 2-fibre product”.

PolarizedCurves = 𝒞urves ×_{𝒮paces'_{fp, flat, proper}} 𝒫olarized, the stack of families of curves endowed with a relatively ample invertible module, as a category fibred in groupoids over the big fppf site of Spec(ℤ).

def polarizedCurves :
    CatFiberedInGroupoids.{u, u + 1, u + 1, u + 1} (BigFppfOver B integerBase hZ)

AlgebraicGeometry.polarizedCurvesToPolarizedStack, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedCurvesStack.lean, line 64. The attribute's comment: “the projection to Polarized”.

The projection PolarizedCurves ⟶ 𝒫olarized.

def polarizedCurvesToPolarizedStack :
    polarizedCurves B hZ ⟶
      polarizedFiberedCategory B hZ
        (polarizedProjection_comp_schemeOverIntegers_isFiberedInGroupoids B)

AlgebraicGeometry.polarizedCurvesToCurves, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedCurvesStack.lean, line 72. The attribute's comment: “the projection to Curves”.

The projection PolarizedCurves ⟶ 𝒞urves, forgetting the polarization.

def polarizedCurvesToCurves : polarizedCurves B hZ ⟶ curvesFiberedCategory B hZ

AlgebraicGeometry.isTwoFibreProduct_polarizedCurvesSquareUnconditional, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedCurvesStack.lean, line 78. The attribute's comment: “the square is a 2-fibre product”.

The square of AlgebraicGeometry.polarizedCurvesSquareUnconditional is a 2-fibre product, being the canonical one.

def isTwoFibreProduct_polarizedCurvesSquareUnconditional :
    Bicategory.IsTwoFibreProduct (polarizedCurvesSquareUnconditional B hZ)

Tag 0DPZ, a lemma

Tag 0DPZ in the Stacks Project.

AlgebraicGeometry.isRepresentableByAlgebraicSpaces_polarizedCurvesToPolarized, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedCurves.lean, line 195. The attribute's comment: “representability by algebraic spaces, given Stacks 0D3Z”.

Stacks 0DPZ. The projection PolarizedCurves ⟶ 𝒫olarized is representable by algebraic spaces, being the base change of the inclusion of Stacks 0D50, which is representable by algebraic spaces by Stacks 0D5B.

theorem isRepresentableByAlgebraicSpaces_polarizedCurvesToPolarized
    (h3Z : (polarizedProjection B ⋙ schemeOverIntegers B).IsFiberedInGroupoids) :
    Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
      (polarizedCurvesToPolarized B hZ h3Z).hom

AlgebraicGeometry.isOpenImmersion_polarizedCurvesToPolarized, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedCurves.lean, line 209. The attribute's comment: “open immersion, given Stacks 0D3Z”.

Stacks 0DPZ. The projection PolarizedCurves ⟶ 𝒫olarized is an open immersion, being the base change of the inclusion of Stacks 0D50, which is an open immersion by Stacks 0D5B.

theorem isOpenImmersion_polarizedCurvesToPolarized
    (h3Z : (polarizedProjection B ⋙ schemeOverIntegers B).IsFiberedInGroupoids) :
    Stack.IsOpenImmersion B integerBase hZ (polarizedCurvesToPolarized B hZ h3Z)

AlgebraicGeometry.isClosedImmersion_polarizedCurvesToPolarized, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedCurves.lean, line 222. The attribute's comment: “closed immersion, given Stacks 0D3Z”.

Stacks 0DPZ. The projection PolarizedCurves ⟶ 𝒫olarized is a closed immersion, being the base change of the inclusion of Stacks 0D50, which is a closed immersion by Stacks 0D5B.

theorem isClosedImmersion_polarizedCurvesToPolarized
    (h3Z : (polarizedProjection B ⋙ schemeOverIntegers B).IsFiberedInGroupoids) :
    Stack.IsClosedImmersion B integerBase hZ (polarizedCurvesToPolarized B hZ h3Z)

AlgebraicGeometry.isRepresentableByAlgebraicSpaces_polarizedCurvesToPolarizedUnconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedCurvesUnconditional.lean, line 264. The attribute's comment: “representability by algebraic spaces”.

The projection PolarizedCurves ⟶ 𝒫olarized is representable by algebraic spaces.

theorem isRepresentableByAlgebraicSpaces_polarizedCurvesToPolarizedUnconditional :
    Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
      (polarizedCurvesToPolarizedUnconditional B hZ).hom

AlgebraicGeometry.isOpenImmersion_polarizedCurvesToPolarizedUnconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedCurvesUnconditional.lean, line 272. The attribute's comment: “open immersion”.

The projection PolarizedCurves ⟶ 𝒫olarized is an open immersion.

theorem isOpenImmersion_polarizedCurvesToPolarizedUnconditional :
    Stack.IsOpenImmersion B integerBase hZ (polarizedCurvesToPolarizedUnconditional B hZ)

AlgebraicGeometry.isClosedImmersion_polarizedCurvesToPolarizedUnconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedCurvesUnconditional.lean, line 279. The attribute's comment: “closed immersion”.

The projection PolarizedCurves ⟶ 𝒫olarized is a closed immersion.

theorem isClosedImmersion_polarizedCurvesToPolarizedUnconditional :
    Stack.IsClosedImmersion B integerBase hZ (polarizedCurvesToPolarizedUnconditional B hZ)

AlgebraicGeometry.isRepresentableByAlgebraicSpaces_polarizedCurvesToPolarized_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedCurvesUnconditionalImmersion.lean, line 127. The attribute's comment: “representability by algebraic spaces”.

The projection PolarizedCurves ⟶ 𝒫olarized is representable by algebraic spaces.

theorem isRepresentableByAlgebraicSpaces_polarizedCurvesToPolarized_unconditional :
    Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
      (polarizedCurvesToPolarizedUnconditionalUp B hZ).hom

AlgebraicGeometry.isOpenImmersion_polarizedCurvesToPolarized_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedCurvesUnconditionalImmersion.lean, line 140. The attribute's comment: “open immersion”.

The projection PolarizedCurves ⟶ 𝒫olarized is an open immersion.

theorem isOpenImmersion_polarizedCurvesToPolarized_unconditional :
    Stack.IsOpenImmersion B integerBase hZ (polarizedCurvesToPolarizedUnconditionalUp B hZ)

AlgebraicGeometry.isClosedImmersion_polarizedCurvesToPolarized_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedCurvesUnconditionalImmersion.lean, line 152. The attribute's comment: “closed immersion”.

The projection PolarizedCurves ⟶ 𝒫olarized is a closed immersion.

theorem isClosedImmersion_polarizedCurvesToPolarized_unconditional :
    Stack.IsClosedImmersion B integerBase hZ (polarizedCurvesToPolarizedUnconditionalUp B hZ)

Tag 0DQ0, a lemma

Tag 0DQ0 in the Stacks Project.

AlgebraicGeometry.isSmooth_and_isSurjective_polarizedCurvesToCurves, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PolarizedCurvesToCurvesSmoothSurjective.lean, line 80.

The projection PolarizedCurves ⟶ 𝒞urves is smooth and surjective.

The 1-morphism is AlgebraicGeometry.polarizedCurvesToCurvesAlgebraicOfPolarized, the projection of the 2-fibre product PolarizedCurves = 𝒞urves ×_{𝒮paces'_{fp, flat, proper}} 𝒫olarized of Stacks 0DPY, read in the 2-category of algebraic stacks of Stacks 03YP; smoothness is Stacks 075U and surjectivity is Stacks 04ZS.

theorem isSmooth_and_isSurjective_polarizedCurvesToCurves :
    Stack.AlgebraicStacks.IsSmooth B integerBase hZ
        (polarizedCurvesToCurvesAlgebraicOfPolarized B hZ
          (polarizedCurvesToCurves_isAlgebraic_smooth_surjective.{w, u} B hZ).2.1.1
          (curvesFiberedCategory_isAlgebraicStack.{u, w} B hZ)) ∧
      Stack.IsSurjective B integerBase hZ
        (polarizedCurvesToCurvesAlgebraicOfPolarized B hZ
          (polarizedCurvesToCurves_isAlgebraic_smooth_surjective.{w, u} B hZ).2.1.1
          (curvesFiberedCategory_isAlgebraicStack.{u, w} B hZ))

Tag 0E6F, a lemma

Tag 0E6F in the Stacks Project.

AlgebraicGeometry.CurveFamily.exists_etaleCovering_isPullback_isProjectiveMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurveFamiliesEtaleLocallyHProjective.lean, line 351.

Families of curves are étale locally H-projective schemes. Let X ⟶ S be a family of curves. Then there is an étale covering {S_j ⟶ S} (a family of étale morphisms of the site whose images cover S) such that each X_j = X ×_S S_j is a scheme Z — a cartesian square of algebraic spaces with schemeSpace Z at its corner — and Z ⟶ S_j is H-projective.

theorem exists_etaleCovering_isPullback_isProjectiveMorphism (X : CurveFamily B hZ) :
    ∃ (J : Type u) (U : J → BigFppfOver B integerBase hZ) (φ : ∀ j, U j ⟶ X.base),
      (∀ j, Etale ((𝒯).map (φ j))) ∧
      (∀ s : (𝒯).obj X.base, ∃ j, s ∈ Set.range ((𝒯).map (φ j))) ∧
      ∀ j, ∃ (Z : BigFppfOver B integerBase hZ) (p : schemeSpace Z ⟶ X.total) (q : Z ⟶ U j),
        IsPullback p (schemeSpaceMap q) X.toBase (schemeSpaceMap (φ j)) ∧
        IsProjectiveMorphism ((𝒯).map q)

Sources

LeanAlgebraicGeometry.polarizedCurvesSquareUnconditional · AlgebraicGeometry.polarizedCurves · AlgebraicGeometry.polarizedCurvesToPolarizedStack · AlgebraicGeometry.polarizedCurvesToCurves · AlgebraicGeometry.isTwoFibreProduct_polarizedCurvesSquareUnconditional · AlgebraicGeometry.isRepresentableByAlgebraicSpaces_polarizedCurvesToPolarized · AlgebraicGeometry.isOpenImmersion_polarizedCurvesToPolarized · AlgebraicGeometry.isClosedImmersion_polarizedCurvesToPolarized

Section109.5 Properties of the stack of curves #

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

Tag 0DSQ, a lemma

Tag 0DSQ in the Stacks Project.

AlgebraicGeometry.isSeparated_and_isRelativelyFinitePresentation_diagonal_curves, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesDiagonalUnconditional.lean, line 58.

Stacks 0DSQ. The diagonal of the algebraic stack Curves over Spec ℤ is separated and of finite presentation.

theorem isSeparated_and_isRelativelyFinitePresentation_diagonal_curves :
    Stack.IsSeparated B integerBase hZ
        (Stack.relativeDiagonal.{u, u, u + 1} B integerBase hZ
          (curvesAlgebraicStack B hZ
            (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, w} B hZ)).val
          (Stack.schemeStack.{u, w} B integerBase hZ (Over.mk (𝟙 (B.obj hZ)))).val
          (Stack.structureMorphism B integerBase hZ (curvesAlgebraicStack B hZ
            (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, w} B hZ))).hom) ∧
      Stack.AlgebraicStacks.IsRelativelyFinitePresentation B integerBase hZ
        (Stack.AlgebraicStacks.relativeDiagonal B integerBase hZ
          (Stack.structureMorphism B integerBase hZ (curvesAlgebraicStack B hZ
            (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, w} B hZ))))

Tag 0DSS, a lemma

Tag 0DSS in the Stacks Project.

AlgebraicGeometry.isQuasiSeparated_and_isLocallyOfFinitePresentation_curvesAlgebraicStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesQuasiSeparatedLocallyFinitePresentation.lean, line 53.

Stacks 0DSS. The morphism Curves → Spec(ℤ) of the algebraic stack of curves is quasi-separated and locally of finite presentation.

Quasi-separatedness is the quasi-compactness and quasi-separatedness of the diagonal, given by the finite presentation of the diagonal in Stacks 0DSQ (AlgebraicGeometry.isSeparated_and_isRelativelyFinitePresentation_diagonal_curves); local finite presentation is Stacks 0CMY applied to Stacks 0D55 (AlgebraicGeometry.isLimitPreserving_curvesFiberedCategory_unconditional).

theorem isQuasiSeparated_and_isLocallyOfFinitePresentation_curvesAlgebraicStack :
    Stack.AlgebraicStacks.IsQuasiSeparated B integerBase hZ
        (Stack.structureMorphism B integerBase hZ (curvesAlgebraicStack B hZ
          (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, w} B hZ))) ∧
      Stack.AlgebraicStacks.IsLocallyOfFinitePresentation B integerBase hZ
        (Stack.structureMorphism B integerBase hZ (curvesAlgebraicStack B hZ
          (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, w} B hZ)))

Sources

LeanAlgebraicGeometry.isSeparated_and_isRelativelyFinitePresentation_diagonal_curves · AlgebraicGeometry.isQuasiSeparated_and_isLocallyOfFinitePresentation_curvesAlgebraicStack

Section109.6 Open substacks of the stack of curves #

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

Tag 0E0E, the section

Tag 0E0E in the Stacks Project.

AlgebraicGeometry.isOpenImmersion_curvesSubstackInclusion_and_factors_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesOpenSubstack.lean, line 376. The attribute's comment: “the open substack Curves^P cut out by a property P with condition (o), and its universal property (1); part (2) is the special case of (1) at the family of a proper scheme of dimension at most one over a field”.

Stacks 0E0E. For a property P of families of curves satisfying condition (o): Curves^P ⊂ Curves is an open substack — P is invariant under isomorphism, and the inclusion is representable by algebraic spaces and an open immersion — and the classifying morphism of a family factors through Curves^P exactly when the family has P.

theorem isOpenImmersion_curvesSubstackInclusion_and_factors_iff
    (hP : IsOpenCurvesLocus B hZ P) :
    (P.IsClosedUnderIsomorphisms ∧
      Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (curvesSubstackInclusion B hZ P hP.prop_of_hom).hom ∧
      Stack.IsOpenImmersion B integerBase hZ (curvesSubstackInclusion B hZ P hP.prop_of_hom)) ∧
    ∀ (U : BigFppfOver B integerBase hZ)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
      y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
      ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤ P.FullSubcategory, z ⋙ P.ι = y) ↔
        P (y.obj (Over.mk (𝟙 U.left))))

Sources

LeanAlgebraicGeometry.isOpenImmersion_curvesSubstackInclusion_and_factors_iff

Section109.7 Curves with finite reduced automorphism groups #

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

Tag 0DSU, an example

Tag 0DSU in the Stacks Project.

AlgebraicGeometry.isClosedImmersion_doublePointsToProjectiveLine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ProjectiveLinesGluedAtDoublePoints.lean, line 238. The attribute's comment: “the three double points form a closed subscheme of the projective line”.

Stacks 0DSU. For three pairwise distinct points of the affine line, the three double points Spec(k[t]/(t - aᵢ)²) form a closed subscheme of P¹_k.

theorem isClosedImmersion_doublePointsToProjectiveLine (hpts : Function.Injective pts) :
    IsClosedImmersion (doublePointsToProjectiveLine k pts)

AlgebraicGeometry.isPushout_gluingScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ProjectiveLinesGluedAtDoublePoints.lean, line 256. The attribute's comment: “the two affine lines glue to the spectrum of the equalizer of the two reductions”.

Stacks 0DSU. Gluing two copies of A¹_k along the three double points gives the spectrum of the equalizer of the two reduction maps k[t] × k[t] ⇉ ∏ᵢ k[t]/(t - aᵢ)²: the functions on the affine part of the glued curve are the pairs of polynomials agreeing to first order at the three points.

theorem isPushout_gluingScheme (hpts : Function.Injective pts) :
    IsPushout (doublePointsToAffineLine k pts) (doublePointsToAffineLine k pts)
      (Spec.map (CommRingCat.ofHom (gluingSubringSnd pts)))
      (Spec.map (CommRingCat.ofHom (gluingSubringFst pts)))

AlgebraicGeometry.gluedCurve, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ProjectiveLinesGluedAtDoublePoints.lean, line 270. The attribute's comment: “the curve obtained by gluing two projective lines along three double points”.

Stacks 0DSU. The curve X of the example: two copies of P¹_k glued along the closed subscheme of the three double points Spec(k[t]/(t - aᵢ)²), that is, the pushout of T ⟶ P¹_k with itself.

def gluedCurve : Scheme.{u}

AlgebraicGeometry.isPushout_gluedCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ProjectiveLinesGluedAtDoublePoints.lean, line 287. The attribute's comment: “the glued curve is the pushout of the two projective lines”.

Stacks 0DSU. The glued curve is the pushout of the two copies of P¹_k along the three double points.

theorem isPushout_gluedCurve :
    IsPushout (doublePointsToProjectiveLine k pts) (doublePointsToProjectiveLine k pts)
      (gluedCurveInl k pts hpts) (gluedCurveInr k pts hpts)

AlgebraicGeometry.epsTranslate, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ProjectiveLinesGluedAtDoublePoints.lean, line 451. The attribute's comment: “the automorphism of the equalizer diagram sending t to t + epsilon”.

Stacks 0DSU. The automorphism of the equalizer diagram k[ε][t] × k[ε][t] ⇉ ∏ᵢ k[ε][t]/(t - aᵢ)² over the dual numbers of a field of characteristic 2 given by the substitution t ↦ t + ε on both coordinates.

def epsTranslate : gluingSubring pts ≃+* gluingSubring pts

AlgebraicGeometry.epsTranslate_ne_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ProjectiveLinesGluedAtDoublePoints.lean, line 457. The attribute's comment: “non-triviality of the automorphism sending t to t + epsilon”.

Stacks 0DSU. The substitution t ↦ t + ε on the equalizer diagram is not the identity.

theorem epsTranslate_ne_one : epsTranslate k pts ≠ RingEquiv.refl _

AlgebraicGeometry.map_fst_epsTranslate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ProjectiveLinesGluedAtDoublePoints.lean, line 465. The attribute's comment: “the automorphism sending t to t + epsilon is the identity modulo epsilon”.

Stacks 0DSU. The substitution t ↦ t + ε becomes the identity modulo ε.

theorem map_fst_epsTranslate (x : gluingSubring pts) :
    ((Polynomial.mapRingHom (TrivSqZeroExt.fstHom k k k).toRingHom) (epsTranslate k pts x).1.1,
        (Polynomial.mapRingHom (TrivSqZeroExt.fstHom k k k).toRingHom)
          (epsTranslate k pts x).1.2) =
      ((Polynomial.mapRingHom (TrivSqZeroExt.fstHom k k k).toRingHom) x.1.1,
        (Polynomial.mapRingHom (TrivSqZeroExt.fstHom k k k).toRingHom) x.1.2)

AlgebraicGeometry.isAffineOpen_gluedCurveAffinePart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ProjectiveLinesGluedAtDoublePointsAffinePart.lean, line 250. The attribute's comment: “the affine open part U of X, the image of the two affine lines”.

U is an affine open of the glued curve.

theorem isAffineOpen_gluedCurveAffinePart : IsAffineOpen (gluedCurveAffinePart k pts hpts)

AlgebraicGeometry.gluedCurveAffinePartSectionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ProjectiveLinesGluedAtDoublePointsAffinePart.lean, line 257. The attribute's comment: “O_X(U) is the equalizer of k[t] × k[t] ⇉ ∏ k[t]/(t - a_i)²”.

The functions on U are the equalizer O_X(U) ⟶ k[t] × k[t] ⇉ ∏ᵢ k[t]/(t - aᵢ)²: the ring of sections of X over the affine part is the ring of pairs of polynomials agreeing to first order at the three points.

def gluedCurveAffinePartSectionsEquiv :
    Γ(gluedCurve k pts hpts, gluedCurveAffinePart k pts hpts) ≃+* gluingSubring pts

AlgebraicGeometry.gluedCurveDualNumbersAut, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ProjectiveLinesGluedAtDoublePointsDualNumbers.lean, line 398. The attribute's comment: “the automorphism t ↦ t + ε extends to an automorphism of X over A = k[ε]”.

The automorphism t ↦ t + ε of the equalizer diagram extends to an automorphism of X over A = k[ε]. For k of characteristic 2, the automorphism of X_A = X ×_{Spec k} Spec k[ε] over Spec k[ε] which is the translation t ↦ t + ε on both copies of ℙ¹_{k[ε]}.

def gluedCurveDualNumbersAut :
    Aut (Over.mk (pullback.snd (gluedCurveToBase k pts hpts) (dualNumbersToBase k)))

AlgebraicGeometry.projectiveLineXChart_comp_gluedCurveDualNumbersAut, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ProjectiveLinesGluedAtDoublePointsDualNumbers.lean, line 415. The attribute's comment: “the automorphism of X_A is the substitution t ↦ t + ε on the two affine lines”.

The automorphism of X_A restricts on the two affine lines Spec k[ε][t] to the substitution t ↦ t + ε of the equalizer diagram O(U_A) ⟶ k[ε][t] × k[ε][t] ⇉ ∏ᵢ k[ε][t]/(t - aᵢ)²; on the equalizer itself this substitution is AlgebraicGeometry.epsTranslate.

theorem projectiveLineXChart_comp_gluedCurveDualNumbersAut (b : Bool) :
    projectiveLineXChart (DualNumber k) ≫ gluedCurveDualNumbersComponent k pts hpts b ≫
        (gluedCurveDualNumbersAut k pts hpts).asIso.hom.left =
      Spec.map (CommRingCat.ofHom (translate (DualNumber.eps : DualNumber k)).toRingHom) ≫
        projectiveLineXChart (DualNumber k) ≫ gluedCurveDualNumbersComponent k pts hpts b

AlgebraicGeometry.gluedCurveDualNumbersAut_ne_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ProjectiveLinesGluedAtDoublePointsDualNumbers.lean, line 440. The attribute's comment: “the automorphism of X over A is nontrivial”.

The automorphism of X_A is not the identity: it moves the k[ε]-point t = 0 of the first copy of ℙ¹_{k[ε]} to the point t = ε.

theorem gluedCurveDualNumbersAut_ne_one : gluedCurveDualNumbersAut k pts hpts ≠ 1

AlgebraicGeometry.finite_aut_gluedCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ProjectiveLinesGluedAtDoublePointsFiniteAutomorphisms.lean, line 338. The attribute's comment: “the automorphism group of X over k is finite”.

The automorphism group of X over k is finite. For k algebraically closed and three distinct points, the group of automorphisms over k of the curve obtained by gluing two copies of ℙ¹_k along the three double points Spec(k[t]/(t - aᵢ)²) is finite.

theorem finite_aut_gluedCurve :
    Finite (Aut (Over.mk (gluedCurveToBase k pts hpts)))

AlgebraicGeometry.finite_autFunctor_gluedCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ProjectiveLinesGluedAtDoublePointsNonreducedAut.lean, line 104. The attribute's comment: “the automorphism group of X over k, the k-points of Aut(X), is finite”.

Aut(X)(k) is finite.

theorem finite_autFunctor_gluedCurve :
    Finite ((Scheme.autFunctor (gluedCurveOver k pts hpts)).obj (op (pointOver k)))

AlgebraicGeometry.autFunctor_map_gluedCurveDualNumbersAut, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ProjectiveLinesGluedAtDoublePointsNonreducedAut.lean, line 210. The attribute's comment: “the automorphism t ↦ t + ε becomes the identity modulo ε”.

The automorphism t ↦ t + ε of X_{k[ε]} restricts to the identity over the closed point of Spec k[ε]: its image under Aut(X)(k[ε]) ⟶ Aut(X)(k) is the identity.

theorem autFunctor_map_gluedCurveDualNumbersAut :
    (Scheme.autFunctor (gluedCurveOver k pts hpts)).map (dualNumbersClosedPoint k).op
      (gluedCurveDualNumbersAut k pts hpts) =
        (1 : Aut ((Over.pullback (pointOver k).hom).obj (gluedCurveOver k pts hpts)))

AlgebraicGeometry.not_exists_isReduced_represents_autFunctor_gluedCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/ProjectiveLinesGluedAtDoublePointsNonreducedAut.lean, line 224. The attribute's comment: “Aut(X) is non-reduced”.

The automorphism group scheme of X is non-reduced. For k algebraically closed of characteristic 2 and three distinct points, no reduced scheme locally of finite type over k represents the automorphism functor T ↦ Aut_T(X_T) of the curve X obtained by gluing two copies of ℙ¹_k along the double points at the three points.

theorem not_exists_isReduced_represents_autFunctor_gluedCurve :
    ¬ ∃ (G : Over (Spec (.of k))) (_ : IsReduced G.left) (_ : LocallyOfFiniteType G.hom),
      Nonempty (yoneda.obj G ≅ Scheme.autFunctor (gluedCurveOver k pts hpts))

Tag 0DSV, an example

Tag 0DSV in the Stacks Project.

AlgebraicGeometry.GenusOne.autScheme_topologicalKrullDim_eq_one_of_genus_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GenusOne/AutomorphismSchemeDimension.lean, line 271. The attribute's comment: “genus one: the automorphism group scheme of a smooth proper genus one curve over an algebraically closed field exists and has dimension one”.

Stacks Project, Tag 0DSV, genus one. The automorphism group scheme of a smooth proper curve of genus one over an algebraically closed field has dimension one. The automorphism functor T ↦ Aut_T(X ×_k T) of X over k is representable by a scheme over k, and every scheme representing it has dimension one.

theorem autScheme_topologicalKrullDim_eq_one_of_genus_eq_one
    (hg : genus f = 1) :
    (∃ G : Over (Spec (.of k)), Nonempty ((Scheme.autFunctor (Over.mk f)).RepresentableBy G)) ∧
      ∀ (G : Over (Spec (.of k))), (Scheme.autFunctor (Over.mk f)).RepresentableBy G →
        topologicalKrullDim G.left = 1

AlgebraicGeometry.GenusZero.autFunctor_projectiveLine_representableBy_projectiveGeneralLinearTwo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GenusZero/AutomorphismSchemeDimension.lean, line 63. The attribute's comment: “genus zero: Aut(P^1_k) = PGL_{2,k} as functors, an invertible matrix acting by its Moebius map, and PGL_{2,k} has dimension three”.

Stacks Project, Tag 0DSV, genus zero. Aut(ℙ¹_k) = PGL_{2,k} as functors. The scheme PGL_{2,k} represents the automorphism functor of the projective line over k, the point of PGL_{2,k} given by an invertible matrix M over a k-algebra A corresponding to the Möbius automorphism of M; and PGL_{2,k} has dimension three.

theorem autFunctor_projectiveLine_representableBy_projectiveGeneralLinearTwo :
    (∃ R : (Scheme.autFunctor (projectiveLineOver k)).RepresentableBy
        (projectiveGeneralLinearTwoScheme k),
      ∀ {A : Type u} [CommRing A] (h : Spec (.of A) ⟶ Spec (.of k))
        (M : Matrix (Fin 2) (Fin 2) A) (hM : IsUnit M.det),
        R.homEquiv (evaluationOver h M hM) = mobiusAutFunctor h M hM) ∧
      topologicalKrullDim (projectiveGeneralLinearTwoScheme k).left = 3

AlgebraicGeometry.GenusZero.autScheme_topologicalKrullDim_eq_three_of_genus_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GenusZero/AutomorphismSchemeSmoothCurve.lean, line 90. The attribute's comment: “genus zero: the automorphism functor of a smooth proper genus zero curve over an algebraically closed field is represented by PGL_{2,k}, and every representing scheme has dimension three”.

Stacks Project, Tag 0DSV, genus zero. The automorphism group scheme of a smooth proper curve of genus zero over an algebraically closed field is PGL_{2,k} and has dimension three. The automorphism functor T ↦ Aut_T(X ×_k T) of X over k is represented by PGL_{2,k}, and every scheme representing it has dimension three.

theorem autScheme_topologicalKrullDim_eq_three_of_genus_eq_zero (hg : genus f = 0) :
    Nonempty ((Scheme.autFunctor (Over.mk f)).RepresentableBy
        (projectiveGeneralLinearTwoScheme k)) ∧
      ∀ G : Over (Spec (.of k)), (Scheme.autFunctor (Over.mk f)).RepresentableBy G →
        topologicalKrullDim G.left = 3

Tag 0DSW, a lemma

Tag 0DSW in the Stacks Project.

AlgebraicGeometry.curvesSmall.exists_deligneMumfordLocus_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesDeligneMumfordLocusUnconditional.lean, line 60.

There exists an open substack Curves^DM ⊂ Curves of the algebraic stack of curves over Spec ℤ such that

Curves^DM is the maximal open substack of Curves which is DM: it is Deligne–Mumford, and every Deligne–Mumford open substack of Curves is contained in it;

for a family of curves X → S, the classifying morphism S → Curves factors through Curves^DM if and only if the group algebraic space Aut_S(X) is unramified over S;

for a field-valued point x : Spec k → Curves, classifying a proper X of dimension ≤ 1 over k, the following are equivalent: x factors through Curves^DM; Aut(X) is geometrically reduced over k of dimension 0; Aut(X) → Spec k is unramified.

theorem exists_deligneMumfordLocus_unconditional :
    ∃ W : Stack.OpenSubstack (curvesAlgebraicStack B hZ
        (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, w} B hZ)),
      (Stack.AlgebraicStacks.IsAbsolutelyDM B integerBase hZ B.contains_terminal
          W.toAlgebraicStack ∧
        ∀ V : Stack.OpenSubstack (curvesAlgebraicStack B hZ
            (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, w} B hZ)),
          Stack.AlgebraicStacks.IsAbsolutelyDM B integerBase hZ B.contains_terminal
              V.toAlgebraicStack →
            V.property ≤ W.property) ∧
      (∀ F : CurveFamily B hZ,
        W.property (ShrinkHoms.toShrinkHoms F) ↔
          Space.IsUnramified B integerBase hZ (CurveFamily.autFunctorProjection F)) ∧
      ∀ x : Stack.FieldValuedPoint B integerBase hZ (curvesAlgebraicStack B hZ
          (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, w} B hZ)).val.val,
        List.TFAE
          [W.property x.obj,
            Space.IsGeometricallyReduced x.carrier B
                (Stack.contains_spectrum_fieldValuedPoint B integerBase hZ x)
                (Stack.automorphismGroupSpaceOverField B integerBase hZ _ x)
                (Stack.isAlgebraicSpace_automorphismGroupSpaceOverField B integerBase hZ _ x) ∧
              Space.dimension B (Spec (.of x.carrier))
                (Stack.contains_spectrum_fieldValuedPoint B integerBase hZ x)
                (Stack.automorphismGroupSpaceOverField B integerBase hZ _ x)
                (Stack.isAlgebraicSpace_automorphismGroupSpaceOverField B integerBase hZ _ x) = 0,
            Stack.IsUnramifiedAutomorphismGroupSpace B integerBase hZ
              (curvesAlgebraicStack B hZ
                (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, w} B hZ)) x]

Tag 0E6G, a lemma

Tag 0E6G in the Stacks Project.

AlgebraicGeometry.curvesSmall.tfae_curvesDMLocus_unramified_derivations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesDMLocusDerivations.lean, line 57.

Let X be a proper scheme of dimension at most one over a field k, and x : Spec k → Curves the point of the algebraic stack of curves classifying it. The following are equivalent: 1. (Stacks 0DSW (3)(a)) x factors through Curves^DM, the maximal DM open substack; 2. (Stacks 0DSW (3)(b)) Aut(X) is geometrically reduced over k and has dimension 0; 3. (Stacks 0DSW (3)(c)) Aut(X) → Spec k is unramified; 4. Der_k(𝒪_X, 𝒪_X) = 0, i.e. the type of k-derivations of 𝒪_X into 𝒪_X is a subsingleton (it has the zero derivation).

theorem tfae_curvesDMLocus_unramified_derivations :
    List.TFAE
      [Stack.dmLocus B integerBase hZ B.contains_terminal
          (curvesAlgebraicStack B hZ (curvesFiberedCategory_isAlgebraicStack.{u, w} B hZ))
          (curveFieldPoint X hk hdim (curvesFiberedCategory_isAlgebraicStack B hZ)).obj,
        Space.IsGeometricallyReduced k B hk
            (Stack.automorphismGroupSpaceOverField B integerBase hZ _
              (curveFieldPoint X hk hdim (curvesFiberedCategory_isAlgebraicStack.{u, w} B hZ)))
            (Stack.isAlgebraicSpace_automorphismGroupSpaceOverField B integerBase hZ _
              (curveFieldPoint X hk hdim (curvesFiberedCategory_isAlgebraicStack B hZ))) ∧
          Space.dimension B (Spec (.of k)) hk
            (Stack.automorphismGroupSpaceOverField B integerBase hZ _
              (curveFieldPoint X hk hdim (curvesFiberedCategory_isAlgebraicStack.{u, w} B hZ)))
            (Stack.isAlgebraicSpace_automorphismGroupSpaceOverField B integerBase hZ _
              (curveFieldPoint X hk hdim (curvesFiberedCategory_isAlgebraicStack B hZ))) = 0,
        Stack.IsUnramifiedAutomorphismGroupSpace B integerBase hZ
          (curvesAlgebraicStack B hZ (curvesFiberedCategory_isAlgebraicStack.{u, w} B hZ))
          (curveFieldPoint X hk hdim (curvesFiberedCategory_isAlgebraicStack B hZ)),
        Subsingleton (schemeMorphismDerivations (Λ := k) (k := k) (𝟙 X.left) X.hom)]

Sources

LeanAlgebraicGeometry.isClosedImmersion_doublePointsToProjectiveLine · AlgebraicGeometry.isPushout_gluingScheme · AlgebraicGeometry.gluedCurve · AlgebraicGeometry.isPushout_gluedCurve · AlgebraicGeometry.epsTranslate · AlgebraicGeometry.epsTranslate_ne_one · AlgebraicGeometry.map_fst_epsTranslate · AlgebraicGeometry.isAffineOpen_gluedCurveAffinePart

Section109.8 Cohen-Macaulay curves #

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

Tag 0E0I, a lemma

Tag 0E0I in the Stacks Project.

AlgebraicGeometry.CurveFamily.isOpen_cohenMacaulayBaseLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesCohenMacaulay.lean, line 169. The attribute's comment: “the open locus in the base”.

Stacks 0E0I. The locus of points of the base of a family of curves over which the family is Cohen–Macaulay is open.

The family is flat and locally of finite presentation, so its Cohen–Macaulay locus in the total space is open by Tag 0E10, and it is proper, so the image of the complement of that locus is closed in the base.

theorem CurveFamily.isOpen_cohenMacaulayBaseLocus (X : CurveFamily B hZ) :
    IsOpen (Space.cohenMacaulayBaseLocus B integerBase hZ X.toBase.hom)

AlgebraicGeometry.CurveFamily.preimage_cohenMacaulayBaseLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesCohenMacaulay.lean, line 179. The attribute's comment: “base change of the open locus in the base”. References: EGA IV (6.8.2), “partial”.

Stacks 0E0I. The open locus in the base over which a family of curves is Cohen–Macaulay commutes with base change: for a morphism of families of curves, the locus of the source is the inverse image of the locus of the target under the morphism of base schemes.

theorem CurveFamily.preimage_cohenMacaulayBaseLocus {X Y : CurveFamily B hZ} (φ : X ⟶ Y) :
    Space.pointsMap B integerBase hZ (schemeSpace X.base).obj (schemeSpaceMap φ.baseMap).hom ⁻¹'
        Space.cohenMacaulayBaseLocus B integerBase hZ Y.toBase.hom =
      Space.cohenMacaulayBaseLocus B integerBase hZ X.toBase.hom

AlgebraicGeometry.curvesCM_isStrictlyFull, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesCohenMacaulay.lean, line 212. The attribute's comment: “strict fullness of the Cohen–Macaulay subcategory”.

Stacks 0E0I. The condition that a family of curves be Cohen–Macaulay is invariant under isomorphism, so Curves^{CM} is a strictly full subcategory of the category of families of curves: the first of the three conditions making it an open substack.

An isomorphism of families of curves is a morphism of families, so this is base-change invariance of Cohen–Macaulayness applied to the inverse isomorphism.

theorem curvesCM_isStrictlyFull :
    (show ObjectProperty (CurveFamily B hZ) from
      IsCohenMacaulayFamily B hZ).IsClosedUnderIsomorphisms

AlgebraicGeometry.CurvesCM, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesCohenMacaulay.lean, line 220. The attribute's comment: “the Cohen–Macaulay subcategory of the category of curves”.

Stacks 0E0I. The subcategory Curves^{CM}: the strictly full subcategory of families of curves whose structure morphism is Cohen–Macaulay.

abbrev CurvesCM

AlgebraicGeometry.exists_cohenMacaulayCurves_openSubstack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesCohenMacaulayOverField.lean, line 152.

There is an open substack Curves^{CM} ⊂ Curves such that

for a family of curves X → S, the classifying morphism S → Curves factors through Curves^{CM} if and only if X → S is Cohen–Macaulay;

for a scheme X proper over a field k with dim(X) ≤ 1, the classifying morphism Spec(k) → Curves factors through Curves^{CM} if and only if X is Cohen–Macaulay.

Curves is the category fibred in groupoids of families of curves of Stacks 0D4Z, AlgebraicGeometry.curvesFiberedCategory, over the big fppf site of Spec(ℤ), and an open substack is an AlgebraicGeometry.Stack.FiberedOpenSubstack: a strictly full subcategory, fibred in groupoids (so closed under base change), whose inclusion is representable by algebraic spaces and an open immersion. That is Stacks 04YM without its clause "Curves^{CM} is an algebraic stack", which for an algebraic Curves follows from the others by Stacks 05UM, so that the two notions agree there (AlgebraicGeometry.Stack.openSubstackEquivFibered); the source produces the open substack by the method of Section 109.6, which only uses the open locus in the base and its compatibility with base change, and nothing here depends on Curves being algebraic (Stacks 0D5A).

The classifying morphism of a family F factoring through Curves^{CM} is F lying in the image on objects of the inclusion Curves^{CM} → Curves; in part (2) the family is AlgebraicGeometry.curveFamilyOfProperOverFieldEqSpec, the family X → Spec(k) attached to a proper morphism g of the site onto the spectrum of a field, and dimension is topological Krull dimension.

theorem exists_cohenMacaulayCurves_openSubstack :
    ∃ U : Stack.FiberedOpenSubstack (curvesFiberedCategory B hZ),
      (∀ F : CurveFamily B hZ,
        (∃ Y : U.toFibered.val.obj, (CatFiberedInGroupoids.homFunctor U.inclusion).obj Y = F) ↔
          IsCohenMacaulayFamily B hZ F) ∧
      (∀ {T W : BigFppfOver B integerBase hZ} (g : T ⟶ W) (k : Type u) [Field k]
          (hW : (BigFppfOver.toScheme B integerBase hZ).obj W = Spec (.of k))
          (hproper : IsProper ((BigFppfOver.toScheme B integerBase hZ).map g))
          (hdim : topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) ≤ 1),
        (∃ Y : U.toFibered.val.obj, (CatFiberedInGroupoids.homFunctor U.inclusion).obj Y =
            curveFamilyOfProperOverFieldEqSpec B hZ g k hW hproper hdim) ↔
          IsCohenMacaulay ((BigFppfOver.toScheme B integerBase hZ).obj T))

Tag 0E1F, a lemma

Tag 0E1F in the Stacks Project.

AlgebraicGeometry.CurveFamily.preimage_cohenMacaulayDimOneBaseLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesCohenMacaulay.lean, line 347. The attribute's comment: “base change of the locus in the base of Cohen–Macaulay relative dimension one”.

Stacks 0E1F. The locus in the base over which a family of curves is Cohen–Macaulay and has relative dimension one commutes with base change: for a morphism of families of curves, the locus of the source is the inverse image of the locus of the target under the morphism of base schemes.

theorem CurveFamily.preimage_cohenMacaulayDimOneBaseLocus {X Y : CurveFamily B hZ} (φ : X ⟶ Y) :
    Space.pointsMap B integerBase hZ (schemeSpace X.base).obj (schemeSpaceMap φ.baseMap).hom ⁻¹'
        CurveFamily.cohenMacaulayDimOneBaseLocus B hZ Y =
      CurveFamily.cohenMacaulayDimOneBaseLocus B hZ X

AlgebraicGeometry.CurveFamily.isOpen_relativeDimensionOneBaseLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesCohenMacaulay.lean, line 380. The attribute's comment: “the open locus in the base of relative dimension one, for a Cohen–Macaulay family”.

Stacks 0E1F. For a Cohen–Macaulay family of curves the locus in the base over which the family has relative dimension one is open.

By Tag 0E11 the total space is the disjoint union of open-and-closed subspaces of constant relative dimension, and since relative dimension at a point is unique the locus of relative dimension one in the total space is the point set of the piece of relative dimension one. That set is open, so its complement is closed, and the family is proper, so the image of that complement — the complement of the locus in the base — is closed.

theorem CurveFamily.isOpen_relativeDimensionOneBaseLocus (X : CurveFamily B hZ)
    (hX : IsCohenMacaulayFamily B hZ X) :
    IsOpen (CurveFamily.relativeDimensionOneBaseLocus B hZ X)

AlgebraicGeometry.CurveFamily.isOpen_cohenMacaulayDimOneBaseLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesCohenMacaulay.lean, line 422. The attribute's comment: “the open locus in the base of Cohen–Macaulay relative dimension one, for a CM family”.

Stacks 0E1F. For a Cohen–Macaulay family of curves the locus in the base over which the family is Cohen–Macaulay and has relative dimension one is open: the Cohen–Macaulay locus is then the whole base.

theorem CurveFamily.isOpen_cohenMacaulayDimOneBaseLocus (X : CurveFamily B hZ)
    (hX : IsCohenMacaulayFamily B hZ X) :
    IsOpen (CurveFamily.cohenMacaulayDimOneBaseLocus B hZ X)

AlgebraicGeometry.curvesCM1_isStrictlyFull, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesCohenMacaulay.lean, line 464. The attribute's comment: “strict fullness of the Cohen–Macaulay subcategory of relative dimension one”.

Stacks 0E1F. The condition that a family of curves be Cohen–Macaulay of relative dimension one is invariant under isomorphism, so Curves^{CM,1} is a strictly full subcategory of the category of families of curves: the first of the three conditions making it an open substack.

An isomorphism of families of curves is a morphism of families, so this is base-change invariance of the condition applied to the inverse isomorphism.

theorem curvesCM1_isStrictlyFull :
    (show ObjectProperty (CurveFamily B hZ) from
      IsCohenMacaulayDimOneFamily B hZ).IsClosedUnderIsomorphisms

AlgebraicGeometry.CurvesCM1, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesCohenMacaulay.lean, line 472. The attribute's comment: “the Cohen–Macaulay subcategory of relative dimension one”.

Stacks 0E1F. The subcategory Curves^{CM,1}: the strictly full subcategory of families of curves whose structure morphism is Cohen–Macaulay of relative dimension one.

abbrev CurvesCM1

AlgebraicGeometry.CurveFamily.cohenMacaulayDimOneBaseLocus_isOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesCohenMacaulayDimOne.lean, line 113. The attribute's comment: “the open locus in the base of Cohen–Macaulay relative dimension one, for an arbitrary family”.

The locus of Cohen–Macaulay relative dimension one is open. For every family of curves f : X → S, the set of points of S over which f is Cohen–Macaulay and has relative dimension one is open.

The set of points of the total space at which f is Cohen–Macaulay of relative dimension one is open (Tags 0E10 and 0E11), and f is proper, so the image of its complement — the complement of the locus — is closed.

theorem CurveFamily.cohenMacaulayDimOneBaseLocus_isOpen (X : CurveFamily B hZ) :
    IsOpen (CurveFamily.cohenMacaulayDimOneBaseLocus B hZ X)

AlgebraicGeometry.isOpenCurvesLocus_isCohenMacaulayDimOneFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesCohenMacaulayDimOne.lean, line 128. The attribute's comment: “condition (o) of 0E0E: the open locus in the base, for an arbitrary family”.

Condition (o) of Section 0E0E for Curves^{CM,1}. For every family of curves X → S there is an open subset S' of the base such that a family of curves mapping to X → S is Cohen–Macaulay of relative dimension one exactly when its base maps into S': the locus of Cohen–Macaulay relative dimension one, which is open for every family and commutes with base change.

theorem isOpenCurvesLocus_isCohenMacaulayDimOneFamily :
    IsOpenCurvesLocus B hZ (IsCohenMacaulayDimOneFamily B hZ)

AlgebraicGeometry.isCohenMacaulayDimOneFamily_curveFamilyOfSchemeMorphism_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesCohenMacaulayDimOne.lean, line 158. The attribute's comment: “part (2), on the family of curves of the proper scheme: Cohen–Macaulay and equidimensional of dimension one”.

Part (2) of Stacks 0E1F, on the family. Let g : T ⟶ U be a morphism of the big fppf site of the integers whose target scheme is the spectrum of a field k, whose underlying morphism of schemes is proper, and whose source scheme has dimension at most one. Then the family of curves of g is Cohen–Macaulay of relative dimension one exactly when the source scheme is Cohen–Macaulay and equidimensional of dimension one, every irreducible component of it having dimension one.

theorem isCohenMacaulayDimOneFamily_curveFamilyOfSchemeMorphism_iff
    {T U : BigFppfOver B integerBase hZ} (g : T ⟶ U) (k : Type u) [Field k]
    (hU : (BigFppfOver.toScheme B integerBase hZ).obj U = Spec (.of k))
    (hproper : IsProper ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hdim : topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) ≤ 1) :
    IsCohenMacaulayDimOneFamily B hZ
        (curveFamilyOfSchemeMorphism B hZ g
          (flat_of_eq_spec_field _ k hU) hproper
          (locallyOfFinitePresentation_of_eq_spec_field _ k hU)
          (Space.isQuasiCompact_yoneda_map B integerBase hZ g inferInstance)
          ((Space.isSeparated_yoneda_map_iff B integerBase hZ g).2 inferInstance)
          ((Space.isQuasiSeparated_yoneda_map_iff B integerBase hZ g).2 inferInstance)
          hdim) ↔
      (IsCohenMacaulay ((BigFppfOver.toScheme B integerBase hZ).obj T) ∧
        TopologicalSpace.Equidimensional ((BigFppfOver.toScheme B integerBase hZ).obj T) ∧
        ∀ W ∈ irreducibleComponents ((BigFppfOver.toScheme B integerBase hZ).obj T),
          topologicalKrullDim W = (1 : WithBot ℕ∞))

AlgebraicGeometry.isOpenImmersion_curvesSubstackInclusion_cohenMacaulayDimOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesCohenMacaulayDimOneSubstack.lean, line 89. The attribute's comment: “the inclusion of Curves^{CM,1} into Curves is representable by algebraic spaces and an open immersion”.

Stacks 0E1F, Curves^{CM,1} is open in Curves. The inclusion into the category fibred in groupoids of families of curves of the full subcategory Curves^{CM,1} of the families which are Cohen–Macaulay of relative dimension one is representable by algebraic spaces and an open immersion.

theorem isOpenImmersion_curvesSubstackInclusion_cohenMacaulayDimOne :
    Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (curvesSubstackInclusion B hZ (IsCohenMacaulayDimOneFamily B hZ)
          (isOpenCurvesLocus_isCohenMacaulayDimOneFamily B hZ).prop_of_hom).hom ∧
      Stack.IsOpenImmersion B integerBase hZ
        (curvesSubstackInclusion B hZ (IsCohenMacaulayDimOneFamily B hZ)
          (isOpenCurvesLocus_isCohenMacaulayDimOneFamily B hZ).prop_of_hom)

AlgebraicGeometry.factorsThrough_curvesSubstack_cohenMacaulayDimOne_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesCohenMacaulayDimOneSubstack.lean, line 103. The attribute's comment: “part (1)”.

Stacks 0E1F, part (1). Let X → S be a family of curves and z : (Sch/S) → Curves a classifying morphism for it, a scheme-valued point together with an isomorphism z(S) ≅ X. Then z factors through Curves^{CM,1}, over the site and up to a 2-isomorphism, if and only if X → S is Cohen–Macaulay and has relative dimension one.

theorem factorsThrough_curvesSubstack_cohenMacaulayDimOne_iff
    (S : BigFppfOver B integerBase hZ)
    (z : BigFppfOver B S.left.1 S.left.2 ⥤ (curvesFiberedCategory B hZ).val.obj)
    (hz : z ⋙ (curvesFiberedCategory B hZ).val.p = Over.map S.hom)
    (X : CurveFamily B hZ) (ξ : z.obj (Over.mk (𝟙 S.left)) ≅ X) :
    (∃ g : BasedCategory.ofFunctor (Over.map S.hom) ⥤ᵇ
          Stack.objectPropertySubcategory B integerBase hZ (curvesFiberedCategory B hZ).val
            (IsCohenMacaulayDimOneFamily B hZ),
        Nonempty (g.comp (Stack.objectPropertyInclusion B integerBase hZ
          (curvesFiberedCategory B hZ).val (IsCohenMacaulayDimOneFamily B hZ)) ≅
            { toFunctor := z, w := hz })) ↔
      Space.IsCohenMacaulay B integerBase hZ X.toBase.hom ∧
        Space.HasRelativeDimension 1 B integerBase hZ X.toBase.hom

AlgebraicGeometry.factorsThrough_curvesSubstack_cohenMacaulayDimOne_over_field_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesCohenMacaulayDimOneSubstack.lean, line 126. The attribute's comment: “part (2)”.

Stacks 0E1F, part (2). Let g : T ⟶ W be a morphism of the big fppf site of the integers whose target scheme is the spectrum of a field k, whose underlying morphism of schemes is proper, and whose source scheme X has dimension at most one, and let z : (Sch/Spec(k)) → Curves classify the family of curves of g. Then z factors through Curves^\{CM,1} if and only if X is Cohen–Macaulay and equidimensional of dimension one, every irreducible component of it having dimension one.

theorem factorsThrough_curvesSubstack_cohenMacaulayDimOne_over_field_iff
    {T W : BigFppfOver B integerBase hZ} (g : T ⟶ W) (k : Type u) [Field k]
    (hW : (BigFppfOver.toScheme B integerBase hZ).obj W = Spec (.of k))
    (hproper : IsProper ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hdim : topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) ≤ 1)
    (z : BigFppfOver B W.left.1 W.left.2 ⥤ (curvesFiberedCategory B hZ).val.obj)
    (hz : z ⋙ (curvesFiberedCategory B hZ).val.p = Over.map W.hom)
    (ξ : z.obj (Over.mk (𝟙 W.left)) ≅ curveFamilyOfSchemeMorphism B hZ g
      (flat_of_eq_spec_field _ k hW) hproper
      (locallyOfFinitePresentation_of_eq_spec_field _ k hW)
      (Space.isQuasiCompact_yoneda_map B integerBase hZ g inferInstance)
      ((Space.isSeparated_yoneda_map_iff B integerBase hZ g).2 inferInstance)
      ((Space.isQuasiSeparated_yoneda_map_iff B integerBase hZ g).2 inferInstance) hdim) :
    (∃ q : BasedCategory.ofFunctor (Over.map W.hom) ⥤ᵇ
          Stack.objectPropertySubcategory B integerBase hZ (curvesFiberedCategory B hZ).val
            (IsCohenMacaulayDimOneFamily B hZ),
        Nonempty (q.comp (Stack.objectPropertyInclusion B integerBase hZ
          (curvesFiberedCategory B hZ).val (IsCohenMacaulayDimOneFamily B hZ)) ≅
            { toFunctor := z, w := hz })) ↔
      (IsCohenMacaulay ((BigFppfOver.toScheme B integerBase hZ).obj T) ∧
        TopologicalSpace.Equidimensional ((BigFppfOver.toScheme B integerBase hZ).obj T) ∧
        ∀ C ∈ irreducibleComponents ((BigFppfOver.toScheme B integerBase hZ).obj T),
          topologicalKrullDim C = (1 : WithBot ℕ∞))

Sources

LeanAlgebraicGeometry.CurveFamily.isOpen_cohenMacaulayBaseLocus · AlgebraicGeometry.CurveFamily.preimage_cohenMacaulayBaseLocus · AlgebraicGeometry.curvesCM_isStrictlyFull · AlgebraicGeometry.CurvesCM · AlgebraicGeometry.exists_cohenMacaulayCurves_openSubstack · AlgebraicGeometry.CurveFamily.preimage_cohenMacaulayDimOneBaseLocus · AlgebraicGeometry.CurveFamily.isOpen_relativeDimensionOneBaseLocus · AlgebraicGeometry.CurveFamily.isOpen_cohenMacaulayDimOneBaseLocus

Section109.9 Curves of a given genus #

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

Tag 0E6I, a lemma

Tag 0E6I in the Stacks Project.

AlgebraicGeometry.curvesH01_isOpenSubstack_and_factors_iff_and_over_field_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesH01OpenSubstack.lean, line 68.

There is an open substack Curves^{h0,1} ⊂ Curves of the stack of curves — the strictly full subcategory of families with f_*𝒪_X = 𝒪_S universally and fibres of dimension 1 is invariant under isomorphism and its inclusion is representable by algebraic spaces and an open immersion — such that 1. the classifying morphism of a family of curves f : X → S factors through Curves^{h0,1} exactly when f_*𝒪_X = 𝒪_S, this holds after arbitrary base change, and the fibres of f have dimension 1; 2. for a scheme X proper over a field k with dim(X) ≤ 1, the classifying morphism Spec k → Curves of X factors through Curves^{h0,1} exactly when H⁰(X, 𝒪_X) = k and dim(X) = 1.

theorem curvesH01_isOpenSubstack_and_factors_iff_and_over_field_iff :
    (ObjectProperty.IsClosedUnderIsomorphisms (IsH01CurveFamily B hZ) ∧
      Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (curvesSubstackInclusion B hZ (IsH01CurveFamily B hZ)
          (CurveFamily.isOpenCurvesLocus_isH01CurveFamily (B := B) (hZ := hZ)).prop_of_hom).hom ∧
      Stack.IsOpenImmersion B integerBase hZ
        (curvesSubstackInclusion B hZ (IsH01CurveFamily B hZ)
          (CurveFamily.isOpenCurvesLocus_isH01CurveFamily (B := B) (hZ := hZ)).prop_of_hom)) ∧
    (∀ (U : BigFppfOver B integerBase hZ)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
      y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
      ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
          ObjectProperty.FullSubcategory (IsH01CurveFamily B hZ),
          z ⋙ ObjectProperty.ι (IsH01CurveFamily B hZ) = y) ↔
        IsH01CurveFamily B hZ (y.obj (Over.mk (𝟙 U.left))))) ∧
    (∀ {T W : BigFppfOver B integerBase hZ} (g : T ⟶ W) (k : Type u) [Field k]
      (hW : (BigFppfOver.toScheme B integerBase hZ).obj W = Spec (.of k))
      (hproper : IsProper ((BigFppfOver.toScheme B integerBase hZ).map g))
      (hdim : topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) ≤ 1)
      (U : BigFppfOver B integerBase hZ)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
      y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
      (y.obj (Over.mk (𝟙 U.left)) ≅
        curveFamilyOfSchemeMorphism B hZ g (flat_of_eq_spec_field _ k hW) hproper
          (locallyOfFinitePresentation_of_eq_spec_field _ k hW)
          (Space.isQuasiCompact_yoneda_map B integerBase hZ g inferInstance)
          ((Space.isSeparated_yoneda_map_iff B integerBase hZ g).2 inferInstance)
          ((Space.isQuasiSeparated_yoneda_map_iff B integerBase hZ g).2 inferInstance) hdim) →
      ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
          ObjectProperty.FullSubcategory (IsH01CurveFamily B hZ),
          z ⋙ ObjectProperty.ι (IsH01CurveFamily B hZ) = y) ↔
        Function.Bijective ((BigFppfOver.toScheme B integerBase hZ).map g ≫ eqToHom hW).appTop ∧
          topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) = 1))

AlgebraicGeometry.curvesH01_isOpenSubstack_and_factors_iff_and_properOverField_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesH01Unconditional.lean, line 69. The attribute's comment: “the open substack Curves^{h0,1} of Curves (closed under isomorphisms, inclusion representable by algebraic spaces and an open immersion), with (1) for a family of curves f : X → S, the classifying morphism factors through it iff f_*O_X = O_S, universally, and the fibres have dimension 1, and (2) for a scheme X proper over a field k with dim(X) ≤ 1, the classifying morphism Spec(k) → Curves factors through it iff H^0(X, O_X) = k and dim(X) = 1. Unconditional: 0E0R at i = 0 and 0E6B (a) are proved, not assumed”.

Curves^{h0,1}, the strictly full subcategory of Curves of families of curves f : X → S with f_*𝒪_X = 𝒪_S, this holding after arbitrary base change, and whose fibres have dimension 1 (AlgebraicGeometry.IsH01CurveFamily), is an open substack of Curves: it is closed under isomorphisms and its inclusion curvesSubstackInclusion is representable by algebraic spaces and an open immersion. Moreover 1. for a family of curves over a scheme S = U, classified by y (a morphism over U from the site of U to Curves), the classifying morphism factors through Curves^{h0,1} if and only if the family y(U) has f_*𝒪_X = 𝒪_S, universally, and fibres of dimension 1; 2. for a scheme X = T proper over a field k (the scheme of W being Spec k) with dim(X) ≤ 1, and y a classifying morphism Spec(k) → Curves of the attached family of curves, y factors through Curves^{h0,1} if and only if k ⟶ H⁰(X, 𝒪_X) is bijective and dim(X) = 1.

theorem curvesH01_isOpenSubstack_and_factors_iff_and_properOverField_iff :
    (ObjectProperty.IsClosedUnderIsomorphisms (IsH01CurveFamily B hZ) ∧
      Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (curvesSubstackInclusion B hZ (IsH01CurveFamily B hZ)
          CurveFamily.isOpenCurvesLocus_isH01CurveFamily.prop_of_hom).hom ∧
      Stack.IsOpenImmersion B integerBase hZ
        (curvesSubstackInclusion B hZ (IsH01CurveFamily B hZ)
          CurveFamily.isOpenCurvesLocus_isH01CurveFamily.prop_of_hom)) ∧
    (∀ (U : BigFppfOver B integerBase hZ)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
      y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
      ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
          ObjectProperty.FullSubcategory (IsH01CurveFamily B hZ),
          z ⋙ ObjectProperty.ι (IsH01CurveFamily B hZ) = y) ↔
        IsH01CurveFamily B hZ (y.obj (Over.mk (𝟙 U.left))))) ∧
    (∀ {T W : BigFppfOver B integerBase hZ} (g : T ⟶ W) (k : Type u) [Field k]
      (hW : (BigFppfOver.toScheme B integerBase hZ).obj W = Spec (.of k))
      (hproper : IsProper ((BigFppfOver.toScheme B integerBase hZ).map g))
      (hdim : topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) ≤ 1)
      (y : BigFppfOver B W.left.1 W.left.2 ⥤ CurveFamily B hZ),
      y ⋙ curvesProjectionOver B hZ = Over.map W.hom →
      (y.obj (Over.mk (𝟙 W.left)) ≅ curveFamilyOfProperOverFieldEqSpec B hZ g k hW hproper hdim) →
      ((∃ z : BigFppfOver B W.left.1 W.left.2 ⥤
          ObjectProperty.FullSubcategory (IsH01CurveFamily B hZ),
          z ⋙ ObjectProperty.ι (IsH01CurveFamily B hZ) = y) ↔
        Function.Bijective ((Scheme.ΓSpecIso (.of k)).inv ≫
            ((BigFppfOver.toScheme B integerBase hZ).map g ≫ eqToHom hW).appTop) ∧
          topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) = 1))

Tag 0E6J, a lemma

Tag 0E6J in the Stacks Project.

AlgebraicGeometry.CurveFamily.isCohenMacaulayDimOneFamily_of_hasUniversallyBijectiveGlobalFunctions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesH01.lean, line 469. The attribute's comment: “the objects of Curves^{h0,1} (f_*O_X = O_S universally and fibres of dimension 1) lie in Curves^{CM,1} (Cohen-Macaulay of relative dimension 1)”.

Stacks 0E6J. Curves^{h0,1} ⊂ Curves^{CM,1}: a family of curves f : X ⟶ S with f_*𝒪_X = 𝒪_S, universally, and all of whose fibres have dimension one is Cohen–Macaulay of relative dimension one.

At a point of X the family is the base change of the family over the spectrum of a field representing the image point; that family is again of this kind, and is Cohen–Macaulay of relative dimension one by Tag 0BY5 (AlgebraicGeometry.CurveFamily.isCohenMacaulayDimOneFamily_of_base_eq_spec). Both properties at a point are read off a base change along the cartesian square (Tags 0E10 and 04NS).

theorem CurveFamily.isCohenMacaulayDimOneFamily_of_hasUniversallyBijectiveGlobalFunctions
    (X : CurveFamily B hZ) (hΓ : HasUniversallyBijectiveGlobalFunctions B hZ X)
    (hdim : ∀ y, Space.fiberDimension B integerBase hZ X.toBase.hom y = 1) :
    IsCohenMacaulayDimOneFamily B hZ X

Tag 0E1J, a lemma

Tag 0E1J in the Stacks Project.

AlgebraicGeometry.CurveFamily.isIso_structureSharp_and_baseChange_of_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurveFamilyFirstHigherDirectImage.lean, line 190. The attribute's comment: “(1)”.

Let f : X → S be a family of curves with κ(s) = H⁰(X_s, 𝒪_{X_s}) for every point s ∈ S. Then f_*𝒪_X = 𝒪_S — the structure map 𝒪_S ⟶ f_*𝒪_X is an isomorphism — and this holds universally: the same is true of the base change of f along every morphism Y ⟶ S from an algebraic space.

theorem isIso_structureSharp_and_baseChange_of_residueField (X : CurveFamily B hZ)
    (h : X.HasResidueFieldGlobalFunctions) :
    IsIso (Space.structureSharp B integerBase hZ X.toBase) ∧
      ∀ (Y : AlgebraicSpaces B integerBase hZ) (g : Y ⟶ schemeSpace X.base),
        IsIso (Space.structureSharp B integerBase hZ (pullback.snd X.toBase g))

AlgebraicGeometry.CurveFamily.isFiniteLocallyFreeOnSite_firstDirectImage_of_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurveFamilyFirstHigherDirectImage.lean, line 203. The attribute's comment: “(2)”.

Let f : X → S be a family of curves with κ(s) = H⁰(X_s, 𝒪_{X_s}) for every point s ∈ S. Then R¹f_*𝒪_X is a finite locally free 𝒪_S-module: every object of the small étale site of S has a covering on whose members it is finite free (Stacks 03DL (2)).

theorem isFiniteLocallyFreeOnSite_firstDirectImage_of_residueField (X : CurveFamily B hZ)
    (h : X.HasResidueFieldGlobalFunctions) :
    SheafOfModules.IsFiniteLocallyFreeOnSite (X.firstDirectImage B hZ)

AlgebraicGeometry.CurveFamily.nonempty_modulePullback_firstDirectImage_iso_of_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurveFamilyFirstHigherDirectImage.lean, line 214. The attribute's comment: “(3)”.

Let f : X → S be a family of curves with κ(s) = H⁰(X_s, 𝒪_{X_s}) for every point s ∈ S. For every morphism h : S' → S, with f' : X' → S' the base change — that is, for every morphism of families of curves a : X' ⟶ X, whose square is cartesian, over h = a.baseMap — we have h^*(R¹f_*𝒪_X) ≅ R¹f'_*𝒪_{X'}.

theorem nonempty_modulePullback_firstDirectImage_iso_of_residueField (X : CurveFamily B hZ)
    (h : X.HasResidueFieldGlobalFunctions) (F : CurveFamily B hZ) (a : F ⟶ X) :
    Nonempty ((Space.modulePullback B integerBase hZ (schemeSpaceMap a.baseMap)).obj
        (X.firstDirectImage B hZ) ≅ F.firstDirectImage B hZ)

Tag 0E6K, a lemma

Tag 0E6K in the Stacks Project.

AlgebraicGeometry.curvesGenus_isOpenSubstack_and_factors_iff_and_decomposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesGenusDecomposition.lean, line 144.

Stacks 0E6K. There is a decomposition into open and closed substacks Curves^{h0,1} = ∐_{g ≥ 0} Curves_g, where (1) the classifying morphism of a family of curves f : X → S factors through Curves_g exactly when f_*𝒪_X = 𝒪_S, this holds after arbitrary base change, the fibres of f have dimension 1, and R¹f_*𝒪_X is a locally free 𝒪_S-module of rank g; and (2) for a scheme X proper over a field k with dim(X) ≤ 1, the classifying morphism Spec(k) → Curves factors through Curves_g exactly when dim(X) = 1, k = H⁰(X, 𝒪_X) and the genus of X is g.

In the statement: Curves^{h0,1} and each Curves_g are open substacks of Curves (strictly full subcategories whose inclusions are representable by algebraic spaces and open immersions), each Curves_g lies in Curves^{h0,1}, parts (1) and (2) are the factorization criteria, and the decomposition is read on every family G over a scheme S in Curves^{h0,1}: the loci in |S| of the Curves_g are open and closed, pairwise disjoint and cover |S|.

theorem curvesGenus_isOpenSubstack_and_factors_iff_and_decomposition :
    (ObjectProperty.IsClosedUnderIsomorphisms (IsH01CurveFamily B hZ) ∧
      Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (curvesSubstackInclusion B hZ (IsH01CurveFamily B hZ)
          CurveFamily.isOpenCurvesLocus_isH01CurveFamily.prop_of_hom).hom ∧
      Stack.IsOpenImmersion B integerBase hZ
        (curvesSubstackInclusion B hZ (IsH01CurveFamily B hZ)
          CurveFamily.isOpenCurvesLocus_isH01CurveFamily.prop_of_hom)) ∧
    (∀ g : ℕ,
      (ObjectProperty.IsClosedUnderIsomorphisms (IsGenusCurveFamily B hZ g) ∧
        Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
          (curvesSubstackInclusion B hZ (IsGenusCurveFamily B hZ g)
            (isGenusCurveFamily_of_hom g)).hom ∧
        Stack.IsOpenImmersion B integerBase hZ
          (curvesSubstackInclusion B hZ (IsGenusCurveFamily B hZ g)
            (isGenusCurveFamily_of_hom g))) ∧
      (∀ X : CurveFamily B hZ, IsGenusCurveFamily B hZ g X → IsH01CurveFamily B hZ X) ∧
      (∀ (U : BigFppfOver B integerBase hZ)
        (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
        y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
        ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
            ObjectProperty.FullSubcategory (IsGenusCurveFamily B hZ g),
            z ⋙ ObjectProperty.ι (IsGenusCurveFamily B hZ g) = y) ↔
          IsGenusCurveFamily B hZ g (y.obj (Over.mk (𝟙 U.left))))) ∧
      (∀ (k : Type u) [Field k] (hk : B.Contains (Spec (.of k)))
        (X : Over (Spec (.of k))) [IsProper X.hom] (hdim : topologicalKrullDim X.left ≤ 1)
        (U : BigFppfOver B integerBase hZ)
        (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
        y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
        (y.obj (Over.mk (𝟙 U.left)) ≅ curveFamilyOfScheme X B hZ hk hdim) →
        ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
            ObjectProperty.FullSubcategory (IsGenusCurveFamily B hZ g),
            z ⋙ ObjectProperty.ι (IsGenusCurveFamily B hZ g) = y) ↔
          (topologicalKrullDim X.left = 1 ∧ Function.Bijective X.hom.appTop) ∧
            genus X.hom = g))) ∧
    ∀ G : CurveFamily B hZ, IsH01CurveFamily B hZ G →
      ∃ Ω : ℕ → Set (Space.points B integerBase hZ (schemeSpace G.base).obj),
        (∀ g, IsOpen (Ω g) ∧ IsClosed (Ω g)) ∧ Pairwise (fun g g' => Disjoint (Ω g) (Ω g')) ∧
          (⋃ g, Ω g) = Set.univ ∧
          ∀ (g : ℕ) (F : CurveFamily B hZ) (a : F ⟶ G),
            IsGenusCurveFamily B hZ g F ↔
              Set.range (Space.pointsMap B integerBase hZ (schemeSpace F.base).obj
                (schemeSpaceMap a.baseMap).hom) ⊆ Ω g

Sources

LeanAlgebraicGeometry.curvesH01_isOpenSubstack_and_factors_iff_and_over_field_iff · AlgebraicGeometry.curvesH01_isOpenSubstack_and_factors_iff_and_properOverField_iff · AlgebraicGeometry.CurveFamily.isCohenMacaulayDimOneFamily_of_hasUniversallyBijectiveGlobalFunctions · AlgebraicGeometry.CurveFamily.isIso_structureSharp_and_baseChange_of_residueField · AlgebraicGeometry.CurveFamily.isFiniteLocallyFreeOnSite_firstDirectImage_of_residueField · AlgebraicGeometry.CurveFamily.nonempty_modulePullback_firstDirectImage_iso_of_residueField · AlgebraicGeometry.curvesGenus_isOpenSubstack_and_factors_iff_and_decomposition

Section109.10 Geometrically reduced curves #

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

Tag 0E0G, a lemma

Tag 0E0G in the Stacks Project.

AlgebraicGeometry.curvesGeomred_isOpenSubstack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesGeometricallyReducedOpen.lean, line 338. The attribute's comment: “the open substack Curves^{geomred} of Curves”.

Stacks 0E0G, the open substack. Curves^{geomred}, the strictly full subcategory of families of curves whose fibres are geometrically reduced (Stacks 0E08), is an open substack of Curves: its inclusion is representable by algebraic spaces and an open immersion.

theorem curvesGeomred_isOpenSubstack :
    ObjectProperty.IsClosedUnderIsomorphisms (IsGeometricallyReducedFamily B hZ) ∧
      Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (curvesSubstackInclusion B hZ _ (isOpenCurvesLocus_curvesGeomred B hZ).prop_of_hom).hom ∧
      Stack.IsOpenImmersion B integerBase hZ
        (curvesSubstackInclusion B hZ _ (isOpenCurvesLocus_curvesGeomred B hZ).prop_of_hom)

AlgebraicGeometry.factors_curvesGeomred_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesGeometricallyReducedOpen.lean, line 351. The attribute's comment: “part (1): the classifying morphism of a family of curves factors through Curves^{geomred} iff the fibres of the family are geometrically reduced”.

Stacks 0E0G, part (1). The classifying morphism of a family of curves X ⟶ S factors through Curves^{geomred} exactly when the fibres of X ⟶ S are geometrically reduced (Stacks 0E08).

theorem factors_curvesGeomred_iff (U : BigFppfOver B integerBase hZ)
    (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ)
    (hy : y ⋙ curvesProjectionOver B hZ = Over.map U.hom) :
    (∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
        (IsGeometricallyReducedFamily B hZ).FullSubcategory,
        z ⋙ (IsGeometricallyReducedFamily B hZ).ι = y) ↔
      IsGeometricallyReducedFamily B hZ (y.obj (Over.mk (𝟙 U.left)))

AlgebraicGeometry.factors_curvesGeomred_over_field_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesGeometricallyReducedOpen.lean, line 367. The attribute's comment: “part (2): for a proper scheme of dimension at most one over a field, the classifying morphism factors through Curves^{geomred} iff the scheme is geometrically reduced over the field”.

Stacks 0E0G, part (2). Let X be a proper scheme of dimension at most one over a field k (with Spec k in the site, so that the classifying morphism Spec k ⟶ Curves of X exists). The classifying morphism of X factors through Curves^{geomred} exactly when X is geometrically reduced over k.

theorem factors_curvesGeomred_over_field_iff
    (k : Type u) [Field k] (hk : B.Contains (Spec (.of k)))
    (X : Over (Spec (.of k))) [IsProper X.hom] (hdim : topologicalKrullDim X.left ≤ 1)
    (U : BigFppfOver B integerBase hZ)
    (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ)
    (hy : y ⋙ curvesProjectionOver B hZ = Over.map U.hom)
    (e : y.obj (Over.mk (𝟙 U.left)) ≅ curveFamilyOfScheme X B hZ hk hdim) :
    (∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
        (IsGeometricallyReducedFamily B hZ).FullSubcategory,
        z ⋙ (IsGeometricallyReducedFamily B hZ).ι = y) ↔
      IsGeometricallyReducedOver X.hom

AlgebraicGeometry.curvesGeomred_isOpenSubstack_and_factors_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesGeometricallyReducedOpen.lean, line 389. The attribute's comment: “the whole statement: the open substack Curves^{geomred} and parts (1) and (2)”.

Stacks 0E0G. There is an open substack Curves^{geomred} ⊂ Curves — the strictly full subcategory of families of curves with geometrically reduced fibres, whose inclusion is representable by algebraic spaces and an open immersion — such that (1) the classifying morphism of a family of curves X ⟶ S factors through it exactly when the fibres of X ⟶ S are geometrically reduced (Stacks 0E08), and (2) for a proper scheme X of dimension at most one over a field k, the classifying morphism of X factors through it exactly when X is geometrically reduced over k.

theorem curvesGeomred_isOpenSubstack_and_factors_iff :
    (ObjectProperty.IsClosedUnderIsomorphisms (IsGeometricallyReducedFamily B hZ) ∧
      Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (curvesSubstackInclusion B hZ _ (isOpenCurvesLocus_curvesGeomred B hZ).prop_of_hom).hom ∧
      Stack.IsOpenImmersion B integerBase hZ
        (curvesSubstackInclusion B hZ _ (isOpenCurvesLocus_curvesGeomred B hZ).prop_of_hom)) ∧
    (∀ (U : BigFppfOver B integerBase hZ)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
      y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
      ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
          (IsGeometricallyReducedFamily B hZ).FullSubcategory,
          z ⋙ (IsGeometricallyReducedFamily B hZ).ι = y) ↔
        IsGeometricallyReducedFamily B hZ (y.obj (Over.mk (𝟙 U.left))))) ∧
    (∀ (k : Type u) [Field k] (hk : B.Contains (Spec (.of k)))
      (X : Over (Spec (.of k))) [IsProper X.hom] (hdim : topologicalKrullDim X.left ≤ 1)
      (U : BigFppfOver B integerBase hZ)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
      y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
      (y.obj (Over.mk (𝟙 U.left)) ≅ curveFamilyOfScheme X B hZ hk hdim) →
      ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
          (IsGeometricallyReducedFamily B hZ).FullSubcategory,
          z ⋙ (IsGeometricallyReducedFamily B hZ).ι = y) ↔
        IsGeometricallyReducedOver X.hom))

Tag 0E1G, a lemma

Tag 0E1G in the Stacks Project.

AlgebraicGeometry.isCohenMacaulay_of_geometricallyReduced_of_topologicalKrullDim_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GeometricallyReducedCohenMacaulay.lean, line 85. The attribute's comment: “the inclusion read on a curve over a field, the curves being the objects of the stack parametrized by a field-valued point”. References: EGA IV (5.7.8), “special case”.

A geometrically reduced curve is Cohen–Macaulay. A scheme of dimension at most one which is locally of finite type and geometrically reduced over a field is Cohen–Macaulay.

theorem isCohenMacaulay_of_geometricallyReduced_of_topologicalKrullDim_le_one {k : Type u}
    [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [GeometricallyReduced f]
    [LocallyOfFiniteType f] (hX : topologicalKrullDim X ≤ 1) :
    IsCohenMacaulay X

AlgebraicGeometry.isCohenMacaulay_fiber_of_geometricallyReduced_of_topologicalKrullDim_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Curves/GeometricallyReducedCohenMacaulay.lean, line 97. The attribute's comment: “the inclusion read fibrewise on a family of curves”. References: EGA IV (5.7.8), “special case”.

A geometrically reduced fibre of dimension at most one is Cohen–Macaulay. For a morphism of schemes which is locally of finite type with geometrically reduced fibres, every fibre of dimension at most one is Cohen–Macaulay.

theorem isCohenMacaulay_fiber_of_geometricallyReduced_of_topologicalKrullDim_le_one
    {X S : Scheme.{u}} (f : X ⟶ S) [GeometricallyReduced f] [LocallyOfFiniteType f] (s : S)
    (hX : topologicalKrullDim (f.fiber s) ≤ 1) :
    IsCohenMacaulay (f.fiber s)

AlgebraicGeometry.Space.isCohenMacaulay_schemeSpaceMap_of_geometricallyReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesGeometricallyReduced.lean, line 55. The attribute's comment: “the inclusion read on the structure morphism of a family of curves over a field, whose Cohen–Macaulayness is the defining condition of the Cohen–Macaulay open substack”.

A geometrically reduced family of curves over a field is Cohen–Macaulay. Let g : T ⟶ U be a morphism of the big fppf site of the integers which is flat and locally of finite type, whose target scheme is the spectrum of a field, and whose source scheme is geometrically reduced of dimension at most one. Then the induced morphism of algebraic spaces is Cohen–Macaulay, which is the defining condition of Curves^{CM}.

theorem Space.isCohenMacaulay_schemeSpaceMap_of_geometricallyReduced
    {T U : BigFppfOver B integerBase hZ} (g : T ⟶ U) (k : Type u) [Field k]
    (hU : (BigFppfOver.toScheme B integerBase hZ).obj U = Spec (.of k))
    [Flat ((BigFppfOver.toScheme B integerBase hZ).map g)]
    [LocallyOfFiniteType ((BigFppfOver.toScheme B integerBase hZ).map g)]
    [GeometricallyReduced ((BigFppfOver.toScheme B integerBase hZ).map g)]
    (hdim : topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) ≤ 1) :
    Space.IsCohenMacaulay B integerBase hZ (schemeSpaceMap g).hom

AlgebraicGeometry.curvesGeomred_le_curvesCM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesGeometricallyReducedSupplement.lean, line 180. The attribute's comment: “the inclusion of the conditions cutting the two subcategories out of the category of families of curves”.

Curves^{geomred} ⊂ Curves^{CM}: a family of curves whose fibres are geometrically reduced is Cohen–Macaulay.

theorem curvesGeomred_le_curvesCM :
    (show ObjectProperty (CurveFamily B hZ) from IsGeometricallyReducedCurveFamily B hZ) ≤
      (show ObjectProperty (CurveFamily B hZ) from IsCohenMacaulayFamily B hZ)

Sources

LeanAlgebraicGeometry.curvesGeomred_isOpenSubstack · AlgebraicGeometry.factors_curvesGeomred_iff · AlgebraicGeometry.factors_curvesGeomred_over_field_iff · AlgebraicGeometry.curvesGeomred_isOpenSubstack_and_factors_iff · AlgebraicGeometry.isCohenMacaulay_of_geometricallyReduced_of_topologicalKrullDim_le_one · AlgebraicGeometry.isCohenMacaulay_fiber_of_geometricallyReduced_of_topologicalKrullDim_le_one · AlgebraicGeometry.Space.isCohenMacaulay_schemeSpaceMap_of_geometricallyReduced · AlgebraicGeometry.curvesGeomred_le_curvesCM

Section109.11 Geometrically reduced and connected curves #

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

Tag 0E1I, a lemma

Tag 0E1I in the Stacks Project.

AlgebraicGeometry.curvesGrc1_isOpenSubstack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesGrc1OpenSubstack.lean, line 101. The attribute's comment: “the open substack Curves^{grc,1} of Curves”.

Stacks 0E1I, the open substack. Curves^{grc,1}, the strictly full subcategory of families of curves whose geometric fibres are reduced, connected and of dimension 1, is an open substack of Curves: its inclusion is representable by algebraic spaces and an open immersion.

theorem curvesGrc1_isOpenSubstack :
    ObjectProperty.IsClosedUnderIsomorphisms (IsGrc1CurveFamily B hZ) ∧
      Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (curvesSubstackInclusion B hZ (IsGrc1CurveFamily B hZ)
          isOpenCurvesLocus_isGrc1CurveFamily.prop_of_hom).hom ∧
      Stack.IsOpenImmersion B integerBase hZ
        (curvesSubstackInclusion B hZ (IsGrc1CurveFamily B hZ)
          isOpenCurvesLocus_isGrc1CurveFamily.prop_of_hom)

AlgebraicGeometry.factors_curvesGrc1_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesGrc1OpenSubstack.lean, line 116. The attribute's comment: “part (1): the classifying morphism of a family of curves factors through Curves^{grc,1} iff its geometric fibres are reduced, connected and of dimension 1”.

Stacks 0E1I, part (1). The classifying morphism of a family of curves X ⟶ S factors through Curves^{grc,1} exactly when the geometric fibres of X ⟶ S are reduced, connected and of dimension 1.

theorem factors_curvesGrc1_iff (U : BigFppfOver B integerBase hZ)
    (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ)
    (hy : y ⋙ curvesProjectionOver B hZ = Over.map U.hom) :
    (∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
        ObjectProperty.FullSubcategory (IsGrc1CurveFamily B hZ),
        z ⋙ ObjectProperty.ι (IsGrc1CurveFamily B hZ) = y) ↔
      IsGrc1CurveFamily B hZ (y.obj (Over.mk (𝟙 U.left)))

AlgebraicGeometry.factors_curvesGrc1_over_field_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesGrc1OpenSubstack.lean, line 133. The attribute's comment: “part (2): for a proper scheme of dimension at most one over a field, the classifying morphism factors through Curves^{grc,1} iff the scheme is geometrically reduced, geometrically connected and of dimension 1”.

Stacks 0E1I, part (2). Let X be a proper scheme of dimension at most one over a field k (with Spec k in the site, so that the classifying morphism Spec k ⟶ Curves of X exists), and let y be a scheme-valued point of Curves over U classifying the family of curves of X. Then y factors through Curves^{grc,1} exactly when X is geometrically reduced over k, geometrically connected over k, and of dimension 1.

theorem factors_curvesGrc1_over_field_iff (k : Type u) [Field k]
    (hk : B.Contains (Spec (.of k))) (X : Over (Spec (.of k))) [IsProper X.hom]
    (hdim : topologicalKrullDim X.left ≤ 1) (U : BigFppfOver B integerBase hZ)
    (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ)
    (hy : y ⋙ curvesProjectionOver B hZ = Over.map U.hom)
    (e : y.obj (Over.mk (𝟙 U.left)) ≅ curveFamilyOfScheme X B hZ hk hdim) :
    (∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
        ObjectProperty.FullSubcategory (IsGrc1CurveFamily B hZ),
        z ⋙ ObjectProperty.ι (IsGrc1CurveFamily B hZ) = y) ↔
      GeometricallyReduced X.hom ∧ GeometricallyConnected X.hom ∧
        topologicalKrullDim X.left = 1

AlgebraicGeometry.curvesGrc1_isOpenSubstack_and_factors_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesGrc1OpenSubstack.lean, line 164. The attribute's comment: “the whole statement: the open substack Curves^{grc,1} and parts (1) and (2)”.

Stacks 0E1I. There is an open substack Curves^{grc,1} ⊂ Curves — the strictly full subcategory of families of curves whose geometric fibres are reduced, connected and of dimension 1, whose inclusion is representable by algebraic spaces and an open immersion — such that (1) the classifying morphism of a family of curves X ⟶ S factors through it exactly when the geometric fibres of X ⟶ S are reduced, connected and of dimension 1, and (2) for a proper scheme X of dimension at most one over a field k, the classifying morphism of X factors through it exactly when X is geometrically reduced, geometrically connected and of dimension 1.

theorem curvesGrc1_isOpenSubstack_and_factors_iff :
    (ObjectProperty.IsClosedUnderIsomorphisms (IsGrc1CurveFamily B hZ) ∧
      Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (curvesSubstackInclusion B hZ (IsGrc1CurveFamily B hZ)
          isOpenCurvesLocus_isGrc1CurveFamily.prop_of_hom).hom ∧
      Stack.IsOpenImmersion B integerBase hZ
        (curvesSubstackInclusion B hZ (IsGrc1CurveFamily B hZ)
          isOpenCurvesLocus_isGrc1CurveFamily.prop_of_hom)) ∧
    (∀ (U : BigFppfOver B integerBase hZ)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
      y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
      ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
          ObjectProperty.FullSubcategory (IsGrc1CurveFamily B hZ),
          z ⋙ ObjectProperty.ι (IsGrc1CurveFamily B hZ) = y) ↔
        IsGrc1CurveFamily B hZ (y.obj (Over.mk (𝟙 U.left))))) ∧
    (∀ (k : Type u) [Field k] (hk : B.Contains (Spec (.of k))) (X : Over (Spec (.of k)))
      [IsProper X.hom] (hdim : topologicalKrullDim X.left ≤ 1) (U : BigFppfOver B integerBase hZ)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
      y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
      (y.obj (Over.mk (𝟙 U.left)) ≅ curveFamilyOfScheme X B hZ hk hdim) →
      ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
          ObjectProperty.FullSubcategory (IsGrc1CurveFamily B hZ),
          z ⋙ ObjectProperty.ι (IsGrc1CurveFamily B hZ) = y) ↔
        GeometricallyReduced X.hom ∧ GeometricallyConnected X.hom ∧
          topologicalKrullDim X.left = 1))

Tag 0E6L, a lemma

Tag 0E6L in the Stacks Project.

AlgebraicGeometry.curvesGrc1_le_curvesH01_isOpenSubstack_and_firstHigherDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesGrc1H01OpenSubstacks.lean, line 51.

Curves^{grc,1} and Curves^{h0,1} are open substacks of Curves (each is closed under isomorphisms, and its inclusion into Curves is representable by algebraic spaces and an open immersion), and Curves^{grc,1} ⊂ Curves^{h0,1}. In particular, for a family of curves f : X → S whose geometric fibres are reduced, connected and of dimension 1, R¹f_*𝒪_X is a finite locally free 𝒪_S-module whose formation commutes with arbitrary base change: for every morphism h : S' → S of base schemes, h^*(R¹f_*𝒪_X) ≅ R¹f'_*𝒪_{X'} where f' : X' → S' is the base change.

The conclusions are stated for the defining properties of the substacks: IsGrc1CurveFamily and IsH01CurveFamily, the strictly full subcategories of Curves they cut out, and curvesSubstackInclusion their inclusions.

theorem curvesGrc1_le_curvesH01_isOpenSubstack_and_firstHigherDirectImage :
    (ObjectProperty.IsClosedUnderIsomorphisms (IsGrc1CurveFamily B hZ) ∧
      Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (curvesSubstackInclusion B hZ (IsGrc1CurveFamily B hZ)
          isOpenCurvesLocus_isGrc1CurveFamily.prop_of_hom).hom ∧
      Stack.IsOpenImmersion B integerBase hZ
        (curvesSubstackInclusion B hZ (IsGrc1CurveFamily B hZ)
          isOpenCurvesLocus_isGrc1CurveFamily.prop_of_hom)) ∧
    (ObjectProperty.IsClosedUnderIsomorphisms (IsH01CurveFamily B hZ) ∧
      Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (curvesSubstackInclusion B hZ (IsH01CurveFamily B hZ)
          CurveFamily.isOpenCurvesLocus_isH01CurveFamily.prop_of_hom).hom ∧
      Stack.IsOpenImmersion B integerBase hZ
        (curvesSubstackInclusion B hZ (IsH01CurveFamily B hZ)
          CurveFamily.isOpenCurvesLocus_isH01CurveFamily.prop_of_hom)) ∧
    IsGrc1CurveFamily B hZ ≤ IsH01CurveFamily B hZ ∧
    ∀ X : CurveFamily B hZ, IsGrc1CurveFamily B hZ X →
      X.HasFiniteLocallyFreeFirstHigherDirectImage ∧
        X.FirstHigherDirectImageCommutesWithBaseChange

Tag 0E1K, a lemma

Tag 0E1K in the Stacks Project.

AlgebraicGeometry.curvesGrcDimOne_genus_decomposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesReducedConnectedGenusDecomposition.lean, line 454. The attribute's comment: “the decomposition Curves^{grc,1} = ∐_g Curves^{grc,1}_g into open and closed substacks (each inclusion representable, an open and a closed immersion; on the base of every object the genus loci are clopen, disjoint and covering), with the characterizations (1) and (2)”.

Stacks 0E1K. There is a decomposition into open and closed substacks Curves^{grc,1} = ∐_{g ≥ 0} Curves^{grc,1}_g, where Curves^{grc,1} is the stack of families of curves whose geometric fibres are reduced, connected and of dimension 1 (AlgebraicGeometry.curvesGrcDimOne) and Curves^{grc,1}_g its full subcategory AlgebraicGeometry.curvesGrcDimOneOfGenus:

each Curves^{grc,1}_g ⊂ Curves^{grc,1} is an open and closed substack — strictly full, with inclusion representable by algebraic spaces, an open immersion and a closed immersion;

they decompose Curves^{grc,1}: over the base S of every family in Curves^{grc,1} their loci are open and closed, pairwise disjoint and cover S, and a family mapping to it lies in Curves^{grc,1}_g exactly when its base maps into the locus of g;

(1) the classifying morphism S → Curves of a family of curves f : X → S factors through Curves^{grc,1}_g exactly when the geometric fibres of f are reduced, connected, of dimension 1 and R¹f_*𝒪_X is a locally free 𝒪_S-module of rank g;

(2) for a proper scheme X over a field k with dim(X) ≤ 1, the classifying morphism Spec(k) → Curves factors through Curves^{grc,1}_g exactly when X is geometrically reduced, geometrically connected, of dimension 1 and of genus g.

theorem curvesGrcDimOne_genus_decomposition :
    (∀ g : ℕ, (IsGrcDimOneFibreGenus B hZ g).IsClosedUnderIsomorphisms ∧
      Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (curvesGrcDimOneOfGenusInclusion B hZ g).hom ∧
      Stack.IsOpenImmersion B integerBase hZ (curvesGrcDimOneOfGenusInclusion B hZ g) ∧
      Stack.IsClosedImmersion B integerBase hZ (curvesGrcDimOneOfGenusInclusion B hZ g)) ∧
    (∀ X : (IsGrcDimOneFamily B hZ).FullSubcategory,
      (∀ g, IsClopen (CurveFamily.fibreGenusLocus B hZ X.obj g)) ∧
      Pairwise (fun g g' => Disjoint (CurveFamily.fibreGenusLocus B hZ X.obj g)
        (CurveFamily.fibreGenusLocus B hZ X.obj g')) ∧
      (⋃ g, CurveFamily.fibreGenusLocus B hZ X.obj g) = Set.univ ∧
      ∀ (g : ℕ) (F : (IsGrcDimOneFamily B hZ).FullSubcategory) (a : F ⟶ X),
        (IsGrcDimOneFibreGenus B hZ g F ↔
          Set.range (Space.pointsMap B integerBase hZ (schemeSpace F.obj.base).obj
            (schemeSpaceMap a.hom.baseMap).hom) ⊆ CurveFamily.fibreGenusLocus B hZ X.obj g)) ∧
    (∀ (g : ℕ) (U : BigFppfOver B integerBase hZ)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
      y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
      ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤ (IsGrcDimOneFibreGenus B hZ g).FullSubcategory,
          z ⋙ (IsGrcDimOneFibreGenus B hZ g).ι ⋙ (IsGrcDimOneFamily B hZ).ι = y) ↔
        IsGrcDimOneFamily B hZ (y.obj (Over.mk (𝟙 U.left))) ∧
          CurveFamily.HasGenus B hZ (y.obj (Over.mk (𝟙 U.left))) g)) ∧
    (∀ (g : ℕ) (k : Type u) [Field k] (hk : B.Contains (Spec (.of k)))
      (X : Over (Spec (.of k))) [IsProper X.hom] (hdim : topologicalKrullDim X.left ≤ 1)
      (U : BigFppfOver B integerBase hZ)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
      y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
      (y.obj (Over.mk (𝟙 U.left)) ≅ curveFamilyOfScheme X B hZ hk hdim) →
      ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤ (IsGrcDimOneFibreGenus B hZ g).FullSubcategory,
          z ⋙ (IsGrcDimOneFibreGenus B hZ g).ι ⋙ (IsGrcDimOneFamily B hZ).ι = y) ↔
        IsGeometricallyReducedOver X.hom ∧ GeometricallyConnected X.hom ∧
          topologicalKrullDim X.left = 1 ∧ genus X.hom = g))

Sources

LeanAlgebraicGeometry.curvesGrc1_isOpenSubstack · AlgebraicGeometry.factors_curvesGrc1_iff · AlgebraicGeometry.factors_curvesGrc1_over_field_iff · AlgebraicGeometry.curvesGrc1_isOpenSubstack_and_factors_iff · AlgebraicGeometry.curvesGrc1_le_curvesH01_isOpenSubstack_and_firstHigherDirectImage · AlgebraicGeometry.curvesGrcDimOne_genus_decomposition

Section109.12 Gorenstein curves #

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

Tag 0E1M, a lemma

Tag 0E1M in the Stacks Project.

AlgebraicGeometry.isOpenImmersion_curvesSubstackInclusion_gorenstein, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesGorensteinSubstack.lean, line 84. The attribute's comment: “the inclusion of Curves^{Gorenstein} into Curves is representable by algebraic spaces and an open immersion”.

Stacks 0E1M, Curves^{Gorenstein} is open in Curves. The inclusion into the category fibred in groupoids of families of curves of the full subcategory Curves^{Gorenstein} of the Gorenstein families is representable by algebraic spaces and an open immersion.

theorem isOpenImmersion_curvesSubstackInclusion_gorenstein :
    Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (curvesSubstackInclusion B hZ (IsGorensteinFamily B hZ)
          (isOpenCurvesLocus_isGorensteinFamily B hZ).prop_of_hom).hom ∧
      Stack.IsOpenImmersion B integerBase hZ
        (curvesSubstackInclusion B hZ (IsGorensteinFamily B hZ)
          (isOpenCurvesLocus_isGorensteinFamily B hZ).prop_of_hom)

AlgebraicGeometry.factorsThrough_curvesSubstack_gorenstein_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesGorensteinSubstack.lean, line 98. The attribute's comment: “part (1)”.

Stacks 0E1M, part (1). Let X → S be a family of curves and z : (Sch/S) → Curves a classifying morphism for it, a scheme-valued point together with an isomorphism z(S) ≅ X. Then z factors through Curves^{Gorenstein}, over the site and up to a 2-isomorphism, if and only if X → S is Gorenstein.

theorem factorsThrough_curvesSubstack_gorenstein_iff
    (S : BigFppfOver B integerBase hZ)
    (z : BigFppfOver B S.left.1 S.left.2 ⥤ (curvesFiberedCategory B hZ).val.obj)
    (hz : z ⋙ (curvesFiberedCategory B hZ).val.p = Over.map S.hom)
    (X : CurveFamily B hZ) (ξ : z.obj (Over.mk (𝟙 S.left)) ≅ X) :
    (∃ g : BasedCategory.ofFunctor (Over.map S.hom) ⥤ᵇ
          Stack.objectPropertySubcategory B integerBase hZ (curvesFiberedCategory B hZ).val
            (IsGorensteinFamily B hZ),
        Nonempty (g.comp (Stack.objectPropertyInclusion B integerBase hZ
          (curvesFiberedCategory B hZ).val (IsGorensteinFamily B hZ)) ≅
            { toFunctor := z, w := hz })) ↔
      Space.IsGorenstein B integerBase hZ X.toBase.hom

AlgebraicGeometry.factorsThrough_curvesSubstack_gorenstein_over_field_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesGorensteinSubstack.lean, line 118. The attribute's comment: “part (2)”.

Stacks 0E1M, part (2). Let g : T ⟶ W be a morphism of the big fppf site of the integers whose target scheme is the spectrum of a field k, whose underlying morphism of schemes is proper, and whose source scheme X has dimension at most one, and let z : (Sch/Spec(k)) → Curves classify the family of curves of g. Then z factors through Curves^\{Gorenstein} if and only if X is Gorenstein.

theorem factorsThrough_curvesSubstack_gorenstein_over_field_iff
    {T W : BigFppfOver B integerBase hZ} (g : T ⟶ W) (k : Type u) [Field k]
    (hW : (BigFppfOver.toScheme B integerBase hZ).obj W = Spec (.of k))
    (hproper : IsProper ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hdim : topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) ≤ 1)
    (z : BigFppfOver B W.left.1 W.left.2 ⥤ (curvesFiberedCategory B hZ).val.obj)
    (hz : z ⋙ (curvesFiberedCategory B hZ).val.p = Over.map W.hom)
    (ξ : z.obj (Over.mk (𝟙 W.left)) ≅ curveFamilyOfSchemeMorphism B hZ g
      (flat_of_eq_spec_field _ k hW) hproper
      (locallyOfFinitePresentation_of_eq_spec_field _ k hW)
      (Space.isQuasiCompact_yoneda_map B integerBase hZ g inferInstance)
      ((Space.isSeparated_yoneda_map_iff B integerBase hZ g).2 inferInstance)
      ((Space.isQuasiSeparated_yoneda_map_iff B integerBase hZ g).2 inferInstance) hdim) :
    (∃ q : BasedCategory.ofFunctor (Over.map W.hom) ⥤ᵇ
          Stack.objectPropertySubcategory B integerBase hZ (curvesFiberedCategory B hZ).val
            (IsGorensteinFamily B hZ),
        Nonempty (q.comp (Stack.objectPropertyInclusion B integerBase hZ
          (curvesFiberedCategory B hZ).val (IsGorensteinFamily B hZ)) ≅
            { toFunctor := z, w := hz })) ↔
      IsGorenstein ((BigFppfOver.toScheme B integerBase hZ).obj T)

Tag 0E6M, a lemma

Tag 0E6M in the Stacks Project.

AlgebraicGeometry.isOpenImmersion_curvesSubstackInclusion_gorensteinDimOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesGorensteinDimOneSubstack.lean, line 121. The attribute's comment: “the inclusion of Curves^{Gorenstein,1} into Curves is representable by algebraic spaces and an open immersion”.

Curves^{Gorenstein,1} is open in Curves. The inclusion into the category fibred in groupoids of families of curves of the full subcategory Curves^{Gorenstein,1} of the families which are Gorenstein of relative dimension one is representable by algebraic spaces and an open immersion.

theorem isOpenImmersion_curvesSubstackInclusion_gorensteinDimOne :
    Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (curvesSubstackInclusion B hZ (IsGorensteinDimOneFamily B hZ)
          (isOpenCurvesLocus_isGorensteinDimOneFamily B hZ
            (isOpenCurvesLocus_isGorensteinFamily_and_over_field_iff B hZ)).prop_of_hom).hom ∧
      Stack.IsOpenImmersion B integerBase hZ
        (curvesSubstackInclusion B hZ (IsGorensteinDimOneFamily B hZ)
          (isOpenCurvesLocus_isGorensteinDimOneFamily B hZ
            (isOpenCurvesLocus_isGorensteinFamily_and_over_field_iff B hZ)).prop_of_hom)

AlgebraicGeometry.factorsThrough_curvesSubstack_gorensteinDimOne_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesGorensteinDimOneSubstack.lean, line 144. The attribute's comment: “part (1)”.

Let X → S be a family of curves and z : (Sch/S) → Curves a classifying morphism for it, a scheme-valued point together with an isomorphism z(S) ≅ X. Then z factors through Curves^{Gorenstein,1}, over the site and up to a 2-isomorphism, if and only if X → S is Gorenstein and has relative dimension one.

theorem factorsThrough_curvesSubstack_gorensteinDimOne_iff
    (S : BigFppfOver B integerBase hZ)
    (z : BigFppfOver B S.left.1 S.left.2 ⥤ (curvesFiberedCategory B hZ).val.obj)
    (hz : z ⋙ (curvesFiberedCategory B hZ).val.p = Over.map S.hom)
    (X : CurveFamily B hZ) (ξ : z.obj (Over.mk (𝟙 S.left)) ≅ X) :
    (∃ g : BasedCategory.ofFunctor (Over.map S.hom) ⥤ᵇ
          Stack.objectPropertySubcategory B integerBase hZ (curvesFiberedCategory B hZ).val
            (IsGorensteinDimOneFamily B hZ),
        Nonempty (g.comp (Stack.objectPropertyInclusion B integerBase hZ
          (curvesFiberedCategory B hZ).val (IsGorensteinDimOneFamily B hZ)) ≅
            { toFunctor := z, w := hz })) ↔
      Space.IsGorenstein B integerBase hZ X.toBase.hom ∧
        Space.HasRelativeDimension 1 B integerBase hZ X.toBase.hom

AlgebraicGeometry.factorsThrough_curvesSubstack_gorensteinDimOne_over_field_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesGorensteinDimOneSubstack.lean, line 165. The attribute's comment: “part (2)”.

Let g : T ⟶ W be a morphism of the big fppf site of the integers whose target scheme is the spectrum of a field k, whose underlying morphism of schemes is proper, and whose source scheme X has dimension at most one, and let z : (Sch/Spec(k)) → Curves classify the family of curves of g. Then z factors through Curves^{Gorenstein,1} if and only if X is Gorenstein and equidimensional of dimension one, every irreducible component of it having dimension one.

theorem factorsThrough_curvesSubstack_gorensteinDimOne_over_field_iff
    {T W : BigFppfOver B integerBase hZ} (g : T ⟶ W) (k : Type u) [Field k]
    (hW : (BigFppfOver.toScheme B integerBase hZ).obj W = Spec (.of k))
    (hproper : IsProper ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hdim : topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) ≤ 1)
    (z : BigFppfOver B W.left.1 W.left.2 ⥤ (curvesFiberedCategory B hZ).val.obj)
    (hz : z ⋙ (curvesFiberedCategory B hZ).val.p = Over.map W.hom)
    (ξ : z.obj (Over.mk (𝟙 W.left)) ≅ curveFamilyOfSchemeMorphism B hZ g
      (flat_of_eq_spec_field _ k hW) hproper
      (locallyOfFinitePresentation_of_eq_spec_field _ k hW)
      (Space.isQuasiCompact_yoneda_map B integerBase hZ g inferInstance)
      ((Space.isSeparated_yoneda_map_iff B integerBase hZ g).2 inferInstance)
      ((Space.isQuasiSeparated_yoneda_map_iff B integerBase hZ g).2 inferInstance) hdim) :
    (∃ q : BasedCategory.ofFunctor (Over.map W.hom) ⥤ᵇ
          Stack.objectPropertySubcategory B integerBase hZ (curvesFiberedCategory B hZ).val
            (IsGorensteinDimOneFamily B hZ),
        Nonempty (q.comp (Stack.objectPropertyInclusion B integerBase hZ
          (curvesFiberedCategory B hZ).val (IsGorensteinDimOneFamily B hZ)) ≅
            { toFunctor := z, w := hz })) ↔
      (IsGorenstein ((BigFppfOver.toScheme B integerBase hZ).obj T) ∧
        TopologicalSpace.Equidimensional ((BigFppfOver.toScheme B integerBase hZ).obj T) ∧
        ∀ C ∈ irreducibleComponents ((BigFppfOver.toScheme B integerBase hZ).obj T),
          topologicalKrullDim C = (1 : WithBot ℕ∞))

Sources

LeanAlgebraicGeometry.isOpenImmersion_curvesSubstackInclusion_gorenstein · AlgebraicGeometry.factorsThrough_curvesSubstack_gorenstein_iff · AlgebraicGeometry.factorsThrough_curvesSubstack_gorenstein_over_field_iff · AlgebraicGeometry.isOpenImmersion_curvesSubstackInclusion_gorensteinDimOne · AlgebraicGeometry.factorsThrough_curvesSubstack_gorensteinDimOne_iff · AlgebraicGeometry.factorsThrough_curvesSubstack_gorensteinDimOne_over_field_iff

Section109.13 Local complete intersection curves #

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

Tag 0DZV, a lemma

Tag 0DZV in the Stacks Project.

AlgebraicGeometry.isLciFamily_iff_isSyntomicFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesLocalCompleteIntersection.lean, line 135. The attribute's comment: “part (1), the equivalence of (b) and (c) for a family of curves: its structure morphism is a local complete intersection morphism if and only if it is syntomic”.

Stacks 0DZV, part (1). The equivalence of conditions (b) and (c): a family of curves has a local complete intersection structure morphism exactly when its structure morphism is syntomic.

A syntomic morphism of algebraic spaces is one which is flat and a local complete intersection morphism, by Tag 06C9, and the structure morphism of a family of curves is flat, so the flatness half of that conjunction is supplied by the family itself.

theorem isLciFamily_iff_isSyntomicFamily (X : CurveFamily B hZ) :
    IsLciFamily B hZ X ↔ Space.IsSyntomic B integerBase hZ X.toBase.hom

AlgebraicGeometry.curvesLci_isStrictlyFull, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesLocalCompleteIntersection.lean, line 174. The attribute's comment: “strict fullness of the local complete intersection subcategory of the category of families of curves, which is the first of the three conditions of Tag 04YM making it an open substack; the remaining two rest on the algebraicity of the stack of curves (Tag 0D5A), which this library does not have”.

Stacks 0DZV. The condition that a family of curves have a local complete intersection structure morphism is invariant under isomorphism, so Curves^{lci} is a strictly full subcategory of the category of families of curves: the first of the three conditions making it an open substack.

An isomorphism of families of curves is a morphism of families, so this is base-change invariance of the condition applied to the inverse isomorphism.

theorem curvesLci_isStrictlyFull :
    (show ObjectProperty (CurveFamily B hZ) from
      IsLciFamily B hZ).IsClosedUnderIsomorphisms

AlgebraicGeometry.CurvesLci, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesLocalCompleteIntersection.lean, line 185. The attribute's comment: “the local complete intersection subcategory of the category of families of curves, which is the underlying full subcategory of the open substack Curves^{lci} of the source; the stack of curves is not constructed in this library, so this is a subcategory of the category of families of curves of Tag 0D4Z and not an open substack of a stack”.

Stacks 0DZV. The subcategory Curves^{lci}: the strictly full subcategory of families of curves whose structure morphism is a local complete intersection morphism.

abbrev CurvesLci

AlgebraicGeometry.isLciFamily_curveFamilyOfSchemeMorphism_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesLocalCompleteIntersection.lean, line 211. The attribute's comment: “part (2), condition (b): for the family of curves attached to a proper flat morphism of schemes of finite presentation whose source has dimension at most one, the structure morphism of the family is a local complete intersection morphism if and only if that morphism of schemes is one, i.e. — over the spectrum of a field — if and only if the proper scheme is a local complete intersection over the field”.

Stacks 0DZV, part (2). Condition (b) read on the family of curves attached to a proper flat morphism of schemes of finite presentation whose source has dimension at most one: that family has a local complete intersection structure morphism exactly when the morphism of schemes is a local complete intersection morphism.

Over the spectrum of a field the right-hand side is the condition that the proper scheme be a local complete intersection over that field, which is condition (b) of part (2) of the source; see AlgebraicGeometry.factorsThroughCurvesLci_over_field_iff. No hypothesis on the base is needed, so the statement is proved over an arbitrary base scheme of the site.

Both sides pass through syntomicity. The every-étale-chart condition of Tag 03MJ at a morphism of the site is the scheme-level condition itself for a property étale local on the source and target, which syntomicity is by Tag 04R3; at the level of schemes syntomicity is flatness together with the local complete intersection property by Tag 069K, and the morphism is flat by hypothesis; at the level of algebraic spaces it is the same conjunction by Tag 06C9, whose flatness half the family supplies.

theorem isLciFamily_curveFamilyOfSchemeMorphism_iff
    {T W : BigFppfOver B integerBase hZ} (g : T ⟶ W)
    (hflat : Flat ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hproper : IsProper ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hlfp : LocallyOfFinitePresentation ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hqc : Space.IsQuasiCompact B integerBase hZ (schemeSpaceMap g).hom)
    (hsep : Space.IsSeparated B integerBase hZ (schemeSpaceMap g).hom)
    (hqsep : Space.IsQuasiSeparated B integerBase hZ (schemeSpaceMap g).hom)
    (hdim : topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) ≤ 1) :
    IsLciFamily B hZ
        (curveFamilyOfSchemeMorphism B hZ g hflat hproper hlfp hqc hsep hqsep hdim) ↔
      IsLocalCompleteIntersectionMorphism
        ((BigFppfOver.toScheme B integerBase hZ).map g)

AlgebraicGeometry.factorsThroughCurvesLci_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesLocalCompleteIntersection.lean, line 258. The attribute's comment: “part (1), the equivalence of (a) and (b): the classifying 1-morphism factors through the local complete intersection substack if and only if every family of curves in its image has a local complete intersection structure morphism. The stack of curves is not constructed in this library (Tag 0D5A is not proved here), so the algebraic stack, the identification of its objects with families of curves, and the open substack together with its specification are carried as explicit named hypotheses”.

Stacks 0DZV, part (1). The equivalence of conditions (a) and (b). Let 𝒳 be an algebraic stack over the big fppf site of the integers whose objects are identified with families of curves by Φ, and let V be an open substack of 𝒳 whose objects are exactly those identified with families having a local complete intersection structure morphism. Then a 1-morphism into 𝒳 from a category over the site factors through V, over the site and up to a 2-isomorphism, if and only if every family of curves in its image has a local complete intersection structure morphism.

This result assumes what Stacks 0D5A would supply and this library does not have: an algebraic stack of curves, and the fact that the local complete intersection condition cuts an open substack out of it. Granted those, it is the criterion of Stacks 0507 together with the translation of membership of the substack into the condition on the corresponding family.

theorem factorsThroughCurvesLci_iff
    {𝒳 : Stack.AlgebraicStacks.{u, w} B integerBase hZ}
    (Φ : 𝒳.val.val.obj ⥤ CurveFamily B hZ) (V : Stack.OpenSubstack 𝒳)
    (hV : ∀ Z : 𝒳.val.val.obj, V.property Z ↔ IsLciFamily B hZ (Φ.obj Z))
    {𝒟 : BasedCategory.{u, u + 1} (BigFppfOver B integerBase hZ)} (f : 𝒟 ⥤ᵇ 𝒳.val.val) :
    (∃ q : 𝒟 ⥤ᵇ Stack.fullSubcategoryBased 𝒳 V.property,
        Nonempty (q.comp (Stack.fullSubcategoryBasedInclusion 𝒳 V.property) ≅ f)) ↔
      ∀ Y : 𝒟.obj, IsLciFamily B hZ (Φ.obj (f.obj Y))

AlgebraicGeometry.factorsThroughCurvesLci_over_field_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesLocalCompleteIntersection.lean, line 299. The attribute's comment: “part (2), the equivalence of (a) and (b): for a proper flat morphism of finite presentation from a scheme of dimension at most one to the spectrum of a field, the classifying 1-morphism factors through the local complete intersection substack if and only if the source is a local complete intersection over that field. As in part (1) the algebraic stack of curves, the identification of its objects with families of curves, and the open substack together with its specification are carried as explicit named hypotheses, the stack of curves not being constructed in this library. The hypothesis that the base be the spectrum of a field is kept, making this the instance the source states, but is not used: the equivalence holds over any base scheme of the site”.

Stacks 0DZV, part (2). The equivalence of conditions (a) and (b) for a proper scheme over a field of dimension at most one. Let X → Spec(k) be a proper flat morphism of schemes of finite presentation over a field k whose source has dimension at most one, and let f be a 1-morphism into the stack of curves all of whose objects classify the attached family of curves. Then f factors through the local complete intersection open substack exactly when X is a local complete intersection over k, that is, exactly when X → Spec(k) is a local complete intersection morphism.

The hypothesis _hk that the base be the spectrum of a field is what makes this the statement of part (2) of the source rather than a statement over an arbitrary base, and it is deliberately kept although the argument does not use it: the underlying equivalence AlgebraicGeometry.isLciFamily_curveFamilyOfSchemeMorphism_iff holds over an arbitrary base scheme of the site, so this statement is a strict instance of it and nothing is weakened by its presence. Nonemptiness of the source category of f is used, to convert the universally quantified right-hand side of AlgebraicGeometry.factorsThroughCurvesLci_iff into the single condition the source states. Properness, finite presentation, flatness and the dimension bound are the hypotheses of AlgebraicGeometry.curveFamilyOfSchemeMorphism and are all used, through it.

Like AlgebraicGeometry.factorsThroughCurvesLci_iff this assumes an algebraic stack of curves and that the condition cuts an open substack out of it; neither is available in this library, Stacks 0D5A not being proved here.

theorem factorsThroughCurvesLci_over_field_iff
    {𝒳 : Stack.AlgebraicStacks.{u, w} B integerBase hZ}
    (Φ : 𝒳.val.val.obj ⥤ CurveFamily B hZ) (V : Stack.OpenSubstack 𝒳)
    (hV : ∀ Z : 𝒳.val.val.obj, V.property Z ↔ IsLciFamily B hZ (Φ.obj Z))
    {T W : BigFppfOver B integerBase hZ} (g : T ⟶ W)
    (hflat : Flat ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hproper : IsProper ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hlfp : LocallyOfFinitePresentation ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hqc : Space.IsQuasiCompact B integerBase hZ (schemeSpaceMap g).hom)
    (hsep : Space.IsSeparated B integerBase hZ (schemeSpaceMap g).hom)
    (hqsep : Space.IsQuasiSeparated B integerBase hZ (schemeSpaceMap g).hom)
    (hdim : topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) ≤ 1)
    (k : Type u) [Field k]
    (_hk : (BigFppfOver.toScheme B integerBase hZ).obj W = Spec (.of k))
    {𝒟 : BasedCategory.{u, u + 1} (BigFppfOver B integerBase hZ)} (f : 𝒟 ⥤ᵇ 𝒳.val.val)
    (hne : Nonempty 𝒟.obj)
    (hf : ∀ Y : 𝒟.obj, Φ.obj (f.obj Y) =
      curveFamilyOfSchemeMorphism B hZ g hflat hproper hlfp hqc hsep hqsep hdim) :
    (∃ q : 𝒟 ⥤ᵇ Stack.fullSubcategoryBased 𝒳 V.property,
        Nonempty (q.comp (Stack.fullSubcategoryBasedInclusion 𝒳 V.property) ≅ f)) ↔
      IsLocalCompleteIntersectionMorphism
        ((BigFppfOver.toScheme B integerBase hZ).map g)

AlgebraicGeometry.isOpenImmersion_curvesSubstackInclusion_lci, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesLocalCompleteIntersectionSubstack.lean, line 101. The attribute's comment: “the inclusion of Curves^{lci} into Curves is representable by algebraic spaces and an open immersion”.

Stacks 0DZV, Curves^{lci} is open in Curves. The inclusion into the category fibred in groupoids of families of curves of the full subcategory Curves^{lci} of the families whose structure morphism is a local complete intersection morphism is representable by algebraic spaces and an open immersion.

theorem isOpenImmersion_curvesSubstackInclusion_lci :
    Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (curvesSubstackInclusion B hZ (IsLciFamily B hZ)
          (isOpenCurvesLocus_isLciFamily B hZ).prop_of_hom).hom ∧
      Stack.IsOpenImmersion B integerBase hZ
        (curvesSubstackInclusion B hZ (IsLciFamily B hZ)
          (isOpenCurvesLocus_isLciFamily B hZ).prop_of_hom)

AlgebraicGeometry.factorsThrough_curvesSubstack_lci_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesLocalCompleteIntersectionSubstack.lean, line 118. The attribute's comment: “part (1)”.

Stacks 0DZV, part (1). Let X → S be a family of curves and z : (Sch/S) → Curves a classifying morphism for it, a scheme-valued point together with an isomorphism z(S) ≅ X. Then the following are equivalent:

(a) z factors through Curves^{lci}, over the site and up to a 2-isomorphism;

(b) X → S is a local complete intersection morphism;

(c) X → S is syntomic.

theorem factorsThrough_curvesSubstack_lci_tfae (S : BigFppfOver B integerBase hZ)
    (z : BigFppfOver B S.left.1 S.left.2 ⥤ (curvesFiberedCategory B hZ).val.obj)
    (hz : z ⋙ (curvesFiberedCategory B hZ).val.p = Over.map S.hom)
    (X : CurveFamily B hZ) (ξ : z.obj (Over.mk (𝟙 S.left)) ≅ X) :
    List.TFAE
      [∃ g : BasedCategory.ofFunctor (Over.map S.hom) ⥤ᵇ
            Stack.objectPropertySubcategory B integerBase hZ
              (curvesFiberedCategory B hZ).val (IsLciFamily B hZ),
          Nonempty (g.comp (Stack.objectPropertyInclusion B integerBase hZ
            (curvesFiberedCategory B hZ).val (IsLciFamily B hZ)) ≅ { toFunctor := z, w := hz }),
        Space.IsLocalCompleteIntersection B integerBase hZ X.toBase.hom,
        Space.IsSyntomic B integerBase hZ X.toBase.hom]

AlgebraicGeometry.factorsThrough_curvesSubstack_lci_over_field_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesLocalCompleteIntersectionSubstack.lean, line 142. The attribute's comment: “part (2)”.

Stacks 0DZV, part (2). Let g : T ⟶ W be a morphism of the big fppf site of the integers whose target scheme is the spectrum of a field k, whose underlying morphism of schemes is proper, and whose source scheme X has dimension at most one, and let z : (Sch/Spec(k)) → Curves classify the family of curves of g. Then z factors through Curves^\{lci} if and only if X is a local complete intersection over k, that is, g is a local complete intersection morphism.

theorem factorsThrough_curvesSubstack_lci_over_field_iff
    {T W : BigFppfOver B integerBase hZ} (g : T ⟶ W) (k : Type u) [Field k]
    (hW : (BigFppfOver.toScheme B integerBase hZ).obj W = Spec (.of k))
    (hproper : IsProper ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hdim : topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) ≤ 1)
    (z : BigFppfOver B W.left.1 W.left.2 ⥤ (curvesFiberedCategory B hZ).val.obj)
    (hz : z ⋙ (curvesFiberedCategory B hZ).val.p = Over.map W.hom)
    (ξ : z.obj (Over.mk (𝟙 W.left)) ≅ curveFamilyOfSchemeMorphism B hZ g
      (flat_of_eq_spec_field _ k hW) hproper
      (locallyOfFinitePresentation_of_eq_spec_field _ k hW)
      (Space.isQuasiCompact_yoneda_map B integerBase hZ g inferInstance)
      ((Space.isSeparated_yoneda_map_iff B integerBase hZ g).2 inferInstance)
      ((Space.isQuasiSeparated_yoneda_map_iff B integerBase hZ g).2 inferInstance) hdim) :
    (∃ q : BasedCategory.ofFunctor (Over.map W.hom) ⥤ᵇ
          Stack.objectPropertySubcategory B integerBase hZ
            (curvesFiberedCategory B hZ).val (IsLciFamily B hZ),
        Nonempty (q.comp (Stack.objectPropertyInclusion B integerBase hZ
          (curvesFiberedCategory B hZ).val (IsLciFamily B hZ)) ≅
            { toFunctor := z, w := hz })) ↔
      IsLocalCompleteIntersectionMorphism ((BigFppfOver.toScheme B integerBase hZ).map g)

Sources

LeanAlgebraicGeometry.isLciFamily_iff_isSyntomicFamily · AlgebraicGeometry.curvesLci_isStrictlyFull · AlgebraicGeometry.CurvesLci · AlgebraicGeometry.isLciFamily_curveFamilyOfSchemeMorphism_iff · AlgebraicGeometry.factorsThroughCurvesLci_iff · AlgebraicGeometry.factorsThroughCurvesLci_over_field_iff · AlgebraicGeometry.isOpenImmersion_curvesSubstackInclusion_lci · AlgebraicGeometry.factorsThrough_curvesSubstack_lci_tfae

Section109.14 Curves with isolated singularities #

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

Tag 0DZW, a lemma

Tag 0DZW in the Stacks Project.

AlgebraicGeometry.CurvesWithFiniteNonSmoothLocus, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurveFamiliesIsolatedSingularities.lean, line 79. The attribute's comment: “the substack of curves with isolated singularities”.

Stacks 0DZW. The strictly full subcategory Curves⁺ ⊂ Curves of the families of curves whose non-smooth locus, with its reduced closed subspace structure, is finite over the base.

abbrev CurvesWithFiniteNonSmoothLocus

AlgebraicGeometry.curvesWithFiniteNonSmoothLocusProjection, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurveFamiliesIsolatedSingularities.lean, line 84. The attribute's comment: “the projection of the substack”.

Stacks 0DZW. The projection taking a family of curves with isolated singularities to its base scheme, which is how Curves⁺ is regarded as a category over the big fppf site.

abbrev curvesWithFiniteNonSmoothLocusProjection :
    CurvesWithFiniteNonSmoothLocus B hZ ⥤ B.Schemes

AlgebraicGeometry.CurvesPlus, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesFiniteSingularities.lean, line 81. The attribute's comment: “the_substack_curves”.

Stacks 0DZW. The substack Curves⁺: the strictly full subcategory of families of curves whose reduced non-smooth locus is finite over the base.

abbrev CurvesPlus

AlgebraicGeometry.CurveFamily.isFiniteNonSmoothLocus_iff_forall_isClosedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesPlusOpenLocus.lean, line 225. The attribute's comment: “part (1), condition (b) with 'any': every closed subspace structure on the singular locus is finite over the base”.

Stacks 0DZW, part (1), condition (b) with "any". A family of curves X → S lies in Curves⁺ exactly when every closed subspace Z ⊂ X whose set of points is the singular locus of X → S is finite over S.

theorem CurveFamily.isFiniteNonSmoothLocus_iff_forall_isClosedSubspace (X : CurveFamily B hZ) :
    IsFiniteNonSmoothLocus B hZ X ↔
      ∀ Z : Subfunctor X.total.1, Space.IsClosedSubspace B integerBase hZ Z →
        Set.range (Space.pointsMap B integerBase hZ Z.toFunctor Z.ι) =
          CurveFamily.nonSmoothLocus B hZ X →
        Space.IsFinite B integerBase hZ (Z.ι ≫ X.toBase.hom)

AlgebraicGeometry.CurveFamily.isFiniteNonSmoothLocus_iff_exists_isClosedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesPlusOpenLocus.lean, line 242. The attribute's comment: “part (1), condition (b) with 'some': some closed subspace structure on the singular locus is finite over the base”.

Stacks 0DZW, part (1), condition (b) with "some". A family of curves X → S lies in Curves⁺ exactly when some closed subspace Z ⊂ X whose set of points is the singular locus of X → S is finite over S.

theorem CurveFamily.isFiniteNonSmoothLocus_iff_exists_isClosedSubspace (X : CurveFamily B hZ) :
    IsFiniteNonSmoothLocus B hZ X ↔
      ∃ Z : Subfunctor X.total.1, Space.IsClosedSubspace B integerBase hZ Z ∧
        Set.range (Space.pointsMap B integerBase hZ Z.toFunctor Z.ι) =
          CurveFamily.nonSmoothLocus B hZ X ∧
        Space.IsFinite B integerBase hZ (Z.ι ≫ X.toBase.hom)

AlgebraicGeometry.curvesPlus_isOpenSubstack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesPlusOpenSubstack.lean, line 102. The attribute's comment: “Curves⁺ is an open substack of Curves: a strictly full subcategory whose inclusion is representable by algebraic spaces and an open immersion”.

Stacks 0DZW, the open substack. Curves⁺ is an open substack of the stack of curves: it is a strictly full subcategory, and its inclusion into Curves is representable by algebraic spaces and an open immersion.

theorem curvesPlus_isOpenSubstack :
    (show ObjectProperty (CurveFamily B hZ) from
        IsFiniteNonSmoothLocus B hZ).IsClosedUnderIsomorphisms ∧
      Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ (curvesPlusInclusion B hZ).hom ∧
      Stack.IsOpenImmersion B integerBase hZ (curvesPlusInclusion B hZ)

AlgebraicGeometry.curvesPlus_classifying_factors_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesPlusOpenSubstack.lean, line 173. The attribute's comment: “part (1): for every family of curves X → S, the classifying morphism factors through Curves⁺ iff the singular locus with some, equivalently any, closed subspace structure is finite over S”.

Stacks 0DZW, part (1). For a family of curves X → S and its classifying morphism S → Curves, the classifying morphism factors through Curves⁺ exactly when some closed subspace structure on the singular locus of X → S is finite over S, and exactly when every closed subspace structure on it is.

theorem curvesPlus_classifying_factors_iff (X : CurveFamily B hZ)
    (y : BasedCategory.ofFunctor (Over.map X.base.hom) ⥤ᵇ (curvesFiberedCategory B hZ).val)
    (hy : IsClassifyingMorphism B hZ X y) :
    ((∃ g : BasedCategory.ofFunctor (Over.map X.base.hom) ⥤ᵇ
          (curvesPlusFiberedCategory B hZ).val,
        Nonempty (g.comp (curvesPlusInclusion B hZ).hom ≅ y)) ↔
      ∃ Z : Subfunctor X.total.1, Space.IsClosedSubspace B integerBase hZ Z ∧
        Set.range (Space.pointsMap B integerBase hZ Z.toFunctor Z.ι) =
          CurveFamily.nonSmoothLocus B hZ X ∧
        Space.IsFinite B integerBase hZ (Z.ι ≫ X.toBase.hom)) ∧
    ((∃ g : BasedCategory.ofFunctor (Over.map X.base.hom) ⥤ᵇ
          (curvesPlusFiberedCategory B hZ).val,
        Nonempty (g.comp (curvesPlusInclusion B hZ).hom ≅ y)) ↔
      ∀ Z : Subfunctor X.total.1, Space.IsClosedSubspace B integerBase hZ Z →
        Set.range (Space.pointsMap B integerBase hZ Z.toFunctor Z.ι) =
          CurveFamily.nonSmoothLocus B hZ X →
        Space.IsFinite B integerBase hZ (Z.ι ≫ X.toBase.hom))

AlgebraicGeometry.curvesPlus_classifying_factors_iff_of_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesPlusOpenSubstack.lean, line 284. The attribute's comment: “part (2): for a proper scheme X of dimension at most one over a field k, the classifying morphism Spec(k) → Curves factors through Curves⁺ iff X → Spec(k) is smooth except at finitely many points”.

Stacks 0DZW, part (2). Let X be a proper scheme of dimension at most one over a field k. The classifying morphism Spec(k) → Curves of the attached family of curves factors through Curves⁺ exactly when X → Spec(k) is smooth except at finitely many points.

theorem curvesPlus_classifying_factors_iff_of_field
    (hdim : topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) ≤ 1)
    (y : BasedCategory.ofFunctor (Over.map W.hom) ⥤ᵇ (curvesFiberedCategory B hZ).val)
    (hy : IsClassifyingMorphism B hZ (curveFamilyOfProperOverField B hZ k g e hproper hdim) y) :
    (∃ g' : BasedCategory.ofFunctor (Over.map W.hom) ⥤ᵇ (curvesPlusFiberedCategory B hZ).val,
        Nonempty (g'.comp (curvesPlusInclusion B hZ).hom ≅ y)) ↔
      {x : (BigFppfOver.toScheme B integerBase hZ).obj T |
        ¬ InfinitesimalLifting.SmoothAt ((BigFppfOver.toScheme B integerBase hZ).map g) x}.Finite

AlgebraicGeometry.exists_curvesPlus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesPlusOpenSubstack.lean, line 311. The attribute's comment: “the open substack Curves⁺ ⊂ Curves together with parts (1) and (2)”.

Stacks 0DZW. There is an open substack Curves⁺ of the stack of curves — a strictly full subcategory whose inclusion is representable by algebraic spaces and an open immersion — such that

for every family of curves X → S and its classifying morphism, the classifying morphism factors through Curves⁺ iff the singular locus of X → S with some closed subspace structure is finite over S, iff it is finite over S with every closed subspace structure;

for every proper scheme X of dimension at most one over a field k, the classifying morphism Spec(k) → Curves factors through Curves⁺ iff X → Spec(k) is smooth except at finitely many points.

theorem exists_curvesPlus :
    ∃ (P : ObjectProperty (CurveFamily B hZ))
        (hP : ∀ {F G : CurveFamily B hZ}, (F ⟶ G) → P G → P F),
      P.IsClosedUnderIsomorphisms ∧
      Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ (curvesSubInclusion B hZ P hP).hom ∧
      Stack.IsOpenImmersion B integerBase hZ (curvesSubInclusion B hZ P hP) ∧
      (∀ (X : CurveFamily B hZ)
        (y : BasedCategory.ofFunctor (Over.map X.base.hom) ⥤ᵇ (curvesFiberedCategory B hZ).val),
        IsClassifyingMorphism B hZ X y →
          ((∃ g : BasedCategory.ofFunctor (Over.map X.base.hom) ⥤ᵇ
                (curvesSubFiberedCategory B hZ P hP).val,
              Nonempty (g.comp (curvesSubInclusion B hZ P hP).hom ≅ y)) ↔
            ∃ Z : Subfunctor X.total.1, Space.IsClosedSubspace B integerBase hZ Z ∧
              Set.range (Space.pointsMap B integerBase hZ Z.toFunctor Z.ι) =
                CurveFamily.nonSmoothLocus B hZ X ∧
              Space.IsFinite B integerBase hZ (Z.ι ≫ X.toBase.hom)) ∧
          ((∃ g : BasedCategory.ofFunctor (Over.map X.base.hom) ⥤ᵇ
                (curvesSubFiberedCategory B hZ P hP).val,
              Nonempty (g.comp (curvesSubInclusion B hZ P hP).hom ≅ y)) ↔
            ∀ Z : Subfunctor X.total.1, Space.IsClosedSubspace B integerBase hZ Z →
              Set.range (Space.pointsMap B integerBase hZ Z.toFunctor Z.ι) =
                CurveFamily.nonSmoothLocus B hZ X →
              Space.IsFinite B integerBase hZ (Z.ι ≫ X.toBase.hom))) ∧
      (∀ (k : Type u) [Field k] {T W : BigFppfOver B integerBase hZ} (g : T ⟶ W)
        (e : (BigFppfOver.toScheme B integerBase hZ).obj W ≅ Spec (.of k))
        (hproper : IsProper ((BigFppfOver.toScheme B integerBase hZ).map g))
        (hdim : topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) ≤ 1)
        (y : BasedCategory.ofFunctor (Over.map W.hom) ⥤ᵇ (curvesFiberedCategory B hZ).val),
        IsClassifyingMorphism B hZ (curveFamilyOfProperOverField B hZ k g e hproper hdim) y →
          ((∃ g' : BasedCategory.ofFunctor (Over.map W.hom) ⥤ᵇ
                (curvesSubFiberedCategory B hZ P hP).val,
              Nonempty (g'.comp (curvesSubInclusion B hZ P hP).hom ≅ y)) ↔
            {x : (BigFppfOver.toScheme B integerBase hZ).obj T |
              ¬ InfinitesimalLifting.SmoothAt
                ((BigFppfOver.toScheme B integerBase hZ).map g) x}.Finite))

AlgebraicGeometry.curvesPlus_isStrictlyFull, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesPlusStrictlyFull.lean, line 233. The attribute's comment: “open_substack”.

Stacks 0DZW. Membership in the subcategory Curves⁺ of families of curves whose reduced non-smooth locus is finite over the base is invariant under isomorphism, so Curves⁺ is a strictly full subcategory.

theorem curvesPlus_isStrictlyFull :
    (show ObjectProperty (CurveFamily B hZ) from
      IsFiniteNonSmoothLocus B hZ).IsClosedUnderIsomorphisms

Sources

LeanAlgebraicGeometry.CurvesWithFiniteNonSmoothLocus · AlgebraicGeometry.curvesWithFiniteNonSmoothLocusProjection · AlgebraicGeometry.CurvesPlus · AlgebraicGeometry.CurveFamily.isFiniteNonSmoothLocus_iff_forall_isClosedSubspace · AlgebraicGeometry.CurveFamily.isFiniteNonSmoothLocus_iff_exists_isClosedSubspace · AlgebraicGeometry.curvesPlus_isOpenSubstack · AlgebraicGeometry.curvesPlus_classifying_factors_iff · AlgebraicGeometry.curvesPlus_classifying_factors_iff_of_field

Section109.15 The smooth locus of the stack of curves #

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

Tag 0DZU, a lemma

Tag 0DZU in the Stacks Project.

AlgebraicGeometry.curvesSmoothLocus_property_iff_isSmooth_schemeDeformation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmoothLocusUnobstructed.lean, line 83.

Let k be a field, let X be a proper scheme of dimension at most one over k, and let Λ be a Cohen ring for k: a complete discrete valuation ring whose maximal ideal is generated by a prime number p (IsCohenRing), with a surjection Λ → k, so that k is its residue field. Then the following are equivalent:

the classifying morphism Spec(k) → Curves of X factors through the open substack where Curves → Spec(ℤ) is smooth;

the deformation category Def_X of X over 𝒞_Λ is unobstructed.

The stack Curves is read on its small model AlgebraicGeometry.curvesAlgebraicStack, the presentation at which it is an object of the 2-category of algebraic stacks; the classifying morphism of X is the object AlgebraicGeometry.curvesSmallPoint over Spec(k), and it factors through an open substack exactly when it is an object of that substack. The open substack where Curves → Spec(ℤ) is smooth is the maximal one of Stacks 0DZR, AlgebraicGeometry.curvesSmoothLocus. Unobstructedness of Def_X is smoothness of its projection to 𝒞_Λ (Stacks 06HG).

theorem curvesSmoothLocus_property_iff_isSmooth_schemeDeformation
    {k Λ : Type u} [Field k] [CommRing Λ] [IsDomain Λ] [IsCohenRing Λ] [Algebra Λ k]
    (hsurj : Function.Surjective (algebraMap Λ k))
    (X : Over (Spec (.of k))) [IsProper X.hom] (hk : B.Contains (Spec (.of k)))
    (hdim : topologicalKrullDim X.left ≤ 1) :
    (curvesSmoothLocus.{u, w} B hZ).property (curvesSmallPoint B hZ X hk hdim) ↔
      IsSmooth (baseProjection (schemeDeformationCategoryProjection (Λ := Λ) X))

Tag 0DZX, a lemma

Tag 0DZX in the Stacks Project.

AlgebraicGeometry.curvesLciPlus_isOpenSubstack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesLciPlus.lean, line 111. The attribute's comment: “the open substack Curves^{lci+} = Curves^{lci} ∩ Curves^{+} of Curves”.

Stacks 0DZX. Curves^{lci+} = Curves^{lci} ∩ Curves^{+}, the strictly full subcategory of families of curves with local complete intersection structure morphism and singular locus finite over the base, is an open substack of Curves: its inclusion is representable by algebraic spaces and an open immersion.

theorem curvesLciPlus_isOpenSubstack :
    ObjectProperty.IsClosedUnderIsomorphisms
        (fun F : CurveFamily B hZ => IsLciFamily B hZ F ∧ IsFiniteNonSmoothLocus B hZ F) ∧
      Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (curvesSubstackInclusion B hZ _ (isOpenCurvesLocus_lciPlus B hZ).prop_of_hom).hom ∧
      Stack.IsOpenImmersion B integerBase hZ
        (curvesSubstackInclusion B hZ _ (isOpenCurvesLocus_lciPlus B hZ).prop_of_hom)

AlgebraicGeometry.factors_curvesLciPlus_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesLciPlus.lean, line 126. The attribute's comment: “part (2): the classifying morphism of a family of curves factors through Curves^{lci+} iff the family is a local complete intersection morphism whose singular locus, with any (equivalently, some) closed subspace structure, is finite over the base”.

Stacks 0DZX, part (2). The classifying morphism of a family of curves X ⟶ S factors through Curves^{lci+} exactly when X ⟶ S is a local complete intersection morphism and its singular locus, with any (equivalently, some) closed subspace structure, is finite over S.

theorem factors_curvesLciPlus_iff (U : BigFppfOver B integerBase hZ)
    (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ)
    (hy : y ⋙ curvesProjectionOver B hZ = Over.map U.hom) :
    let X := y.obj (Over.mk (𝟙 U.left))
    ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
        (IsLciPlusFamily B hZ).FullSubcategory,
        z ⋙ (IsLciPlusFamily B hZ).ι = y) ↔
      IsLciFamily B hZ X ∧
        ∀ Z : Subfunctor X.total.obj, Space.IsClosedSubspace B integerBase hZ Z →
          Set.range (Space.pointsMap B integerBase hZ Z.toFunctor Z.ι) =
            {x : Space.points B integerBase hZ X.total.obj |
              ¬ Space.IsSmoothAt B integerBase hZ X.toBase.hom x} →
          Space.IsFinite B integerBase hZ (Z.ι ≫ X.toBase.hom)) ∧
    ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
        (IsLciPlusFamily B hZ).FullSubcategory,
        z ⋙ (IsLciPlusFamily B hZ).ι = y) ↔
      IsLciFamily B hZ X ∧
        ∃ Z : Subfunctor X.total.obj, Space.IsClosedSubspace B integerBase hZ Z ∧
          Set.range (Space.pointsMap B integerBase hZ Z.toFunctor Z.ι) =
            {x : Space.points B integerBase hZ X.total.obj |
              ¬ Space.IsSmoothAt B integerBase hZ X.toBase.hom x} ∧
          Space.IsFinite B integerBase hZ (Z.ι ≫ X.toBase.hom))

AlgebraicGeometry.factors_curvesLciPlus_over_field_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesLciPlus.lean, line 185. The attribute's comment: “part (3): for a proper scheme of dimension at most one over a field, the classifying morphism factors through Curves^{lci+} iff the scheme is a local complete intersection over the field and is smooth over it except at finitely many points”.

Stacks 0DZX, part (3). Let X be a proper scheme of dimension at most one over a field k (with Spec k in the site, so that the classifying morphism Spec k ⟶ Curves of X exists). The classifying morphism of X factors through Curves^{lci+} exactly when X is a local complete intersection over k and X ⟶ Spec(k) is smooth except at finitely many points.

theorem factors_curvesLciPlus_over_field_iff
    (k : Type u) [Field k] (hk : B.Contains (Spec (.of k)))
    (X : Over (Spec (.of k))) [IsProper X.hom] (hdim : topologicalKrullDim X.left ≤ 1)
    (U : BigFppfOver B integerBase hZ)
    (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ)
    (hy : y ⋙ curvesProjectionOver B hZ = Over.map U.hom)
    (e : y.obj (Over.mk (𝟙 U.left)) ≅ curveFamilyOfScheme X B hZ hk hdim) :
    (∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
        (IsLciPlusFamily B hZ).FullSubcategory,
        z ⋙ (IsLciPlusFamily B hZ).ι = y) ↔
      IsLocalCompleteIntersectionMorphism X.hom ∧ (X.hom.smoothLocus : Set X.left)ᶜ.Finite

AlgebraicGeometry.isSmoothOverIntegers_curvesLciPlus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesLciPlusSmoothUnconditional.lean, line 44. The attribute's comment: “part (1): Curves^{lci+} → Spec(ℤ) is smooth, on the algebraic stack of curves”.

The morphism Curves^{lci+} → Spec(ℤ) is smooth. Here Curves^{lci+} = Curves^{lci} ∩ Curves^{+} is the open substack of the algebraic stack of curves (Stacks 0D5A) of the families of curves which are local complete intersection morphisms with singular locus finite over the base, and smoothness over Spec(ℤ) is smoothness of its inclusion followed by the structure morphism of the stack of curves.

theorem isSmoothOverIntegers_curvesLciPlus :
    IsSmoothOverIntegers B hZ (curvesFiberedCategory_isAlgebraicStack.{u, z} B hZ)
      (isOpenCurvesLocus_lciPlus B hZ)

Sources

LeanAlgebraicGeometry.curvesSmoothLocus_property_iff_isSmooth_schemeDeformation · AlgebraicGeometry.curvesLciPlus_isOpenSubstack · AlgebraicGeometry.factors_curvesLciPlus_iff · AlgebraicGeometry.factors_curvesLciPlus_over_field_iff · AlgebraicGeometry.isSmoothOverIntegers_curvesLciPlus

Section109.16 Smooth curves #

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

Tag 0DZZ, a lemma

Tag 0DZZ in the Stacks Project.

AlgebraicGeometry.CurveFamily.isOpen_smoothBaseLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmooth.lean, line 220. The attribute's comment: “the open locus in the base of smoothness”.

Stacks 0DZZ. The locus of points of the base of a family of curves over which the family is smooth is open.

The set of points of the total space at which the structure morphism is smooth is open by Tag 0DZI, so its complement is closed, and the family is proper, so the image of that complement — the complement of the locus in the base — is closed.

theorem CurveFamily.isOpen_smoothBaseLocus (X : CurveFamily B hZ) :
    IsOpen (CurveFamily.smoothBaseLocus B hZ X)

AlgebraicGeometry.CurveFamily.preimage_smoothBaseLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmooth.lean, line 241. The attribute's comment: “base change of the open locus in the base of smoothness”.

Stacks 0DZZ. The open locus in the base over which a family of curves is smooth commutes with base change: for a morphism of families of curves, the locus of the source is the inverse image of the locus of the target under the morphism of base schemes.

theorem CurveFamily.preimage_smoothBaseLocus {X Y : CurveFamily B hZ} (φ : X ⟶ Y) :
    Space.pointsMap B integerBase hZ (schemeSpace X.base).obj (schemeSpaceMap φ.baseMap).hom ⁻¹'
        CurveFamily.smoothBaseLocus B hZ Y =
      CurveFamily.smoothBaseLocus B hZ X

AlgebraicGeometry.CurveFamily.exists_isOpenSubspace_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmooth.lean, line 274. The attribute's comment: “the open subspace of the base over which a family becomes smooth, compatibly with base change”.

Stacks 0DZZ. The open subspace of the base of a family of curves over which the family becomes smooth, in the form the source's proof produces it: for a family of curves G there is an open subspace W of its base such that a family F mapping to G is smooth exactly when the morphism of base schemes factors through W.

This is the open S' ⊂ S of the source, and the equivalence is its compatibility with arbitrary base change: W is the open locus of smoothness of G in its base, factoring through it is having image in that locus, and the locus of F is the inverse image of the locus of G.

theorem CurveFamily.exists_isOpenSubspace_smooth (G : CurveFamily B hZ) :
    ∃ W : Subfunctor (schemeSpace G.base).obj,
      Space.IsOpenSubspace B integerBase hZ W ∧
      ∀ (F : CurveFamily B hZ) (a : F ⟶ G),
        IsSmoothFamily B hZ F ↔
          ∃ t : (schemeSpace F.base).obj ⟶ W.toFunctor,
            t ≫ W.ι = (schemeSpaceMap a.baseMap).hom

AlgebraicGeometry.curvesSmooth_isStrictlyFull, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmooth.lean, line 317. The attribute's comment: “strict fullness of the smooth subcategory”.

Stacks 0DZZ. The condition that a family of curves be smooth is invariant under isomorphism, so Curves^{smooth} is a strictly full subcategory of the category of families of curves: the first of the three conditions making it an open substack.

An isomorphism of families of curves is a morphism of families, so this is base-change invariance of smoothness applied to the inverse isomorphism.

theorem curvesSmooth_isStrictlyFull :
    (show ObjectProperty (CurveFamily B hZ) from
      IsSmoothFamily B hZ).IsClosedUnderIsomorphisms

AlgebraicGeometry.CurvesSmooth, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmooth.lean, line 325. The attribute's comment: “the smooth subcategory of the category of curves”.

Stacks 0DZZ. The subcategory Curves^{smooth}: the strictly full subcategory of families of curves whose structure morphism is smooth.

abbrev CurvesSmooth

AlgebraicGeometry.isSmoothDimOneFamily_iff_isSmoothFamily_and_isCohenMacaulayDimOneFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmooth.lean, line 347. The attribute's comment: “Curves^{smooth,1} is Curves^{smooth} intersected with Curves^{CM,1}”.

Stacks 0DZZ. Curves^{smooth,1} is the intersection of Curves^{smooth} with Curves^{CM,1}: a family of curves is smooth of relative dimension one exactly when it is smooth and is Cohen–Macaulay of relative dimension one.

theorem isSmoothDimOneFamily_iff_isSmoothFamily_and_isCohenMacaulayDimOneFamily
    (X : CurveFamily B hZ) :
    IsSmoothDimOneFamily B hZ X ↔
      IsSmoothFamily B hZ X ∧ IsCohenMacaulayDimOneFamily B hZ X

AlgebraicGeometry.CurveFamily.isOpen_smoothDimOneBaseLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmooth.lean, line 364. The attribute's comment: “the open locus in the base of smooth relative dimension one”.

Stacks 0DZZ. For a Cohen–Macaulay family of curves the locus in the base over which the family is smooth and has relative dimension one is open: the locus of smoothness is open, and so is the locus of relative dimension one by Tag 0E1F.

theorem CurveFamily.isOpen_smoothDimOneBaseLocus (X : CurveFamily B hZ)
    (hX : IsCohenMacaulayFamily B hZ X) :
    IsOpen (CurveFamily.smoothDimOneBaseLocus B hZ X)

AlgebraicGeometry.CurveFamily.isOpen_smoothDimOneBaseLocus_of_isSmoothFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmooth.lean, line 373. The attribute's comment: “the open locus in the base of smooth relative dimension one, for a smooth family”.

Stacks 0DZZ. For a smooth family of curves the locus in the base over which the family is smooth and has relative dimension one is open: a smooth family is Cohen–Macaulay.

theorem CurveFamily.isOpen_smoothDimOneBaseLocus_of_isSmoothFamily (X : CurveFamily B hZ)
    (hX : IsSmoothFamily B hZ X) :
    IsOpen (CurveFamily.smoothDimOneBaseLocus B hZ X)

AlgebraicGeometry.CurveFamily.isOpen_smoothDimOneBaseLocus_of_any, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmooth.lean, line 445. The attribute's comment: “the open locus in the base of smooth relative dimension one, for any family”.

Stacks 0DZZ. For any family of curves the locus in the base over which the family is smooth and has relative dimension one is open.

This needs no hypothesis on the family: the set of points of the total space at which the structure morphism is smooth and has relative dimension one is open, so its complement is closed, and the family is proper, so the image of that complement — the complement of the locus in the base — is closed.

theorem CurveFamily.isOpen_smoothDimOneBaseLocus_of_any (X : CurveFamily B hZ) :
    IsOpen (CurveFamily.smoothDimOneBaseLocus B hZ X)

AlgebraicGeometry.CurveFamily.preimage_smoothDimOneBaseLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmooth.lean, line 462. The attribute's comment: “base change of the locus in the base of smooth relative dimension one”.

Stacks 0DZZ. The locus in the base over which a family of curves is smooth and has relative dimension one commutes with base change: for a morphism of families of curves, the locus of the source is the inverse image of the locus of the target under the morphism of base schemes.

theorem CurveFamily.preimage_smoothDimOneBaseLocus {X Y : CurveFamily B hZ} (φ : X ⟶ Y) :
    Space.pointsMap B integerBase hZ (schemeSpace X.base).obj (schemeSpaceMap φ.baseMap).hom ⁻¹'
        CurveFamily.smoothDimOneBaseLocus B hZ Y =
      CurveFamily.smoothDimOneBaseLocus B hZ X

AlgebraicGeometry.CurveFamily.exists_isOpenSubspace_smoothDimOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmooth.lean, line 490. The attribute's comment: “the open subspace of the base over which a family becomes smooth of relative dimension one, compatibly with base change”.

Stacks 0DZZ. The open subspace of the base of a family of curves over which the family becomes smooth of relative dimension one, in the form the source's proof produces it: for a family of curves G there is an open subspace W of its base such that a family F mapping to G is smooth of relative dimension one exactly when the morphism of base schemes factors through W.

This is the open S' ⊂ S of the source for Curves^{smooth,1}, and the equivalence is its compatibility with arbitrary base change.

theorem CurveFamily.exists_isOpenSubspace_smoothDimOne (G : CurveFamily B hZ) :
    ∃ W : Subfunctor (schemeSpace G.base).obj,
      Space.IsOpenSubspace B integerBase hZ W ∧
      ∀ (F : CurveFamily B hZ) (a : F ⟶ G),
        IsSmoothDimOneFamily B hZ F ↔
          ∃ t : (schemeSpace F.base).obj ⟶ W.toFunctor,
            t ≫ W.ι = (schemeSpaceMap a.baseMap).hom

AlgebraicGeometry.curvesSmooth1_isStrictlyFull, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmooth.lean, line 529. The attribute's comment: “strict fullness of the smooth subcategory of relative dimension one”.

Stacks 0DZZ. The condition that a family of curves be smooth of relative dimension one is invariant under isomorphism, so Curves^{smooth,1} is a strictly full subcategory of the category of families of curves: the first of the three conditions making it an open substack.

theorem curvesSmooth1_isStrictlyFull :
    (show ObjectProperty (CurveFamily B hZ) from
      IsSmoothDimOneFamily B hZ).IsClosedUnderIsomorphisms

AlgebraicGeometry.CurvesSmooth1, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmooth.lean, line 537. The attribute's comment: “the smooth subcategory of relative dimension one”.

Stacks 0DZZ. The subcategory Curves^{smooth,1}: the strictly full subcategory of families of curves whose structure morphism is smooth of relative dimension one.

abbrev CurvesSmooth1

AlgebraicGeometry.curvesSmooth1_le_curvesSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmooth.lean, line 543. The attribute's comment: “the chain of subcategories”.

Stacks 0DZZ. The chain Curves^{smooth,1} ⊂ Curves^{smooth}: a family of curves which is smooth of relative dimension one is smooth.

theorem curvesSmooth1_le_curvesSmooth :
    (show ObjectProperty (CurveFamily B hZ) from IsSmoothDimOneFamily B hZ) ≤
      (show ObjectProperty (CurveFamily B hZ) from IsSmoothFamily B hZ)

AlgebraicGeometry.isSmoothFamily_curveFamilyOfSchemeMorphism_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmooth.lean, line 618. The attribute's comment: “part (2): smoothness of the proper scheme”.

Stacks 0DZZ, part (2). The family of curves attached to a proper flat morphism of schemes of finite presentation whose source has dimension at most one is smooth exactly when that morphism of schemes is smooth.

theorem isSmoothFamily_curveFamilyOfSchemeMorphism_iff
    {T U : BigFppfOver B integerBase hZ} (g : T ⟶ U)
    (hflat : Flat ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hproper : IsProper ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hlfp : LocallyOfFinitePresentation ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hqc : Space.IsQuasiCompact B integerBase hZ (schemeSpaceMap g).hom)
    (hsep : Space.IsSeparated B integerBase hZ (schemeSpaceMap g).hom)
    (hqsep : Space.IsQuasiSeparated B integerBase hZ (schemeSpaceMap g).hom)
    (hdim : topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) ≤ 1) :
    IsSmoothFamily B hZ
        (curveFamilyOfSchemeMorphism B hZ g hflat hproper hlfp hqc hsep hqsep hdim) ↔
      Smooth ((BigFppfOver.toScheme B integerBase hZ).map g)

AlgebraicGeometry.isSmoothDimOneFamily_curveFamilyOfSchemeMorphism_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmooth.lean, line 640. The attribute's comment: “part (2): the proper scheme is smooth and equidimensional of dimension one”.

Stacks 0DZZ, part (2). For a proper flat morphism of schemes of finite presentation with nonempty source of dimension at most one onto the spectrum of a field, the attached family of curves is smooth of relative dimension one exactly when the source is smooth over the field and equidimensional of dimension one.

The source is assumed nonempty because an empty source has relative dimension one vacuously while its dimension is -∞.

theorem isSmoothDimOneFamily_curveFamilyOfSchemeMorphism_iff
    {T U : BigFppfOver B integerBase hZ} (g : T ⟶ U)
    (hflat : Flat ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hproper : IsProper ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hlfp : LocallyOfFinitePresentation ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hqc : Space.IsQuasiCompact B integerBase hZ (schemeSpaceMap g).hom)
    (hsep : Space.IsSeparated B integerBase hZ (schemeSpaceMap g).hom)
    (hqsep : Space.IsQuasiSeparated B integerBase hZ (schemeSpaceMap g).hom)
    (hdim : topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) ≤ 1)
    (k : Type u) [Field k]
    (hU : (BigFppfOver.toScheme B integerBase hZ).obj U = Spec (.of k))
    (hne : Nonempty ((BigFppfOver.toScheme B integerBase hZ).obj T)) :
    IsSmoothDimOneFamily B hZ
        (curveFamilyOfSchemeMorphism B hZ g hflat hproper hlfp hqc hsep hqsep hdim) ↔
      (Smooth ((BigFppfOver.toScheme B integerBase hZ).map g) ∧
        Equidimensional ((BigFppfOver.toScheme B integerBase hZ).obj T) ∧
        topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) =
          (1 : WithBot ℕ∞))

AlgebraicGeometry.isSmoothDimOneFamily_curveFamilyOfSchemeMorphism_iff_irreducibleComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmooth.lean, line 679. The attribute's comment: “part (2): the proper scheme is smooth and every irreducible component of it has dimension one”.

Stacks 0DZZ, part (2). For a proper flat morphism of schemes of finite presentation whose source has dimension at most one onto the spectrum of a field, the attached family of curves is smooth of relative dimension one exactly when the source is smooth over the field and equidimensional of dimension one — that is, every irreducible component of the source has dimension one.

This is the whole of part (2) for Curves^{smooth,1}, with no hypothesis beyond those of the source: "equidimensional of dimension one" is read componentwise, as the definition of Tag 0058 reads it, and so the equivalence also holds for an empty source, which is smooth of relative dimension one and has no irreducible component.

theorem isSmoothDimOneFamily_curveFamilyOfSchemeMorphism_iff_irreducibleComponents
    {T U : BigFppfOver B integerBase hZ} (g : T ⟶ U)
    (hflat : Flat ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hproper : IsProper ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hlfp : LocallyOfFinitePresentation ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hqc : Space.IsQuasiCompact B integerBase hZ (schemeSpaceMap g).hom)
    (hsep : Space.IsSeparated B integerBase hZ (schemeSpaceMap g).hom)
    (hqsep : Space.IsQuasiSeparated B integerBase hZ (schemeSpaceMap g).hom)
    (hdim : topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) ≤ 1)
    (k : Type u) [Field k]
    (hU : (BigFppfOver.toScheme B integerBase hZ).obj U = Spec (.of k)) :
    IsSmoothDimOneFamily B hZ
        (curveFamilyOfSchemeMorphism B hZ g hflat hproper hlfp hqc hsep hqsep hdim) ↔
      (Smooth ((BigFppfOver.toScheme B integerBase hZ).map g) ∧
        TopologicalSpace.Equidimensional ((BigFppfOver.toScheme B integerBase hZ).obj T) ∧
        ∀ W ∈ irreducibleComponents ((BigFppfOver.toScheme B integerBase hZ).obj T),
          topologicalKrullDim W = (1 : WithBot ℕ∞))

Tag 0E1N, a lemma

Tag 0E1N in the Stacks Project.

AlgebraicGeometry.isSmoothOverIntegers_isSmoothFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmoothOverIntegers.lean, line 67. The attribute's comment: “Curves^{smooth} → Spec(ℤ) is smooth, on the algebraic stack of curves”.

The morphism Curves^{smooth} → Spec(ℤ) is smooth: the open substack of the algebraic stack of curves (Stacks 0D5A) where the family of curves is smooth, followed by the structure morphism to Spec(ℤ), is a smooth morphism of algebraic stacks.

theorem isSmoothOverIntegers_isSmoothFamily :
    IsSmoothOverIntegers B hZ (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, w} B hZ)
      (isOpenCurvesLocus_isSmoothFamily B hZ)

Tag 0E81, a lemma

Tag 0E81 in the Stacks Project.

AlgebraicGeometry.curvesSmoothH0_isOpenSubstack_and_factors_iff_and_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmoothH0Open.lean, line 231. The attribute's comment: “the open substack Curves^{smooth,h0} (the moduli stack M of 0E82), its family characterization (1) and the five equivalent conditions (2) over a field”.

There is an open substack Curves^{smooth,h0} ⊂ Curves — the moduli stack 𝓜 = AlgebraicGeometry.moduliSmoothCurves of Stacks 0E82, the strictly full subcategory of families of curves satisfying AlgebraicGeometry.IsSmoothH0Family; its inclusion AlgebraicGeometry.moduliSmoothCurvesInclusion is representable by algebraic spaces and an open immersion — such that:

for a family of curves f : X → S, classified by a scheme-valued point y of Curves over S, the classifying morphism factors through Curves^{smooth,h0} exactly when f_*𝒪_X = 𝒪_S, this holding after any base change, and f is smooth of relative dimension 1 (IsSmoothH0Family of the family y(S));

for a scheme X = T proper over a field k = W with dim X ≤ 1, classified by y over Spec k, the following are equivalent: (a) the classifying morphism factors through Curves^{smooth,h0}; (b) X is smooth, dim X = 1 and k = H⁰(X, 𝒪_X); (c) X is smooth, dim X = 1 and geometrically connected; (d) X is smooth, dim X = 1 and geometrically integral; (e) X_{k̄} is a smooth curve over an algebraic closure k̄ of k.

Part (1)(a) of the source says "factors through Curves^{smooth}"; the substack meant is the one constructed, Curves^{smooth,h0} (see the module documentation).

theorem curvesSmoothH0_isOpenSubstack_and_factors_iff_and_tfae :
    ((ObjectProperty.IsClosedUnderIsomorphisms (IsSmoothH0Family B hZ) ∧
      Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (moduliSmoothCurvesInclusion B hZ).hom ∧
      Stack.IsOpenImmersion B integerBase hZ (moduliSmoothCurvesInclusion B hZ)) ∧
    ∀ (U : BigFppfOver B integerBase hZ)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
      y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
      ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
          ObjectProperty.FullSubcategory (IsSmoothH0Family B hZ),
          z ⋙ ObjectProperty.ι (IsSmoothH0Family B hZ) = y) ↔
        IsSmoothH0Family B hZ (y.obj (Over.mk (𝟙 U.left))))) ∧
    ∀ {T W : BigFppfOver B integerBase hZ} (g : T ⟶ W) (k : Type u) [Field k]
      (hW : (BigFppfOver.toScheme B integerBase hZ).obj W = Spec (.of k))
      (hflat : Flat ((BigFppfOver.toScheme B integerBase hZ).map g))
      (hproper : IsProper ((BigFppfOver.toScheme B integerBase hZ).map g))
      (hlfp : LocallyOfFinitePresentation ((BigFppfOver.toScheme B integerBase hZ).map g))
      (hqc : Space.IsQuasiCompact B integerBase hZ (schemeSpaceMap g).hom)
      (hsep : Space.IsSeparated B integerBase hZ (schemeSpaceMap g).hom)
      (hqsep : Space.IsQuasiSeparated B integerBase hZ (schemeSpaceMap g).hom)
      (hdim : topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) ≤ 1)
      (y : BigFppfOver B W.left.1 W.left.2 ⥤ CurveFamily B hZ)
      (_hy : y ⋙ curvesProjectionOver B hZ = Over.map W.hom)
      (_e : y.obj (Over.mk (𝟙 W.left)) ≅
        curveFamilyOfSchemeMorphism B hZ g hflat hproper hlfp hqc hsep hqsep hdim),
      List.TFAE [
        ∃ z : BigFppfOver B W.left.1 W.left.2 ⥤
            ObjectProperty.FullSubcategory (IsSmoothH0Family B hZ),
          z ⋙ ObjectProperty.ι (IsSmoothH0Family B hZ) = y,
        Smooth ((BigFppfOver.toScheme B integerBase hZ).map g ≫ eqToHom hW) ∧
          topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) = 1 ∧
          IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫
            ((BigFppfOver.toScheme B integerBase hZ).map g ≫ eqToHom hW).appTop),
        Smooth ((BigFppfOver.toScheme B integerBase hZ).map g ≫ eqToHom hW) ∧
          topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) = 1 ∧
          GeometricallyConnected ((BigFppfOver.toScheme B integerBase hZ).map g ≫ eqToHom hW),
        Smooth ((BigFppfOver.toScheme B integerBase hZ).map g ≫ eqToHom hW) ∧
          topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) = 1 ∧
          GeometricallyIntegral ((BigFppfOver.toScheme B integerBase hZ).map g ≫ eqToHom hW),
        Smooth (pullback.snd ((BigFppfOver.toScheme B integerBase hZ).map g ≫ eqToHom hW)
            (Spec.map (CommRingCat.ofHom (algebraMap k (AlgebraicClosure k))))) ∧
          IsCurve (AlgebraicClosure k)
            (pullback.snd ((BigFppfOver.toScheme B integerBase hZ).map g ≫ eqToHom hW)
              (Spec.map (CommRingCat.ofHom (algebraMap k (AlgebraicClosure k)))))]

Tag 0E82, a definition

Tag 0E82 in the Stacks Project.

AlgebraicGeometry.moduliSmoothCurves, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ModuliCurves.lean, line 79. The attribute's comment: “the moduli stack of smooth proper curves, 𝓜 = Curves^{smooth, h0}”.

The moduli stack 𝓜 = Curves^{smooth, h0} of smooth proper curves: the substack of the stack of curves of the families of curves f : X → S which are smooth of relative dimension one with f_*𝒪_X = 𝒪_S, this holding after any base change (condition (1)(b) of Stacks 0E81), as a category fibred in groupoids over the big fppf site of Spec(ℤ).

def moduliSmoothCurves :
    CatFiberedInGroupoids.{u, u + 1, u + 1, u + 1} (BigFppfOver B integerBase hZ)

AlgebraicGeometry.moduliSmoothCurvesOfGenus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ModuliSmoothCurvesOfGenus.lean, line 85. The attribute's comment: “the moduli stack of smooth proper curves of genus g, 𝓜_g”.

The moduli stack 𝓜_g of smooth proper curves of genus g: the substack of the stack of curves of the families f : X → S which are smooth of relative dimension one with f_*𝒪_X = 𝒪_S, universally, and whose fibre over every point of S has genus g, as a category fibred in groupoids over the big fppf site of Spec(ℤ). It lies in 𝓜 = AlgebraicGeometry.moduliSmoothCurves, and its points are the smooth proper curves of genus g over fields, as in part (2) of Stacks 0E83.

def moduliSmoothCurvesOfGenus (g : ℕ) :
    CatFiberedInGroupoids.{u, u + 1, u + 1, u + 1} (BigFppfOver B integerBase hZ)

Tag 0E83, a lemma

Tag 0E83 in the Stacks Project.

AlgebraicGeometry.moduliSmoothCurves_openClosedDecomposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ModuliSmoothCurvesGenusDecomposition.lean, line 173. The attribute's comment: “the decomposition 𝓜 = ∐_{g ≥ 0} 𝓜_g into open and closed substacks, read on the scheme-valued points of 𝓜”.

The decomposition 𝓜 = ∐_{g ≥ 0} 𝓜_g into open and closed substacks. Let G be a family of curves in 𝓜 (AlgebraicGeometry.moduliSmoothCurves) over a scheme S, that is, a scheme-valued point S → 𝓜. Then:

the loci S_g ⊂ S of points whose fibre has genus g are open and closed in S, pairwise disjoint, and cover S;

for every g, 𝓜_g ×_𝓜 S is the open subscheme S_g: there is an open subspace W of S with points S_g such that a family F mapping to G (a base change of G along T → S) lies in 𝓜_g (AlgebraicGeometry.moduliSmoothCurvesOfGenus) exactly when T → S factors through W, exactly when T → S maps every point into S_g.

So each 𝓜_g ⊂ 𝓜 is an open and closed substack, these substacks are pairwise disjoint, and together they cover 𝓜.

theorem moduliSmoothCurves_openClosedDecomposition (G : CurveFamily B hZ)
    (hG : IsSmoothH0Family B hZ G) :
    (∀ g : ℕ, IsClopen (CurveFamily.fibreGenusLocus B hZ G g)) ∧
      Pairwise (fun g g' : ℕ => Disjoint (CurveFamily.fibreGenusLocus B hZ G g)
        (CurveFamily.fibreGenusLocus B hZ G g')) ∧
      (⋃ g : ℕ, CurveFamily.fibreGenusLocus B hZ G g) = Set.univ ∧
      ∀ g : ℕ, ∃ W : Subfunctor (schemeSpace G.base).obj,
        Space.IsOpenSubspace B integerBase hZ W ∧
        Set.range (Space.pointsMap B integerBase hZ W.toFunctor W.ι) =
          CurveFamily.fibreGenusLocus B hZ G g ∧
        ∀ (F : CurveFamily B hZ) (a : F ⟶ G),
          (IsSmoothH0FamilyOfFibreGenus B hZ g F ↔
            ∃ t : (schemeSpace F.base).obj ⟶ W.toFunctor,
              t ≫ W.ι = (schemeSpaceMap a.baseMap).hom) ∧
          (IsSmoothH0FamilyOfFibreGenus B hZ g F ↔
            Set.range (Space.pointsMap B integerBase hZ (schemeSpace F.base).obj
              (schemeSpaceMap a.baseMap).hom) ⊆ CurveFamily.fibreGenusLocus B hZ G g)

AlgebraicGeometry.factors_moduliSmoothCurvesOfGenus_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ModuliSmoothCurvesGenusDecomposition.lean, line 244. The attribute's comment: “part (1), with smooth of relative dimension one in (b): read with smooth of arbitrary relative dimension, (b) ⟹ (a) fails for g = 0, see not_factors_moduliSmoothCurvesOfGenus_zero_of_identity”.

Let f : X → S be a family of curves, classified by a scheme-valued point y of the stack of curves over S with y(S) ≅ X. The following are equivalent:

(a) the classifying morphism S → Curves factors through 𝓜_g (AlgebraicGeometry.moduliSmoothCurvesOfGenus): y lifts to the full subcategory of the families of 𝓜_g;

(b) X → S is smooth of relative dimension one, f_*𝒪_X = 𝒪_S and this holds after any base change, and R¹f_*𝒪_X is a locally free 𝒪_S-module of rank g.

The source writes "smooth" in (b); with no relative dimension (b) ⟹ (a) fails for g = 0 (AlgebraicGeometry.not_factors_moduliSmoothCurvesOfGenus_zero_of_identity), and (b) is stated with the relative dimension one that membership in 𝓜 (Stacks 0E81) requires.

theorem factors_moduliSmoothCurvesOfGenus_iff (g : ℕ) (U : BigFppfOver B integerBase hZ)
    (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ)
    (_hy : y ⋙ curvesProjectionOver B hZ = Over.map U.hom) (X : CurveFamily B hZ)
    (e : y.obj (Over.mk (𝟙 U.left)) ≅ X) :
    (∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
        ObjectProperty.FullSubcategory (IsSmoothH0FamilyOfFibreGenus B hZ g),
        z ⋙ ObjectProperty.ι (IsSmoothH0FamilyOfFibreGenus B hZ g) = y) ↔
      IsSmoothDimOneFamily B hZ X ∧ HasUniversallyBijectiveGlobalFunctions B hZ X ∧
        CurveFamily.HasGenus B hZ X g

AlgebraicGeometry.factors_moduliSmoothCurvesOfGenus_over_field_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ModuliSmoothCurvesGenusDecomposition.lean, line 323. The attribute's comment: “part (2): over a field, (a) the classifying morphism factors through 𝓜_g, (b)-(e) the conditions on X”.

Let X be a scheme proper over a field k with dim(X) ≤ 1, let k̄ be an algebraic closure of k and g ≥ 0. The following are equivalent:

(a) the classifying morphism Spec(k) → Curves of X factors through 𝓜_g (AlgebraicGeometry.moduliSmoothCurvesOfGenus): a scheme-valued point y of Curves over U with y(U) ≅ X lifts to the full subcategory of the families of 𝓜_g;

(b) X is smooth, dim(X) = 1, k = H⁰(X, 𝒪_X), and X has genus g;

(c) X is smooth, dim(X) = 1, X is geometrically connected, and X has genus g;

(d) X is smooth, dim(X) = 1, X is geometrically integral, and X has genus g;

(e) X_{k̄} is a smooth curve of genus g over k̄.

theorem factors_moduliSmoothCurvesOfGenus_over_field_iff (g : ℕ) {k : Type u} [Field k]
    (hk : B.Contains (Spec (.of k))) (X : Over (Spec (.of k))) [IsProper X.hom]
    (hdim : topologicalKrullDim X.left ≤ 1) (K : Type u) [Field K] [Algebra k K]
    [IsAlgClosure k K] :
    (∀ (U : BigFppfOver B integerBase hZ)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
      y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
      (y.obj (Over.mk (𝟙 U.left)) ≅ curveFamilyOfScheme X B hZ hk hdim) →
      ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
          ObjectProperty.FullSubcategory (IsSmoothH0FamilyOfFibreGenus B hZ g),
          z ⋙ ObjectProperty.ι (IsSmoothH0FamilyOfFibreGenus B hZ g) = y) ↔
        Smooth X.hom ∧ topologicalKrullDim X.left = 1 ∧
          IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ X.hom.appTop) ∧ genus X.hom = g)) ∧
    List.TFAE [
      Smooth X.hom ∧ topologicalKrullDim X.left = 1 ∧
        IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ X.hom.appTop) ∧ genus X.hom = g,
      Smooth X.hom ∧ topologicalKrullDim X.left = 1 ∧ GeometricallyConnected X.hom ∧
        genus X.hom = g,
      Smooth X.hom ∧ topologicalKrullDim X.left = 1 ∧ GeometricallyIntegral X.hom ∧
        genus X.hom = g,
      Smooth (pullback.snd X.hom (Spec.map (CommRingCat.ofHom (algebraMap k K)))) ∧
        IsCurve K (pullback.snd X.hom (Spec.map (CommRingCat.ofHom (algebraMap k K)))) ∧
        genus (pullback.snd X.hom (Spec.map (CommRingCat.ofHom (algebraMap k K)))) = g]

Tag 0E84, a lemma

Tag 0E84 in the Stacks Project.

AlgebraicGeometry.isSmoothOverIntegers_moduliSmoothCurves_and_moduliSmoothCurvesOfGenus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ModuliSmoothCurvesSmoothness.lean, line 67. The attribute's comment: “both morphisms 𝓜 → Spec(ℤ) and 𝓜_g → Spec(ℤ), for every g”.

The morphisms 𝓜 → Spec(ℤ) and, for every g, 𝓜_g → Spec(ℤ) are smooth. Here 𝓜 = Curves^{smooth, h0} and 𝓜_g are the open substacks of the algebraic stack of curves (Stacks 0D5A) of the families smooth of relative dimension one with f_*𝒪_X = 𝒪_S universally, and of those with moreover all fibres of genus g. Both are open substacks of Curves^{lci+}, which is smooth over Spec(ℤ) (Stacks 0DZX).

theorem isSmoothOverIntegers_moduliSmoothCurves_and_moduliSmoothCurvesOfGenus :
    IsSmoothOverIntegers B hZ (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, w} B hZ)
        (C1590Private.isOpenCurvesLocus_isSmoothH0Family_of B hZ
          (C1590Private.isOpenCurvesLocus_hasUniversallyBijectiveGlobalFunctions_of
            (C1590Private.isOpenCurvesLocus_hasBijectiveGlobalFunctionsOnFieldFibres_of
              (C1590Private.hasEtaleLocalSchemeCharts B hZ))
            (C1590Private.hasUniversallyBijectiveGlobalFunctions_of
              (C1590Private.hasEtaleLocalSchemeCharts B hZ)))) ∧
      ∀ g : ℕ, IsSmoothOverIntegers B hZ
        (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, w} B hZ)
        (IsOpenCurvesLocus.of_iff (Q := IsSmoothH0FamilyOfFibreGenus B hZ g)
          (C1590Private.isOpenCurvesLocus_isSmoothH0FamilyOfFibreGenus_of
            (C1590Private.isOpenCurvesLocus_hasUniversallyBijectiveGlobalFunctions_of
              (C1590Private.isOpenCurvesLocus_hasBijectiveGlobalFunctionsOnFieldFibres_of
                (C1590Private.hasEtaleLocalSchemeCharts B hZ))
              (C1590Private.hasUniversallyBijectiveGlobalFunctions_of
                (C1590Private.hasEtaleLocalSchemeCharts B hZ)))
            (C1590Private.prestableGenusLociOpen_of (C1590Private.hasEtaleLocalSchemeCharts B hZ))
            g)
          fun _ => Iff.rfl)

Sources

LeanAlgebraicGeometry.CurveFamily.isOpen_smoothBaseLocus · AlgebraicGeometry.CurveFamily.preimage_smoothBaseLocus · AlgebraicGeometry.CurveFamily.exists_isOpenSubspace_smooth · AlgebraicGeometry.curvesSmooth_isStrictlyFull · AlgebraicGeometry.CurvesSmooth · AlgebraicGeometry.isSmoothDimOneFamily_iff_isSmoothFamily_and_isCohenMacaulayDimOneFamily · AlgebraicGeometry.CurveFamily.isOpen_smoothDimOneBaseLocus · AlgebraicGeometry.CurveFamily.isOpen_smoothDimOneBaseLocus_of_isSmoothFamily

Section109.17 Density of smooth curves #

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

Tag 0E86, a lemma

Tag 0E86 in the Stacks Project.

AlgebraicGeometry.curvesPointSet_smooth_isOpen_dense_in_lciPlus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSmoothDensePoints.lean, line 140.

Stacks 0E86. The inclusion |Curves^{smooth}| ⊂ |Curves^{lci+}| is that of an open dense subset.

Curves^{smooth} is the substack of the stack of curves of smooth families of curves, and Curves^{lci+} that of families X ⟶ S which are local complete intersection morphisms whose singular locus is finite over S (Stacks 0DZX); |Curves^{smooth}| and |Curves^{lci+}| are their images in |Curves|, with the topology of Stacks 04Y8, and |Curves^{lci+}| carries the subspace topology.

theorem curvesPointSet_smooth_isOpen_dense_in_lciPlus :
    curvesPointSet B hZ (IsSmoothFamily B hZ) ⊆ curvesPointSet B hZ (IsLciPlusFamily B hZ) ∧
      IsOpen (Subtype.val ⁻¹' curvesPointSet B hZ (IsSmoothFamily B hZ) :
        Set (curvesPointSet B hZ (IsLciPlusFamily B hZ))) ∧
      Dense (Subtype.val ⁻¹' curvesPointSet B hZ (IsSmoothFamily B hZ) :
        Set (curvesPointSet B hZ (IsLciPlusFamily B hZ)))

Sources

LeanAlgebraicGeometry.curvesPointSet_smooth_isOpen_dense_in_lciPlus

Section109.18 Nodal curves #

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

Tag 0DSY, a lemma

Tag 0DSY in the Stacks Project.

AlgebraicGeometry.nodalCurvesOpenSubstack, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesNodal.lean, line 1133. The attribute's comment: “the open substack and part (1): the characterisation on every family of curves, given a presentation of the algebraic stack of curves. Part (2), the characterisation for a proper scheme over a field, is NOT asserted here”.

Stacks 0DSY, part (1). The open substack Curves^{nodal} of families of curves which are at-worst-nodal of relative dimension one, together with the characterisation of its objects: an object of the stack belongs to it exactly when the family of curves it classifies is at-worst-nodal of relative dimension one.

The algebraic stack of curves is a hypothesis: 𝒳 is any algebraic stack over the big fppf site of the integers whose objects are identified with families of curves by an equivalence E over that site.

Part (2) of the source, the characterisation for a proper scheme over a field, is not asserted here.

The definition carries @[no_expose]: its body names the private helpers that build the substack, so it may not be exposed. Nothing downstream needs to unfold it — the characterisation of its objects is the second component of the subtype.

def nodalCurvesOpenSubstack
    (𝒳 : Stack.AlgebraicStacks.{u, w} B integerBase hZ)
    (E : CurveFamily B hZ ≌ 𝒳.val.val.obj)
    (hE : E.functor ⋙ 𝒳.val.val.p = curvesProjectionOver B hZ) :
    {U : Stack.OpenSubstack 𝒳 //
      ∀ F : CurveFamily B hZ,
        U.property (E.functor.obj F) ↔
          Space.IsAtWorstNodalOfRelativeDimensionOne B integerBase hZ F.toBase.hom}

AlgebraicGeometry.classifying_factors_nodalCurvesOpenSubstack_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesNodal.lean, line 1202. The attribute's comment: “part (1): the classifying morphism of a family factors through the nodal open substack iff the family is at-worst-nodal of relative dimension one, given a presentation of the algebraic stack of curves. Part (2), the characterisation for a proper scheme over a field, is NOT asserted here”.

Stacks 0DSY, part (1). The classifying object of a family of curves lifts through the inclusion of the nodal open substack exactly when the family is at-worst-nodal of relative dimension one.

As for AlgebraicGeometry.nodalCurvesOpenSubstack, the algebraic stack of curves and its identification with families of curves are hypotheses.

theorem classifying_factors_nodalCurvesOpenSubstack_iff
    (𝒳 : Stack.AlgebraicStacks.{u, w} B integerBase hZ)
    (E : CurveFamily B hZ ≌ 𝒳.val.val.obj)
    (hE : E.functor ⋙ 𝒳.val.val.p = curvesProjectionOver B hZ)
    (F : CurveFamily B hZ) :
    (∃ Y : (nodalCurvesOpenSubstack B hZ 𝒳 E hE).1.property.FullSubcategory,
      Y.obj = E.functor.obj F) ↔
      Space.IsAtWorstNodalOfRelativeDimensionOne B integerBase hZ F.toBase.hom

AlgebraicGeometry.lifts_nodalCurves_curveFamilyOfProperOverField_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesNodalOverField.lean, line 190. The attribute's comment: “part (2): for a scheme X proper over a field k with dim(X) ≤ 1, the classifying morphism Spec(k) → Curves factors through Curves^{nodal} if and only if the singularities of X are at-worst-nodal and X is equidimensional of dimension 1. Factoring through the substack is lifting the classifying object through the inclusion of the strictly full subcategory of at-worst-nodal families, as in AlgebraicGeometry.lifts_nodalCurves_iff; no part of Tag 04S6 is assumed, and this declaration carries no hypothesis beyond the source's”.

Stacks 0DSY, part (2). Let k be a field and let X ⟶ Spec(k) be a morphism of the big fppf site of the integers which is proper and whose source has dimension at most one. The classifying morphism Spec(k) → Curves of the attached family of curves factors through Curves^{nodal} — that is, that family lifts through the inclusion of the strictly full subcategory of families which are at-worst-nodal of relative dimension one — if and only if the singularities of X are at worst nodal and X is equidimensional of dimension one.

The hypotheses are those of the source: X is proper over the field and of dimension at most one. Nothing else is assumed; in particular this does not use the hypothesis AlgebraicGeometry.Stack.Bootstrap04S6Spaces on which AlgebraicGeometry.nodalCurvesOpenSubstackUnconditional — the open substack itself, part of the same tag — is conditional, because factoring through the substack is tested by lifting the classifying object through the inclusion, and that inclusion is constructed unconditionally.

"Equidimensional of dimension one" is read as the source's definition reads it: X is equidimensional and every irreducible component of X has dimension one.

theorem lifts_nodalCurves_curveFamilyOfProperOverField_iff
    {T W : BigFppfOver B integerBase hZ} (g : T ⟶ W) (k : Type u) [Field k]
    (hW : (BigFppfOver.toScheme B integerBase hZ).obj W = Spec (.of k))
    (hproper : IsProper ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hdim : topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) ≤ 1) :
    letI : ((BigFppfOver.toScheme B integerBase hZ).obj T).Over (Spec (.of k)) :=
      ⟨(BigFppfOver.toScheme B integerBase hZ).map g ≫ eqToHom hW⟩
    ((∃ Y : (isNodalCurveFamily B hZ).FullSubcategory,
        Y.obj = curveFamilyOfProperOverFieldEqSpec B hZ g k hW hproper hdim) ↔
      (Stacks.Curves.HasAtWorstNodalSingularities k
          ((BigFppfOver.toScheme B integerBase hZ).obj T) ∧
        Equidimensional ((BigFppfOver.toScheme B integerBase hZ).obj T) ∧
        ∀ Z ∈ irreducibleComponents ((BigFppfOver.toScheme B integerBase hZ).obj T),
          topologicalKrullDim Z = (1 : WithBot ℕ∞)))

AlgebraicGeometry.lifts_nodalCurvesInclusion_curveFamilyOfProperOverField_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesNodalOverField.lean, line 236. The attribute's comment: “part (2), stated through the inclusion 1-morphism AlgebraicGeometry.nodalCurvesInclusion of the open substack: for a scheme X proper over a field k with dim(X) ≤ 1, the classifying morphism Spec(k) → Curves factors through Curves^nodal if and only if the singularities of X are at-worst-nodal and X is equidimensional of dimension 1. Unconditional: no presentation of Curves as an algebraic stack (Tag 0D5A) and no part of Tag 04S6 is assumed, and this declaration carries no hypothesis beyond the source's”.

Stacks 0DSY, part (2). Let k be a field and let X ⟶ Spec(k) be a morphism of the big fppf site of the integers which is proper and whose source has dimension at most one. The classifying morphism Spec(k) → Curves of the attached family of curves factors through the open substack Curves^{nodal} if and only if the singularities of X are at worst nodal and X is equidimensional of dimension one.

This is AlgebraicGeometry.lifts_nodalCurves_curveFamilyOfProperOverField_iff with factoring through Curves^{nodal} read as being in the image on objects of the 1-morphism AlgebraicGeometry.nodalCurvesInclusion, so that the statement is about the same object as the other registrations of the tag: the strictly full subcategory AlgebraicGeometry.nodalCurvesFiberedCategory of the fibred category of families of curves, whose inclusion is proved representable by algebraic spaces and an open immersion in AlgebraicGeometry.isRepresentableByAlgebraicSpaces_nodalCurvesInclusion and AlgebraicGeometry.isOpenImmersion_nodalCurvesInclusion.

The hypotheses are those of the source: X is proper over the field and of dimension at most one. Nothing else is assumed; in particular there is no algebraic stack 𝒳, no equivalence identifying it with the category of families of curves, and no part of Stacks 04S6.

"Equidimensional of dimension one" is read as the source's definition reads it: X is equidimensional and every irreducible component of X has dimension one.

theorem lifts_nodalCurvesInclusion_curveFamilyOfProperOverField_iff
    {T W : BigFppfOver B integerBase hZ} (g : T ⟶ W) (k : Type u) [Field k]
    (hW : (BigFppfOver.toScheme B integerBase hZ).obj W = Spec (.of k))
    (hproper : IsProper ((BigFppfOver.toScheme B integerBase hZ).map g))
    (hdim : topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) ≤ 1) :
    letI : ((BigFppfOver.toScheme B integerBase hZ).obj T).Over (Spec (.of k)) :=
      ⟨(BigFppfOver.toScheme B integerBase hZ).map g ≫ eqToHom hW⟩
    ((∃ Y : (nodalCurvesFiberedCategory B hZ).based.obj,
        (CatFiberedInGroupoids.homFunctor (nodalCurvesInclusion B hZ)).obj Y =
          curveFamilyOfProperOverFieldEqSpec B hZ g k hW hproper hdim) ↔
      (Stacks.Curves.HasAtWorstNodalSingularities k
          ((BigFppfOver.toScheme B integerBase hZ).obj T) ∧
        Equidimensional ((BigFppfOver.toScheme B integerBase hZ).obj T) ∧
        ∀ Z ∈ irreducibleComponents ((BigFppfOver.toScheme B integerBase hZ).obj T),
          topologicalKrullDim Z = (1 : WithBot ℕ∞)))

AlgebraicGeometry.isNodalCurveFamily_of_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesNodalUnconditional.lean, line 70. The attribute's comment: “the open substack Curves^nodal, base-change clause: the at-worst-nodal condition is inherited along every morphism of families of curves, and a morphism of families is a cartesian square, so the subcategory is closed under base change. Unconditional: no presentation of Curves as an algebraic stack (Tag 0D5A) and no part of Tag 04S6 is assumed”.

A family of curves mapping to an at-worst-nodal family of relative dimension one is itself at-worst-nodal of relative dimension one.

theorem isNodalCurveFamily_of_hom {F G : CurveFamily B hZ} (a : F ⟶ G)
    (hG : isNodalCurveFamily B hZ G) : isNodalCurveFamily B hZ F

AlgebraicGeometry.isClosedUnderIsomorphisms_isNodalCurveFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesNodalUnconditional.lean, line 80. The attribute's comment: “the open substack Curves^nodal, strict-fullness clause: the at-worst-nodal condition is invariant under isomorphism of families of curves, so it cuts a strictly full subcategory out of Curves. Unconditional: no presentation of Curves as an algebraic stack (Tag 0D5A) and no part of Tag 04S6 is assumed”.

Stacks 0DSY. The nodal condition cuts a strictly full subcategory out of the category of families of curves: it is invariant under isomorphism.

theorem isClosedUnderIsomorphisms_isNodalCurveFamily :
    (isNodalCurveFamily B hZ).IsClosedUnderIsomorphisms

AlgebraicGeometry.nodalCurvesOpenSubstackUnconditional, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesNodalUnconditional.lean, line 111. The attribute's comment: “the open substack and part (1): the characterisation on every family of curves, given a presentation of the algebraic stack of curves. Part (2), the characterisation for a proper scheme over a field, is registered separately on AlgebraicGeometry.lifts_nodalCurves_curveFamilyOfProperOverField_iff”.

Stacks 0DSY, part (1). The open substack Curves^{nodal} of families of curves which are at-worst-nodal of relative dimension one, together with the characterisation of its objects: an object of the stack belongs to it exactly when the family of curves it classifies is at-worst-nodal of relative dimension one.

This is AlgebraicGeometry.curvesOpenSubstackOfBaseLocus, the method of Section 109.6, at the locus AlgebraicGeometry.exists_nodal_baseOpen.

The algebraic stack of curves is a hypothesis: 𝒳 is any algebraic stack over the big fppf site of the integers whose objects are identified with families of curves by an equivalence E over that site. Nothing else is assumed; in particular no part of Stacks 04S6 is, the algebraic-stack field of the substack coming from the unconditional Stacks 05UM.

Part (2) of the source, the characterisation for a proper scheme over a field, is not asserted here.

The definition carries @[no_expose]: its body names the private helpers that build the substack, so it may not be exposed. Nothing downstream needs to unfold it — the characterisation of its objects is the second component of the subtype.

def nodalCurvesOpenSubstackUnconditional
    (𝒳 : Stack.AlgebraicStacks.{u, w} B integerBase hZ)
    (E : CurveFamily B hZ ≌ 𝒳.val.val.obj)
    (hE : E.functor ⋙ 𝒳.val.val.p = curvesProjectionOver B hZ) :
    {U : Stack.OpenSubstack 𝒳 //
      ∀ F : CurveFamily B hZ,
        U.property (E.functor.obj F) ↔
          Space.IsAtWorstNodalOfRelativeDimensionOne B integerBase hZ F.toBase.hom}

AlgebraicGeometry.classifying_factors_nodalCurvesOpenSubstack_iff_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesNodalUnconditional.lean, line 133. The attribute's comment: “part (1): the classifying morphism of a family factors through the nodal open substack iff the family is at-worst-nodal of relative dimension one, given a presentation of the algebraic stack of curves. Part (2), the characterisation for a proper scheme over a field, is registered separately on AlgebraicGeometry.lifts_nodalCurves_curveFamilyOfProperOverField_iff”.

Stacks 0DSY, part (1). The classifying object of a family of curves lifts through the inclusion of the nodal open substack exactly when the family is at-worst-nodal of relative dimension one.

As for AlgebraicGeometry.nodalCurvesOpenSubstackUnconditional, the algebraic stack of curves and its identification with families of curves are hypotheses, and nothing else is assumed.

theorem classifying_factors_nodalCurvesOpenSubstack_iff_unconditional
    (𝒳 : Stack.AlgebraicStacks.{u, w} B integerBase hZ)
    (E : CurveFamily B hZ ≌ 𝒳.val.val.obj)
    (hE : E.functor ⋙ 𝒳.val.val.p = curvesProjectionOver B hZ)
    (F : CurveFamily B hZ) :
    (∃ Y : (nodalCurvesOpenSubstackUnconditional B hZ 𝒳 E hE).1.property.FullSubcategory,
      Y.obj = E.functor.obj F) ↔
      Space.IsAtWorstNodalOfRelativeDimensionOne B integerBase hZ F.toBase.hom

AlgebraicGeometry.nodalCurvesFiberedCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesNodalUnconditional.lean, line 158. The attribute's comment: “the open substack Curves^nodal itself, as the strictly full subcategory of Curves spanned by the families which are at-worst-nodal of relative dimension one, read as an object of the 2-category of categories fibred in groupoids over the big fppf site of Spec(Z). Unconditional: no presentation of Curves as an algebraic stack (Tag 0D5A) and no part of Tag 04S6 is assumed”.

Stacks 0DSY. The category Curves^{nodal} of families of curves which are at-worst-nodal of relative dimension one, as an object of the 2-category of categories fibred in groupoids over the big fppf site of Spec(ℤ).

def nodalCurvesFiberedCategory :
    CatFiberedInGroupoids.{u, u + 1, u + 1, u + 1} (BigFppfOver B integerBase hZ)

AlgebraicGeometry.nodalCurvesInclusion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesNodalUnconditional.lean, line 168. The attribute's comment: “the inclusion Curves^nodal ⊂ Curves of the open substack, as a 1-morphism of categories fibred in groupoids over the big fppf site of Spec(Z). Unconditional: no presentation of Curves as an algebraic stack (Tag 0D5A) and no part of Tag 04S6 is assumed”.

Stacks 0DSY. The inclusion Curves^{nodal} ⊂ Curves, as a 1-morphism of categories fibred in groupoids over the big fppf site of Spec(ℤ).

def nodalCurvesInclusion :
    nodalCurvesFiberedCategory B hZ ⟶ curvesFiberedCategory B hZ

AlgebraicGeometry.isRepresentableByAlgebraicSpaces_nodalCurvesInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesNodalUnconditional.lean, line 178. The attribute's comment: “the open substack Curves^nodal, representability clause: the inclusion Curves^nodal ⊂ Curves is representable by algebraic spaces. Unconditional: no presentation of Curves as an algebraic stack (Tag 0D5A) and no part of Tag 04S6 is assumed”.

Stacks 0DSY. The inclusion Curves^{nodal} ⊂ Curves is representable by algebraic spaces.

theorem isRepresentableByAlgebraicSpaces_nodalCurvesInclusion :
    Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ (nodalCurvesInclusion B hZ).hom

AlgebraicGeometry.isOpenImmersion_nodalCurvesInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesNodalUnconditional.lean, line 189. The attribute's comment: “the open substack Curves^nodal, open-immersion clause: the inclusion Curves^nodal ⊂ Curves is an open immersion in the sense of Tag 04XB. Unconditional: no presentation of Curves as an algebraic stack (Tag 0D5A) and no part of Tag 04S6 is assumed”.

Stacks 0DSY. The inclusion Curves^{nodal} ⊂ Curves is an open immersion: every algebraic space representing one of its base changes along a scheme-valued point of Curves has open immersion structural morphism.

theorem isOpenImmersion_nodalCurvesInclusion :
    Stack.IsOpenImmersion B integerBase hZ (nodalCurvesInclusion B hZ)

AlgebraicGeometry.lifts_nodalCurves_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesNodalUnconditional.lean, line 201. The attribute's comment: “part (1): the classifying morphism of a family of curves factors through Curves^nodal -- that is, the family lifts through the inclusion of the strictly full subcategory -- if and only if the family is at-worst-nodal of relative dimension one. Unconditional: no presentation of Curves as an algebraic stack (Tag 0D5A) and no part of Tag 04S6 is assumed”.

Stacks 0DSY, part (1). A family of curves lifts through the inclusion Curves^{nodal} ⊂ Curves exactly when it is at-worst-nodal of relative dimension one.

theorem lifts_nodalCurves_iff (F : CurveFamily B hZ) :
    (∃ Y : (isNodalCurveFamily B hZ).FullSubcategory, Y.obj = F) ↔
      Space.IsAtWorstNodalOfRelativeDimensionOne B integerBase hZ F.toBase.hom

AlgebraicGeometry.lifts_nodalCurvesInclusion_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesNodalUnconditional.lean, line 225. The attribute's comment: “part (1), stated through the inclusion 1-morphism AlgebraicGeometry.nodalCurvesInclusion of the open substack: a family of curves is in the image on objects of Curves^nodal ⟶ Curves if and only if it is at-worst-nodal of relative dimension one. Unconditional: no presentation of Curves as an algebraic stack (Tag 0D5A) and no part of Tag 04S6 is assumed”.

Stacks 0DSY, part (1). The classifying morphism of a family of curves factors through Curves^{nodal} exactly when the family is at-worst-nodal of relative dimension one, where factoring through Curves^{nodal} is being in the image on objects of the 1-morphism AlgebraicGeometry.nodalCurvesInclusion itself.

This is AlgebraicGeometry.lifts_nodalCurves_iff read through that 1-morphism, so that part (1) is asserted about the very object whose inclusion is proved representable by algebraic spaces and an open immersion in AlgebraicGeometry.isRepresentableByAlgebraicSpaces_nodalCurvesInclusion and AlgebraicGeometry.isOpenImmersion_nodalCurvesInclusion.

The declaration carries no hypothesis beyond the site and its containing Spec(ℤ): there is no algebraic stack 𝒳 and no equivalence identifying it with the category of families of curves.

theorem lifts_nodalCurvesInclusion_iff (F : CurveFamily B hZ) :
    (∃ Y : (nodalCurvesFiberedCategory B hZ).based.obj,
        (CatFiberedInGroupoids.homFunctor (nodalCurvesInclusion B hZ)).obj Y = F) ↔
      Space.IsAtWorstNodalOfRelativeDimensionOne B integerBase hZ F.toBase.hom

Tag 0E00, a lemma

Tag 0E00 in the Stacks Project.

AlgebraicGeometry.isSmoothOverIntegers_curvesNodal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesNodalSmooth.lean, line 52.

The morphism Curves^{nodal} → Spec(ℤ) is smooth. Here Curves^{nodal} is the open substack of the algebraic stack of curves (Stacks 0D5A) of the families of curves which are at-worst-nodal of relative dimension one (Stacks 0DSY).

theorem isSmoothOverIntegers_curvesNodal :
    IsSmoothOverIntegers B hZ (C1590Private.isAlgebraicStack_curvesFiberedCategory.{u, w} B hZ)
      (isOpenCurvesLocus_isAtWorstNodal B hZ)

Sources

LeanAlgebraicGeometry.nodalCurvesOpenSubstack · AlgebraicGeometry.classifying_factors_nodalCurvesOpenSubstack_iff · AlgebraicGeometry.lifts_nodalCurves_curveFamilyOfProperOverField_iff · AlgebraicGeometry.lifts_nodalCurvesInclusion_curveFamilyOfProperOverField_iff · AlgebraicGeometry.isNodalCurveFamily_of_hom · AlgebraicGeometry.isClosedUnderIsomorphisms_isNodalCurveFamily · AlgebraicGeometry.nodalCurvesOpenSubstackUnconditional · AlgebraicGeometry.classifying_factors_nodalCurvesOpenSubstack_iff_unconditional

Section109.19 The relative dualizing sheaf #

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

Tag 0E6P, a lemma

Tag 0E6P in the Stacks Project.

AlgebraicGeometry.CurveFamily.exists_iso_shift_relativeDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeDualizingSheaf.lean, line 153.

Let f : X ⟶ S be a family of curves with Cohen–Macaulay fibres equidimensional of dimension one (Stacks 0E1F: f is Cohen–Macaulay in the sense of Stacks 0E0V and has relative dimension one in the sense of part (2) of Stacks 06LR), and let (ω^•_{X/S}, τ) be a relative dualizing complex of f (Stacks 0E5X). Then ω^•_{X/S} = ω_{X/S}[1] for a pseudo-coherent 𝒪_X-module ω_{X/S} flat over S whose formation commutes with arbitrary base change: for every morphism of families of curves X' ⟶ X over S' ⟶ S (a cartesian square), every relative dualizing complex of X'/S' is (g'^*ω_{X/S})[1], g' : X' ⟶ X the projection.

theorem CurveFamily.exists_iso_shift_relativeDualizingComplex (X : CurveFamily B hZ)
    (hcm : Space.IsCohenMacaulay B integerBase hZ X.toBase.hom)
    (hdim : Space.HasRelativeDimension 1 B integerBase hZ X.toBase.hom)
    (D : RelativeDualizingComplex B.contains_terminal X.toBase X.proper X.flat
      X.finitePresentation) :
    ∃ F : Space.Modules.{u, u} B integerBase hZ X.total.1 X.total.2,
      Nonempty (D.ω ≅ ((DerivedCategory.singleFunctor _ 0).obj F)⟦(1 : ℤ)⟧) ∧
      (Space.smallEtaleRingedSite B integerBase hZ X.total.1 X.total.2).IsPseudoCoherent
        ((DerivedCategory.singleFunctor _ 0).obj F) ∧
      Space.IsFlatOver B integerBase hZ X.total.2 X.toBase.hom F ∧
      ∀ {X' : CurveFamily B hZ} (φ : X' ⟶ X)
        (D' : RelativeDualizingComplex B.contains_terminal X'.toBase X'.proper X'.flat
          X'.finitePresentation),
        Nonempty (D'.ω ≅ (smallEtaleDerivedModulePullback B integerBase hZ φ.totalMap).obj
          (((DerivedCategory.singleFunctor _ 0).obj F)⟦(1 : ℤ)⟧)) ∧
        Nonempty ((smallEtaleDerivedModulePullback B integerBase hZ φ.totalMap).obj
            ((DerivedCategory.singleFunctor
              (SheafOfModules.{u} (ringedToposStructureRingSheaf B integerBase hZ X.total))
                0).obj F) ≅
          (DerivedCategory.singleFunctor
            (SheafOfModules.{u} (ringedToposStructureRingSheaf B integerBase hZ X'.total)) 0).obj
            ((modulePullback B integerBase hZ φ.totalMap).obj F))

Tag 0E6Q, a definition

Tag 0E6Q in the Stacks Project.

AlgebraicGeometry.CurveFamily.relativeDualizingSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeDualizingSheaf.lean, line 131.

Let f : X ⟶ S be a family of curves and (ω^•_{X/S}, τ) its relative dualizing complex (Stacks 0E5X). The relative dualizing sheaf of f is the 𝒪_X-module ω_{X/S} = H^{-1}(ω^•_{X/S}). For a Cohen–Macaulay family of relative dimension one it is the pseudo-coherent module flat over S of Stacks 0E6P, with ω^•_{X/S} = ω_{X/S}[1] (AlgebraicGeometry.CurveFamily.exists_iso_shift_relativeDualizingComplex).

def CurveFamily.relativeDualizingSheaf (X : CurveFamily B hZ)
    (D : RelativeDualizingComplex B.contains_terminal X.toBase X.proper X.flat
      X.finitePresentation) :
    Space.Modules.{u, u} B integerBase hZ X.total.1 X.total.2

Tag 0E6R, a lemma

Tag 0E6R in the Stacks Project.

AlgebraicGeometry.CurveFamily.isInvertibleModule_relativeDualizingSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/RelativeDualizingSheaf.lean, line 582.

Let f : X ⟶ S be a family of curves with Gorenstein fibres equidimensional of dimension one (Curves^{Gorenstein, 1} of Stacks 0E6M: f is Gorenstein in the sense of Stacks 0E14 and has relative dimension one in the sense of part (2) of Stacks 06LR), and let (ω^•_{X/S}, τ) be a relative dualizing complex (Stacks 0E5X). Then the relative dualizing sheaf ω_{X/S} = H^{-1}(ω^•_{X/S}) (Stacks 0E6Q) is an invertible 𝒪_X-module, and its formation commutes with arbitrary base change: for every morphism of families of curves X' ⟶ X over S' ⟶ S (a cartesian square) and every relative dualizing complex of X'/S', the relative dualizing sheaf of X'/S' is the pullback of ω_{X/S} along the projection g' : X' ⟶ X.

theorem CurveFamily.isInvertibleModule_relativeDualizingSheaf (X : CurveFamily B hZ)
    (hX : IsGorensteinDimOneFamily B hZ X)
    (D : RelativeDualizingComplex B.contains_terminal X.toBase X.proper X.flat
      X.finitePresentation) :
    Space.IsInvertibleModule X.total (X.relativeDualizingSheaf D) ∧
      ∀ {X' : CurveFamily B hZ} (φ : X' ⟶ X)
        (D' : RelativeDualizingComplex B.contains_terminal X'.toBase X'.proper X'.flat
          X'.finitePresentation),
        Nonempty (X'.relativeDualizingSheaf D' ≅
          (modulePullback B integerBase hZ φ.totalMap).obj (X.relativeDualizingSheaf D))

Sources

LeanAlgebraicGeometry.CurveFamily.exists_iso_shift_relativeDualizingComplex · AlgebraicGeometry.CurveFamily.relativeDualizingSheaf · AlgebraicGeometry.CurveFamily.isInvertibleModule_relativeDualizingSheaf

Section109.20 Prestable curves #

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

Tag 0E6T, a definition

Tag 0E6T in the Stacks Project.

AlgebraicGeometry.IsPrestableCurveFamily, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PrestableCurveFamilies.lean, line 88.

Stacks 0E6T. A family of curves is prestable when its structure morphism is at-worst-nodal of relative dimension one and the direct image of its structure sheaf is the structure sheaf of the base, universally.

abbrev IsPrestableCurveFamily (X : CurveFamily B hZ) : Prop

Tag 0E6U, a lemma

Tag 0E6U in the Stacks Project.

AlgebraicGeometry.factors_curvesPrestable_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesPrestableSubstack.lean, line 75. The attribute's comment: “part (1)”.

The classifying morphism of a family of curves X ⟶ S factors through the strictly full subcategory Curves^{prestable} of prestable families (Stacks 0E6T) exactly when X ⟶ S is prestable: a scheme-valued point y of Curves over U lifts to Curves^{prestable} exactly when the family y(U) it classifies is prestable.

theorem factors_curvesPrestable_iff (U : BigFppfOver B integerBase hZ)
    (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ)
    (hy : y ⋙ curvesProjectionOver B hZ = Over.map U.hom) :
    (∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
        ObjectProperty.FullSubcategory (IsPrestableCurveFamily B hZ),
        z ⋙ ObjectProperty.ι (IsPrestableCurveFamily B hZ) = y) ↔
      IsPrestableCurveFamily B hZ (y.obj (Over.mk (𝟙 U.left)))

AlgebraicGeometry.factors_curvesPrestable_over_field_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesPrestableSubstack.lean, line 94. The attribute's comment: “part (2)”.

Let X be a proper scheme over a field k with dim(X) ≤ 1 (with Spec k in the site, so that its classifying morphism Spec k ⟶ Curves exists). The classifying morphism of X factors through Curves^{prestable} exactly when the singularities of X are at-worst-nodal, dim(X) = 1 and k = H⁰(X, 𝒪_X).

theorem factors_curvesPrestable_over_field_iff
    (k : Type u) [Field k] (hk : B.Contains (Spec (.of k)))
    (X : Over (Spec (.of k))) [IsProper X.hom] (hdim : topologicalKrullDim X.left ≤ 1)
    (U : BigFppfOver B integerBase hZ)
    (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ)
    (hy : y ⋙ curvesProjectionOver B hZ = Over.map U.hom)
    (e : y.obj (Over.mk (𝟙 U.left)) ≅ curveFamilyOfScheme X B hZ hk hdim) :
    (∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
        ObjectProperty.FullSubcategory (IsPrestableCurveFamily B hZ),
        z ⋙ ObjectProperty.ι (IsPrestableCurveFamily B hZ) = y) ↔
      ((letI : X.left.Over (Spec (.of k)) := ⟨X.hom⟩;
        Stacks.Curves.HasAtWorstNodalSingularities k X.left) ∧
        topologicalKrullDim X.left = 1 ∧ IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ X.hom.appTop))

AlgebraicGeometry.curvesPrestable_isOpenSubstack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesPrestableSubstack.lean, line 143. The attribute's comment: “the open substack Curves^{prestable} of Curves”.

Curves^{prestable}, the strictly full subcategory of prestable families of curves (Stacks 0E6T), is an open substack of Curves: prestability is invariant under isomorphism, and the inclusion Curves^{prestable} ⟶ Curves is representable by algebraic spaces and an open immersion.

theorem curvesPrestable_isOpenSubstack :
    ObjectProperty.IsClosedUnderIsomorphisms (IsPrestableCurveFamily B hZ) ∧
      Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (curvesSubstackInclusion B hZ (IsPrestableCurveFamily B hZ)
          CurveFamily.isPrestableCurveFamily_of_hom).hom ∧
      Stack.IsOpenImmersion B integerBase hZ
        (curvesSubstackInclusion B hZ (IsPrestableCurveFamily B hZ)
          CurveFamily.isPrestableCurveFamily_of_hom)

AlgebraicGeometry.curvesPrestable_isOpenSubstack_and_factors_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesPrestableSubstack.lean, line 163. The attribute's comment: “the whole statement: the open substack Curves^{prestable} and parts (1) and (2)”.

There is an open substack Curves^{prestable} ⊂ Curves — the strictly full subcategory of prestable families of curves, whose inclusion is representable by algebraic spaces and an open immersion — such that

the classifying morphism of a family of curves X ⟶ S factors through it exactly when X ⟶ S is a prestable family of curves, and

for a scheme X proper over a field k with dim(X) ≤ 1, the classifying morphism Spec k ⟶ Curves of X factors through it exactly when the singularities of X are at-worst-nodal, dim(X) = 1 and k = H⁰(X, 𝒪_X).

theorem curvesPrestable_isOpenSubstack_and_factors_iff :
    (ObjectProperty.IsClosedUnderIsomorphisms (IsPrestableCurveFamily B hZ) ∧
      Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (curvesSubstackInclusion B hZ (IsPrestableCurveFamily B hZ)
          CurveFamily.isPrestableCurveFamily_of_hom).hom ∧
      Stack.IsOpenImmersion B integerBase hZ
        (curvesSubstackInclusion B hZ (IsPrestableCurveFamily B hZ)
          CurveFamily.isPrestableCurveFamily_of_hom)) ∧
    (∀ (U : BigFppfOver B integerBase hZ)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
      y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
      ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
          ObjectProperty.FullSubcategory (IsPrestableCurveFamily B hZ),
          z ⋙ ObjectProperty.ι (IsPrestableCurveFamily B hZ) = y) ↔
        IsPrestableCurveFamily B hZ (y.obj (Over.mk (𝟙 U.left))))) ∧
    (∀ (k : Type u) [Field k] (hk : B.Contains (Spec (.of k)))
      (X : Over (Spec (.of k))) [IsProper X.hom] (hdim : topologicalKrullDim X.left ≤ 1)
      (U : BigFppfOver B integerBase hZ)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
      y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
      (y.obj (Over.mk (𝟙 U.left)) ≅ curveFamilyOfScheme X B hZ hk hdim) →
      ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
          ObjectProperty.FullSubcategory (IsPrestableCurveFamily B hZ),
          z ⋙ ObjectProperty.ι (IsPrestableCurveFamily B hZ) = y) ↔
        ((letI : X.left.Over (Spec (.of k)) := ⟨X.hom⟩;
          Stacks.Curves.HasAtWorstNodalSingularities k X.left) ∧
          topologicalKrullDim X.left = 1 ∧
          IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ X.hom.appTop))))

Tag 0E6V, a lemma

Tag 0E6V in the Stacks Project.

AlgebraicGeometry.curvesPrestableGenus_isOpenSubstack_and_factors_iff_and_decomposition_and_over_field_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesPrestableGenusDecomposition.lean, line 229.

Stacks 0E6V. There is a decomposition Curves^{prestable} = ∐_{g ≥ 0} Curves^{prestable}_g into open and closed substacks, where 1. the classifying morphism of a family of curves f : X → S factors through Curves^{prestable}_g exactly when f is a prestable family of curves and R¹f_*𝒪_X is a locally free 𝒪_S-module of rank g; 2. for a scheme X proper over a field k with dim(X) ≤ 1 (a proper morphism p : T ⟶ W of the site with W = Spec k), the classifying morphism Spec k → Curves of X factors through Curves^{prestable}_g exactly when the singularities of X are at-worst-nodal, dim(X) = 1, k = H⁰(X, 𝒪_X) and the genus of X is g.

Each Curves^{prestable}_g is an open substack of Curves contained in Curves^{prestable} (the first conjunct, with the second), and over every scheme-valued point of Curves^{prestable} — a prestable family G over a scheme S — the loci Ω_g ⊂ S of the Curves^{prestable}_g are open and closed, pairwise disjoint and cover S, a family mapping to G lying in Curves^{prestable}_g exactly when its base maps into Ω_g (the third conjunct): this is the decomposition into open and closed substacks.

theorem curvesPrestableGenus_isOpenSubstack_and_factors_iff_and_decomposition_and_over_field_iff :
    (∀ g : ℕ,
      (ObjectProperty.IsClosedUnderIsomorphisms (IsPrestableGenusCurveFamily B hZ g) ∧
        Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
          (curvesSubstackInclusion B hZ (IsPrestableGenusCurveFamily B hZ g)
            (isOpenCurvesLocus_isPrestableGenusCurveFamily g).prop_of_hom).hom ∧
        Stack.IsOpenImmersion B integerBase hZ
          (curvesSubstackInclusion B hZ (IsPrestableGenusCurveFamily B hZ g)
            (isOpenCurvesLocus_isPrestableGenusCurveFamily g).prop_of_hom)) ∧
      (∀ X : CurveFamily B hZ, IsPrestableGenusCurveFamily B hZ g X →
        IsPrestableCurveFamily B hZ X) ∧
      ∀ (U : BigFppfOver B integerBase hZ)
        (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
        y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
        ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
            ObjectProperty.FullSubcategory (IsPrestableGenusCurveFamily B hZ g),
            z ⋙ ObjectProperty.ι (IsPrestableGenusCurveFamily B hZ g) = y) ↔
          IsPrestableCurveFamily B hZ (y.obj (Over.mk (𝟙 U.left))) ∧
            RingedSite.IsFiniteLocallyFreeOfRank
              (Space.smallEtaleRingedSite B integerBase hZ
                (schemeSpace (y.obj (Over.mk (𝟙 U.left))).base).1
                (schemeSpace (y.obj (Over.mk (𝟙 U.left))).base).2)
              ((y.obj (Over.mk (𝟙 U.left))).firstDirectImage B hZ) g)) ∧
    (∀ G : CurveFamily B hZ, IsPrestableCurveFamily B hZ G →
      ∃ Ω : ℕ → Set (Space.points B integerBase hZ (schemeSpace G.base).obj),
        (∀ g, IsOpen (Ω g) ∧ IsClosed (Ω g)) ∧ Pairwise (fun g g' => Disjoint (Ω g) (Ω g')) ∧
          (⋃ g, Ω g) = Set.univ ∧
          ∀ (g : ℕ) (F : CurveFamily B hZ) (a : F ⟶ G),
            IsPrestableGenusCurveFamily B hZ g F ↔
              Set.range (Space.pointsMap B integerBase hZ (schemeSpace F.base).obj
                (schemeSpaceMap a.baseMap).hom) ⊆ Ω g) ∧
    (∀ (g : ℕ) (k : Type u) [Field k] {T W : BigFppfOver B integerBase hZ} (p : T ⟶ W)
      (hW : (BigFppfOver.toScheme B integerBase hZ).obj W = Spec (.of k))
      (hproper : IsProper ((BigFppfOver.toScheme B integerBase hZ).map p))
      (hdim : topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) ≤ 1)
      (U : BigFppfOver B integerBase hZ)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
      y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
      (y.obj (Over.mk (𝟙 U.left)) ≅ curveFamilyOverFieldOfProper B hZ p k hW hproper hdim) →
      letI : ((BigFppfOver.toScheme B integerBase hZ).obj T).Over (Spec (.of k)) :=
        ⟨(BigFppfOver.toScheme B integerBase hZ).map p ≫ eqToHom hW⟩
      ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
          ObjectProperty.FullSubcategory (IsPrestableGenusCurveFamily B hZ g),
          z ⋙ ObjectProperty.ι (IsPrestableGenusCurveFamily B hZ g) = y) ↔
        (Stacks.Curves.HasAtWorstNodalSingularities k
            ((BigFppfOver.toScheme B integerBase hZ).obj T) ∧
          topologicalKrullDim ((BigFppfOver.toScheme B integerBase hZ).obj T) = 1 ∧
          Function.Bijective
            ((BigFppfOver.toScheme B integerBase hZ).map p ≫ eqToHom hW).appTop ∧
          genus ((BigFppfOver.toScheme B integerBase hZ).map p ≫ eqToHom hW) = g)))

Tag 0E6W, a lemma

Tag 0E6W in the Stacks Project.

AlgebraicGeometry.isSmoothOverIntegers_curvesPrestable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesPrestableSmooth.lean, line 76. The attribute's comment: “the morphism Curves^{prestable} → Spec(ℤ) is smooth”.

The morphism Curves^{prestable} → Spec(ℤ) is smooth. Here Curves^{prestable} is the open substack of the algebraic stack of curves (Stacks 0D5A) of the prestable families of curves (Stacks 0E6U).

theorem isSmoothOverIntegers_curvesPrestable :
    IsSmoothOverIntegers B hZ (isAlgebraicStack_curvesFiberedCategory.{u, w} B hZ)
      (isOpenCurvesLocus_isPrestableCurveFamily B hZ)

AlgebraicGeometry.isSmoothOverIntegers_curvesPrestableOfGenus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesPrestableSmooth.lean, line 86. The attribute's comment: “the morphism Curves^{prestable}_g → Spec(ℤ) is smooth, for every g”.

For every g, the morphism Curves^{prestable}_g → Spec(ℤ) is smooth. Here Curves^{prestable}_g is the open substack of the algebraic stack of curves (Stacks 0D5A) of the prestable families f : X → S with R¹f_*𝒪_X locally free of rank g (Stacks 0E6V, part (1)).

theorem isSmoothOverIntegers_curvesPrestableOfGenus (g : ℕ) :
    IsSmoothOverIntegers B hZ (isAlgebraicStack_curvesFiberedCategory.{u, w} B hZ)
      (isOpenCurvesLocus_isPrestableGenusCurveFamily (B := B) (hZ := hZ) g)

Sources

LeanAlgebraicGeometry.IsPrestableCurveFamily · AlgebraicGeometry.factors_curvesPrestable_iff · AlgebraicGeometry.factors_curvesPrestable_over_field_iff · AlgebraicGeometry.curvesPrestable_isOpenSubstack · AlgebraicGeometry.curvesPrestable_isOpenSubstack_and_factors_iff · AlgebraicGeometry.curvesPrestableGenus_isOpenSubstack_and_factors_iff_and_decomposition_and_over_field_iff · AlgebraicGeometry.isSmoothOverIntegers_curvesPrestable · AlgebraicGeometry.isSmoothOverIntegers_curvesPrestableOfGenus

Section109.21 Semistable curves #

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

Tag 0E6Y, a lemma

Tag 0E6Y in the Stacks Project.

AlgebraicGeometry.CurveFamily.hasNoRationalTailFibre_iff_isCounitSurjectiveAbove, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/NoRationalTailDualizingPowerCounit.lean, line 149.

Let f : X → S be a prestable family of curves of genus g ≥ 1, with relative dualizing complex ω^•_{X/S} and relative dualizing sheaf ω_{X/S} = H^{-1}(ω^•_{X/S}). Let s ∈ S and m ≥ 2. The fibre X_s has no rational tail if and only if f^*f_*ω_{X/S}^{⊗ m} ⟶ ω_{X/S}^{⊗ m} is surjective over f⁻¹(U) for some open U ∋ s.

theorem hasNoRationalTailFibre_iff_isCounitSurjectiveAbove (X : CurveFamily B hZ)
    (hX : IsPrestableCurveFamily B hZ X) {g : ℕ} (hg : X.HasGenus B hZ g) (hg1 : 1 ≤ g)
    (D : Space.RelativeDualizingComplex B.contains_terminal X.toBase X.proper X.flat
      X.finitePresentation)
    (s : (BigFppfOver.toScheme B integerBase hZ).obj X.base) {m : ℕ} (hm : 2 ≤ m) :
    X.HasNoRationalTailFibre B hZ (X.residueFieldPoint s) ↔
      X.IsCounitSurjectiveAbove
        (@Space.invertibleTensorPower B integerBase hZ X.total.1 X.total.2
          (X.dualizingSheafOfComplex D) (isInvertible_dualizingSheafOfComplex hX D) m) s

Tag 0E6Z, a definition

Tag 0E6Z in the Stacks Project.

AlgebraicGeometry.IsSemistableCurveFamily, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/SemistableCurveFamilies.lean, line 78.

Stacks 0E6Z. A family of curves is semistable when it is prestable and, for every point of the base, its fibre there has genus at least one and no rational tail.

abbrev IsSemistableCurveFamily (X : CurveFamily B hZ) : Prop

Tag 0E70, a lemma

Tag 0E70 in the Stacks Project.

AlgebraicGeometry.curvesSemistable_isOpenSubstack_and_factors_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSemistableSubstack.lean, line 97. The attribute's comment: “the whole statement: the open substack Curves^{semistable} and parts (1) and (2)”.

There is an open substack Curves^{semistable} ⊂ Curves — the strictly full subcategory of semistable families of curves (Stacks 0E6Z), whose inclusion is representable by algebraic spaces and an open immersion — such that

the classifying morphism of a family of curves X ⟶ S factors through it exactly when X ⟶ S is a semistable family of curves, and

for a scheme X proper over a field k with dim(X) ≤ 1 (with Spec k in the site, so that its classifying morphism Spec k ⟶ Curves exists), the classifying morphism of X factors through it (a) exactly when (b) the singularities of X are at-worst-nodal, dim(X) = 1, k = H⁰(X, 𝒪_X), the genus of X is at least one and X has no rational tail, and (a) exactly when (c) the singularities of X are at-worst-nodal, dim(X) = 1, k = H⁰(X, 𝒪_X) and ω_X^{⊗ m} is globally generated for every m ≥ 2.

theorem curvesSemistable_isOpenSubstack_and_factors_iff :
    (ObjectProperty.IsClosedUnderIsomorphisms (IsSemistableCurveFamily B hZ) ∧
      Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (curvesSubstackInclusion B hZ (IsSemistableCurveFamily B hZ)
          (CurveFamily.isSemistableCurveFamily_of_hom B hZ)).hom ∧
      Stack.IsOpenImmersion B integerBase hZ
        (curvesSubstackInclusion B hZ (IsSemistableCurveFamily B hZ)
          (CurveFamily.isSemistableCurveFamily_of_hom B hZ))) ∧
    (∀ (U : BigFppfOver B integerBase hZ)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
      y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
      ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
          ObjectProperty.FullSubcategory (IsSemistableCurveFamily B hZ),
          z ⋙ ObjectProperty.ι (IsSemistableCurveFamily B hZ) = y) ↔
        IsSemistableCurveFamily B hZ (y.obj (Over.mk (𝟙 U.left))))) ∧
    (∀ (k : Type u) [Field k] (hk : B.Contains (Spec (.of k)))
      (X : Over (Spec (.of k))) [IsProper X.hom] (hdim : topologicalKrullDim X.left ≤ 1)
      (U : BigFppfOver B integerBase hZ)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
      y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
      (y.obj (Over.mk (𝟙 U.left)) ≅ curveFamilyOfScheme X B hZ hk hdim) →
      ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
          ObjectProperty.FullSubcategory (IsSemistableCurveFamily B hZ),
          z ⋙ ObjectProperty.ι (IsSemistableCurveFamily B hZ) = y) ↔
        letI : X.left.Over (Spec (.of k)) := ⟨X.hom⟩
        Stacks.Curves.HasAtWorstNodalSingularities k X.left ∧ topologicalKrullDim X.left = 1 ∧
          IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ X.hom.appTop) ∧ 1 ≤ genus X.hom ∧
            ∀ C : X.left.IdealSheafData, ¬ IsRationalTail k X.left C) ∧
      ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
          ObjectProperty.FullSubcategory (IsSemistableCurveFamily B hZ),
          z ⋙ ObjectProperty.ι (IsSemistableCurveFamily B hZ) = y) ↔
        letI : X.left.Over (Spec (.of k)) := ⟨X.hom⟩
        haveI : IsProper (X.left ↘ Spec (.of k)) := inferInstanceAs (IsProper X.hom)
        ∃ (hnodal : Stacks.Curves.HasAtWorstNodalSingularities k X.left)
          (hdim1 : topologicalKrullDim X.left = 1)
          (hΓ : IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ X.hom.appTop)),
          haveI : IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X.left ↘ Spec (.of k)).appTop) := hΓ
          haveI := connectedSpace_of_isIso_globalSections k (X.left ↘ Spec (.of k))
          letI := isInvertible_dualizingSheafOverField_of_hasAtWorstNodalSingularities k X.left
            hdim1 hnodal
          ∀ m : ℕ, 2 ≤ m → SheafOfModules.IsGeneratedByGlobalSections
            (tensorPower X.left.presheaf X.left.ringCatSheaf.2
              (Stacks.Duality.dualizingSheafOverField (X.left ↘ Spec (.of k))) m)))

Tag 0E71, a lemma

Tag 0E71 in the Stacks Project.

AlgebraicGeometry.curvesSemistableOfGenus_isOpenSubstack_and_factors_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSemistableGenusDecomposition.lean, line 93. The attribute's comment: “the decomposition Curves^{semistable} = ∐_{g ≥ 1} Curves^{semistable}_g into open and closed substacks, and part (1)”.

For every g, Curves^{semistable}_g is an open substack of Curves contained in Curves^{semistable}: its inclusion is representable by algebraic spaces and an open immersion. Part (1): the classifying morphism of a family of curves f : X → S factors through Curves^{semistable}_g exactly when f is semistable and R¹f_*𝒪_X is a locally free 𝒪_S-module of rank g. Over every semistable family with base S, the loci of the Curves^{semistable}_g are open and closed subsets of S, pairwise disjoint, empty for g = 0 and covering S for g ≥ 1: so Curves^{semistable} = ∐_{g ≥ 1} Curves^{semistable}_g as open and closed substacks.

theorem curvesSemistableOfGenus_isOpenSubstack_and_factors_iff :
    (∀ g : ℕ,
      ((show ObjectProperty (CurveFamily B hZ) from
          IsSemistableCurveFamilyOfFibreGenus B hZ g).IsClosedUnderIsomorphisms ∧
        Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
          (curvesSubstackInclusion B hZ (IsSemistableCurveFamilyOfFibreGenus B hZ g)
            (isOpenCurvesLocus_isSemistableCurveFamilyOfFibreGenus
              (isOpenCurvesLocus_isSemistableCurveFamily_of
                (isOpenCurvesLocus_hasBijectiveGlobalFunctionsOnFieldFibres_of
                  (hasEtaleLocalSchemeCharts B hZ))
                (hasUniversallyBijectiveGlobalFunctions_of (hasEtaleLocalSchemeCharts B hZ))
                (prestableSemistableFibresOpen B hZ))
              (prestableGenusLociOpen_of (hasEtaleLocalSchemeCharts B hZ)) g).prop_of_hom).hom ∧
        Stack.IsOpenImmersion B integerBase hZ
          (curvesSubstackInclusion B hZ (IsSemistableCurveFamilyOfFibreGenus B hZ g)
            (isOpenCurvesLocus_isSemistableCurveFamilyOfFibreGenus
              (isOpenCurvesLocus_isSemistableCurveFamily_of
                (isOpenCurvesLocus_hasBijectiveGlobalFunctionsOnFieldFibres_of
                  (hasEtaleLocalSchemeCharts B hZ))
                (hasUniversallyBijectiveGlobalFunctions_of (hasEtaleLocalSchemeCharts B hZ))
                (prestableSemistableFibresOpen B hZ))
              (prestableGenusLociOpen_of (hasEtaleLocalSchemeCharts B hZ)) g).prop_of_hom)) ∧
      (∀ X : CurveFamily B hZ,
        IsSemistableCurveFamilyOfFibreGenus B hZ g X → IsSemistableCurveFamily B hZ X) ∧
      ∀ (U : BigFppfOver B integerBase hZ)
        (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
        y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
        ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
            ObjectProperty.FullSubcategory (IsSemistableCurveFamilyOfFibreGenus B hZ g),
            z ⋙ ObjectProperty.ι (IsSemistableCurveFamilyOfFibreGenus B hZ g) = y) ↔
          IsSemistableCurveFamily B hZ (y.obj (Over.mk (𝟙 U.left))) ∧
            CurveFamily.HasGenus B hZ (y.obj (Over.mk (𝟙 U.left))) g)) ∧
    ∀ G : CurveFamily B hZ, IsSemistableCurveFamily B hZ G →
      ∃ Ω : ℕ → Set ((BigFppfOver.toScheme B integerBase hZ).obj G.base),
        (∀ g, IsOpen (Ω g) ∧ IsClosed (Ω g)) ∧ Pairwise (fun g g' => Disjoint (Ω g) (Ω g')) ∧
          Ω 0 = ∅ ∧ ⋃ (g : ℕ) (_ : 1 ≤ g), Ω g = Set.univ ∧
          ∀ (g : ℕ) (F : CurveFamily B hZ) (a : F ⟶ G),
            IsSemistableCurveFamilyOfFibreGenus B hZ g F ↔
              Set.range ((BigFppfOver.toScheme B integerBase hZ).map a.baseMap) ⊆ Ω g

AlgebraicGeometry.factors_curvesSemistableOfGenus_over_field_iff_noRationalTail_and_globallyGenerated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSemistableGenusDecomposition.lean, line 146. The attribute's comment: “part (2): (a) ⇔ (b) and (a) ⇔ (c), for a proper scheme of dimension at most one over a field”.

Let g ≥ 1 and let X be a proper scheme of dimension at most one over a field k (with Spec k in the site, so that the classifying morphism Spec k ⟶ Curves of X exists). The classifying morphism of X factors through Curves^{semistable}_g (a) exactly when (b) the singularities of X are at-worst-nodal, dim X = 1, k = H⁰(X, 𝒪_X), the genus of X is g and X has no rational tail, and (a) exactly when (c) the singularities of X are at-worst-nodal, dim X = 1, k = H⁰(X, 𝒪_X), the genus of X is g and ω_X^{⊗m} is globally generated for every m ≥ 2.

theorem factors_curvesSemistableOfGenus_over_field_iff_noRationalTail_and_globallyGenerated
    {g : ℕ} (hg : 1 ≤ g)
    {k : Type u} [Field k] (X : Over (Spec (.of k))) [IsProper X.hom]
    (hk : B.Contains (Spec (.of k))) (hdim : topologicalKrullDim X.left ≤ 1)
    (U : BigFppfOver B integerBase hZ) (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ)
    (hy : y ⋙ curvesProjectionOver B hZ = Over.map U.hom)
    (e : y.obj (Over.mk (𝟙 U.left)) ≅ curveFamilyOfScheme X B hZ hk hdim) :
    ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
        ObjectProperty.FullSubcategory (IsSemistableCurveFamilyOfFibreGenus B hZ g),
        z ⋙ ObjectProperty.ι (IsSemistableCurveFamilyOfFibreGenus B hZ g) = y) ↔
      letI : X.left.Over (Spec (.of k)) := ⟨X.hom⟩
      Stacks.Curves.HasAtWorstNodalSingularities k X.left ∧ topologicalKrullDim X.left = 1 ∧
        IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ X.hom.appTop) ∧ genus X.hom = g ∧
          ∀ C : X.left.IdealSheafData, ¬ IsRationalTail k X.left C) ∧
    ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
        ObjectProperty.FullSubcategory (IsSemistableCurveFamilyOfFibreGenus B hZ g),
        z ⋙ ObjectProperty.ι (IsSemistableCurveFamilyOfFibreGenus B hZ g) = y) ↔
      letI : X.left.Over (Spec (.of k)) := ⟨X.hom⟩
      haveI : IsProper (X.left ↘ Spec (.of k)) := inferInstanceAs (IsProper X.hom)
      ∃ (hnodal : Stacks.Curves.HasAtWorstNodalSingularities k X.left)
        (hdim1 : topologicalKrullDim X.left = 1)
        (hΓ : IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ X.hom.appTop)),
        haveI : IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X.left ↘ Spec (.of k)).appTop) := hΓ
        haveI := connectedSpace_of_isIso_globalSections k (X.left ↘ Spec (.of k))
        letI := isInvertible_dualizingSheafOverField_of_hasAtWorstNodalSingularities k X.left
          hdim1 hnodal
        genus X.hom = g ∧ ∀ m : ℕ, 2 ≤ m → SheafOfModules.IsGeneratedByGlobalSections
          (tensorPower X.left.presheaf X.left.ringCatSheaf.2
            (Stacks.Duality.dualizingSheafOverField (X.left ↘ Spec (.of k))) m))

Tag 0E72, a lemma

Tag 0E72 in the Stacks Project.

AlgebraicGeometry.isSmoothOverIntegers_curvesSemistable_and_curvesSemistableOfGenus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesSemistableSmoothness.lean, line 64. The attribute's comment: “both morphisms Curves^{semistable} → Spec(ℤ) and Curves^{semistable}_g → Spec(ℤ), for every g”.

The morphisms Curves^{semistable} → Spec(ℤ) and, for every g, Curves^{semistable}_g → Spec(ℤ) are smooth. Here Curves^{semistable} and Curves^{semistable}_g are the open substacks of the algebraic stack of curves (Stacks 0D5A) of the semistable families and of the semistable families with all fibres of genus g.

theorem isSmoothOverIntegers_curvesSemistable_and_curvesSemistableOfGenus :
    IsSmoothOverIntegers B hZ (isAlgebraicStack_curvesFiberedCategory.{u, w} B hZ)
        (isOpenCurvesLocus_isSemistableCurveFamily_of
          (isOpenCurvesLocus_hasBijectiveGlobalFunctionsOnFieldFibres_of
            (hasEtaleLocalSchemeCharts B hZ))
          (hasUniversallyBijectiveGlobalFunctions_of (hasEtaleLocalSchemeCharts B hZ))
          (prestableSemistableFibresOpen B hZ)) ∧
      ∀ g : ℕ, IsSmoothOverIntegers B hZ (isAlgebraicStack_curvesFiberedCategory.{u, w} B hZ)
        (isOpenCurvesLocus_isSemistableCurveFamilyOfFibreGenus
          (isOpenCurvesLocus_isSemistableCurveFamily_of
            (isOpenCurvesLocus_hasBijectiveGlobalFunctionsOnFieldFibres_of
              (hasEtaleLocalSchemeCharts B hZ))
            (hasUniversallyBijectiveGlobalFunctions_of (hasEtaleLocalSchemeCharts B hZ))
            (prestableSemistableFibresOpen B hZ))
          (prestableGenusLociOpen_of (hasEtaleLocalSchemeCharts B hZ)) g)

Sources

LeanAlgebraicGeometry.CurveFamily.hasNoRationalTailFibre_iff_isCounitSurjectiveAbove · AlgebraicGeometry.IsSemistableCurveFamily · AlgebraicGeometry.curvesSemistable_isOpenSubstack_and_factors_iff · AlgebraicGeometry.curvesSemistableOfGenus_isOpenSubstack_and_factors_iff · AlgebraicGeometry.factors_curvesSemistableOfGenus_over_field_iff_noRationalTail_and_globallyGenerated · AlgebraicGeometry.isSmoothOverIntegers_curvesSemistable_and_curvesSemistableOfGenus

Section109.22 Stable curves #

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

Tag 0E74, a lemma

Tag 0E74 in the Stacks Project.

AlgebraicGeometry.CurveFamily.hasNoRationalTailNoRationalBridge_iff_exists_isAffineOpen_isRelativelyAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/StableFamilyRelativeDualizingAmple.lean, line 403.

Let f : X → S be a prestable family of curves of genus g ≥ 2 (genus g read as in Stacks 0E6V: R¹f_*𝒪_X finite locally free of rank g) and let s ∈ S. The following are equivalent:

the fibre X_s has no rational tail and no rational bridge (Stacks 0E3H, 0E3M); the fibre is presented by a scheme V of the site with a cartesian square over Spec κ(s) → S, as in Stacks 0E75;

for some affine open U ∋ s, the relative dualizing sheaf ω_{f⁻¹(U)/U} (AlgebraicGeometry.CurveFamily.relativeDualizingSheafOver) is ample on f⁻¹(U) relative to U, for every presentation X₁ = f⁻¹(U) of the restricted family by a cartesian square.

theorem hasNoRationalTailNoRationalBridge_iff_exists_isAffineOpen_isRelativelyAmple
    (X : CurveFamily B hZ) (hX : IsPrestableCurveFamily B hZ X) (g : ℕ)
    (hgen : CurveFamily.HasGenus B hZ X g) (hg : 2 ≤ g)
    (s : (BigFppfOver.toScheme B integerBase hZ).obj X.base) :
    (∃ (V : BigFppfOver B integerBase hZ) (v : V ⟶ X.residuePoint B hZ s)
        (q : yoneda.obj V ⟶ X.total.obj),
        X.IsFibrePresentation B hZ s v q ∧
          HasNoRationalTailNoRationalBridge
            (((BigFppfOver.toScheme B integerBase hZ).obj X.base).residueField s)
            (X.fibreMap B hZ s v)) ↔
      ∃ U : ((BigFppfOver.toScheme B integerBase hZ).obj X.base).Opens,
        ∃ hU : IsAffineOpen U, s ∈ U ∧
        ∀ ⦃X₁ : AlgebraicSpaces B integerBase hZ⦄ (p₁ : X₁ ⟶ X.total)
          (f₁ : X₁ ⟶ schemeSpace (Space.openSub X.base U))
          (h : IsPullback p₁ f₁ X.toBase (schemeSpaceMap (Space.openSubHom X.base U))),
            Space.IsRelativelyAmple B integerBase hZ f₁ (X.relativeDualizingSheafOver hU h)

Tag 0E75, a definition

Tag 0E75 in the Stacks Project.

AlgebraicGeometry.IsStableCurveFamily, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/StableCurveFamilies.lean, line 108. References: SGA 7 I (5.1), “special case”.

Stacks 0E75. A family of curves is stable when it is prestable and, for every point of the base, its fibre there has genus at least two and has neither a rational tail nor a rational bridge.

The constituents. The family is an AlgebraicGeometry.CurveFamily: flat, proper, of finite presentation and of relative dimension at most one, from an algebraic space to a scheme of the site. Prestability is AlgebraicGeometry.IsPrestableCurveFamily. A point of the base is an AlgebraicGeometry.Space.FieldValuedPoint, a field p.carrier together with a morphism from its spectrum to the base, and the CategoryTheory.IsPullback clause exhibits the scheme V of the site as the fibre of the family over that point. The conditions on the fibre are collected in AlgebraicGeometry.HasGenusTwoNoRationalTailNoRationalBridge: its AlgebraicGeometry.genus over p.carrier is at least two, no ideal sheaf of V satisfies AlgebraicGeometry.IsRationalTail, and none satisfies AlgebraicGeometry.IsRationalBridge.

abbrev IsStableCurveFamily (X : CurveFamily B hZ) : Prop

Tag 0E76, a lemma

Tag 0E76 in the Stacks Project.

AlgebraicGeometry.curvesStable_isOpenSubstack_and_factors_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/CurvesStableOpenSubstack.lean, line 191.

There is an open substack Curves^{stable} ⊂ Curves — the strictly full subcategory of stable families of curves (Stacks 0E75), invariant under isomorphism, whose inclusion into Curves is representable by algebraic spaces and an open immersion — such that

given a family of curves f : X → U, the classifying morphism U → Curves factors through Curves^{stable} if and only if X → U is a stable family of curves: a scheme-valued point y of Curves over U lifts to Curves^{stable} exactly when the family y(U) it classifies is stable;

given a scheme X proper over a field k with dim(X) ≤ 1, the following are equivalent:

(a) the classifying morphism Spec(k) → Curves of X factors through Curves^{stable} (every scheme-valued point y with y(U) ≅ X lifts);

(b) the singularities of X are at-worst-nodal, dim(X) = 1, k = H⁰(X, 𝒪_X), the genus of X is at least two, and X has no rational tails and no rational bridges;

(c) the singularities of X are at-worst-nodal, dim(X) = 1, k = H⁰(X, 𝒪_X), and the dualizing sheaf ω_X is ample.

theorem curvesStable_isOpenSubstack_and_factors_iff :
    (ObjectProperty.IsClosedUnderIsomorphisms (IsStableCurveFamily B hZ) ∧
      Stack.IsRepresentableByAlgebraicSpaces B integerBase hZ
        (curvesSubstackInclusion B hZ (IsStableCurveFamily B hZ)
          CurveFamily.isStableCurveFamily_of_hom).hom ∧
      Stack.IsOpenImmersion B integerBase hZ
        (curvesSubstackInclusion B hZ (IsStableCurveFamily B hZ)
          CurveFamily.isStableCurveFamily_of_hom)) ∧
    (∀ (U : BigFppfOver B integerBase hZ)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
      y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
      ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
          ObjectProperty.FullSubcategory (IsStableCurveFamily B hZ),
          z ⋙ ObjectProperty.ι (IsStableCurveFamily B hZ) = y) ↔
        IsStableCurveFamily B hZ (y.obj (Over.mk (𝟙 U.left))))) ∧
    ∀ {k : Type u} [Field k] (hk : B.Contains (Spec (.of k)))
      (X : Over (Spec (.of k))) [IsProper X.hom] (hdim : topologicalKrullDim X.left ≤ 1),
      (∀ (U : BigFppfOver B integerBase hZ)
        (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
        y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
        (y.obj (Over.mk (𝟙 U.left)) ≅ curveFamilyOfScheme X B hZ hk hdim) →
        ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
            ObjectProperty.FullSubcategory (IsStableCurveFamily B hZ),
            z ⋙ ObjectProperty.ι (IsStableCurveFamily B hZ) = y) ↔
          letI : X.left.Over (Spec (.of k)) := ⟨X.hom⟩
          haveI : IsProper (X.left ↘ Spec (.of k)) := inferInstanceAs (IsProper X.hom)
          Stacks.Curves.HasAtWorstNodalSingularities k X.left ∧ topologicalKrullDim X.left = 1 ∧
            IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ X.hom.appTop) ∧ 2 ≤ genus X.hom ∧
            (∀ C : X.left.IdealSheafData, ¬ IsRationalTail k X.left C) ∧
            ∀ C : X.left.IdealSheafData, ¬ IsRationalBridge k X.left C)) ∧
      ((letI : X.left.Over (Spec (.of k)) := ⟨X.hom⟩
        haveI : IsProper (X.left ↘ Spec (.of k)) := inferInstanceAs (IsProper X.hom)
        Stacks.Curves.HasAtWorstNodalSingularities k X.left ∧ topologicalKrullDim X.left = 1 ∧
          IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ X.hom.appTop) ∧ 2 ≤ genus X.hom ∧
          (∀ C : X.left.IdealSheafData, ¬ IsRationalTail k X.left C) ∧
          ∀ C : X.left.IdealSheafData, ¬ IsRationalBridge k X.left C) ↔
        letI : X.left.Over (Spec (.of k)) := ⟨X.hom⟩
        haveI : IsProper (X.left ↘ Spec (.of k)) := inferInstanceAs (IsProper X.hom)
        ∃ (hnodal : Stacks.Curves.HasAtWorstNodalSingularities k X.left)
          (hdim1 : topologicalKrullDim X.left = 1)
          (hH0 : IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X.left ↘ Spec (.of k)).appTop)),
            haveI := hH0
            haveI := connectedSpace_of_isIso_globalSections k (X.left ↘ Spec (.of k))
            letI := isInvertible_dualizingSheafOverField_of_hasAtWorstNodalSingularities k X.left
              hdim1 hnodal
            Scheme.Modules.IsAmple X.left
              (Stacks.Duality.dualizingSheafOverField (X.left ↘ Spec (.of k))))

Tag 0E77, a definition

Tag 0E77 in the Stacks Project.

AlgebraicGeometry.moduliStableCurves, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ModuliCurves.lean, line 91. The attribute's comment: “the moduli stack of stable curves, 𝓜̄ = Curves^{stable}”.

The moduli stack 𝓜̄ = Curves^{stable} of stable curves: the substack of the stack of curves of the families of curves which are stable (Stacks 0E75), as a category fibred in groupoids over the big fppf site of Spec(ℤ).

def moduliStableCurves :
    CatFiberedInGroupoids.{u, u + 1, u + 1, u + 1} (BigFppfOver B integerBase hZ)

AlgebraicGeometry.moduliStableCurvesOfGenus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ModuliStableCurvesOfGenus.lean, line 143. The attribute's comment: “the moduli stack of stable curves of genus g, 𝓜̄_g”.

Stacks 0E77, 𝓜̄_g. The moduli stack 𝓜̄_g of stable curves of genus g: the substack of the stack of curves of the families f : X → S which are stable (Stacks 0E75) and whose fibre over every point of S has genus g, as a category fibred in groupoids over the big fppf site of Spec(ℤ). It lies in 𝓜̄ = AlgebraicGeometry.moduliStableCurves, and its points are the stable curves of genus g over fields, as in part (2) of Stacks 0E78.

def moduliStableCurvesOfGenus (g : ℕ) :
    CatFiberedInGroupoids.{u, u + 1, u + 1, u + 1} (BigFppfOver B integerBase hZ)

Tag 0E78, a lemma

Tag 0E78 in the Stacks Project.

AlgebraicGeometry.moduliStableCurves_decomposition_moduliStableCurvesOfGenus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ModuliStableCurvesGenusDecomposition.lean, line 130. The attribute's comment: “the decomposition of the moduli stack of stable curves into the open and closed substacks of stable curves of genus g >= 2, read on the scheme-valued points of the moduli stack, together with parts (1) and (2)”. References: SGA 7 I (5.1), “(2), special case”.

The decomposition of 𝓜̄ by the genus. The moduli stack of stable curves decomposes into open and closed substacks 𝓜̄ = ∐_{g ≥ 2} 𝓜̄_g (AlgebraicGeometry.moduliStableCurves, AlgebraicGeometry.moduliStableCurvesOfGenus), and:

Decomposition. For every scheme-valued point of 𝓜̄, that is every stable family of curves G over a scheme S, the loci fibreGenusLocus G g of the points of S whose fibre has genus g are open and closed in S; for g ≥ 2 they are pairwise disjoint and cover S; and an object F ⟶ G of 𝓜̄ over S lies in 𝓜̄_g exactly when its base lands in the locus of g. So 𝓜̄_g ×_{𝓜̄} S is the open and closed subscheme of S on that locus.

(1) Given a family of curves f : X → U, its classifying morphism U → Curves factors through 𝓜̄_g if and only if X → U is a stable family of curves and R¹f_*𝒪_X is a locally free 𝒪_U-module of rank g.

(2) Given a proper scheme X over a field k with dim(X) ≤ 1, the following are equivalent: (a) the classifying morphism Spec(k) → Curves factors through 𝓜̄_g; (b) the singularities of X are at-worst-nodal, dim(X) = 1, k = H⁰(X, 𝒪_X), the genus of X is g, and X has no rational tails or bridges; (c) the singularities of X are at-worst-nodal, dim(X) = 1, k = H⁰(X, 𝒪_X), the genus of X is g, and ω_X is ample.

theorem moduliStableCurves_decomposition_moduliStableCurvesOfGenus :
    (∀ G : CurveFamily B hZ, IsStableCurveFamily B hZ G →
      (∀ g : ℕ, IsClopen (CurveFamily.fibreGenusLocus B hZ G g)) ∧
        Pairwise (Function.onFun Disjoint
          fun g : {g : ℕ // 2 ≤ g} => CurveFamily.fibreGenusLocus B hZ G g) ∧
        ⋃ g : {g : ℕ // 2 ≤ g}, CurveFamily.fibreGenusLocus B hZ G g = Set.univ ∧
        ∀ (g : ℕ) (F : CurveFamily B hZ) (a : F ⟶ G),
          (IsStableCurveFamilyOfFibreGenus B hZ g F ↔
            Set.range (Space.pointsMap B integerBase hZ (schemeSpace F.base).obj
              (schemeSpaceMap a.baseMap).hom) ⊆ CurveFamily.fibreGenusLocus B hZ G g)) ∧
    (∀ (g : ℕ) (U : BigFppfOver B integerBase hZ)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
      y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
      ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
          ObjectProperty.FullSubcategory (IsStableCurveFamilyOfFibreGenus B hZ g),
          z ⋙ ObjectProperty.ι (IsStableCurveFamilyOfFibreGenus B hZ g) = y) ↔
        IsStableCurveFamily B hZ (y.obj (Over.mk (𝟙 U.left))) ∧
          CurveFamily.HasGenus B hZ (y.obj (Over.mk (𝟙 U.left))) g)) ∧
    ∀ {g : ℕ} (_hg : 2 ≤ g) {k : Type u} [Field k] (hk : B.Contains (Spec (.of k)))
      (X : Over (Spec (.of k))) [IsProper X.hom] (hdim : topologicalKrullDim X.left ≤ 1),
      (∀ (U : BigFppfOver B integerBase hZ)
        (y : BigFppfOver B U.left.1 U.left.2 ⥤ CurveFamily B hZ),
        y ⋙ curvesProjectionOver B hZ = Over.map U.hom →
        (y.obj (Over.mk (𝟙 U.left)) ≅ curveFamilyOfScheme X B hZ hk hdim) →
        ((∃ z : BigFppfOver B U.left.1 U.left.2 ⥤
            ObjectProperty.FullSubcategory (IsStableCurveFamilyOfFibreGenus B hZ g),
            z ⋙ ObjectProperty.ι (IsStableCurveFamilyOfFibreGenus B hZ g) = y) ↔
          letI : X.left.Over (Spec (.of k)) := ⟨X.hom⟩
          haveI : IsProper (X.left ↘ Spec (.of k)) := inferInstanceAs (IsProper X.hom)
          Stacks.Curves.HasAtWorstNodalSingularities k X.left ∧ topologicalKrullDim X.left = 1 ∧
            IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ X.hom.appTop) ∧ genus X.hom = g ∧
            (∀ C : X.left.IdealSheafData, ¬ IsRationalTail k X.left C) ∧
            ∀ C : X.left.IdealSheafData, ¬ IsRationalBridge k X.left C)) ∧
      ((letI : X.left.Over (Spec (.of k)) := ⟨X.hom⟩
        haveI : IsProper (X.left ↘ Spec (.of k)) := inferInstanceAs (IsProper X.hom)
        Stacks.Curves.HasAtWorstNodalSingularities k X.left ∧ topologicalKrullDim X.left = 1 ∧
          IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ X.hom.appTop) ∧ genus X.hom = g ∧
          (∀ C : X.left.IdealSheafData, ¬ IsRationalTail k X.left C) ∧
          ∀ C : X.left.IdealSheafData, ¬ IsRationalBridge k X.left C) ↔
        letI : X.left.Over (Spec (.of k)) := ⟨X.hom⟩
        haveI : IsProper (X.left ↘ Spec (.of k)) := inferInstanceAs (IsProper X.hom)
        ∃ (hnodal : Stacks.Curves.HasAtWorstNodalSingularities k X.left)
          (hdim1 : topologicalKrullDim X.left = 1)
          (hH0 : IsIso ((Scheme.ΓSpecIso (.of k)).inv ≫ (X.left ↘ Spec (.of k)).appTop)),
          genus X.hom = g ∧
            haveI := hH0
            haveI := connectedSpace_of_isIso_globalSections k (X.left ↘ Spec (.of k))
            letI := isInvertible_dualizingSheafOverField_of_hasAtWorstNodalSingularities k X.left
              hdim1 hnodal
            Scheme.Modules.IsAmple X.left
              (Stacks.Duality.dualizingSheafOverField (X.left ↘ Spec (.of k))))

Tag 0E79, a lemma

Tag 0E79 in the Stacks Project.

AlgebraicGeometry.isSmoothOverIntegers_moduliStableCurves_and_moduliStableCurvesOfGenus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/StableCurvesSmoothOverSpecZ.lean, line 118. The attribute's comment: “both morphisms: 𝓜̄ → Spec(ℤ) (first conjunct) and 𝓜̄_g → Spec(ℤ) for every g (second conjunct, for 𝓜̄_g cut out by R¹f_*𝒪_X locally free of rank g as in 0E78 (1), and by all fibres of genus g as in 0E77) are smooth”.

Stacks 0E79. The morphisms 𝓜̄ → Spec(ℤ) and, for every g, 𝓜̄_g → Spec(ℤ) are smooth. Here 𝓜̄ is the open substack of the algebraic stack of curves (Stacks 0D5A) of the stable families (Stacks 0E76), and 𝓜̄_g is its open substack of the stable families of genus g. The second conjunct states smoothness of 𝓜̄_g in both forms of its families: stable with R¹f_*𝒪_X locally free of rank g (part (1) of Stacks 0E78, AlgebraicGeometry.IsStableCurveFamilyOfGenus), and stable with every fibre of genus g (Stacks 0E77, AlgebraicGeometry.IsStableCurveFamilyOfFibreGenus); the two properties of families agree (AlgebraicGeometry.isStableCurveFamilyOfFibreGenus_iff_isStableCurveFamilyOfGenus), so they cut out the same open substack. Both 𝓜̄ and 𝓜̄_g are open substacks of Curves^{nodal}, which is smooth over Spec(ℤ) (Stacks 0E00).

The statement assumes nothing beyond the site B containing Spec(ℤ); the algebraicity of Curves (Stacks 0D5A), its limit preservation (Stacks 0D55) and the openness of 𝓜̄ and 𝓜̄_g are all proved.

theorem isSmoothOverIntegers_moduliStableCurves_and_moduliStableCurvesOfGenus :
    IsSmoothOverIntegers B hZ (isAlgebraicStack_curvesFiberedCategory.{u, w} B hZ)
        (isOpenCurvesLocus_isStableCurveFamily B hZ) ∧
      ∀ g : ℕ,
        IsSmoothOverIntegers B hZ (isAlgebraicStack_curvesFiberedCategory.{u, w} B hZ)
            (isOpenCurvesLocus_isStableCurveFamilyOfGenus_of_fibreGenus B hZ g) ∧
          IsSmoothOverIntegers B hZ (isAlgebraicStack_curvesFiberedCategory.{u, w} B hZ)
            (isOpenCurvesLocus_isStableCurveFamilyOfFibreGenus B hZ g)

Tag 0E7A, a lemma

Tag 0E7A in the Stacks Project.

AlgebraicGeometry.curvesSmall.moduliStableCurves_isOpenSubstack_curvesDM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ModuliStableCurvesOpenInCurvesDM.lean, line 54.

The stacks 𝓜̄ and 𝓜̄_g are open substacks of Curves^{DM}; in particular they are DM (Stacks 050D) and Deligne–Mumford stacks (Stacks 03YO).

In the statement, Curves is the algebraic stack AlgebraicGeometry.curvesAlgebraicStack (the small model of the stack of curves, equivalent over the site to the category of families of curves through AlgebraicGeometry.curvesSmallEquivalence), algebraic by Stacks 0D5A (AlgebraicGeometry.curvesFiberedCategory_isAlgebraicStack). W is Curves^{DM}: the open substack whose objects are those of the Deligne–Mumford locus Stack.dmLocus (Stacks 0DSW), and it is DM. M is 𝓜̄: an open substack of Curves whose objects are exactly the stable families of curves (Stacks 0E75), the families of AlgebraicGeometry.moduliStableCurves; M_g is 𝓜̄_g: an open substack whose objects are exactly the stable families whose fibre over every point has genus g, the families of AlgebraicGeometry.moduliStableCurvesOfGenus (Stacks 0E77, 0E78). Both are contained in W (an open substack of Curves contained in the open substack W is an open substack of W), DM, and Deligne–Mumford stacks.

The statement holds for every g, not only in the range g ≥ 2 of Stacks 0E77.

theorem moduliStableCurves_isOpenSubstack_curvesDM (g : ℕ) :
    ∃ W M Mg : Stack.OpenSubstack
        (curvesAlgebraicStack B hZ (curvesFiberedCategory_isAlgebraicStack.{u, w} B hZ)),
      (W.property =
          Stack.dmLocus B integerBase hZ B.contains_terminal
            (curvesAlgebraicStack B hZ (curvesFiberedCategory_isAlgebraicStack.{u, w} B hZ)) ∧
        Stack.AlgebraicStacks.IsAbsolutelyDM B integerBase hZ B.contains_terminal
          W.toAlgebraicStack) ∧
      ((∀ F : CurveFamily B hZ,
          M.property ((curvesSmallEquivalence B hZ
            (curvesFiberedCategory_isAlgebraicStack.{u, w} B hZ)).functor.obj F) ↔
            IsStableCurveFamily B hZ F) ∧
        M.property ≤ W.property ∧
        Stack.AlgebraicStacks.IsAbsolutelyDM B integerBase hZ B.contains_terminal
          M.toAlgebraicStack ∧
        Stack.IsDeligneMumfordStack.{u, w} B integerBase hZ M.toAlgebraicStack.val.val) ∧
      ((∀ F : CurveFamily B hZ,
          Mg.property ((curvesSmallEquivalence B hZ
            (curvesFiberedCategory_isAlgebraicStack.{u, w} B hZ)).functor.obj F) ↔
            IsStableCurveFamilyOfFibreGenus B hZ g F) ∧
        Mg.property ≤ W.property ∧
        Stack.AlgebraicStacks.IsAbsolutelyDM B integerBase hZ B.contains_terminal
          Mg.toAlgebraicStack ∧
        Stack.IsDeligneMumfordStack.{u, w} B integerBase hZ Mg.toAlgebraicStack.val.val)

Tag 0E87, a lemma

Tag 0E87 in the Stacks Project.

AlgebraicGeometry.curvesPointSet_moduliSmoothOfGenus_isOpen_dense_in_stableOfGenus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/ModuliSmoothCurvesOpenDense.lean, line 323.

Let g ≥ 2. The inclusion |𝓜_g| ⊂ |𝓜̄_g| is that of an open dense subset.

𝓜_g is the substack of the stack of curves of families f : X → S which are smooth of relative dimension one with f_*𝒪_X = 𝒪_S universally and R¹f_*𝒪_X locally free of rank g (Stacks 0E83), and 𝓜̄_g that of stable families with R¹f_*𝒪_X locally free of rank g (Stacks 0E78); |𝓜_g| and |𝓜̄_g| are their images in |Curves|, with the topology of Stacks 04Y8, and |𝓜̄_g| carries the subspace topology.

theorem curvesPointSet_moduliSmoothOfGenus_isOpen_dense_in_stableOfGenus
    (g : ℕ) (hg : 2 ≤ g) :
    curvesPointSet B hZ (fun F => IsSmoothH0Family B hZ F ∧ CurveFamily.HasGenus B hZ F g) ⊆
        curvesPointSet B hZ (IsStableCurveFamilyOfGenus B hZ g) ∧
      IsOpen (Subtype.val ⁻¹' curvesPointSet B hZ
          (fun F => IsSmoothH0Family B hZ F ∧ CurveFamily.HasGenus B hZ F g) :
        Set (curvesPointSet B hZ (IsStableCurveFamilyOfGenus B hZ g))) ∧
      Dense (Subtype.val ⁻¹' curvesPointSet B hZ
          (fun F => IsSmoothH0Family B hZ F ∧ CurveFamily.HasGenus B hZ F g) :
        Set (curvesPointSet B hZ (IsStableCurveFamilyOfGenus B hZ g)))

Sources

LeanAlgebraicGeometry.CurveFamily.hasNoRationalTailNoRationalBridge_iff_exists_isAffineOpen_isRelativelyAmple · AlgebraicGeometry.IsStableCurveFamily · AlgebraicGeometry.curvesStable_isOpenSubstack_and_factors_iff · AlgebraicGeometry.moduliStableCurves · AlgebraicGeometry.moduliStableCurvesOfGenus · AlgebraicGeometry.moduliStableCurves_decomposition_moduliStableCurvesOfGenus · AlgebraicGeometry.isSmoothOverIntegers_moduliStableCurves_and_moduliStableCurvesOfGenus · AlgebraicGeometry.curvesSmall.moduliStableCurves_isOpenSubstack_curvesDM

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

109.3 The stack of curves to 109.22 Stable curves

Section109.3 The stack of curves#

Tag 0DMK, a lemma

Sources

Section109.4 The stack of polarized curves#

Tag 0DPY, the section

Tag 0DPZ, a lemma

Tag 0DQ0, a lemma

Tag 0E6F, a lemma

Sources

Section109.5 Properties of the stack of curves#

Tag 0DSQ, a lemma

Tag 0DSS, a lemma

Sources

Section109.6 Open substacks of the stack of curves#

Tag 0E0E, the section

Sources

Section109.7 Curves with finite reduced automorphism groups#

Tag 0DSU, an example

Tag 0DSV, an example

Tag 0DSW, a lemma

Tag 0E6G, a lemma

Sources

Section109.8 Cohen-Macaulay curves#

Tag 0E0I, a lemma

Tag 0E1F, a lemma

Sources

Section109.9 Curves of a given genus#

Tag 0E6I, a lemma

Tag 0E6J, a lemma

Tag 0E1J, a lemma

Tag 0E6K, a lemma

Sources

Section109.10 Geometrically reduced curves#

Tag 0E0G, a lemma

Tag 0E1G, a lemma

Sources

Section109.11 Geometrically reduced and connected curves#

Tag 0E1I, a lemma

Tag 0E6L, a lemma

Tag 0E1K, a lemma

Sources

Section109.12 Gorenstein curves#

Tag 0E1M, a lemma

Tag 0E6M, a lemma

Sources

Section109.13 Local complete intersection curves#

Tag 0DZV, a lemma

Sources

Section109.14 Curves with isolated singularities#

Tag 0DZW, a lemma

Sources

Section109.15 The smooth locus of the stack of curves#

Tag 0DZU, a lemma

Tag 0DZX, a lemma

Sources

Section109.16 Smooth curves#

Tag 0DZZ, a lemma

Tag 0E1N, a lemma

Tag 0E81, a lemma

Tag 0E82, a definition

Tag 0E83, a lemma

Tag 0E84, a lemma

Sources

Section109.17 Density of smooth curves#

Tag 0E86, a lemma

Sources

Section109.18 Nodal curves#

Tag 0DSY, a lemma

Tag 0E00, a lemma

Sources

Section109.19 The relative dualizing sheaf#

Tag 0E6P, a lemma

Tag 0E6Q, a definition

Tag 0E6R, a lemma

Sources

Section109.20 Prestable curves#

Tag 0E6T, a definition

Tag 0E6U, a lemma

Tag 0E6V, a lemma

Section109.3 The stack of curves #

Section109.4 The stack of polarized curves #

Section109.5 Properties of the stack of curves #

Section109.6 Open substacks of the stack of curves #

Section109.7 Curves with finite reduced automorphism groups #

Section109.8 Cohen-Macaulay curves #

Section109.9 Curves of a given genus #

Section109.10 Geometrically reduced curves #

Section109.11 Geometrically reduced and connected curves #

Section109.12 Gorenstein curves #

Section109.13 Local complete intersection curves #

Section109.14 Curves with isolated singularities #

Section109.15 The smooth locus of the stack of curves #

Section109.16 Smooth curves #

Section109.17 Density of smooth curves #

Section109.18 Nodal curves #

Section109.19 The relative dualizing sheaf #

Section109.20 Prestable curves #

Section109.21 Semistable curves #

Section109.22 Stable curves #