Representation of line bundles by Cartier divisor sheaves #

Let X be an integral scheme. This file proves that every line bundle L on X is isomorphic to the sheaf 𝒪_X(D) of a Cartier divisor D, so that D ↦ 𝒪_X(D) maps the Cartier divisors onto the isomorphism classes of line bundles. This is the surjectivity half of the dictionary CaCl(X) ≅ Pic(X) between Cartier divisors modulo principal divisors and line bundles; unlike its Weil-divisor counterpart on curves, it needs no regularity or dimension hypothesis.

The divisor is read off from the rational embedding of L. A rank-one trivialization of L on a dense open subset realizes L inside the sheaf 𝒦_X of rational functions (Scheme.Modules.rationalTrivializationHom), and over the domain V of any local rank-one trivialization the image consists of the regular multiples of one nonzero rational function f_V. On overlaps these functions differ by regular units, so the classes of the f_V⁻¹ glue to a Cartier divisor D. Since f_V⁻¹ is an equation of D over V, the sections of 𝒪_X(D) over an open subset of V are the rational functions g for which g / f_V is regular, which are exactly the rational functions of the sections of L there.

Main declarations #

Scheme.Modules.exists_cartierDivisor_restrict_eq: the local basis functions of a rationally trivialized line bundle glue to a Cartier divisor;
Scheme.CartierDivisor.isoSheafOfRestrictEq: for such a divisor D, the isomorphism L ≅ 𝒪_X(D) through which the rational embedding of L factors (Scheme.CartierDivisor.isoSheafOfRestrictEq_hom_sheafι);
Scheme.CartierDivisor.exists_nonempty_iso_sheaf: every line bundle is isomorphic to the sheaf of a Cartier divisor;
Scheme.CartierDivisor.toLineBundleClass, the class of 𝒪_X(D), which is trivial for principal divisors (Scheme.CartierDivisor.toLineBundleClass_principalCartierDivisor) and surjective onto the line-bundle classes (Scheme.CartierDivisor.toLineBundleClass_surjective).

References #

R. Hartshorne, Algebraic Geometry, Proposition II.6.15.

source

theorem AlgebraicGeometry.Scheme.Modules.rationalUnitClass_trivializationGeneratorRationalUnit_eq {X : Scheme} [IsIntegral X] (M : X.Modules) {U V₁ V₂ W : X.Opens} (e : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M U) (hU : Dense ↑U) (t₁ : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M V₁) (t₂ : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M V₂) (i₁ : W ⟶ V₁) (i₂ : W ⟶ V₂) [Nonempty ↥↑V₁] [Nonempty ↥↑V₂] [Nonempty ↥↑W] :

(TauCeti.AlgebraicGeometry.Scheme.rationalUnitClass X W) (Additive.ofMul (M.trivializationGeneratorRationalUnit e hU t₁)) = (TauCeti.AlgebraicGeometry.Scheme.rationalUnitClass X W) (Additive.ofMul (M.trivializationGeneratorRationalUnit e hU t₂))

On a nonempty open subset W of the domains of two rank-one trivializations of a sheaf of modules, the rational functions of their basis sections have the same Cartier-divisor class: they differ by a regular unit on W.

source

theorem AlgebraicGeometry.Scheme.Modules.exists_cartierDivisor_restrict_eq {X : Scheme} [IsIntegral X] (M : X.Modules) [TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X M] {U : X.Opens} (e : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M U) (hU : Dense ↑U) :

∃ (E : TauCeti.AlgebraicGeometry.Scheme.CartierDivisor X), ∀ (V : X.Opens) [inst : Nonempty ↥↑V] (t : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M V), TopCat.Presheaf.restrictOpen E V ⋯ = (TauCeti.AlgebraicGeometry.Scheme.rationalUnitClass X V) (-Additive.ofMul (M.trivializationGeneratorRationalUnit e hU t))

The Cartier divisor of a rationally trivialized line bundle. Let M be a line bundle on an integral scheme, with a chosen rank-one trivialization on a dense open subset. There is a Cartier divisor whose restriction to the domain V of every nonempty rank-one trivialization t is the class of the inverse of the rational function of the basis section of t.

source

noncomputable def TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.isoSheafOfRestrictEq {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {M : X.Modules} [SheafOfModules.isInvertible X M] {U : X.Opens} {e : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M U} {hU : Dense ↑U} {D : CartierDivisor X} (hD : ∀ (V : X.Opens) [inst : Nonempty ↥↑V] (t : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M V), TopCat.Presheaf.restrictOpen D V ⋯ = (rationalUnitClass X V) (-Additive.ofMul (M.trivializationGeneratorRationalUnit e hU t))) :

M ≅ D.sheaf

If D is the class of the inverse of the rational basis function over the domain of every rank-one trivialization of M, then the rational embedding of M factors through an isomorphism M ≅ 𝒪_X(D).

Equations