The sheaf of principal parts of a Weil divisor #
Let X be a Noetherian integral scheme whose local rings at codimension-one points are discrete
valuation rings, and let D be a Weil divisor on X. This file builds the sheaf of principal
parts of D concretely, as the direct sum of the skyscraper sheaves K(X) / 𝒪_X(D)_x at the
codimension-one points x: its sections over U are the finitely supported families of principal
parts at the codimension-one points of U. When the codimension-one points are closed, as on a
curve, it is the quotient 𝒦_X / 𝒪_X(D), that is, it sits in a short exact sequence
0 ⟶ 𝒪_X(D) ⟶ 𝒦_X ⟶ 𝒦_X / 𝒪_X(D) ⟶ 0
of 𝒪_X-modules whose last two terms are flasque. This is the flasque resolution of 𝒪_X(D)
through which its cohomology on a curve is computed.
Main declarations #
SchemeWeilDivisor.stalkSubmodule D x, the stalk𝒪_X(D)_x ⊆ K(X)at a codimension-one point, andSchemeWeilDivisor.PrincipalPart D x, the quotientK(X) / 𝒪_X(D)_x;SchemeWeilDivisor.principalParts D, the sheaf of principal parts, together with the descriptionprincipalParts_presheaf_map_applyof its restriction maps and the instance saying that it is flasque;SchemeWeilDivisor.toPrincipalParts D : 𝒦_X ⟶ principalParts D, taking a rational function to its principal partsSchemeWeilDivisor.principalPartAt, with kernel𝒪_X(D)(toPrincipalParts_app_eq_zero_iff,isLimitKernelForkSheafι);SchemeWeilDivisor.exists_toPrincipalParts_app_eqandSchemeWeilDivisor.epi_toPrincipalParts: if the codimension-one points are closed, principal parts can be prescribed locally, sotoPrincipalParts Dis an epimorphism;SchemeWeilDivisor.principalPartsShortComplex_shortExact, the resulting short exact sequence.
The sheaf 𝒪_X(D) and its inclusion into 𝒦_X are
TauCeti/AlgebraicGeometry/WeilDivisor/Scheme/Sheaf.lean, the finiteness of the points at which a
rational function violates the order bound is SchemeWeilDivisor.finite_setOf_ord_lt, the sheaf
condition is checked through Mathlib's TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing, and
surjectivity through TopCat.Sheaf.isLocallySurjective_iff_epi.
References #
- R. Hartshorne, Algebraic Geometry, II, Exercise 1.21 (the sheaf
𝒦 / 𝒪on a curve as a sum of skyscraper sheaves). - J.-P. Serre, Algebraic Groups and Class Fields, Chapter II, §5 (répartitions and the
cohomology of
𝒪_X(D)).
The stalk of 𝒪_X(D) at a codimension-one point x, as a submodule of the function field
over the local ring at x: the rational functions which vanish or have order at least -D(x)
at x.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The module of principal parts of D at a codimension-one point x: the quotient of the
function field by the stalk of 𝒪_X(D) at x.
Equations
- D.PrincipalPart x = (↑X.functionField ⧸ D.stalkSubmodule x)
Instances For
The finitely supported families of principal parts of D at the codimension-one points of
U.
Equations
- D.principalPartsSections U = Π₀ (x : { x : TauCeti.AlgebraicGeometry.CodimensionOnePoint X // ↑x ∈ U }), D.PrincipalPart ↑x
Instances For
Restriction of a finitely supported family of principal parts to a smaller open subset.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pointwise module structure on finitely supported families of principal parts.
Equations
Instances For
The sheaf of 𝒪_X-modules of principal parts of a Weil divisor D on a Noetherian integral
scheme: its sections over U are the finitely supported families of principal parts
K(X) / 𝒪_X(D)_x at the codimension-one points x of U. When the codimension-one points are
closed it is the quotient 𝒦_X / 𝒪_X(D), by principalPartsShortComplex_shortExact.
Equations
- D.principalParts = { val := TauCeti.AlgebraicGeometry.SchemeWeilDivisor.principalPartsPresheaf✝ D, isSheaf := ⋯ }
Instances For
Sections of the sheaf of principal parts are finitely supported families of local principal parts. This equivalence is the public interface to the sealed sheaf construction.
Equations
Instances For
Under principalPartsSectionsEquiv, restriction is principalPartsRestrict.
A function on U acts on a section of principalParts D through its germs at the
codimension-one points.
The restriction maps of the sheaf of principal parts forget the points outside the smaller
open subset. This pointwise form complements the whole-section simp lemma
principalPartsSectionsEquiv_map.
The sheaf of principal parts is flasque: a finitely supported family on a smaller open subset extends by zero.
The principal part at a codimension-one point x of U of a section of 𝒦_X over U.
Equations
Instances For
Over a nonempty open subset, the principal part at x is the class of the rational function
in K(X) / 𝒪_X(D)_x.
The principal part of a section of 𝒦_X at a codimension-one point vanishes exactly when the
rational function lies in the stalk of 𝒪_X(D) there.
A fixed rational function has a nonzero principal part at finitely many codimension-one points only.
The principal parts of a section of 𝒦_X over U at the codimension-one points of U are
finitely supported: a nonzero rational function violates the order bound imposed by D at
finitely many codimension-one points only.
The principal parts of the sections of 𝒦_X over U, as an additive map into the
sections of the principal-parts sheaf.
Equations
Instances For
The principal parts of r • s are those of s multiplied by the germs of r.
Principal parts commute with restriction.
The morphism from 𝒦_X to the sheaf of principal parts of D, taking a rational function to
its principal parts at the codimension-one points.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The kernel of toPrincipalParts D is 𝒪_X(D), on sections: a rational function on U
has vanishing principal parts at every codimension-one point of U exactly when it is a section
of 𝒪_X(D) over U.
The sequence 𝒪_X(D) ⟶ 𝒦_X ⟶ principalParts D of 𝒪_X-modules. It is exact in the middle
(principalPartsShortComplex_exact), and short exact when the codimension-one points are closed
(principalPartsShortComplex_shortExact).
Equations
- D.principalPartsShortComplex = { X₁ := D.sheaf, X₂ := TauCeti.AlgebraicGeometry.Scheme.rationalFunctions X, X₃ := D.principalParts, f := D.sheafι, g := D.toPrincipalParts, zero := ⋯ }
Instances For
The first object of the principal-parts short complex is 𝒪_X(D).
The middle object of the principal-parts short complex is the sheaf of rational functions.
The third object of the principal-parts short complex is the sheaf of principal parts.
The first arrow of the principal-parts short complex is the inclusion into rational functions.
The second arrow of the principal-parts short complex takes a rational function to its principal parts.
𝒪_X(D) is the kernel of toPrincipalParts D : 𝒦_X ⟶ principalParts D.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The sequence 𝒪_X(D) ⟶ 𝒦_X ⟶ principalParts D is exact in the middle.
Principal parts can be prescribed locally. If the codimension-one points are closed, a
finitely supported family of principal parts on U is, near any point y of U, the family of
principal parts of a single rational function: take a rational function with the prescribed
principal part at y, and delete the finitely many other points at which the family or that
function has a nonzero principal part.
toPrincipalParts D is an epimorphism when the codimension-one points are closed.
The short exact sequence of principal parts 0 ⟶ 𝒪_X(D) ⟶ 𝒦_X ⟶ principalParts D ⟶ 0, on
a Noetherian integral scheme whose codimension-one points are closed and have discrete valuation
rings as local rings.