The sheaf of a principal Weil divisor is a line bundle #
Let X be a locally Noetherian integral scheme of dimension at most one whose codimension-one
local rings are discrete valuation rings. This file identifies the sheaf 𝒪_X(0) of the zero
divisor with the structure sheaf. When X is moreover Noetherian, which is the hypothesis under
which the divisor div g of a rational function is available, it deduces that 𝒪_X(D) is an
invertible sheaf whenever D is the divisor of a nonzero rational function.
Main declarations #
TauCeti.AlgebraicGeometry.SchemeWeilDivisor.mem_sections_zero_iff: the sections of𝒪_X(0)over an open subset are exactly the regular functions there;TauCeti.AlgebraicGeometry.SchemeWeilDivisor.unitIsoSheafZero: the induced isomorphism𝒪_X ≅ 𝒪_X(0);TauCeti.AlgebraicGeometry.SchemeWeilDivisor.sheafPrincipalDivisorIsoUnit: the trivialization𝒪_X(div g) ≅ 𝒪_Xof the sheaf of a principal divisor, whose forward map is multiplication byg(sheafPrincipalDivisorIsoUnit_hom_toRationalFunctions);TauCeti.AlgebraicGeometry.SchemeWeilDivisor.isInvertible_sheaf_principalDivisor: the sheaf of a principal divisor is an invertible sheaf onX.
Together with the already available fact that linearly equivalent divisors have isomorphic
sheaves, this is the statement that the map D ↦ 𝒪_X(D) sends the trivial divisor class to the
trivial line bundle.
The identification 𝒪_X(0) = 𝒪_X follows Hartshorne, Algebraic Geometry, Proposition II.6.11.
The construction reuses the submodule-of-a-sheaf API and the multiplication isomorphisms of
TauCeti/AlgebraicGeometry/WeilDivisor/Scheme/Sheaf.lean, and Mathlib's fully faithful forgetful
functor from 𝒪_X-modules to presheaves of abelian groups.
The sections of 𝒪_X(0) are the regular functions. On a locally Noetherian scheme whose
codimension-one local rings are discrete valuation rings, let U be an open subset of dimension at
most one. A rational function with no poles on U is regular on U, so the sections of the sheaf
of the zero divisor over U are exactly the images of the sections of 𝒪_X.
The sheaf of the zero divisor is the structure sheaf. The canonical factorization of
𝒪_X ⟶ 𝒦_X through 𝒪_X(0) is an isomorphism: it is injective because 𝒪_X ⟶ 𝒦_X is, and
surjective because a rational function without poles is regular.
The isomorphism 𝒪_X ≅ 𝒪_X(0) given by SchemeWeilDivisor.isIso_unitToSheaf_zero.
Equations
Instances For
The forward map of SchemeWeilDivisor.unitIsoSheafZero is the canonical factorization of
𝒪_X ⟶ 𝒦_X through 𝒪_X(0).
The inverse of SchemeWeilDivisor.unitIsoSheafZero, included into 𝒦_X, is the
canonical inclusion of 𝒪_X(0).
The inverse of SchemeWeilDivisor.unitIsoSheafZero, included into 𝒦_X, is the
canonical inclusion of 𝒪_X(0).
The sheaf of the zero divisor is an invertible sheaf, X being locally Noetherian of
dimension at most one.
The sheaf of a principal divisor is trivial. On a Noetherian scheme of dimension at most
one, multiplication by g identifies 𝒪_X(div g) with 𝒪_X(0), which is the structure sheaf.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The trivialization SchemeWeilDivisor.sheafPrincipalDivisorIsoUnit, read inside 𝒦_X, is
multiplication by g: it sends a section s of 𝒪_X(div g) to the regular function g * s.
The trivialization SchemeWeilDivisor.sheafPrincipalDivisorIsoUnit, read inside 𝒦_X, is
multiplication by g: it sends a section s of 𝒪_X(div g) to the regular function g * s.
The inverse principal-divisor trivialization, included into 𝒦_X, is multiplication by
g⁻¹ after including a regular function into the rational functions.
The inverse principal-divisor trivialization, included into 𝒦_X, is multiplication by
g⁻¹ after including a regular function into the rational functions.
The sheaf of a principal Weil divisor is a line bundle. On a Noetherian integral scheme of dimension at most one whose codimension-one local rings are discrete valuation rings, this is the case of the divisor-to-line-bundle dictionary in which the divisor is globally the divisor of a rational function; it sends the trivial divisor class to the trivial line bundle.