The Cartier divisor of a locally principal Weil divisor #
Let X be a locally Noetherian integral scheme of dimension at most one whose codimension-one
local rings are discrete valuation rings. A Weil divisor D on X which is locally principal
is described near every point by one nonzero rational function, its local equation there.
This file glues those local equations into a single Cartier divisor, that is, into a global
section of 𝒦_X^× / 𝒪_X^×.
The gluing is possible because two local equations for the same divisor on the same open subset
differ by a rational function of order zero at every codimension-one point, and such a function is
a regular unit by the one-dimensional algebraic Hartogs' principle of
TauCeti/AlgebraicGeometry/Scheme/Regular.lean. The resulting Cartier divisor is characterized —
and hence uniquely determined — by the requirement that it restrict to the class of g over every
open subset carrying a local equation g.
Main declarations #
SchemeWeilDivisor.rationalUnitClass_eq_of_forall_coeff_eq: two local equations of the same divisor have the same Cartier class;SchemeWeilDivisor.IsLocallyPrincipal.existsUnique_cartierDivisor: the characterizing existence-and-uniqueness statement;SchemeWeilDivisor.IsLocallyPrincipal.cartierDivisor, the Cartier divisor ofD, with its defining propertySchemeWeilDivisor.IsLocallyPrincipal.cartierDivisor_restrict;SchemeWeilDivisor.IsLocallyPrincipal.cartierDivisor_addandSchemeWeilDivisor.cartierDivisor_principalDivisor: the construction is additive and sends the divisor ofgto the principal Cartier divisor ofg;SchemeWeilDivisor.toCartierDivisorHom, the resulting homomorphism from the group of locally principal Weil divisors to the group of Cartier divisors.
The construction follows Hartshorne, Algebraic Geometry, II.6.11, and the Stacks Project, Divisors, Tag 0BE9. The gluing uses Mathlib's unique gluing for sheaves on a topological space, applied to the Cartier-divisor sheaf.
Rational functions with the same orders agree as Cartier divisors. If two nonzero rational
functions have the same order at every codimension-one point of a nonempty open subset U of a
curve, then they have the same class in 𝒦_X^× / 𝒪_X^× over U.
Their ratio has order zero at every codimension-one point of U, hence is a regular unit on U
by the one-dimensional algebraic Hartogs' principle, and regular units have zero class.
Two local equations agree as Cartier divisors. If two nonzero rational functions both have
the coefficients of D as their orders at every codimension-one point of a nonempty open subset
U of a curve, then they have the same class in 𝒦_X^× / 𝒪_X^× over U.
The local criterion for the Cartier divisor of D. If a Cartier divisor E restricts,
near every point, to the class of a local equation of D, then it does so over every nonempty
open subset carrying a local equation of D.
This is the sheaf-separatedness step: the two sections agree on a cover of the given open subset.
The Cartier divisor of a locally principal Weil divisor exists and is unique. On a curve,
a locally principal Weil divisor D determines a unique Cartier divisor whose restriction to
every nonempty open subset carrying a local equation g of D is the class of g.
The Cartier divisor associated with a locally principal Weil divisor on a curve.
Equations
Instances For
The defining property of the associated Cartier divisor. Over a nonempty open subset
carrying a local equation g of D, the Cartier divisor of D restricts to the class of g.
A Cartier divisor which restricts, near every point, to the class of a local equation of D
is the Cartier divisor of D.
The zero Weil divisor has the zero Cartier divisor.
The construction is additive. The Cartier divisor of a sum of locally principal Weil divisors is the sum of their Cartier divisors: local equations multiply.
The Cartier divisor of a locally principal Weil divisor depends only on the divisor.
The construction respects negation.
The Weil-to-Cartier homomorphism. On a curve, the group of locally principal Weil divisors maps to the group of Cartier divisors, compatibly with local equations.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Weil-to-Cartier homomorphism computes the Cartier divisor of the underlying divisor.
A principal Weil divisor has the principal Cartier divisor of the same rational function. The rational function is a global equation, so the two constructions agree over the whole scheme.
The Weil-to-Cartier homomorphism carries principal Weil divisors to principal Cartier divisors.