Locally principal Weil divisors on a scheme #

Let X be a locally Noetherian integral scheme. A Weil divisor D on X is locally principal when every point has an open neighbourhood on which the coefficients of D agree with the orders of one nonzero rational function. On a scheme regular in codimension one (expressed in TauCeti/AlgebraicGeometry/WeilDivisor/Scheme/Sheaf.lean by the codimension-one stalks being discrete valuation rings), this is the local condition used to compare Weil divisors with the Cartier divisors defined in TauCeti/AlgebraicGeometry/CartierDivisor/Basic.lean.

The predicate and its additive subgroup require only IsLocallyNoetherian X. Results involving the globally assembled principal Weil divisors and linear equivalence require IsNoetherian X, which supplies the finite-support condition for orderAt. The local triviality of 𝒪_X(D) additionally requires the codimension-one stalks to be discrete valuation rings, which is the hypothesis under which that sheaf is built.

Main declarations #

SchemeWeilDivisor.IsLocallyPrincipal D is the local-principality predicate;
SchemeWeilDivisor.locallyPrincipalSubgroup X is the subgroup of locally principal Weil divisors;
SchemeWeilDivisor.principalSubgroup_le_locallyPrincipalSubgroup records that principal divisors are locally principal;
WeilDivisor.OrderSystem.LinearlyEquivalent.isLocallyPrincipal_iff shows that local principality depends only on the divisor class;
SchemeWeilDivisor.IsLocallyPrincipal.exists_sections_sub_principalDivisor_eq_sections_zero and SchemeWeilDivisor.IsLocallyPrincipal.exists_iso_sheaf_sections_eq_sections_zero consume the predicate: the sheaf 𝒪_X(D) of TauCeti/AlgebraicGeometry/WeilDivisor/Scheme/Sheaf.lean is isomorphic, near every point, to the sheaf of a divisor whose sections there are those of 𝒪_X(0);
SchemeWeilDivisor.isLocallyPrincipal_of_forall_isClosed_singleton establishes the predicate whenever the codimension-one points of X are closed and their local rings are discrete valuation rings: then every Weil divisor is locally principal, equivalently SchemeWeilDivisor.locallyPrincipalSubgroup_eq_top_of_forall_isClosed_singleton;
SchemeWeilDivisor.isLocallyPrincipal_of_forall_coheight_le_one and SchemeWeilDivisor.locallyPrincipalSubgroup_eq_top specialize this to a curve, where every point has codimension at most one and codimension-one points are therefore closed.

Existence of local equations is the first half of the local comparison of Weil and Cartier divisors: near each point a divisor is the divisor of a nonzero rational function. The matching uniqueness half — that such a function is determined up to a regular unit, so that its class in 𝒦_X^× / 𝒪_X^× is well defined — is in TauCeti/AlgebraicGeometry/WeilDivisor/Scheme/Cartier/Basic.lean.

In higher dimension the same conclusion needs the local rings of X to be unique factorization domains rather than merely one-dimensional; without such a hypothesis a Weil divisor need not be locally principal, and it is that failure which separates the divisor class group of X from its Picard group.

The local-equation formulation follows Hartshorne, Algebraic Geometry, II.6. The Stacks Project, Divisors, Tags 0BE0 and 0BE9, supplies the principal-Weil-divisor and Picard/class-group comparison context. No formalization is vendored. The proofs reuse Tau Ceti's scheme-theoretic principal-divisor and linear-equivalence API.