A place determines its center on a separated scheme

On an integral separated scheme over a field, two points with discrete valuation ring stalks have the same associated function-field place exactly when they coincide. Equality of the places identifies their valuation rings inside the function field. The uniqueness part of the valuative criterion then identifies the two maps from the spectrum of this ring to the scheme, and hence their closed-point images.

In particular the map sending a codimension-one point to its place is injective (CodimensionOnePoint.toPlace_injective). This is the injectivity step in comparing the points of a nonsingular proper curve with the places of its function field, needed to compare divisor and principal-parts constructions.

References

• The Stacks Project, Lemma 26.22.1 (Tag 01KZ), uniqueness in the valuative criterion.
• R. Hartshorne, Algebraic Geometry, Chapter I, Section 6.

@[simp]

theorem TauCeti.AlgebraicGeometry.toPlace_eq_iff {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [X.IsSeparated] {x y : ↥X} [IsDiscreteValuationRing ↑(X.presheaf.stalk x)] [IsDiscreteValuationRing ↑(X.presheaf.stalk y)] : X.toPlace x = X.toPlace y ↔ x = y

On a separated integral scheme, a function-field place has at most one center whose local ring is a discrete valuation ring.

theorem TauCeti.AlgebraicGeometry.CodimensionOnePoint.toPlace_injective {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [X.Over (AlgebraicGeometry.Spec ↧k)] [X.IsSeparated] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] : Function.Injective fun (x : CodimensionOnePoint X) => X.toPlace ↑x

Distinct codimension-one points of a separated integral scheme give distinct function-field places, provided their local rings are discrete valuation rings.