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. Everything is stated for a section s of an arbitrary morphism of schemes f : X ⟶ S, the hypothesis being s ≫ f = 𝟙 S; the k-rational case is the special case S = Spec k.

Main results #

residueDegree_eq_one_of_section: the residue degree of f at a point in the image of a section is 1. Over S = Spec k this is the statement [κ(x₀) : k] = 1 at a k-rational point x₀, and it is the reason a rational point is the right normalization datum.
residueFieldIsoOfSection: consequently the residue field of X at such a point is the residue field of the base, κ(y) ≅ κ(s y), with inverse the residue-field map of s.
residueDegree_comp_of_section: residue degrees over a further base are computed on the base, [κ(s y) : κ(g y)] = [κ(y) : κ(g y)] for g : S ⟶ Z.

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 that the Layer A degree theory runs on: the weight of a point of a curve over k there 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.

This advances TauCetiRoadmap/JacobianChallenge/README.md, "Standing hypotheses" ("A chosen k-rational point x₀. ... the k-point rigidifies/normalizes the Picard functor and supplies the Abel-Jacobi morphism"). Base change of rational points is left to a subsequent file, since it is a statement about pullbacks in an arbitrary category rather than about schemes.

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, and Tau Ceti's residueDegree_comp and residueDegree_eq_one_iff.

Points in the image of a section #

source

theorem TauCeti.AlgebraicGeometry.leftInverse_of_section {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {s : S ⟶ X} (hs : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id S) :

Function.LeftInverse ⇑f ⇑s

On underlying points, a section of f is a right inverse of f.

source

@[simp]

theorem TauCeti.AlgebraicGeometry.section_apply {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {s : S ⟶ X} (hs : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id S) (y : ↥S) :

f (s y) = y

A section of f is a one-sided inverse of f at every point of the base.

Residue degrees at a section #

source

@[simp]

theorem TauCeti.AlgebraicGeometry.residueDegree_eq_one_of_section {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {s : S ⟶ X} (hs : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id S) (y : ↥S) :

AlgebraicGeometry.Scheme.Hom.residueDegree f (s y) = 1

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.

source

theorem TauCeti.AlgebraicGeometry.residueDegree_section_eq_one {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {s : S ⟶ X} (hs : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id S) (y : ↥S) :

AlgebraicGeometry.Scheme.Hom.residueDegree s y = 1

A section has residue degree one at every point of the base.

source

theorem TauCeti.AlgebraicGeometry.residueDegree_comp_of_section {X S Z : AlgebraicGeometry.Scheme} {f : X ⟶ S} {s : S ⟶ X} (hs : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id S) (g : S ⟶ Z) (y : ↥S) :

AlgebraicGeometry.Scheme.Hom.residueDegree (CategoryTheory.CategoryStruct.comp f g) (s y) = AlgebraicGeometry.Scheme.Hom.residueDegree g y

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 #

source

theorem TauCeti.AlgebraicGeometry.residueFieldMap_bijective_of_section {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {s : S ⟶ X} (hs : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id S) (y : ↥S) :

Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.residueFieldMap f (s y)))

The residue-field map of f at a point in the image of a section is bijective.

source

theorem TauCeti.AlgebraicGeometry.residueFieldMap_section_bijective {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {s : S ⟶ X} (hs : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id S) (y : ↥S) :

Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.residueFieldMap s y))

The residue-field map of a section is bijective at every point of the base.

source

theorem TauCeti.AlgebraicGeometry.isIso_residueFieldMap_of_section {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {s : S ⟶ X} (hs : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id S) (y : ↥S) :

CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.residueFieldMap f (s y))

The residue-field map of f at a point in the image of a section is an isomorphism.

source

theorem TauCeti.AlgebraicGeometry.isIso_residueFieldMap_section {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {s : S ⟶ X} (hs : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id S) (y : ↥S) :

CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.residueFieldMap s y)

The residue-field map of a section is an isomorphism at every point of the base.

source

theorem TauCeti.AlgebraicGeometry.residueFieldMap_comp_residueFieldMap_of_section {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {s : S ⟶ X} (hs : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id S) (y : ↥S) :

CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.residueFieldMap f (s y)) (AlgebraicGeometry.Scheme.Hom.residueFieldMap s y)) = CategoryTheory.CategoryStruct.id (S.residueField y)

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).

source

noncomputable def TauCeti.AlgebraicGeometry.residueFieldIsoOfSection {X S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {s : S ⟶ X} (hs : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id S) (y : ↥S) :

S.residueField y ≅ X.residueField (s 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