Documentation

TauCeti.AlgebraicGeometry.WeilDivisor.Scheme.Order

Orders of rational functions at codimension-one points #

For a locally Noetherian integral scheme X, Mathlib defines the order of vanishing Scheme.ord f x : ℤ of a rational function at a point. This file packages its restriction to nonzero rational functions at a codimension-one point as an additive homomorphism

SchemeWeilDivisor.orderAt x : Additive X.functionFieldˣ →+ ℤ.

This is the local algebraic input for the scheme-theoretic principal-divisor map. Constructing that map also requires the separate global theorem that a nonzero rational function has nonzero order at only finitely many codimension-one points; no finiteness assumption is hidden here.

Elementary facts about Scheme.ord itself are recorded first: the order of one vanishes (Scheme.ord_one), the order of an inverse is the negative of the order (Scheme.ord_inv), and a function regular on U has nonnegative order at every point of U (Scheme.ord_germToFunctionField_nonneg), that is, it has no poles where it is defined.

Where the local ring at a codimension-one point is a discrete valuation ring, orderAt is surjective onto ℤ (SchemeWeilDivisor.exists_orderAt_eq): the powers of a uniformizer supply a rational function of each prescribed order.

The construction reuses Mathlib's AlgebraicGeometry.Scheme.ord, ordHom, and ord_eq_unzero_ordHom; no external formalization is vendored.

source
@[simp]
theorem TauCeti.AlgebraicGeometry.Scheme.ord_one {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsLocallyNoetherian X] {x : ↥X} :
AlgebraicGeometry.Scheme.ord 1 x = 0

The constant function one has order zero at every point: it is a global regular unit.

source
@[simp]
theorem TauCeti.AlgebraicGeometry.Scheme.ord_inv {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsLocallyNoetherian X] (f : ↑X.functionField) {x : ↥X} :
AlgebraicGeometry.Scheme.ord f⁻¹ x = -AlgebraicGeometry.Scheme.ord f x

The order of an inverse is the negative of the order. Both sides vanish at the zero function, whose inverse is again zero.

source
theorem TauCeti.AlgebraicGeometry.Scheme.ord_germToFunctionField_nonneg {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsLocallyNoetherian X] {U : X.Opens} [Nonempty ↥↑U] (a : ↑(X.presheaf.obj (Opposite.op U))) {x : ↥X} (hx : x ∈ U) :
0 ≤ AlgebraicGeometry.Scheme.ord ((CategoryTheory.ConcreteCategory.hom (X.germToFunctionField U)) a) x

A regular function on U has nonnegative order at every point of U: it has no poles where it is defined.

source
noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.orderAt {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsLocallyNoetherian X] (x : CodimensionOnePoint X) :
Additive (↑X.functionField)ˣ →+ ℤ

The order of a nonzero rational function at a codimension-one point, as an additive homomorphism from the additive form of the unit group of the function field.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.orderAt_apply {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsLocallyNoetherian X] (x : CodimensionOnePoint X) (f : Additive (↑X.functionField)ˣ) :
    (orderAt x) f = AlgebraicGeometry.Scheme.ord ↑(Additive.toMul f) ↑x

    Evaluating orderAt gives Mathlib's integer-valued order of vanishing.

    source
    theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.exists_orderAt_eq {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsLocallyNoetherian X] (x : CodimensionOnePoint X) [IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] (n : ℤ) :
    ∃ (g : Additive (↑X.functionField)ˣ), (orderAt x) g = n

    Every integer is an order of vanishing. At a codimension-one point whose local ring is a discrete valuation ring, a uniformizer has order one, so its integer powers realize every integer as the order of a nonzero rational function.