The line bundle of a Cartier divisor #
Let X be an integral scheme with sheaf of rational functions 𝒦_X, and let D be a Cartier
divisor on X, that is, a global section of 𝒦_X^× / 𝒪_X^×. Near every point x, D is the
class of a nonzero rational function f, a local equation of D at x, well defined up to a
unit of the local ring 𝒪_{X,x} (Scheme.CartierDivisor.IsLocalEquationAt). This file
constructs the sheaf 𝒪_X(D) ⊆ 𝒦_X.
For nonempty U, its sections are rational functions satisfying
Γ(U, 𝒪_X(D)) = {g ∈ K(X) | f g ∈ 𝒪_{X,x} for every x ∈ U and every local equation f at x}.
Over the empty open subset, there is a unique section. In general the definition uses sections
of 𝒦_X over U, so it also covers this case.
Consequently 𝒪_X(D) = f⁻¹ 𝒪_X over any open subset on which f is an equation of D.
This file also proves that it is a line bundle.
Main declarations #
Scheme.CartierDivisor.sections D U, the displayed submodule ofΓ(𝒦_X, U), described through a single local equation byScheme.CartierDivisor.mem_sections_iff_exists, and, over an open subset on whichfis an equation ofD, asf⁻¹ Γ(X, U)byScheme.CartierDivisor.mem_sections_iff_of_rationalUnitClass_eq;Scheme.CartierDivisor.sheaf D, the sheaf𝒪_X(D)of𝒪_X-modules, with its inclusionScheme.CartierDivisor.sheafι D : 𝒪_X(D) ⟶ 𝒦_X(sheafι_app_mem,range_sheafι_app) and the factorizationScheme.CartierDivisor.sheafLiftthrough it of a morphism to𝒦_Xwhose sections satisfy the defining condition, an isomorphism when that morphism is injective with image𝒪_X(D)(Scheme.CartierDivisor.isIso_sheafLift);Scheme.CartierDivisor.sheafOverIsoOfRestrictEq: divisors that agree on an open subsetVhave isomorphic sheaves overV;Scheme.CartierDivisor.unitIsoSheafPrincipalCartierDivisor: the sheaf of the principal divisor offisf⁻¹ 𝒪_X, trivialized by multiplication byf;Scheme.CartierDivisor.isInvertible_sheafandScheme.CartierDivisor.toInvertibleSheaf:𝒪_X(D)is a line bundle.
References #
- R. Hartshorne, Algebraic Geometry, Section II.6, the construction of
𝓛(D)preceding Proposition II.6.13. TauCeti/AlgebraicGeometry/WeilDivisor/Scheme/Sheaf.lean, whose submodule sheaf construction is the model for this Cartier divisor sheaf.
The sections of 𝒪_X(D) over an open subset U: the rational functions g such that f g
lies in the local ring 𝒪_{X,x} for every point x ∈ U and every local equation f of D
at x.
By IsLocalEquationAt.mul_mem_range_iff it suffices to test one local equation at each point
(mem_sections_iff_exists).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Membership in CartierDivisor.sections, unfolded.
A rational function is a section of 𝒪_X(D) over U as soon as, at every point of U, its
product with some local equation of D lies in the local ring.
Restricting to a smaller open subset preserves the sections of 𝒪_X(D).
The sections of 𝒪_X(D) over an open subset carrying an equation. Let f be an equation
of D over V. Over every nonempty open W ≤ V, a rational function g is a section of
𝒪_X(D) exactly when f g is regular on W; that is, 𝒪_X(D) = f⁻¹ 𝒪_X over V.
Divisors that agree on an open subset V have the same sections over every open W ≤ V.
The 𝒪_X-submodule 𝒪_X(D) of the sheaf 𝒦_X of rational functions. The membership
condition is imposed point by point, so this is a submodule of the sheaf 𝒦_X.
Equations
- D.submodule = { obj := fun (U : (TopologicalSpace.Opens ↥X)ᵒᵖ) => D.sections (Opposite.unop U), map := ⋯, isSheaf := ⋯ }
Instances For
The component of the submodule 𝒪_X(D) ⊆ 𝒦_X at an object of the opposite category.
The sheaf 𝒪_X(D) of 𝒪_X-modules attached to a Cartier divisor D.
Equations
Instances For
The inclusion 𝒪_X(D) ⟶ 𝒦_X.
Instances For
A rational function satisfying the conditions for 𝒪_X(D) as a section of that sheaf.
Equations
Instances For
The inclusion 𝒪_X(D) ⟶ 𝒦_X is injective on sections over every open subset.
Including a section built from a rational function recovers that function.
The inclusion 𝒪_X(D) ⟶ 𝒦_X sends a section of 𝒪_X(D) over U into sections D U.
The sections of 𝒪_X(D) over U are exactly sections D U. Together with
sheafι_app_injective this identifies the sections of 𝒪_X(D) with the submodule of
Γ(𝒦_X, U) which defines it.
The inclusion 𝒪_X(D) ⟶ 𝒦_X is a monomorphism.
A morphism M ⟶ 𝒦_X all of whose sections lie in 𝒪_X(D) factors through 𝒪_X(D).
Equations
- D.sheafLift φ hφ = TauCeti.SheafOfModules.liftToSubmodule D.submodule φ ⋯
Instances For
sheafLift factors φ through 𝒪_X(D): composing it with the inclusion
sheafι D : 𝒪_X(D) ⟶ 𝒦_X recovers φ.
sheafLift factors φ through 𝒪_X(D): composing it with the inclusion
sheafι D : 𝒪_X(D) ⟶ 𝒦_X recovers φ.
On sections, sheafLift followed by the inclusion into 𝒦_X is the original morphism.
A factorization through 𝒪_X(D) is an isomorphism if its map into rational functions is
injective on sections and has image exactly the sections of 𝒪_X(D).
Divisors agreeing on an open subset have isomorphic sheaves there. If D and E have the
same restriction to V, then 𝒪_X(D) and 𝒪_X(E) have the same sections over every open
subset of V, so they are isomorphic over V, compatibly with their inclusions into 𝒦_X
(sheafOverIsoOfRestrictEq_hom_ι, sheafOverIsoOfRestrictEq_inv_ι).
Equations
- D.sheafOverIsoOfRestrictEq E V h = D.submodule.overIsoOfEq E.submodule V ⋯
Instances For
The isomorphism sheafOverIsoOfRestrictEq is compatible with the inclusions into 𝒦_X.
The isomorphism sheafOverIsoOfRestrictEq is compatible with the inclusions into 𝒦_X.
The inverse of sheafOverIsoOfRestrictEq is compatible with the inclusions into 𝒦_X.
The inverse of sheafOverIsoOfRestrictEq is compatible with the inclusions into 𝒦_X.
For a regular function a on U, the rational function f⁻¹ a is a section of the sheaf of
the principal divisor of f over U.
Multiplication by f⁻¹, from 𝒪_X to the sheaf of the principal divisor of f: a regular
function a goes to the section f⁻¹ a of 𝒪_X(div f).
Equations
- One or more equations did not get rendered due to their size.
Instances For
unitToSheafPrincipalCartierDivisor X f, read inside 𝒦_X, is multiplication by f⁻¹.
unitToSheafPrincipalCartierDivisor X f, read inside 𝒦_X, is multiplication by f⁻¹.
The principal-divisor map sends a to f⁻¹ a inside the rational-function sheaf.
Multiplication by f⁻¹ is an isomorphism from 𝒪_X to the sheaf 𝒪_X(div f) of the
principal divisor of f; it is packaged as unitIsoSheafPrincipalCartierDivisor.
The sheaf of a principal Cartier divisor is trivial. Multiplication by f⁻¹ identifies
𝒪_X with 𝒪_X(div f).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The forward map of unitIsoSheafPrincipalCartierDivisor is multiplication by f⁻¹.
The inverse of unitIsoSheafPrincipalCartierDivisor, read inside 𝒦_X, is multiplication by
f: it sends a section g of 𝒪_X(div f) to the regular function f g.
The inverse of unitIsoSheafPrincipalCartierDivisor, read inside 𝒦_X, is multiplication by
f: it sends a section g of 𝒪_X(div f) to the regular function f g.
The sheaf of a Cartier divisor is a line bundle. On an integral scheme, 𝒪_X(D) is
locally free of rank one: over an open subset on which f is an equation of D, it is
f⁻¹ 𝒪_X.
The line bundle 𝒪_X(D) attached to a Cartier divisor D on an integral scheme.
Equations
- D.toInvertibleSheaf = { obj := D.sheaf, property := ⋯ }
Instances For
The underlying sheaf of the line bundle attached to D is 𝒪_X(D).