Cartier divisors with trivial line bundle #
On an integral scheme, 𝒪_X(D) is trivial if and only if D is principal.
This identifies the kernel of the Cartier-divisor-to-line-bundle-class map, the
injectivity input to the Cartier class group–Picard group dictionary.
A global basis of 𝒪_X(D) gives a nonzero rational function q. On an open set
with local equation f, both q and f⁻¹ generate the same free rank-one module,
so f q is a regular unit. Thus D is the principal divisor of q⁻¹.
References #
- R. Hartshorne, Algebraic Geometry, Proposition II.6.15.
theorem
TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.exists_principalCartierDivisor_eq_of_nonempty_iso
{X : AlgebraicGeometry.Scheme}
[AlgebraicGeometry.IsIntegral X]
{D : CartierDivisor X}
(h : Nonempty (CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules ≅ D.sheaf))
:
∃ (f : (↑X.functionField)ˣ), principalCartierDivisor X f = D
A Cartier divisor with trivial associated line bundle is principal. No Noetherian, dimension, or regularity hypothesis is needed.
theorem
TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.toLineBundleClass_eq_one_iff
{X : AlgebraicGeometry.Scheme}
[AlgebraicGeometry.IsIntegral X]
{D : CartierDivisor X}
:
The kernel of the Cartier-divisor-to-line-bundle-class map consists of principal Cartier divisors.