Rational points of a scheme over a base #
A k-rational point of a scheme X over a field k is a morphism Spec k ⟶ X over Spec k,
that is, a section of the structure morphism f : X ⟶ Spec k. This file records what such a
section gives at the level of points and residue fields. The residue-degree results hold for a
section s of an arbitrary morphism of schemes f : X ⟶ S, with hypothesis s ≫ f = 𝟙 S.
Stalk evaluation is surjective over any commutative local ring; the final results identify residue
fields and global functions over a field.
Main results #
residueDegree_eq_one_of_section: the residue degree offat a point in the image of a section is1. OverS = Spec kthis is the statement[κ(x₀) : k] = 1at ak-rational pointx₀, and it is the reason a rational point is the right normalization datum.residueFieldIsoOfSection: consequently the residue field ofXat such a point is the residue field of the base,κ(y) ≅ κ(s y), with inverse the residue-field map ofs.residueDegree_comp_of_section: residue degrees over a further base are computed on the base,[κ(s y) : κ(g y)] = [κ(y) : κ(g y)]forg : S ⟶ Z.residueFieldRingEquivOfSection: over a baseSpec KwithKa field, the residue field at aK-rational point isK, through the evaluation map that Mathlib attaches to anyK-point,X.descResidueField (Scheme.stalkClosedPointTo s). The section hypothesis makes that map bijective (descResidueField_bijective_of_section), which is what lets aK-rational point transportK-structures to the fibre data at the point.isClosed_singleton_of_section: overSpec K, the section gives a closed point ofX.appTop_bijective_of_section: if moreoverXis integral and universally closed overSpec K, aK-rational point forces the global functions ofXto be the constants, that is,f.appTop : Γ(Spec K, ⊤) ⟶ Γ(X, ⊤)is bijective. Mathlib'sisField_of_universallyClosedmakesΓ(X, ⊤)a field, and evaluation at the point is a retraction off.appTop.
The divisor-level consequences live in TauCeti.AlgebraicGeometry.RationalPoint.Degree, which
keeps the results here independent of Weil divisor theory. They are the geometric source of the
weight-one base point hypothesis in divisor degree theory: the weight of a point of a curve over
k is its residue degree [κ(x) : k], and both the class-group splitting
OrderSystem.classGroupAddEquivPicZeroProdInt and the Abel-Jacobi class
OrderSystem.weightedAbelJacobiClass require a base point of weight one.
No external mathematics is vendored; the proofs reuse Mathlib's Scheme.Hom.residueFieldMap,
Scheme.residueFieldCongr and Scheme.Hom.residueDegree API, CategoryTheory.asIso and
CategoryTheory.Iso.inv_ext for the isomorphism, Mathlib's Scheme.descResidueField,
Scheme.stalkClosedPointTo and Scheme.residue_descResidueField for the rational-point
evaluation map, and Tau Ceti's residueDegree_comp and residueDegree_eq_one_iff.
Points in the image of a section #
On underlying points, a section of f is a right inverse of f.
A section of f is a one-sided inverse of f at every point of the base.
Residue degrees at a section #
The residue degree of f at a point in the image of a section is one.
For S = Spec k this says that a k-rational point x₀ of X has residue field κ(x₀) of
degree one over k.
A section has residue degree one at every point of the base.
Residue degrees over a further base are computed on the base: at a point in the image of a
section of f : X ⟶ S, the residue degree of f ≫ g agrees with that of g : S ⟶ Z.
Residue fields at a section #
The residue-field map of f at a point in the image of a section is bijective.
The residue-field map of a section is bijective at every point of the base.
The residue-field map of f at a point in the image of a section is an isomorphism.
The residue-field map of a section is an isomorphism at every point of the base.
The residue-field map of f at a point in the image of a section, followed by the
residue-field map of the section, is the identity of κ(y).
The residue field of X at a point in the image of a section is the residue field of the
base at the corresponding point of the base. The inverse is the residue-field map of the
section.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The forward map of residueFieldIsoOfSection is the residue-field map of f, transported
along f (s y) = y.
The inverse of residueFieldIsoOfSection is the residue-field map of the section.
Stalk evaluation over a local ring #
A section over a commutative local ring R induces a surjection from the stalk at the
image of the closed point of Spec R onto R.
The residue field at a rational point #
Over a field K, the residue field at a rational point is canonically isomorphic to K
through the evaluation map X.descResidueField (Scheme.stalkClosedPointTo s).
The image of a rational-point section is a closed point.
The canonical evaluation map κ(s 0) ⟶ K at a K-rational point is bijective: it is
injective as a map of fields, and surjective because the stalk already surjects onto K.
The residue field of X at a K-rational point is canonically the ground field K, through
the evaluation map of the point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
residueFieldRingEquivOfSection is the evaluation map of the rational point.
Global functions on a proper integral scheme with a rational point are constant. If X
is integral and universally closed over Spec K and has a K-rational point, then pulling back
along the structure morphism identifies the global functions on Spec K with those on X.