Cartier divisors on an integral scheme #
Let X be an integral scheme and let 𝒦_X be its sheaf of rational functions. The Cartier
divisor sheaf is the quotient
𝒦_X^× / 𝒪_X^×,
and a Cartier divisor is a global section of this quotient sheaf. The quotient is a sheaf quotient, not the pointwise quotient of groups of sections: its sections are represented locally by nonzero rational functions, with two representatives identified when their ratio is a regular unit.
Main declarations #
Scheme.regularUnitSheafandScheme.rationalUnitSheafare the sheaves of units of𝒪_Xand𝒦_X, written additively;Scheme.toRationalUnitSheafis the monomorphism𝒪_X^× ⟶ 𝒦_X^×;Scheme.cartierDivisorSheafis its cokernel in sheaves of abelian groups;Scheme.CartierDivisoris the additive group of global sections of that cokernel;Scheme.rationalUnitClasssends a nonzero rational function to its class in the Cartier-divisor sheaf over a nonempty open subset, its local equation there;Scheme.principalCartierDivisorsends a nonzero rational function to its principal Cartier divisor, the case of the whole space.
The rational-function sheaf is constructed in
TauCeti/AlgebraicGeometry/Modules/RationalFunctions.lean; the line bundle 𝒪_X(D) of a Cartier
divisor is constructed in TauCeti/AlgebraicGeometry/CartierDivisor/Sheaf.lean.
The definition follows the Stacks Project, Divisors (Tag 02AR). No formalization is vendored. The sheaf quotient is Mathlib's categorical cokernel in the abelian category of sheaves of abelian groups.
The sheaf 𝒪_X^× of regular units, regarded as a sheaf of additive commutative groups.
Equations
Instances For
The sheaf 𝒦_X^× of nonzero rational functions, regarded as a sheaf of additive
commutative groups.
Equations
Instances For
The inclusion 𝒪_X^× ⟶ 𝒦_X^× of regular units into nonzero rational functions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inclusion of regular units into rational units is injective on sections over every open subset of an integral scheme.
The inclusion 𝒪_X^× ⟶ 𝒦_X^× of regular units into rational units is a
monomorphism.
The Cartier-divisor sheaf 𝒦_X^× / 𝒪_X^×. This is the cokernel in the category of sheaves
of abelian groups, and hence is the sheafification of the pointwise quotient presheaf.
Use Mathlib's generic cokernel.desc, cokernel.π_desc, and cancellation through
cokernel.π for its universal property.
Equations
Instances For
The quotient projection 𝒦_X^× ⟶ 𝒦_X^× / 𝒪_X^×.
Equations
Instances For
The quotient projection to the Cartier-divisor sheaf is an epimorphism.
A regular unit has zero class in the Cartier-divisor sheaf.
A regular unit has zero class in the Cartier-divisor sheaf.
The sequence from regular units to rational units and then to Cartier divisors is exact.
The group of Cartier divisors on X, defined as the global sections of
𝒦_X^× / 𝒪_X^×.
Equations
Instances For
The map on global sections induced by the quotient projection from 𝒦_X^× to the
Cartier-divisor sheaf. Its source is the group of units of Γ(X, 𝒦_X), written additively.
Equations
Instances For
A global regular unit maps to zero under the quotient map to Cartier divisors.
Over a nonempty open subset, the units of the rational-function sheaf are the units of the function field.
Equations
Instances For
The rational-unit equivalence applies the rational-functions equivalence to a unit.
The homomorphism from regular units on U to units of the function field induced by the
germ map at the generic point.
Equations
Instances For
The map on regular units applies the germ map to the underlying section.
The equivalence from rational units to function-field units carries the image of a regular unit to the unit induced by its germ in the function field.
The class in the Cartier-divisor sheaf over a nonempty open subset U of a nonzero rational
function, regarded as a local equation there. The multiplicative group of the function field is
written additively in the domain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Evaluating the rational-unit class applies the quotient map to the corresponding rational unit section.
Restricting a rational unit to a smaller nonempty open subset does not change the underlying nonzero rational function.
The class of a nonzero rational function commutes with restriction to a smaller nonempty open subset: a local equation stays a local equation.
A regular unit on U has zero Cartier-divisor class over U.
A nonzero rational function determines its principal Cartier divisor. The multiplicative group of the function field is written additively in the domain.
Equations
Instances For
The principal Cartier divisor of a nonzero rational function.
Equations
Instances For
The principal-divisor homomorphism sends an additively written rational unit to its principal Cartier divisor.
The principal Cartier divisor of one is zero.
The principal Cartier divisor of a product is the sum of the principal Cartier divisors.
The principal Cartier divisor of an inverse is the negation of the principal Cartier divisor.
A global regular unit has zero principal Cartier divisor.
Restricting a principal Cartier divisor to a nonempty open subset gives the class of the same rational function there: a principal divisor has a global equation.
Restricting a principal Cartier divisor to a nonempty open subset gives the class of the same rational function there.