Places have unique centers on proper curves

Let X be an integral scheme of dimension at most one over a field whose structure morphism satisfies the existence part of the valuative criterion, a proper curve for instance. If the local ring at every codimension-one point is a discrete valuation ring, then every normalized place of the function field of X is attached to a codimension-one point; if X is moreover separated, the codimension-one points are canonically equivalent to those places.

Existence is the valuative criterion, applied to the valuation ring of a place. The closed point of the resulting lift cannot map to the generic point of X, since that would put the whole function field in the valuation ring. The dimension bound therefore makes the image a codimension-one point. Its local ring maps into the valuation ring, which identifies the associated normalized place. Injectivity is CodimensionOnePoint.toPlace_injective, which rests on the uniqueness part of the valuative criterion.

This equivalence permits divisor and principal-parts constructions indexed by codimension-one points of a proper curve to be reindexed by function-field places.

Main results

• CodimensionOnePoint.toPlace_surjective: every place of the function field of such a curve is attached to a codimension-one point;
• CodimensionOnePoint.equivPlace: the resulting equivalence between codimension-one points and places.

References

• The Stacks Project, Lemma 29.42.1 (Tag 0BX5), the valuative criterion for properness.
• R. Hartshorne, Algebraic Geometry, Chapter I, Section 6.

theorem TauCeti.AlgebraicGeometry.CodimensionOnePoint.toPlace_surjective {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) : Function.Surjective fun (x : CodimensionOnePoint X) => X.toPlace ↑x

Every normalized place of the function field of an integral curve over k is attached to a codimension-one point, as soon as the structure morphism satisfies the existence part of the valuative criterion. A proper curve is the motivating instance.

noncomputable def TauCeti.AlgebraicGeometry.CodimensionOnePoint.equivPlace {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) : CodimensionOnePoint X ≃ Place k ↑X.functionField

The codimension-one points of a separated integral curve over k whose structure morphism satisfies the existence part of the valuative criterion, a proper curve for instance, are canonically equivalent to the normalized places of its function field.

Equations

• TauCeti.AlgebraicGeometry.CodimensionOnePoint.equivPlace hex hdim = Equiv.ofBijective (fun (x : TauCeti.AlgebraicGeometry.CodimensionOnePoint X) => X.toPlace ↑x) ⋯

@[simp]

theorem TauCeti.AlgebraicGeometry.CodimensionOnePoint.equivPlace_apply {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] [X.IsSeparated] (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k)) (hdim : ∀ (x : ↥X), Order.coheight x ≤ 1) (x : CodimensionOnePoint X) : (equivPlace hex hdim) x = X.toPlace ↑x

The point-to-place equivalence is induced by Scheme.toPlace.