The two-chart model of a function field is a regular curve

Let F / k be an algebraic function field and x ∈ F transcendental over k. The scheme TauCeti.AlgebraicGeometry.twoChartModel hF hx is glued from Spec 𝒪_x and Spec 𝒪_{x⁻¹}, where 𝒪_x and 𝒪_{x⁻¹} are the rings of functions regular wherever x, respectively x⁻¹, is regular. These are the integral closures of k[x] and k[x⁻¹] in F: Dedekind domains that are finitely generated k-algebras (TauCeti.isDedekindDomain_holomorphyRing_setOf_mem and TauCeti.finiteType_holomorphyRing_setOf_mem). Reading these properties chart by chart shows that the scheme is a curve over k in the sense used to compare it with the function field:

• it is locally of finite type over k and Noetherian;
• it has dimension one, because its function field F has transcendence degree one over k;
• it is regular: every local ring is a regular local ring;
• its points other than the generic point are exactly its points of codimension one, and the local ring at each of them is a discrete valuation ring.

The last property is the hypothesis under which TauCeti.AlgebraicGeometry.Scheme.toPlace attaches a place of the function field to a point, and, with the dimension bound, it is the hypothesis on the local rings in the comparison of the points of a curve with the places of its function field (TauCeti.AlgebraicGeometry.CodimensionOnePoint.equivPlace).

Main results

• TauCeti.AlgebraicGeometry.twoChartModel.locallyOfFiniteType: the structure morphism to Spec k is locally of finite type.
• TauCeti.AlgebraicGeometry.twoChartModel.isNoetherian: the scheme is Noetherian.
• TauCeti.AlgebraicGeometry.twoChartModel.topologicalKrullDim_eq_one: the scheme has dimension one.
• TauCeti.AlgebraicGeometry.twoChartModel.isFunctionField_functionField and TauCeti.AlgebraicGeometry.twoChartModel.isIntegrallyClosedIn_functionField: k(X) is an algebraic function field over k, with exact constant field k whenever k is integrally closed in F.
• TauCeti.AlgebraicGeometry.twoChartModel.coheight_le_one: every point has codimension at most one.
• TauCeti.AlgebraicGeometry.twoChartModel.isRegularLocalRing_stalk: every local ring is a regular local ring.
• TauCeti.AlgebraicGeometry.twoChartModel.isDiscreteValuationRing_stalk: the local ring at a codimension-one point is a discrete valuation ring.
• TauCeti.AlgebraicGeometry.twoChartModel.valuationRing_stalk: every local ring is a valuation ring, the hypothesis under which rational maps from the scheme to proper schemes extend.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section III.2 and Appendix B.
• R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977, Section I.6.

theorem TauCeti.AlgebraicGeometry.twoChartModel.locallyOfFiniteType {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) : AlgebraicGeometry.LocallyOfFiniteType (twoChartModel hF hx ↘ AlgebraicGeometry.Spec ↧k)

The two-chart model is locally of finite type over k, for x transcendental over k: both charts are spectra of finitely generated k-algebras.

theorem TauCeti.AlgebraicGeometry.twoChartModel.isNoetherian {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) : AlgebraicGeometry.IsNoetherian (twoChartModel hF hx)

The two-chart model is a Noetherian scheme, for x transcendental over k: it is of finite type over the field k and covered by two affine charts.

theorem TauCeti.AlgebraicGeometry.twoChartModel.topologicalKrullDim_eq_one {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) : topologicalKrullDim ↥(twoChartModel hF hx) = 1

The two-chart model has dimension one, for x transcendental over k: its dimension is the transcendence degree of its function field F over k.

theorem TauCeti.AlgebraicGeometry.twoChartModel.isFunctionField_functionField {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) : IsFunctionField k ↑(twoChartModel hF hx).functionField

The function field of the two-chart model is an algebraic function field over k, for x transcendental over k.

theorem TauCeti.AlgebraicGeometry.twoChartModel.isIntegrallyClosedIn_functionField {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (hk : IsIntegrallyClosedIn k F) : IsIntegrallyClosedIn k ↑(twoChartModel hF hx).functionField

Exactness of the constant field transfers to the function field of the two-chart model: if k is integrally closed in F, then k is integrally closed in k(twoChartModel hF hx).

theorem TauCeti.AlgebraicGeometry.twoChartModel.coheight_le_one {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (p : ↥(twoChartModel hF hx)) : Order.coheight p ≤ 1

Every point of the two-chart model has codimension at most one, for x transcendental over k.

theorem TauCeti.AlgebraicGeometry.twoChartModel.isRegularLocalRing_stalk {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (p : ↥(twoChartModel hF hx)) : IsRegularLocalRing ↑((twoChartModel hF hx).presheaf.stalk p)

The two-chart model is regular, for x transcendental over k: its local rings are the local rings of the Dedekind domains 𝒪_x and 𝒪_{x⁻¹}, which are regular.

theorem TauCeti.AlgebraicGeometry.twoChartModel.isDiscreteValuationRing_stalk {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (p : CodimensionOnePoint (twoChartModel hF hx)) : IsDiscreteValuationRing ↑((twoChartModel hF hx).presheaf.stalk ↑p)

The local rings of the two-chart model at its codimension-one points are discrete valuation rings, for x transcendental over k: they are regular local rings of dimension one.

theorem TauCeti.AlgebraicGeometry.twoChartModel.valuationRing_stalk {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (p : ↥(twoChartModel hF hx)) : ValuationRing ↑((twoChartModel hF hx).presheaf.stalk p)

The local rings of the two-chart model are valuation rings, for x transcendental over k: at the generic point the local ring is the function field, and at every other point it is a discrete valuation ring.