The sheaf 𝒪_X(D) of a Weil divisor #
For a Weil divisor D on an integral locally Noetherian scheme X which is regular in
codimension one, this file builds the sheaf of 𝒪_X-modules
Γ(U, 𝒪_X(D)) = {f ∈ K(X) | f = 0 or ord_x f ≥ -D(x) for every codimension-one x ∈ U},
as an 𝒪_X-submodule of the sheaf 𝒦_X of rational functions of
TauCeti/AlgebraicGeometry/Modules/RationalFunctions.lean. Regularity in codimension one enters
as the hypothesis that the local ring at every codimension-one point is a discrete valuation
ring. Under this hypothesis, the nonarchimedean order inequality makes the displayed set a
submodule.
Main declarations #
TauCeti.AlgebraicGeometry.SchemeWeilDivisor.sections D U, the displayedΓ(X, U)-submodule ofΓ(𝒦_X, U), withmem_sections_iffits description over a nonempty open subset andrationalFunctionsEquiv_symm_mem_sectionsits membership criterion for a rational function;isEffective_iff_one_mem_sectionsdetects effectivity using the rational section1, whilesections_congrandsections_add_zsmul_ofPoint_eqdescribe its dependence on the divisor's coefficients insideU;TauCeti.AlgebraicGeometry.SchemeWeilDivisor.submodule D, the same data as a submodule of the sheaf𝒦_X— the membership condition is local — andTauCeti.AlgebraicGeometry.SchemeWeilDivisor.sheaf D, the resulting sheaf𝒪_X(D)of𝒪_X-modules, together with its monomorphismsheafι D : 𝒪_X(D) ⟶ 𝒦_X, which is described on sections bysheafι_app_injective,sheafι_app_memandrange_sheafι_app, and the constructionsectionMkof a section from a rational function satisfying the order bound, andsheafLift, the factorization through𝒪_X(D)of a morphism to𝒦_Xsatisfying that bound;TauCeti.AlgebraicGeometry.SchemeWeilDivisor.sheafHomOfLE, the inclusion𝒪_X(D) ⟶ 𝒪_X(E)forD ≤ E, withsheafHomOfLE_app_bijective_of_coeff_eqshowing that it is bijective on sections wherever the divisors' coefficients agree, andTauCeti.AlgebraicGeometry.SchemeWeilDivisor.unitToSheaf, the factorization of𝒪_X ⟶ 𝒦_Xthrough𝒪_X(D)for an effectiveD;TauCeti.AlgebraicGeometry.SchemeWeilDivisor.sheafOverMulIsoOfCoeffEq, multiplication by a local equation as an isomorphism between restricted divisor sheaves;TauCeti.AlgebraicGeometry.SchemeWeilDivisor.sheafMulIso, multiplication by a nonzero rational function as an isomorphism𝒪_X(D) ≅ 𝒪_X(D - div g), andTauCeti.AlgebraicGeometry.SchemeWeilDivisor.nonempty_iso_sheaf_of_linearlyEquivalent: linearly equivalent divisors have isomorphic sheaves.
For a locally principal divisor, the resulting sheaf is invertible; see
SchemeWeilDivisor.IsLocallyPrincipal.isInvertible_sheaf in
TauCeti/AlgebraicGeometry/WeilDivisor/Scheme/LocalTriviality.lean.
No formalization is vendored. The construction reuses Mathlib's AlgebraicGeometry.Scheme.ord
with its order-of-vanishing lemmas, SheafOfModules.Submodule, and the sheaf 𝒦_X and its
multiplication endomorphisms from TauCeti/AlgebraicGeometry/Modules/RationalFunctions.lean.
The sections of 𝒪_X(D) over an open subset U: the rational functions vanishing, or with
order at least -D(x), at every codimension-one point x of U.
Closure under addition uses the nonarchimedean order inequality available when the codimension-one
local rings are discrete valuation rings; closure under multiplication by a regular function is
Scheme.ord_le_smul.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Membership in SchemeWeilDivisor.sections, unfolded: the condition is imposed one
codimension-one point at a time, so it makes sense over an open subset not known to be
nonempty.
A Weil divisor is effective exactly when the rational section 1 belongs to its divisor
sheaf over the whole scheme.
The sections of 𝒪_X(D) over U depend only on the coefficients of D at the
codimension-one points of U.
Altering a divisor at a codimension-one point x₀ leaves the sections of its sheaf unchanged
over every open subset missing x₀: the two divisor sheaves agree away from the closure of
x₀.
Over a nonempty open subset, a section of 𝒦_X lies in 𝒪_X(D) exactly when it vanishes or
has order at least -D at every codimension-one point of that subset.
This is deliberately not tagged @[simp]: the general mem_sections above already rewrites
s ∈ sections D U, for an arbitrary open subset, so tagging this specialization as well is a
simpNF failure. Use it through rw or simp [mem_sections_iff].
A rational function whose order is at least -D at every codimension-one point of a nonempty
open subset U is a section of 𝒪_X(D) over U.
Over an empty open subset, 𝒪_X(D) has all of the (zero) sections of 𝒦_X.
Restricting to a smaller open subset preserves the bound imposed by D.
The 𝒪_X-submodule 𝒪_X(D) of the sheaf 𝒦_X of rational functions: over U it consists
of the rational functions whose divisor is at least -D at every codimension-one point of U.
The membership condition is local, so this really 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 Weil divisor D.
Equations
Instances For
The sections of 𝒪_X(D) over U are the subtype cut out by sections D U.
The inclusion 𝒪_X(D) ⟶ 𝒦_X.
Instances For
A rational function on U satisfying the order bound imposed by D, viewed as a section of
𝒪_X(D) over U.
Together with sheafι_app_mem and sheafι_app_injective this describes the sections of 𝒪_X(D)
completely: they are exactly the rational functions satisfying the bound.
Equations
Instances For
The inclusion 𝒪_X(D) ⟶ 𝒦_X is injective on sections over every open subset.
The section of 𝒪_X(D) built from a rational function includes back into 𝒦_X as that
rational function.
A section of 𝒪_X(D) over U, viewed as a rational function, satisfies the order bound
imposed by D.
The sections of 𝒪_X(D) over U are exactly sections D U. Together with
SchemeWeilDivisor.sheafι_app_injective this identifies the sections of 𝒪_X(D) with the
submodule of Γ(𝒦_X, U) which defines it.
The canonical inclusion 𝒪_X(D) ⟶ 𝒦_X is a monomorphism.
A morphism to 𝒦_X whose sections all satisfy the order bound imposed by D factors through
𝒪_X(D).
Equations
- D.sheafLift φ hφ = TauCeti.SheafOfModules.liftToSubmodule D.submodule φ ⋯
Instances For
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).
sheafLift factors φ through 𝒪_X(D): composing it with the canonical inclusion
sheafι D : 𝒪_X(D) ⟶ 𝒦_X recovers the original morphism φ.
sheafLift factors φ through 𝒪_X(D): composing it with the canonical inclusion
sheafι D : 𝒪_X(D) ⟶ 𝒦_X recovers the original morphism φ.
On sections, sheafLift followed by the inclusion into 𝒦_X is the original morphism.
A larger divisor allows more sections.
A larger divisor allows more sections, as submodules of 𝒦_X.
The inclusion 𝒪_X(D) ⟶ 𝒪_X(E) of the sheaf of a divisor into the sheaf of a larger one.
Equations
Instances For
The inclusion attached to le_refl D is the identity of 𝒪_X(D).
The inclusions attached to D ≤ E and E ≤ F compose to the one attached to D ≤ F.
The inclusions attached to D ≤ E and E ≤ F compose to the one attached to D ≤ F.
The comparison map 𝒪_X(D) ⟶ 𝒪_X(E) of a pair D ≤ E is bijective on sections over an open
subset on which the larger sheaf has no more sections than the smaller one.
The comparison map 𝒪_X(D) ⟶ 𝒪_X(E) of a pair D ≤ E is bijective on sections over an open
subset at whose codimension-one points the two divisors agree.
For an effective divisor D, every regular function on U is a section of 𝒪_X(D).
For an effective divisor D, the inclusion 𝒪_X ⟶ 𝒦_X factors through 𝒪_X(D).
Equations
Instances For
The canonical map 𝒪_X ⟶ 𝒪_X(D) is an isomorphism if every section of 𝒪_X(D) is
regular.
Transporting 𝒪_X(D) along an equality of divisors.
Transporting 𝒪_X(D) along an equality of divisors.
If the coefficients of D and E differ on U by the orders of a nonzero rational
function g, then multiplication by g identifies their divisor sheaves over U.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The forward map of the restricted multiplication isomorphism is multiplication by g.
The forward map of the restricted multiplication isomorphism is multiplication by g.
The inverse map of the restricted multiplication isomorphism is multiplication by g⁻¹.
The inverse map of the restricted multiplication isomorphism is multiplication by g⁻¹.
Multiplying a section of 𝒪_X(D) by a nonzero rational function g gives a section of
𝒪_X(D - div g): multiplying by g shifts every order of vanishing by ord g.
Multiplication by g, as a morphism 𝒪_X(D) ⟶ 𝒪_X(D - div g).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Multiplication by a nonzero rational function is an isomorphism
𝒪_X(D) ≅ 𝒪_X(D - div g): linearly equivalent divisors have isomorphic sheaves.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The forward morphism of sheafMulIso is multiplication by g.
The inverse morphism of sheafMulIso, included into 𝒦_X, is multiplication by g⁻¹.
The inverse morphism of sheafMulIso, included into 𝒦_X, is multiplication by g⁻¹.
Linearly equivalent Weil divisors have isomorphic sheaves. This is the sheaf-level form
of the fact that 𝒪_X(D) depends only on the divisor class of D, and the reason the divisor
class group maps to isomorphism classes of 𝒪_X-modules.