Rational functions represented by generically free rank-one module sections #
A sheaf of modules on an irreducible scheme that is free of rank one on a dense open subset has a rational trivialization. A chosen basis there maps every local section to a rational function and hence gives a morphism from the sheaf of modules to the sheaf of rational functions. For an invertible sheaf on an integral scheme this morphism is injective, so it realizes the line bundle as a subsheaf of the rational functions; this is the embedding from which the divisor of a line bundle is read off.
Main declarations #
Scheme.Modules.rationalFunctionreads a local section as an element of the function field.Scheme.Modules.rationalFunction_smulandScheme.Modules.rationalFunction_mapdescribe its compatibility with scalar multiplication and restriction.Scheme.Modules.rationalTrivializationHomis the resulting morphism to the rational-function sheaf, andScheme.Modules.rationalFunctionsEquiv_rationalTrivializationHom_appcomputes it on every nonempty open subset.Scheme.Modules.rationalFunction_injectiveandScheme.Modules.mono_rationalTrivializationHomshow that, for a line bundle on an integral scheme, this morphism is injective on sections and hence a monomorphism.Scheme.Modules.range_rationalFunctionidentifies the image of a line bundle in the rational functions on any nonempty open subset of a rank-one trivializing chart with the regular multiples of the rational function represented by the restricted basis sectionScheme.Modules.trivializationGeneratorof that chart, andScheme.Modules.isUnit_rationalFunction_trivializationGeneratorshows that this rational function is a unit on every nonempty rank-one trivializing open subset.
The construction follows Hartshorne, Algebraic Geometry, II.6. No formalization is vendored.
The rational function represented by a local section of a sheaf of modules after choosing a free rank-one trivialization on a dense open subset.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Multiplying a module section by a regular function multiplies its rational function by the image of that regular function in the function field.
Rational functions represented by module sections are unchanged by restriction to a nonempty open subset.
The morphism from a sheaf of modules to the rational-function sheaf determined by a free rank-one trivialization on a dense open subset.
Equations
- One or more equations did not get rendered due to their size.
Instances For
On a nonempty open subset, rationalTrivializationHom is the rational function obtained by
restricting to the chosen dense open and reading the section in the chosen basis.
On an integral scheme, the rational function of a local section of a line bundle determines the section: a line bundle embeds into the rational functions through any rational trivialization.
On an integral scheme, a local section of a line bundle has zero rational function exactly when it is zero.
On an integral scheme, the morphism from a line bundle to the rational functions determined by a rational trivialization is injective on sections over every open subset.
On an integral scheme, a line bundle is a subsheaf of the sheaf of rational functions: the morphism determined by any rational trivialization is a monomorphism.
On an open subset W of a rank-one trivializing open subset V, the image of the
rational-trivialization morphism consists exactly of the regular-function multiples of the image
of the restricted distinguished basis section.
On a nonempty open subset W of a rank-one trivializing open subset V, the rational
functions represented by sections are exactly the products of regular functions with the rational
function represented by the restricted distinguished basis section.
The rational function represented by the distinguished basis section on a nonempty rank-one trivializing open subset is a unit of the function field: on the nonempty open subset where both trivializations are defined, its coordinate is a transition unit.
The rational function represented by the distinguished basis section on a nonempty
trivializing open subset, bundled as a unit of the function field. Its regular multiples are
exactly the image of the module sheaf on that open subset (range_rationalFunction).
Equations
- M.trivializationGeneratorRationalUnit e hU t = ⋯.unit
Instances For
The function-field value of the bundled rational coefficient of a local basis section.
On a nonempty open subset W of the domain of a rank-one trivialization t, the rational
function of a section is a regular multiple of the rational function of the basis section of
t.
On a nonempty open subset W of the domains V₁, V₂ of two rank-one trivializations, the
rational functions represented by their restricted basis sections differ by a regular unit on
W, namely the transition unit of existsUnique_map_trivializationGenerator_eq_smul. This is the
transition-unit condition needed to glue the local principal images of range_rationalFunction
over overlapping charts into Cartier-divisor data.