Places attached to points with discrete valuation ring stalks #
Let X be an integral scheme over a field k. When the local ring at a point x is a discrete
valuation ring, its normalized valuation on the function field of X is a place of
X.functionField / k. This file constructs that place and identifies its valuation ring, residue
field, and degree with the scheme-theoretic local ring, residue field, and residue degree at x.
This is the geometric half of the dictionary between the points of a curve and the places of its function field: it lets local data at a point of a scheme — integrality, residues, degrees — be computed with the valuation-theoretic API for places, and conversely.
Main definitions and results #
Scheme.toPlace: the normalized place attached to a point with discrete valuation ring stalk.Scheme.stalkToPlaceIntegersAlgEquiv: the stalk atxis the valuation ring of that place.Scheme.toPlaceResidueFieldAlgEquiv: the residue field of the scheme point is the residue field of its place.Scheme.toPlace_degree_eq_residueDegree: the degree of the place is the scheme-theoretic residue degree ofx.
References #
- R. Hartshorne, Algebraic Geometry, Chapter I, Section 6.
- Q. Liu, Algebraic Geometry and Arithmetic Curves, Chapter 7.
- H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Appendix B.
The normalized place of the function field attached to a point with discrete valuation ring as its stalk.
Equations
- X.toPlace x = TauCeti.Place.ofPrime k (↑X.functionField) (IsDiscreteValuationRing.maximalIdeal ↑(X.presheaf.stalk x))
Instances For
The valuation of the place attached to x is the normalized valuation of the maximal ideal
of the discrete valuation ring 𝒪_{X,x}.
The canonical inclusion of the stalk into the function field lands in the valuation ring of the place attached to the point.
The valuation ring defining the place is the valuation subring of the normalized maximal-ideal valuation of the stalk.
A rational function is integral at the place attached to x exactly when it comes from the
stalk 𝒪_{X,x}. Thus the valuation ring of X.toPlace x is the image of the local ring in the
function field.
The stalk at a point with discrete valuation ring stalk is canonically the valuation ring of its associated place.
Equations
Instances For
The stalk-to-valuation-ring equivalence is the canonical inclusion into the function field.
The residue field of a point with discrete valuation ring stalk is canonically the residue
field of its place. Both are the stalk modulo its maximal ideal; the right-hand description is
the general residue field computation for Place.ofPrime.
Equations
Instances For
The residue-field equivalence sends the residue class of a stalk element to its residue at the associated place.
The degree of the place attached to x is the degree of the scheme-theoretic residue field
κ(x) over the base field.
The degree of the place attached to x is the scheme-theoretic residue degree of x over
the base field.