The function field of an integral scheme of finite type over a field

Let X be an integral scheme locally of finite type over a field k. The function field k(X) is the fraction field of Γ(X, U) for every nonempty affine open U, and Γ(X, U) is a finitely generated k-algebra. Hence k(X) is essentially of finite type over k, and its transcendence degree is the Krull dimension of Γ(X, U) (Noether normalization), which is the dimension of U, which is the dimension of X:

dim X = trdeg_k k(X).

In particular, X is a curve (has dimension one) exactly when k(X) is an algebraic function field of one variable over k. This is what lets the function-field theory (places, repartitions, Weil differentials, the Riemann–Roch theorem of function fields) be applied to integral curves.

Main declarations

• TauCeti.AlgebraicGeometry.essFiniteType_functionField: k(X) is essentially of finite type over k;
• TauCeti.AlgebraicGeometry.topologicalKrullDim_eq_toNat_trdeg_functionField: dim X = trdeg_k k(X);
• TauCeti.AlgebraicGeometry.isFunctionField_functionField_iff: k(X) is an algebraic function field over k if and only if X has dimension one; isFunctionField_functionField_of_forall_coheight_le_one_of_coheight_eq_one reads the dimension off the codimensions of the points.

References

• R. Hartshorne, Algebraic Geometry, Chapter I, Proposition 1.8A and Exercise II.3.20.
• Stacks Project, Tag 00P0 (dimension and transcendence degree of finitely generated domains)

instance TauCeti.AlgebraicGeometry.essFiniteType_functionField (k : Type u) [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] : Algebra.EssFiniteType k ↑X.functionField

The function field of an integral scheme locally of finite type over a field k is essentially of finite type over k: it is a localization of a finitely generated k-algebra.

theorem TauCeti.AlgebraicGeometry.topologicalKrullDim_eq_toNat_trdeg_functionField (k : Type u) [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] : topologicalKrullDim ↥X = ↑(Cardinal.toNat (Algebra.trdeg k ↑X.functionField))

Dimension is transcendence degree. An integral scheme locally of finite type over a field k has dimension the transcendence degree of its function field over k.

theorem TauCeti.AlgebraicGeometry.isFunctionField_functionField_iff (k : Type u) [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] : IsFunctionField k ↑X.functionField ↔ topologicalKrullDim ↥X = 1

Curves have algebraic function fields. An integral scheme locally of finite type over a field k has dimension one exactly when its function field is an algebraic function field of one variable over k.

theorem TauCeti.AlgebraicGeometry.isFunctionField_functionField_of_forall_coheight_le_one_of_coheight_eq_one (k : Type u) [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) {x₀ : ↥X} (hx₀ : Order.coheight x₀ = 1) : IsFunctionField k ↑X.functionField

An integral scheme locally of finite type over k all of whose points have codimension at most one, one of them exactly one, is a curve: its function field is an algebraic function field of one variable over k.