Smooth curves

A scheme X smooth of relative dimension one over a field k has dimension one (TauCeti.AlgebraicGeometry.topologicalKrullDim_eq_of_smoothOfRelativeDimension). So if it is moreover integral and proper over k, it is a curve over k. Its local rings at codimension-one points are discrete valuation rings by TauCeti.AlgebraicGeometry.isDiscreteValuationRing_stalk_of_smooth.

Conversely, over a perfect field k a curve whose local rings at codimension-one points are discrete valuation rings is smooth of relative dimension one over k: all its local rings are then regular (AlgebraicGeometry.Scheme.Hom.smooth_of_isRegularLocalRing_stalk). So over a perfect field the regular proper curves are exactly the smooth ones. Over an imperfect field a regular curve need not be smooth.

Main results

• AlgebraicGeometry.Scheme.IsCurveOver.of_smooth: an integral proper scheme smooth of relative dimension one over k is a curve over k.
• AlgebraicGeometry.Scheme.IsCurveOver.smoothOfRelativeDimension_one_of_perfectField: a regular curve over a perfect field is smooth of relative dimension one.

theorem AlgebraicGeometry.Scheme.IsCurveOver.of_smooth (k : Type u) [Field k] (X : Scheme) [X.Over (Spec ↧k)] [IsIntegral X] [IsProper (X ↘ Spec ↧k)] [SmoothOfRelativeDimension 1 (X ↘ Spec ↧k)] : IsCurveOver k

An integral proper scheme smooth of relative dimension one over k is a curve over k.

theorem AlgebraicGeometry.Scheme.IsCurveOver.smoothOfRelativeDimension_one_of_perfectField (k : Type u) [Field k] (X : Scheme) [X.Over (Spec ↧k)] [PerfectField k] [IsCurveOver k] [∀ (y : TauCeti.AlgebraicGeometry.CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] : SmoothOfRelativeDimension 1 (X ↘ Spec ↧k)

A regular curve over a perfect field is smooth: if the local rings of a curve X over a perfect field k at its codimension-one points are discrete valuation rings, then X is smooth of relative dimension one over k.