The sheaf of rational functions on an integral scheme #
Mathlib defines the function field X.functionField of an irreducible scheme as the stalk of
its structure sheaf at the generic point, but it does not organize the rational functions into a
sheaf on X. On an integral scheme the sheaf of total quotient rings is the constant sheaf with
value K(X), and the constant sheaf with value the stalk at the generic point is the pushforward
of the structure sheaf along the canonical morphism Spec K(X) βΆ X: that morphism hits exactly
the generic point, and on an irreducible space an open subset contains the generic point as soon
as it is nonempty. This file takes that pushforward as the definition, which makes the sheaf
condition and the πͺ_X-module structure automatic.
Main declarations #
TauCeti.AlgebraicGeometry.Scheme.genericPoint_mem, the elementary fact that every nonempty open subset of an irreducible scheme contains the generic point, andTauCeti.AlgebraicGeometry.Scheme.germ_smul_functionField, which says that a function on such a subset acts on the function field through its germ at any of its points;TauCeti.AlgebraicGeometry.Scheme.fromSpecFunctionField, the canonical morphismSpec K(X) βΆ Xfrom the spectrum of the function field, andTauCeti.AlgebraicGeometry.Scheme.fromSpecFunctionField_preimage: it pulls a nonempty open subset back to everything;TauCeti.AlgebraicGeometry.Scheme.rationalFunctionsRing, the sheafπ¦_Xas a sheaf of commutative rings,TauCeti.AlgebraicGeometry.Scheme.rationalFunctions, its underlyingπͺ_X-module sheaf, andTauCeti.AlgebraicGeometry.Scheme.rationalFunctionsSectionsEquiv, the canonical identification of their sections;TauCeti.AlgebraicGeometry.Scheme.toRationalFunctionsRingandTauCeti.AlgebraicGeometry.Scheme.toRationalFunctions, the canonical morphisms fromπͺ_Xas ring and module sheaves, respectively;TauCeti.AlgebraicGeometry.Scheme.rationalFunctionsRingEquiv, the identification of the ring of sections over a nonempty open subset withK(X), compatible with restriction maps, together with the constant-sheaf statements it gives for the ring sheaf,TauCeti.AlgebraicGeometry.Scheme.isIso_rationalFunctionsRing_mapandTauCeti.AlgebraicGeometry.Scheme.subsingleton_rationalFunctionsRing;TauCeti.AlgebraicGeometry.Scheme.rationalFunctionsEquiv, the identificationΞ(π¦_X, U) ββ[Ξ(X, U)] K(X)of its sections over a nonempty open subset with the function field,TauCeti.AlgebraicGeometry.Scheme.rationalFunctionsEquiv_map, the compatibility of these identifications with the restriction maps, and the two statements which say thatπ¦_Xreally is the constant sheaf:TauCeti.AlgebraicGeometry.Scheme.isIso_rationalFunctions_map, the restriction maps between nonempty open subsets are isomorphisms, andTauCeti.AlgebraicGeometry.Scheme.subsingleton_rationalFunctions, the sections over an empty open subset vanish; together these giveTauCeti.AlgebraicGeometry.Scheme.isFlasque_rationalFunctions;TauCeti.AlgebraicGeometry.Scheme.rationalFunctionsMul, multiplication by a rational function as an endomorphism ofπ¦_X, obtained by pushing forward multiplication by the corresponding global function onSpec K(X);rationalFunctionsEquiv_rationalFunctionsMul_appidentifies it with multiplication on sections, andrationalFunctionsMul_mulandrationalFunctionsMul_onemake it multiplicative, so that multiplying by a unit is an automorphism ofπ¦_X(rationalFunctionsMul_comp_invandrationalFunctionsMul_inv_comp);- the module morphism
TauCeti.AlgebraicGeometry.Scheme.toRationalFunctionsisX.germToFunctionFieldon sections (TauCeti.AlgebraicGeometry.Scheme.rationalFunctionsEquiv_toRationalFunctions_app), is injective on sections over every open subset of an integral scheme (TauCeti.AlgebraicGeometry.Scheme.toRationalFunctions_app_injective), and is therefore a monomorphism; TauCeti.AlgebraicGeometry.Scheme.exists_germToFunctionField_eq_of_forall_mem_range: a rational function lying in the local ring at every point of a nonempty open subsetUis regular onU.
The sheaf πͺ_X(D) attached to a Weil divisor is the submodule of π¦_X cut out by an order
bound; it is built in TauCeti/AlgebraicGeometry/WeilDivisor/Scheme/Sheaf.lean, and the
multiplication endomorphisms above are what make it depend only on the divisor class of D.
Cartier divisors are the global sections of π¦_X^*/πͺ_X^*, and the line bundle πͺ_X(D) attached
to a divisor is a subsheaf of π¦_X; both need the sheaf π¦_X and the inclusion πͺ_X βΆ π¦_X
built here. On an integral scheme the sheaf of total quotient rings agrees
with this constant sheaf, so no generality is lost at that stage.
No formalization is vendored. The construction reuses Mathlib's Scheme.functionField,
Scheme.germToFunctionField, Scheme.fromSpecStalk with its computation of the closed point, of
the range and of the maps on sections, Scheme.ΞSpecIso, Scheme.Modules.pushforward and
SheafOfModules.unitToPushforwardObjUnit.
The canonical morphism Spec K(X) βΆ X from the spectrum of the function field of an
irreducible scheme, that is, the morphism from the spectrum of the stalk at the generic point.
Equations
Instances For
The generic point of an irreducible scheme lies in every nonempty open subset.
A function on a nonempty open subset U acts on the function field through its germ at any
point of U.
Equations
- TauCeti.AlgebraicGeometry.Scheme.instUniqueSpecFunctionField X = { default := IsLocalRing.closedPoint βX.functionField, uniq := β― }
The sheaf of commutative rings underlying the rational-function sheaf: the pushforward of
the structure sheaf of Spec K(X) along fromSpecFunctionField.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical morphism of sheaves of rings πͺ_X βΆ π¦_X.
Equations
Instances For
The sheaf π¦_X of rational functions on an integral scheme X: the constant sheaf with
value the function field, realized as the pushforward of the structure sheaf of Spec K(X)
along TauCeti.AlgebraicGeometry.Scheme.fromSpecFunctionField.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The module sheaf and ring sheaf constructions of π¦_X have canonically identified
sections. Their underlying additive presheaves are definitionally equal because both constructions
use Mathlib's pushforward of the structure sheaf.
Equations
Instances For
The identification between module-sheaf and ring-sheaf sections commutes with restriction maps.
On a nonempty open subset, the morphism Spec K(X) βΆ X acts on sections by the germ map to
the function field.
The morphism Spec K(X) βΆ X pulls every nonempty open subset back to the whole of
Spec K(X), its source having a single point, which maps to the generic point.
The sections of the ring sheaf π¦_X over a nonempty open subset are the function field,
as commutative rings.
Equations
Instances For
The ring equivalences identifying sections of π¦_X with the function field commute with
restriction maps.
The sections of π¦_X over a nonempty open subset U are the function field, as a module
over the functions on U.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The module-sheaf identification with the function field is the ring-sheaf identification
transported across rationalFunctionsSectionsEquiv.
The identifications of the sections of π¦_X with the function field are compatible with the
restriction maps: π¦_X is the constant sheaf.
The restriction maps of π¦_X between nonempty open subsets are bijective.
The restriction maps of π¦_X between nonempty open subsets are isomorphisms.
The restriction maps of the ring sheaf π¦_X between nonempty open subsets are bijective.
The restriction maps of the ring sheaf π¦_X between nonempty open subsets are
isomorphisms.
The sheaf π¦_X has no nonzero sections over an empty open subset.
The ring sheaf π¦_X has no nonzero sections over an empty open subset.
The sheaf π¦_X of rational functions on an irreducible scheme is flasque: its restriction
maps between nonempty open subsets are bijective, and its sections over the empty open subset
vanish.
The canonical morphism πͺ_X βΆ π¦_X; it is an inclusion when X is integral, by
toRationalFunctions_app_injective.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The morphisms of ring sheaves and module sheaves πͺ_X βΆ π¦_X agree on sections.
On a nonempty open subset, the inclusion πͺ_X βΆ π¦_X is the germ map to the function
field.
A morphism from the structure sheaf to rational functions is multiplication by the
rational function obtained by evaluating the global section 1.
The action of a regular function on a section of π¦_X is multiplication in the ring of
sections of π¦_X by the image of that function.
Multiplication of two sections of π¦_X over an open subset, as a bilinear map over the
regular functions there.
The product is computed in the ring of sections of the sheaf of rings underlying π¦_X; over a
nonempty open subset it is multiplication in the function field, by
rationalFunctionsEquiv_mulBilin.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The product of two sections of π¦_X is their product in the ring of sections.
Over a nonempty open subset, the product of two sections of π¦_X is their product in the
function field.
Multiplying a section of π¦_X by the image of a regular function is the action of that
function on the section.
Multiplication of sections of π¦_X commutes with the restriction maps.
Multiplication by a rational function, as an endomorphism of π¦_X.
It is the pushforward along Spec K(X) βΆ X of multiplication by the corresponding global
function on Spec K(X), so no sheaf-theoretic gluing is needed to build it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Multiplication by f really is multiplication by f on sections.
Multiplication by a product is the composite of the two multiplications.
Multiplication by 1 is the identity.
Multiplying by a unit g and then by gβ»ΒΉ is the identity on π¦_X.
Multiplying by the inverse of a unit g and then by g is the identity on π¦_X.
Multiplication by gβ»ΒΉ then g cancels on sections.
Multiplication by g then gβ»ΒΉ cancels on sections.
The inclusion πͺ_X βΆ π¦_X is injective on sections over every open subset: over a nonempty
one because the germ map to the function field of an integral scheme is injective, and over an
empty one because there are no nonzero functions there.
A locally regular rational function is regular. On an integral scheme, a rational function
lying in the local ring πͺ_{X,y} at every point y of a nonempty open subset U is the germ of a
section of πͺ_X over U: inside the function field, Ξ(X, U) is the intersection of the local
rings at the points of U.
The morphism πͺ_X βΆ π¦_X of ring sheaves is injective on sections over every open
subset of an integral scheme.