The Weil divisor associated with a Cartier divisor #
On a Noetherian integral curve, a Cartier divisor has an order at every codimension-one point: choose a rational local equation and take its order of vanishing. This does not depend on the equation, since two equations differ by a regular unit near the point. Only finitely many orders are nonzero, so they form a Weil divisor.
This file constructs the resulting homomorphism from Cartier divisors to Weil divisors. It proves that its values are locally principal and that, when the codimension-one local rings are discrete valuation rings, it is inverse to the construction which glues the local equations of a Weil divisor. Consequently, Weil divisors and Cartier divisors are additively equivalent under these hypotheses.
Main declarations #
Scheme.CartierDivisor.orderAtis the order of a Cartier divisor at a codimension-one point;Scheme.CartierDivisor.toWeilDivisorHomsends a Cartier divisor to its Weil divisor;Scheme.CartierDivisor.isLocallyPrincipal_toWeilDivisorsupplies its local equations;SchemeWeilDivisor.equivCartierDivisoris the Weil--Cartier additive equivalence.
The construction follows Hartshorne, Algebraic Geometry, II.6.11, and the Stacks Project, Divisors, Tag 0BE9.
A regular unit on a nonempty open subset has order zero at every point of that subset.
Two rational functions representing the same Cartier-divisor section have the same order at each codimension-one point of the open subset.
A Cartier divisor has a unique order compatible with any rational local equation at a fixed codimension-one point.
The order of a Cartier divisor at a codimension-one point. It is the order of any rational local equation defined near that point.
Equations
- D.orderAt x = Exists.choose ⋯
Instances For
The order of a Cartier divisor is computed by any rational local equation defined near the point.
A Cartier divisor has order zero at every codimension-one point where it vanishes locally.
The zero Cartier divisor has order zero at every codimension-one point.
The order of a sum of Cartier divisors is the sum of their orders.
The order of the negation of a Cartier divisor is the negative of its order.
The order of a difference of Cartier divisors is the difference of their orders.
Only finitely many codimension-one points have nonzero order in a Cartier divisor.
The Weil divisor associated with a Cartier divisor, obtained from its orders at codimension-one points.
Equations
Instances For
The coefficient of the Weil divisor associated with a Cartier divisor is its local order.
The construction from Cartier divisors to Weil divisors is additive.
Equations
- TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.toWeilDivisorHom = { toFun := TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.toWeilDivisor, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The Cartier-to-Weil homomorphism computes the divisor defined by local orders.
The Cartier-to-Weil homomorphism carries principal Cartier divisors to principal Weil divisors.
The Weil divisor associated with a Cartier divisor is locally principal, with the same rational local equations.
Sending a locally principal Weil divisor to its Cartier divisor and taking local orders recovers the original Weil divisor.
Gluing the local equations of the Weil divisor associated with a Cartier divisor recovers the Cartier divisor.
The Weil--Cartier equivalence. On a Noetherian integral curve whose codimension-one local rings are discrete valuation rings, Weil divisors are additively equivalent to Cartier divisors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The forward map of the Weil--Cartier equivalence glues the local equations of a Weil divisor.
The inverse of the Weil--Cartier equivalence is the associated Weil divisor.