The sheaf of a sum of Weil divisors #
Sections of πͺ_X(D) and of πͺ_X(E) multiply inside the sheaf π¦_X of rational functions, and
their product satisfies the order bound imposed by D + E, because orders of vanishing add. This
file assembles those products into a morphism from the sectionwise tensor product of πͺ_X(D) and
πͺ_X(E) to πͺ_X(D + E), and shows that on an integral Noetherian curve whose codimension-one
local rings are discrete valuation rings it becomes an isomorphism after sheafification:
πͺ_X(D) β πͺ_X(E) β
πͺ_X(D + E).
What makes multiplication locally bijective is a local equation: over an open subset on which E
is cut out by a single rational function g, multiplying by g and by gβ»ΒΉ inverts it.
Main declarations #
SchemeWeilDivisor.sectionsMul, the product of a section ofπͺ_X(D)and a section ofπͺ_X(E), withSchemeWeilDivisor.sectionsMulLiftits linear form on the tensor product of sections andSchemeWeilDivisor.tensorPresheafHomthe resulting morphism of presheaves of modules;SchemeWeilDivisor.exists_sectionsMul_eqandSchemeWeilDivisor.sectionsMulLift_injective, the surjectivity and injectivity of multiplication over an open subset on whichEhas a local equation, the latter through the explicit retractionSchemeWeilDivisor.sectionsMulRetraction;SchemeWeilDivisor.tensorProductSheafIso, the isomorphismπͺ_X(D) β πͺ_X(E) β πͺ_X(D + E), whose forward map is the sheafified multiplication (SchemeWeilDivisor.tensorProductSheafIso_hom);SchemeWeilDivisor.toLineBundleClass_addandSchemeWeilDivisor.classGroupToLineBundleClassHom, saying thatD β¦ [πͺ_X(D)]carries addition of divisors, and of divisor classes, to tensor product of line bundles;SchemeWeilDivisor.isUnit_toLineBundleClass: the class ofπͺ_X(D)is invertible, with inverse the class ofπͺ_X(-D).
The construction follows Hartshorne, Algebraic Geometry, II.6.13, and the Stacks Project, Divisors, Tag 0BE0.
Orders of vanishing add. The product inside π¦_X of a section of πͺ_X(D) and a section
of πͺ_X(E) is a section of πͺ_X(D + E).
The product inside π¦_X of a section of πͺ_X(D) and a section of πͺ_X(E), as a section of
πͺ_X(D + E).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The product of two sections, read inside π¦_X, is the product of the two rational
functions.
Multiplying two sections of divisor sheaves commutes with restriction.
Multiplication inside π¦_X, as a linear map on the tensor product of the sections of
πͺ_X(D) and πͺ_X(E) over U.
Equations
- D.sectionsMulLift E U = TensorProduct.lift (LinearMap.mkβ (β(X.presheaf.obj (Opposite.op U))) (D.sectionsMul E U) β― β― β― β―)
Instances For
Multiplication inside π¦_X, as a morphism from the sectionwise tensor product of the
presheaves of modules underlying πͺ_X(D) and πͺ_X(E) to the one underlying πͺ_X(D + E).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The multiplication morphism acts on the sections over U as sectionsMulLift.
A local equation for E over V is a section of πͺ_X(-E) there.
Multiplying a section of πͺ_X(D + E) by a local equation for E gives a section of
πͺ_X(D).
Local surjectivity of multiplication. Where E has a local equation g, every section
of πͺ_X(D + E) over V is the product of a section of πͺ_X(D) and a section of πͺ_X(E):
multiply by g and by gβ»ΒΉ.
Division by a local equation g for E, as a map from the sections of πͺ_X(D + E) over V
to the sectionwise tensor product of the sections of πͺ_X(D) and of πͺ_X(E): it sends s to
(s Β· g) β gβ»ΒΉ.
It retracts multiplication (sectionsMulRetraction_sectionsMul), which is why multiplication is
injective on sections over V.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dividing by a local equation sends s to (s Β· g) β gβ»ΒΉ.
Dividing by a local equation retracts multiplication of sections.
Local injectivity of multiplication. Where E has a local equation, multiplication is
injective on the sectionwise tensor product over V, because dividing by that equation retracts
it.
On a curve, a Weil divisor has a local equation on an arbitrarily small neighbourhood of any point.
Multiplication is locally surjective. On a curve every point has a neighbourhood on which
E has a local equation (exists_localEquation_le), and over such a neighbourhood every section of
πͺ_X(D + E) is a product of sections of πͺ_X(D) and πͺ_X(E) (exists_sectionsMul_eq).
Multiplication is locally injective. On a curve every point has a neighbourhood on which
E has a local equation (exists_localEquation_le), and over such a neighbourhood multiplication
is injective on the sectionwise tensor product (sectionsMulLift_injective).
Multiplication becomes an isomorphism after sheafification: it is locally bijective.
The sheaf of a sum of Weil divisors is the tensor product of their sheaves. On a curve
whose codimension-one local rings are discrete valuation rings, multiplication inside π¦_X
identifies πͺ_X(D) β πͺ_X(E) with πͺ_X(D + E).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The forward map of tensorProductSheafIso is the sheafification of the multiplication morphism
tensorPresheafHom, read through the defining identification of the tensor product
(TauCeti.SheafOfModules.tensorProductIso) and the identification of πͺ_X(D + E) with its own
sheafification (TauCeti.SheafOfModules.sheafificationIso).
The divisor-to-line-bundle map is multiplicative. The class of πͺ_X(D + E) is the
product of the classes of πͺ_X(D) and πͺ_X(E).
Every divisorial line-bundle class is invertible, πͺ_X(-D) inverting πͺ_X(D).
The comparison from the divisor class group to line-bundle classes turns addition of divisor classes into tensor product of line bundles.
The comparison from the divisor class group to line-bundle classes, as an additive homomorphism into the additive form of the tensor-product monoid.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Applying the bundled divisor-class comparison recovers classGroupToLineBundleClass.