The two-chart model of a function field is proper, and its points are the places

Let F / k be an algebraic function field and x ∈ F transcendental over k. The scheme X = 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. It is separated, universally closed and locally of finite type over k, so it is proper over k: a regular proper curve over k with function field F.

On such a curve every point other than the generic point is the centre of exactly one place of its function field (TauCeti.AlgebraicGeometry.CodimensionOnePoint.equivPlace). Composing with the identification k(X) ≃ₐ[k] F gives the equivalence twoChartModel.equivPlace between the codimension-one points of X and the places of F / k. The valuation ring of the place attached to a point is the local ring there, and its degree is the residue degree of the point.

The equivalence is compatible with the two charts: a point lies on the finite chart Spec 𝒪_x exactly when x is regular at its place. So the points of the finite chart are the places at which x has no pole, as for the normalization of the affine line in F, and the remaining points, on the chart at infinity, are the poles of x.

Main results

• TauCeti.AlgebraicGeometry.twoChartModel.isProper: the structure morphism to Spec k is proper.
• TauCeti.AlgebraicGeometry.twoChartModel.equivPlace: the codimension-one points of the two-chart model are equivalent to the places of F / k.
• TauCeti.AlgebraicGeometry.twoChartModel.equivPlace_apply: the place of a point is the place AlgebraicGeometry.Scheme.toPlace attaches to it, transported to F.
• TauCeti.AlgebraicGeometry.twoChartModel.mem_integers_equivPlace_iff: the valuation ring of the place attached to a point is the image of the local ring at that point.
• TauCeti.AlgebraicGeometry.twoChartModel.degree_equivPlace: the degree of that place is the residue degree of the point over k.
• TauCeti.AlgebraicGeometry.twoChartModel.mem_range_ιFinite_iff: a point lies on the finite chart exactly when x is regular at its place.

References

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

theorem TauCeti.AlgebraicGeometry.twoChartModel.isProper {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.IsProper (twoChartModel hF hx ↘ AlgebraicGeometry.Spec ↧k)

The two-chart model is proper over k, for x transcendental over k: it is separated, universally closed, and locally of finite type over k.

noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.equivPlace {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) : CodimensionOnePoint (twoChartModel hF hx) ≃ Place k F

The codimension-one points of the two-chart model are the places of F, for x transcendental over k: a point is sent to the place of k(X) ≃ₐ[k] F whose valuation ring is the local ring at the point.

theorem TauCeti.AlgebraicGeometry.twoChartModel.equivPlace_apply {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)) : (equivPlace hxt) p = Place.map (functionFieldEquiv hxt) ((twoChartModel hF hx).toPlace ↑p)

TauCeti.AlgebraicGeometry.twoChartModel.equivPlace is the place attached to the point by AlgebraicGeometry.Scheme.toPlace, transported along k(X) ≃ₐ[k] F.

theorem TauCeti.AlgebraicGeometry.twoChartModel.mem_integers_equivPlace_iff {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)) (f : F) : f ∈ ((equivPlace hxt) p).integers ↔ ∃ (a : ↑((twoChartModel hF hx).presheaf.stalk ↑p)), (functionFieldEquiv hxt) ((algebraMap ↑((twoChartModel hF hx).presheaf.stalk ↑p) ↑(twoChartModel hF hx).functionField) a) = f

The valuation ring of the place of a point is the local ring at the point: f ∈ F is regular at equivPlace hxt p exactly when it is the image of an element of the stalk at p.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.degree_equivPlace {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)) : ((equivPlace hxt) p).degree = AlgebraicGeometry.Scheme.Hom.residueDegree (twoChartModel hF hx ↘ AlgebraicGeometry.Spec ↧k) ↑p

The degree of the place of a point is the residue degree of the point over k.

theorem TauCeti.AlgebraicGeometry.twoChartModel.mem_range_ιFinite_iff {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)) : ↑p ∈ Set.range ⇑(ιFinite hF hx) ↔ x ∈ ((equivPlace hxt) p).integers

A point lies on the finite chart exactly when x is regular at its place. Hence the points of the finite chart Spec 𝒪_x are the places at which x has no pole, and the points off it are the poles of x.