Proper integral curves over a field

A curve over a field is an integral scheme that is proper and one-dimensional over that field. Its function field is therefore an algebraic function field of one variable. The two-chart model of any algebraic function field provides a regular proper curve with that function field. A rational point of a curve is a point of codimension one, that is, the generic point of a prime divisor.

class AlgebraicGeometry.Scheme.IsCurveOver {X : Scheme} (k : Type u) [Field k] [X.Over (Spec ↧k)] extends AlgebraicGeometry.IsIntegral X, AlgebraicGeometry.IsProper (X ↘ AlgebraicGeometry.Spec ↧k) : Prop

A curve over a field is an integral, proper scheme of dimension one over that field.

• nonempty : Nonempty ↥X
• component_integral (U : X.Opens) [Nonempty ↥↑U] : IsDomain ↑(X.presheaf.obj (Opposite.op U))
• isClosedImmersion_diagonal : IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal (X ↘ Spec ↧k))
• universally_isClosedMap : (topologically @IsClosedMap).universally (X ↘ Spec ↧k)
• finiteType_appLE {U : (Spec ↧k).Opens} : IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map (X ↘ Spec ↧k).base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE (X ↘ Spec ↧k) U V e)).FiniteType
• topologicalKrullDim_eq_one : topologicalKrullDim ↥X = 1

  The curve has dimension one.

@[simp]

theorem AlgebraicGeometry.Scheme.isCurveOver_iff {k : Type u} [Field k] {X : Scheme} [X.Over (Spec ↧k)] : IsCurveOver k ↔ IsIntegral X ∧ IsProper (X ↘ Spec ↧k) ∧ topologicalKrullDim ↥X = 1

The defining properties of a curve over a field.

theorem AlgebraicGeometry.Scheme.IsCurveOver.isFunctionField {k : Type u} [Field k] {X : Scheme} [X.Over (Spec ↧k)] [IsCurveOver k] : TauCeti.IsFunctionField k ↑X.functionField

The function field of a curve over k is an algebraic function field of one variable.

theorem AlgebraicGeometry.Scheme.IsCurveOver.coheight_le_one {k : Type u} [Field k] {X : Scheme} [X.Over (Spec ↧k)] [IsCurveOver k] (x : ↥X) : Order.coheight x ≤ 1

Every point of a curve has coheight at most one.

theorem AlgebraicGeometry.Scheme.IsCurveOver.isNoetherian (k : Type u) [Field k] (X : Scheme) [X.Over (Spec ↧k)] [IsCurveOver k] : IsNoetherian X

A curve over a field is a Noetherian scheme.

theorem AlgebraicGeometry.Scheme.IsCurveOver.valuativeCriterion_existence (k : Type u) [Field k] (X : Scheme) [X.Over (Spec ↧k)] [IsCurveOver k] : ValuativeCriterion.Existence (X ↘ Spec ↧k)

The structure morphism of a curve satisfies the existence part of the valuative criterion.

theorem AlgebraicGeometry.Scheme.IsCurveOver.valuationRing_stalk (k : Type u) [Field k] (X : Scheme) [X.Over (Spec ↧k)] [IsCurveOver k] [∀ (y : TauCeti.AlgebraicGeometry.CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] (p : ↥X) : ValuationRing ↑(X.presheaf.stalk p)

The local rings of a regular proper curve are valuation rings: for a curve X over k whose codimension-one local rings are discrete valuation rings, the local ring at the generic point is the function field, and every other point has codimension one.

theorem AlgebraicGeometry.Scheme.IsCurveOver.coheight_section_eq_one (k : Type u) [Field k] {X : Scheme} [X.Over (Spec ↧k)] [IsCurveOver k] {s : Spec ↧k ⟶ X} (hs : CategoryTheory.CategoryStruct.comp s (X ↘ Spec ↧k) = CategoryTheory.CategoryStruct.id (Spec ↧k)) : Order.coheight (s (IsLocalRing.closedPoint k)) = 1

A rational point of a curve has codimension one. The image of a section of the structure morphism of a curve over k is a closed point; it is not the generic point, since the curve has dimension one, so it has coheight one.