Every regular proper curve is the two-chart model of its function field #
Let X be a curve over a field k (an integral scheme, proper and of dimension one over k)
which is regular, in the sense that its local rings away from the generic point are discrete
valuation rings, and let K = k(X) be its function field. For any x ∈ K transcendental over
k, the two-chart model M = twoChartModel hF hx of K, glued from the
normalizations of k[x] and k[x⁻¹] in K, is a regular proper curve over k with function
field K. This file proves that X is isomorphic to M over k, by the unique isomorphism
whose pullback of rational functions is the identification k(M) ≃ₐ[k] K
(TauCeti.AlgebraicGeometry.twoChartModel.functionFieldEquiv).
Both X and M are integral, have valuation rings as local rings (the function field at the
generic point, a discrete valuation ring elsewhere), and are proper over k. So the
morphism Spec K ⟶ M through the generic point extends uniquely to a k-morphism X ⟶ M, and
the morphism Spec K ⟶ X through the generic point extends uniquely to a k-morphism M ⟶ X
(AlgebraicGeometry.Scheme.homOfFunctionField). Both composites restrict to the identity at the
generic point, and a morphism into a separated scheme is determined there, so they are inverse
isomorphisms (AlgebraicGeometry.Scheme.isoOfFunctionFieldAlgEquiv).
Thus every regular proper curve over k is, up to a canonical isomorphism, the normalization of
the projective line in its function field. This is the object half of the correspondence between
function fields of one variable and regular proper curves; the morphism half, for two-chart
models, is TauCeti.AlgebraicGeometry.twoChartModel.homOfAlgHom.
Main definitions #
AlgebraicGeometry.Scheme.isoTwoChartModel: the isomorphism of a regular proper curveXoverkwith the two-chart model ofk(X)built from a transcendentalx ∈ k(X).
Main results #
- the instances
(X.isoTwoChartModel …).hom.IsOver (Spec k)and(X.isoTwoChartModel …).inv.IsOver (Spec k). AlgebraicGeometry.Scheme.functionFieldMap_isoTwoChartModel_hom: the pullback of rational functions along the isomorphismX ⟶ Mis the identificationk(M) ≃ₐ[k] k(X), andAlgebraicGeometry.Scheme.functionFieldMap_isoTwoChartModel_invthe same for its inverse.AlgebraicGeometry.Scheme.eq_isoTwoChartModel_hom_iff: a dominantk-morphismX ⟶ Mis this isomorphism exactly when its pullback of rational functions is that identification.
References #
- R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977, Theorem I.6.9 and Corollary I.6.12.
- H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Appendix B.
A regular proper curve is the two-chart model of its function field: for a curve X over
k whose codimension-one local rings are discrete valuation rings and x ∈ k(X) transcendental
over k, the isomorphism of X with
the two-chart model of k(X) built from x. It is the unique dominant k-morphism whose
pullback of rational functions is the identification of the function field of the model with
k(X) (eq_isoTwoChartModel_hom_iff).
Instances For
The isomorphism X ⟶ M of isoTwoChartModel is a morphism over k.
The isomorphism M ⟶ X of isoTwoChartModel is a morphism over k.
The pullback of rational functions along X ≅ M is the identification of function
fields: under the identification k(M) ≃ₐ[k] k(X) of the function field of the two-chart model
of k(X), the pullback along the isomorphism X ⟶ M of isoTwoChartModel is the identity.
The pullback of rational functions along the isomorphism M ⟶ X of isoTwoChartModel is the
identification k(X) ≃ₐ[k] k(M) of k(X) with the function field of the two-chart model.
A regular proper curve is the two-chart model of its function field in exactly one way: a
dominant k-morphism f : X ⟶ M to the two-chart model of k(X) is the isomorphism of
isoTwoChartModel exactly when, under the identification k(M) ≃ₐ[k] k(X), its pullback of
rational functions is the identity.