Residue fields at closed points are finite over global functions

Let f : X ⟶ Y be a morphism locally of finite type to an affine Jacobson scheme, for instance a scheme of finite type over a field. The residue field κ(x) at a closed point x of X is a finite extension of the residue field of its image (Hilbert's Nullstellensatz), so evaluation at x makes κ(x) a finite algebra over the global functions of X.

This is the finiteness that bounds the jump dim H⁰(X, 𝒪_X(D + x)) - dim H⁰(X, 𝒪_X(D)) by the degree of a closed point x of a curve.

Main declarations

• AlgebraicGeometry.Scheme.finite_Γevaluation_of_isClosed: the evaluation map Γ(X, ⊤) ⟶ κ(x) at a closed point is finite;
• AlgebraicGeometry.Scheme.Hom.residueDegree_ne_zero_of_isClosed: the residue degree [κ(x) : κ(f x)] at a closed point is finite, hence nonzero.

The input is Mathlib's isFinite_iff_locallyOfFiniteType_of_jacobsonSpace applied to Spec κ(x) ⟶ X ⟶ Y, as in Mathlib's AlgebraicGeometry.residueFieldIsoBase.

theorem AlgebraicGeometry.Scheme.finite_Γevaluation_of_isClosed {X Y : Scheme} [IsAffine Y] [JacobsonSpace ↥Y] (f : X ⟶ Y) [LocallyOfFiniteType f] {x : ↥X} (hx : IsClosed {x}) : (CommRingCat.Hom.hom (X.Γevaluation x)).Finite

At a closed point x of a scheme locally of finite type over an affine Jacobson scheme, the residue field κ(x) is a finite algebra over the global functions via evaluation at x.

theorem AlgebraicGeometry.Scheme.Hom.residueDegree_ne_zero_of_isClosed {X Y : Scheme} [JacobsonSpace ↥Y] (f : X ⟶ Y) [LocallyOfFiniteType f] {x : ↥X} (hx : IsClosed {x}) : residueDegree f x ≠ 0

At a closed point x of a scheme locally of finite type over a Jacobson scheme, the residue field extension κ(f x) ⟶ κ(x) is finite, so its residue degree is nonzero. For a scheme of finite type over a field k this says that closed points have finite degree over k.