Local equations for Cartier divisors #
A Cartier divisor on an integral scheme is a section of the quotient sheaf
𝒦_X^× / 𝒪_X^×. This file extracts the local-equation description from that quotient:
every section is locally represented by a nonzero rational function, and two representatives
differ by a unique regular unit.
Main declarations #
Scheme.exists_local_equationlifts a Cartier-divisor section to a rational unit on a neighbourhood of any chosen point;Scheme.CartierDivisor.exists_local_equation_coverchooses local equations on an open cover indexed by the points of the scheme;Scheme.toCartierDivisorSheaf_app_eq_iffcharacterizes equality of two representatives by their difference coming from a regular unit;Scheme.CartierDivisor.existsUnique_transitionUnitapplies that characterization on the overlap of two local equations of a global Cartier divisor;Scheme.rationalUnitClass_eq_rationalUnitClass_iffrestates it for nonzero rational functions: two of them have the same class over a nonempty open subsetUexactly when they differ by a unit ofΓ(X, U);Scheme.CartierDivisor.IsLocalEquationAt D x f:fis a local equation ofDat the pointx; every point has one (Scheme.CartierDivisor.exists_isLocalEquationAt), two of them differ by a unit of the local ring𝒪_{X,x}(Scheme.CartierDivisor.IsLocalEquationAt.exists_unit_mul_eq), and they only depend on the divisor nearx(Scheme.CartierDivisor.isLocalEquationAt_congr).
The sheaf 𝒪_X(D) is built in TauCeti/AlgebraicGeometry/CartierDivisor/Sheaf.lean as the
subsheaf of 𝒦_X cut out by the local equations, through
Scheme.CartierDivisor.IsLocalEquationAt. The transition units record how two local equations of
D change into one another on an overlap. The construction follows Hartshorne, Algebraic
Geometry, II.6, and the Stacks Project, Divisors, Tag 02AR. No formalization is vendored: local
lifting is Mathlib's
characterization of epimorphisms of sheaves as locally surjective maps, while the transition-unit
criterion uses left exactness of sections and the cokernel exact sequence.
Every local Cartier-divisor section has a rational equation near each point of its domain.
The representative is a section of 𝒦_X^× on a smaller open neighbourhood, and its image in
𝒦_X^× / 𝒪_X^× is the restriction of the given Cartier-divisor section.
Two rational-unit sections have the same image in the Cartier-divisor sheaf exactly when their difference is the image of a regular unit.
The unit is unique by toRationalUnitSheaf_app_injective; the explicit existence-and-uniqueness
form is existsUnique_regularUnit_sub_of_toCartierDivisorSheaf_app_eq. Multiplication and
division of units are written as addition and subtraction because the unit sheaves are regarded
as sheaves of additive commutative groups.
If two rational-unit sections represent the same Cartier divisor, there is a unique regular unit whose image is their difference. In multiplicative notation, this says their ratio is a unique regular unit.
Two nonzero rational functions have the same class in the Cartier-divisor sheaf over a
nonempty open subset U exactly when they differ by a unit of Γ(X, U).
A global Cartier divisor admits an open cover carrying rational local equations.
The cover is indexed by the points of X, with the open indexed by x chosen to contain x.
The displayed supremum records that these opens cover the whole scheme.
Two local equations of a global Cartier divisor determine a unique regular transition unit on their overlap.
In multiplicative notation the displayed difference is the ratio f / g: the transition unit is
the regular unit by which the equation g must be multiplied to give f on U ⊓ V.
A local equation over V restricts to a local equation over every nonempty open W ≤ V.
A nonzero rational function f is a local equation of the Cartier divisor D at the point
x when D is the class of f over some open neighbourhood of x.
Equations
- D.IsLocalEquationAt x f = ∃ (V : X.Opens) (hx : x ∈ V), (TauCeti.AlgebraicGeometry.Scheme.rationalUnitClass X V) (Additive.ofMul f) = TopCat.Presheaf.restrictOpen D V ⋯
Instances For
Unfolding IsLocalEquationAt: f is a local equation of D at x exactly when D is the
class of f over some open neighbourhood of x.
An equation of D over an open subset is a local equation at each of its points.
The product of local equations is a local equation of the sum of Cartier divisors.
The inverse of a local equation is a local equation of the negative divisor.
One is a local equation of the zero Cartier divisor at every point.
A principal Cartier divisor has its defining rational function as a local equation.
Every Cartier divisor has a local equation at every point.
Every point of an open subset has a smaller open neighbourhood on which D has a single
Cartier equation.
Two local equations of D at x differ by a unit of the local ring 𝒪_{X,x}.
Whether f * c lies in the local ring at x does not depend on the choice of the local
equation f of D at x.
Local equations only depend on the restriction of the divisor: divisors that agree on an open
subset V have the same local equations at the points of V.