Germs of sections of the sheaf of a Weil divisor #
The sections of ๐ช_X(D) over an open subset U are the zero rational function together with the
rational functions whose order at every codimension-one point of U is at least -D. Shrinking
U around a point x weakens that condition, and this file identifies what survives in the limit:
a rational function is a section of ๐ช_X(D) on some neighbourhood of x exactly when it is
zero or satisfies the order bound at the codimension-one points which generize x.
Only finitely many codimension-one points can obstruct the bound, because a nonzero rational
function has nonzero order at finitely many of them and D has finite support; deleting the
closures of the obstructing points leaves an open neighbourhood of x on which the bound holds
at every codimension-one point.
Main declarations #
SchemeWeilDivisor.finite_setOf_ord_lt: the codimension-one points at which a nonzero rational function violates the bound imposed byDare finite in number;SchemeWeilDivisor.exists_map_mem_sections_of_forall_specializesandSchemeWeilDivisor.exists_map_mem_sections_iff: the germ criterion, that a section of๐ฆ_Xbecomes a section of๐ช_X(D)nearxexactly when its rational function is zero or satisfies the order bound at every codimension-one generization ofx;SchemeWeilDivisor.exists_map_mem_sections_iff_codimensionOne: at a codimension-one pointxโthe only codimension-one generization isxโitself, so nearxโa section belongs to๐ช_X(D)exactly when its rational function is zero or obeys the bound from the single valuation there, andSchemeWeilDivisor.exists_map_mem_sections_ord_eq: every order allowed by that valuation is attained.
Together with the comparison-map results in
TauCeti/AlgebraicGeometry/WeilDivisor/Scheme/Sheaf.lean, the germ results show that the
comparison ๐ช_X(D) โถ ๐ช_X(D + xโ) is an isomorphism on sections away from closure {xโ} and
compute the sections of both sheaves near xโ. They are the local input for the later construction
of the exact sequence 0 โถ ๐ช_X(D) โถ ๐ช_X(D + xโ) โถ ๐ฎ โถ 0 with ๐ฎ a skyscraper sheaf at xโ,
along which the Euler characteristic of a divisor sheaf is computed by induction on the divisor.
The finiteness input is
TauCeti/AlgebraicGeometry/WeilDivisor/Scheme/Principal.lean, the sections are
TauCeti/AlgebraicGeometry/WeilDivisor/Scheme/Sheaf.lean, the surjectivity of the order at a
codimension-one point with a discrete valuation ring as local ring is
TauCeti/AlgebraicGeometry/WeilDivisor/Scheme/Order.lean, and the topological input is Mathlib's
specialization order (Specializes.mem_open, specializes_iff_mem_closure).
References #
- R. Hartshorne, Algebraic Geometry, II.6.
- The Stacks Project, Divisors, Tag 0BE0.
The codimension-one points at which a nonzero rational function violates the order bound
imposed by D form a finite set: away from the support of D and from the finitely many points
where the function has nonzero order, that bound reads 0 โค 0.
A section of ๐ฆ_X whose rational function is zero or is bounded at the codimension-one
generizations of x is a section of ๐ช_X(D) near x. In the nonzero case, the finitely many
codimension-one points where the bound fails are deleted together with their closures, which leaves
a neighbourhood of x because none of them generizes x.
The germ criterion for the sheaf of a Weil divisor. A section of ๐ฆ_X defined near x
restricts to a section of ๐ช_X(D) on some neighbourhood of x exactly when its rational
function is zero or satisfies the order bound imposed by D at every codimension-one point
generizing x.
The local model of ๐ช_X(D) at a codimension-one point. A codimension-one point xโ has
no codimension-one generization but itself, so a section of ๐ฆ_X is a section of ๐ช_X(D) near
xโ exactly when its rational function is zero or its order at xโ is at least -D xโ.
Every order the local ring at a codimension-one point xโ allows is attained by a section of
๐ช_X(D) near xโ: the bound of exists_map_mem_sections_iff_codimensionOne is sharp.