The function field of a geometrically integral scheme

Let X be an integral scheme over a field k that is geometrically integral over k. Then for every field extension L / k the ring k(X) ⊗[k] L is a domain, and consequently k is algebraically closed in the function field k(X), that is, k is the full field of constants of k(X).

For the first statement, choose a nonempty affine open U of X. The base change Spec (Γ(X, U) ⊗[k] L) of U to L is a nonempty open subscheme of the integral scheme X ×_k Spec L, so Γ(X, U) ⊗[k] L is a domain, and k(X) ⊗[k] L is a localization of it because k(X) is the fraction field of Γ(X, U). The second statement follows by taking for L an algebraic closure of k (TauCeti.algebraicClosure_eq_bot_of_isDomain_tensorProduct).

The constant-field hypothesis IsIntegrallyClosedIn k X.functionField is how the function-field theory of curves (Weil differentials, the genus of the function field, Serre duality for divisor sheaves) is applied to a curve. This file derives it from geometric integrality, which in turn holds for smooth geometrically connected schemes over k (TauCeti.AlgebraicGeometry.Smooth.geometricallyIntegral).

The proof is built on Andrew Yang's formalization of geometrically integral morphisms in Mathlib (AlgebraicGeometry.GeometricallyIntegral, in Mathlib/AlgebraicGeometry/Geometrically/Integral), which supplies the integrality of the base change X ×_k Spec L.

Main results

• TauCeti.AlgebraicGeometry.isDomain_functionField_tensorProduct_of_geometricallyIntegral: k(X) ⊗[k] L is a domain for every field extension L / k;
• TauCeti.AlgebraicGeometry.isIntegrallyClosedIn_functionField_of_geometricallyIntegral: k is algebraically closed in k(X).

instance TauCeti.AlgebraicGeometry.isDomain_functionField_tensorProduct_of_geometricallyIntegral {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.GeometricallyIntegral (X ↘ AlgebraicGeometry.Spec ↧k)] (L : Type u) [Field L] [Algebra k L] : IsDomain (TensorProduct k (↑X.functionField) L)

The function field of a geometrically integral scheme over k stays a domain after extending scalars to any field extension L of k.

theorem TauCeti.AlgebraicGeometry.isIntegrallyClosedIn_functionField_of_geometricallyIntegral {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.GeometricallyIntegral (X ↘ AlgebraicGeometry.Spec ↧k)] : IsIntegrallyClosedIn k ↑X.functionField

The constant field of a geometrically integral scheme. If X is integral and geometrically integral over k, then k is algebraically closed in the function field k(X).