Orders of vanishing at codimension-one points as orders at places #
Let X be a locally Noetherian integral scheme over a field k and let x be a codimension-one
point whose local ring is a discrete valuation ring. This file identifies the order at the place
Scheme.toPlace attached to x with the scheme-theoretic order of vanishing at x, both as a
function on rational functions and as an additive homomorphism on Additive X.functionFieldˣ.
This is the local bridge used to transport divisor and differential constructions between scheme-theoretic codimension-one points and abstract function-field places.
Main results #
CodimensionOnePoint.toPlace_ord: the order at the place is the scheme-theoretic order of vanishing.CodimensionOnePoint.toPlace_ordAddMonoidHom: the corresponding additive order homomorphisms agree.
References #
- R. Hartshorne, Algebraic Geometry, Chapter I, Section 6, and Chapter II, 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.
@[simp]
theorem
TauCeti.AlgebraicGeometry.CodimensionOnePoint.toPlace_ord
{k : Type u}
[Field k]
{X : AlgebraicGeometry.Scheme}
[AlgebraicGeometry.IsIntegral X]
[X.Over (AlgebraicGeometry.Spec ↧k)]
[AlgebraicGeometry.IsLocallyNoetherian X]
(x : CodimensionOnePoint X)
[IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)]
(f : ↑X.functionField)
:
The order at the place attached to a codimension-one point is its scheme-theoretic order of vanishing.
theorem
TauCeti.AlgebraicGeometry.CodimensionOnePoint.toPlace_ordAddMonoidHom
{k : Type u}
[Field k]
{X : AlgebraicGeometry.Scheme}
[AlgebraicGeometry.IsIntegral X]
[X.Over (AlgebraicGeometry.Spec ↧k)]
[AlgebraicGeometry.IsLocallyNoetherian X]
(x : CodimensionOnePoint X)
[IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)]
:
The additive order homomorphism of the place attached to x is the scheme-theoretic order
homomorphism at x.