Every line bundle on a curve is the sheaf of a Weil divisor #
Let X be a Noetherian integral scheme of dimension at most one whose codimension-one local rings
are discrete valuation rings. This file proves that every line bundle L on X is isomorphic to
the sheaf πͺ_X(D) of a Weil divisor D, so that D β¦ πͺ_X(D) identifies the divisor class group
with the isomorphism classes of line bundles: Cl(X) β
Pic(X).
The divisor is read off from the rational embedding of L. A rank-one trivialization of L on a
dense open subset realizes L inside the sheaf π¦_X of rational functions
(Scheme.Modules.rationalTrivializationHom), and over the domain V of any local rank-one
trivialization the image consists of the regular multiples of one nonzero rational function
f_V. The classes of the f_Vβ»ΒΉ glue to a Cartier divisor
(Scheme.Modules.exists_cartierDivisor_restrict_eq), whose Weil divisor D has coefficient
-ord_y f_V at each codimension-one point y β V. A rational function g then lies in the image
of L over an open subset of V exactly when g / f_V has no poles there, which by the algebraic
Hartogs' principle is the order bound defining πͺ_X(D).
Main declarations #
AlgebraicGeometry.Scheme.Modules.exists_coeff_eq_neg_ord: the Weil divisor of a rationally trivialized line bundle;TauCeti.AlgebraicGeometry.SchemeWeilDivisor.isoSheafOfCoeffEq: the isomorphismL β πͺ_X(D)through which the rational embedding ofLfactors (isoSheafOfCoeffEq_hom_sheafΞΉ);TauCeti.AlgebraicGeometry.SchemeWeilDivisor.toLineBundleClass_surjectiveandTauCeti.AlgebraicGeometry.SchemeWeilDivisor.classGroupToLineBundleClass_surjective;TauCeti.AlgebraicGeometry.SchemeWeilDivisor.classGroupAddEquivLineBundleClass, the additive equivalenceCl(X) β+ Pic(X). The Picard group structure itself comes from Cartier divisors on any integral scheme.
The argument follows Hartshorne, Algebraic Geometry, Proposition II.6.13 and Corollary II.6.16, and the Stacks Project, Divisors, Tag 0BE0. No formalization is vendored.
The Weil divisor of a rationally trivialized line bundle. On a Noetherian integral scheme,
a line bundle M with a chosen rank-one trivialization on a dense open subset has a Weil divisor
whose coefficient at every codimension-one point y is minus the order at y of the rational
function of the basis section of any rank-one trivialization defined near y.
If the coefficients of D are minus the orders of the local basis sections of M, then the
rational function of every section of M satisfies the order bound imposed by D.
If the coefficients of D are minus the orders of the local basis sections of M, then
every section of πͺ_X(D) is the rational function of a section of M. Locally the quotient by
a basis section has no poles, hence is regular by the algebraic Hartogs' principle, and the local
preimages glue because M embeds into the rational functions.
A line bundle is the sheaf of its divisor. If the coefficients of D are minus the
orders of the local basis sections of the line bundle M, then the rational embedding of M
factors through an isomorphism M β
πͺ_X(D).
Equations
Instances For
The isomorphism isoSheafOfCoeffEq, followed by the inclusion πͺ_X(D) βΆ π¦_X, is the
rational embedding of the line bundle.
The isomorphism isoSheafOfCoeffEq, followed by the inclusion πͺ_X(D) βΆ π¦_X, is the
rational embedding of the line bundle.
Every line bundle on a curve is the sheaf of a Weil divisor. On a Noetherian integral
scheme of dimension at most one whose codimension-one local rings are discrete valuation rings,
every invertible sheaf is isomorphic to πͺ_X(D) for some Weil divisor D.
Every line-bundle class on such a curve is the class of πͺ_X(D) for a Weil divisor D.
The map from divisor classes to line-bundle classes is surjective.
Cl(X) β
Pic(X). On a Noetherian integral scheme of dimension at most one whose
codimension-one local rings are discrete valuation rings, D β¦ πͺ_X(D) identifies the divisor
class group with the line-bundle classes under tensor product.
Equations
Instances For
The equivalence Cl(X) β+ Pic(X) sends a divisor class to the class of its line bundle.
Negating a divisor class gives the inverse line-bundle class in the Picard group.