The two-chart model of a function field is universally closed

Let F / k be an algebraic function field and x ∈ F nonzero. The scheme TauCeti.AlgebraicGeometry.twoChartModel hF hx is glued from Spec 𝒪_x and Spec 𝒪_{x⁻¹}, where 𝒪_x and 𝒪_{x⁻¹} are the functions regular wherever x, respectively x⁻¹, is regular. This file proves that its structure morphism to Spec k is universally closed.

Universal closedness is what properness over k adds to separatedness and local finite type. It is also, through the existence part of the valuative criterion, the hypothesis under which every place of the function field is centred at a point of the scheme (TauCeti.AlgebraicGeometry.CodimensionOnePoint.toPlace_surjective).

Main results

• TauCeti.AlgebraicGeometry.twoChartModel.valuativeCriterion_existence: the structure morphism of twoChartModel to Spec k satisfies the existence part of the valuative criterion.
• the instance UniversallyClosed (twoChartModel hF hx ↘ Spec (.of k)).

Implementation notes

This is the argument showing that the projective line is universally closed, carried out on the normalizations of its two charts. Let R be a valuation ring with fraction field K. A K-point of the scheme lies in one of the charts, so it is a ring map φ : 𝒪_x → K or 𝒪_{x⁻¹} → K. The functions of 𝒪_x are integral over k[x] and R is integrally closed, so φ takes values in R as soon as φ x does, and then the K-point extends to an R-point. If φ x ∉ R, then φ x is nonzero and (φ x)⁻¹ ∈ R, because R is a valuation ring; the point lies on the overlap of the two charts, where x is a unit, and the same argument applies on the chart at infinity to x⁻¹.

References

• R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977, Theorems II.4.7 and II.4.9.
• The Stacks Project, Tag 01KF, the valuative criterion for universal closedness.

theorem TauCeti.AlgebraicGeometry.twoChartModel.valuativeCriterion_existence {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : AlgebraicGeometry.ValuativeCriterion.Existence (twoChartModel hF hx ↘ AlgebraicGeometry.Spec ↧k)

The two-chart model satisfies the existence part of the valuative criterion over Spec k: for a valuation ring R with fraction field K, every K-point of twoChartModel hF hx over an R-point of Spec k extends to an R-point.

instance TauCeti.AlgebraicGeometry.twoChartModel.universallyClosed {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} : AlgebraicGeometry.UniversallyClosed (twoChartModel hF hx ↘ AlgebraicGeometry.Spec ↧k)

The two-chart model is universally closed over Spec k, by the valuative criterion: it is quasi-compact, being covered by two affine charts.