Nodal reduction of curves

A curve over the fraction field of a discrete valuation ring has nodal reduction when it admits a proper model whose structure morphism is at worst nodal of relative dimension one. This is the reduction condition used before unstable components are contracted; it does not impose the stronger semistability or stability conditions on the special fibre.

The predicate remembers the prescribed generic-fibre identification through TauCeti.Model. It is invariant under isomorphism of that generic fibre. A prestable or smooth proper model is a witness, and a witness remains one after passage to the chosen place of a finite separable field extension.

Nodal reduction is a condition on the special fibre of a proper model alone: a nodal curve has nodal reduction as soon as it has a proper model whose special fibre is at worst nodal. This is how a regular model whose special fibre has been shown to be reduced with at worst nodal singularities yields nodal reduction.

Main declarations

• TauCeti.HasNodalReduction: existence of a proper at-worst-nodal model.
• TauCeti.HasNodalReduction.of_iso: invariance under isomorphism of the generic curve.
• TauCeti.HasNodalReduction.baseChange: preservation under a chosen finite DVR extension.
• TauCeti.hasNodalReduction_iff_exists_specialFiber: a curve has nodal reduction exactly when it is at worst nodal and has a proper model whose special fibre is at worst nodal.

References

• The Stacks Project, Section 55.18, Semistable reduction

def TauCeti.HasNodalReduction (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (C : AlgebraicGeometry.Scheme) (toK : C ⟶ AlgebraicGeometry.Spec ↧K) : Prop

A curve over the fraction field K of a discrete valuation ring R has nodal reduction if it has a proper model over R which is at worst nodal of relative dimension one.

This is an existence predicate: the model and its identification with the prescribed generic fibre are not chosen data. It is deliberately weaker than the prestable, semistable, and stable family predicates.

theorem TauCeti.hasNodalReduction_iff (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (C : AlgebraicGeometry.Scheme) (toK : C ⟶ AlgebraicGeometry.Spec ↧K) : HasNodalReduction R K C toK ↔ ∃ (M : Model R K C toK), M.IsProper ∧ AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne M.toBase

The defining characterization of nodal reduction by a proper nodal model.

theorem TauCeti.HasNodalReduction.of_model {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} (M : Model R K C toK) (hproper : M.IsProper) (hnodal : AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne M.toBase) : HasNodalReduction R K C toK

A proper at-worst-nodal model witnesses nodal reduction.

theorem TauCeti.HasNodalReduction.of_prestable_model {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} (M : Model R K C toK) [AlgebraicGeometry.PrestableFamily M.toBase] : HasNodalReduction R K C toK

A prestable model witnesses nodal reduction.

theorem TauCeti.HasNodalReduction.of_smooth_model {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} (M : Model R K C toK) (hproper : M.IsProper) [AlgebraicGeometry.SmoothOfRelativeDimension 1 M.toBase] : HasNodalReduction R K C toK

A smooth proper relative curve with the prescribed generic fibre has nodal reduction.

theorem TauCeti.HasNodalReduction.of_iso {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C D : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} {toK' : D ⟶ AlgebraicGeometry.Spec ↧K} (h : HasNodalReduction R K C toK) (e : CategoryTheory.Over.mk toK ≅ CategoryTheory.Over.mk toK') : HasNodalReduction R K D toK'

Nodal reduction is preserved when the prescribed generic curve is replaced by an isomorphic object over Spec K.

theorem TauCeti.HasNodalReduction.iff_of_iso {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C D : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} {toK' : D ⟶ AlgebraicGeometry.Spec ↧K} (e : CategoryTheory.Over.mk toK ≅ CategoryTheory.Over.mk toK') : HasNodalReduction R K C toK ↔ HasNodalReduction R K D toK'

Isomorphic generic curves have nodal reduction simultaneously.

theorem TauCeti.HasNodalReduction.baseChange {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} (h : HasNodalReduction R K C toK) (E : FiniteDVRExtension R K) : HasNodalReduction E.localRing E.extensionField (genericFiber K E.extensionField toK).left (genericFiber K E.extensionField toK).hom

Nodal reduction persists after base change to the chosen local ring of a finite separable extension of the fraction field.

theorem TauCeti.HasNodalReduction.of_specialFiber {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} (M : Model R K C toK) (hproper : M.IsProper) (hC : AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne toK) (hs : AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne (specialFiber R M.toBase).hom) : HasNodalReduction R K C toK

A nodal curve over K has nodal reduction if it has a proper model whose special fibre is at worst nodal.

theorem TauCeti.HasNodalReduction.of_smooth_of_specialFiber {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} [AlgebraicGeometry.SmoothOfRelativeDimension 1 toK] (M : Model R K C toK) (hproper : M.IsProper) (hs : AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne (specialFiber R M.toBase).hom) : HasNodalReduction R K C toK

A smooth curve over K has nodal reduction if it has a proper model whose special fibre is at worst nodal.

theorem TauCeti.HasNodalReduction.atWorstNodalOfRelativeDimensionOne {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {C : AlgebraicGeometry.Scheme} {toK : C ⟶ AlgebraicGeometry.Spec ↧K} (h : HasNodalReduction R K C toK) : AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne toK

A curve with nodal reduction is itself at worst nodal.

theorem TauCeti.hasNodalReduction_iff_exists_specialFiber (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (C : AlgebraicGeometry.Scheme) (toK : C ⟶ AlgebraicGeometry.Spec ↧K) : HasNodalReduction R K C toK ↔ AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne toK ∧ ∃ (M : Model R K C toK), M.IsProper ∧ AlgebraicGeometry.AtWorstNodalOfRelativeDimensionOne (specialFiber R M.toBase).hom

Nodal reduction is a condition on the special fibre. A curve over the fraction field of a discrete valuation ring has nodal reduction exactly when it is at worst nodal and has a proper model whose special fibre is at worst nodal.