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ˣ →+ ℤ.

The global finiteness theorem SchemeWeilDivisor.finite_support_orderAt proves that a nonzero rational function has nonzero order at only finitely many codimension-one points. It packages the local maps into SchemeWeilDivisor.orderSystem, the scheme-theoretic order system used to construct principal divisors.

The construction advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A, the "principal divisors" part of "Divisors on a curve". It reuses Mathlib's AlgebraicGeometry.Scheme.ord, representation of a nonzero rational function by a unit on a nonempty affine open, and finiteness of irreducible components in a Noetherian space; no external formalization is vendored.

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.orderAt_eq_ord_stalk_of_eq_algebraMap {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsLocallyNoetherian X] (x : CodimensionOnePoint X) [IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] {a : ↑(X.presheaf.stalk ↑x)} (ha : a ≠ 0) (g : Additive (↑X.functionField)ˣ) (hg : ↑(Additive.toMul g) = (algebraMap ↑(X.presheaf.stalk ↑x) ↑X.functionField) a) :
    (orderAt x) g = ↑(Ring.ord (↑(X.presheaf.stalk ↑x)) a).toNat

    If a nonzero rational function comes from the codimension-one stalk, its order is the finite order of that stalk element. This is the local bridge between scheme-theoretic orders and fibre multiplicities in a discrete valuation ring.

    source
    theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.finite_support_orderAt (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (g : Additive (↑X.functionField)ˣ) :
    (Function.support fun (x : CodimensionOnePoint X) => (orderAt x) g).Finite

    A nonzero rational function on a Noetherian integral scheme has nonzero order at only finitely many codimension-one points.

    source
    noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.orderSystem (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] :
    WeilDivisor.OrderSystem (CodimensionOnePoint X) (Additive (↑X.functionField)ˣ)

    The scheme-theoretic order system on the codimension-one points of a Noetherian integral scheme.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.orderSystem_ord (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (x : CodimensionOnePoint X) :
      (orderSystem X).ord x = orderAt x

      The order homomorphisms of the scheme order system are the geometric orders of vanishing. This projection lemma lets downstream modules use the concrete order system without unfolding its opaque finite-support field.