Principal divisors on Noetherian integral schemes

For a Noetherian integral scheme X, this file combines Mathlib's local orders of vanishing into the global order system on the codimension-one points of X. The only global issue is finite support. A nonzero rational function is a unit on some nonempty affine open U; its order therefore vanishes on U. The codimension-one points outside U are finite: each is the generic point of one of the finitely many irreducible pieces of the closed complement.

The main results are:

• SchemeWeilDivisor.finite_setOfPred_not_mem: a nonempty open misses only finitely many codimension-one points;
• SchemeWeilDivisor.finite_support_orderAt: the orders of a nonzero rational function have finite support;
• WeilDivisor.OrderSystem.ofScheme: the resulting order system, whose generic OrderSystem.principalDivisor is the scheme-theoretic principal divisor;
• SchemeWeilDivisor.isEffective_add_principalDivisor_iff: the coefficientwise criterion for a divisor plus a principal divisor to be effective.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A, item "principal divisors" in "Divisors on a curve". It completes the global step explicitly left open by TauCeti/AlgebraicGeometry/WeilDivisor/Scheme/Order.lean. The proof reuses Mathlib's exists_isUnit_germ_eq, Scheme.ord_of_isUnit, and the decomposition of a closed subset of a Noetherian space into finitely many irreducible closed subsets. No formalization is vendored.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.finite_setOfPred_not_mem {X : AlgebraicGeometry.Scheme} [IrreducibleSpace ↥X] [TopologicalSpace.NoetherianSpace ↥X] (U : X.Opens) [Nonempty ↥↑U] : {x : CodimensionOnePoint X | ↑x ∉ U}.Finite

A nonempty open subset of an irreducible scheme with Noetherian underlying space contains all but finitely many codimension-one points.

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

The orders of a nonzero rational function on a Noetherian integral scheme are nonzero at only finitely many codimension-one points.

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

The orders of vanishing of nonzero rational functions at codimension-one points, assembled into the order system whose principal divisors are scheme-theoretic Weil divisors.

Equations

• TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ofScheme X = { ord := TauCeti.AlgebraicGeometry.SchemeWeilDivisor.orderAt, finite_support := ⋯ }

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ofScheme_ord {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (x : CodimensionOnePoint X) : (ofScheme X).ord x = SchemeWeilDivisor.orderAt x

The order map in the scheme-theoretic order system is the locally defined order map.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.isEffective_add_principalDivisor_iff {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (D : SchemeWeilDivisor X) (g : Additive (↑X.functionField)ˣ) : WeilDivisor.IsEffective (D + (WeilDivisor.OrderSystem.ofScheme X).principalDivisor g) ↔ ∀ (x : CodimensionOnePoint X), -WeilDivisor.coeff D x ≤ AlgebraicGeometry.Scheme.ord ↑(Additive.toMul g) ↑x

A divisor plus a principal divisor is effective exactly when the corresponding rational function has order at least the negative of the divisor coefficient at every codimension-one point.