The divisor of zeros of a global function #
Let X be an integral locally Noetherian scheme and a a nonzero global function on X. At a
codimension-one point x, the order of vanishing of a is zero exactly when a is a unit at
x, and positive exactly when a vanishes at x; the order is never negative because a is a
regular function. When X is moreover Noetherian, the principal divisor of a is therefore an
effective Weil divisor whose support consists exactly of the codimension-one points of the zero
locus V(a), that is, by TauCeti.AlgebraicGeometry.Scheme.maximal_mem_zeroLocus_iff, of the
generic points of the irreducible components of V(a). In particular V(a) has finitely many
irreducible components.
This is the divisor of zeros of a regular function: div(a) = ∑ ord_C(a) [C] over the
components C of V(a), with all coefficients positive. Its application is to a model of a
curve over a discrete valuation ring, where a is the uniformizer and V(a) is the special
fibre, whose components then carry the multiplicities ord_C(π).
Main results #
TauCeti.AlgebraicGeometry.Scheme.ord_germToFunctionField_eq_zero_iff: the order of a nonzero regular function at a codimension-one point vanishes exactly when the function is a unit there;TauCeti.AlgebraicGeometry.Scheme.ord_germToFunctionField_pos_iff: the order of a nonzero regular function at a codimension-one point is positive exactly when the function vanishes there;TauCeti.AlgebraicGeometry.SchemeWeilDivisor.finite_setOf_mem_zeroLocus: the zero locus of a nonzero global function on a Noetherian integral scheme contains finitely many codimension-one points;TauCeti.AlgebraicGeometry.SchemeWeilDivisor.isEffective_principalDivisor_ofMul_mk0: the principal divisor of a nonzero global function is effective;TauCeti.AlgebraicGeometry.SchemeWeilDivisor.mem_support_principalDivisor_ofMul_mk0: its support is the set of codimension-one points of the zero locus.
References #
- R. Hartshorne, Algebraic Geometry, Section II.6, the divisor of a rational function.
The order of a nonzero regular function on U at a codimension-one point of U vanishes
exactly when the function is a unit at that point.
The order of a nonzero regular function on U at a codimension-one point of U is positive
exactly when the function vanishes at that point.
The zero locus of a nonzero global function on a Noetherian integral scheme contains only finitely many codimension-one points: it misses the nonempty open complement of that zero locus.
The principal divisor of a nonzero global function is effective: a regular function has no poles.
The support of the principal divisor of a nonzero global function consists of the codimension-one points at which the function vanishes, that is, the generic points of the irreducible components of its zero locus.