Rational points as degree-one places of an elliptic function field

For an elliptic Weierstrass curve W over a field F, this file completes the point--place dictionary. It first packages the already constructed valuation at infinity as a normalized TauCeti.Place F W.FunctionField. A place at which x has no pole contains the whole coordinate ring: the coordinate ring is integral over F[X], while valuation rings are integrally closed. The general affine-model correspondence therefore identifies it with the place of a unique height-one prime. If x does have a pole, uniqueness of the elliptic valuation at infinity identifies the place with the one at infinity.

The place at infinity has degree one. Together with the existing equivalence between equation solutions and degree-one primes of the coordinate ring, the preceding dichotomy gives the desired equivalence

W.Point ≃ {P : TauCeti.Place F W.FunctionField // P.degree = 1}.

The point at infinity is sent to the place at infinity, and an affine point (x, y) is sent to the normalized adic place of the maximal ideal (X - x, Y - y).

Main definitions

• TauCeti.Place.infinity: the normalized place at infinity of an affine Weierstrass curve.
• WeierstrassCurve.Affine.pointEquivDegreeOnePlace: the point--place dictionary.

Main results

• TauCeti.Place.exists_eq_ofPrime_iff_valuation_X_le_one: a place is on the affine chart exactly when x has no pole there.
• TauCeti.Place.eq_infinity_or_existsUnique_eq_ofPrime: every place is either the place at infinity or the place of a unique height-one prime of the coordinate ring.
• TauCeti.Place.exists_one_lt_valuation_algebraMap_iff_eq_infinity: a place is infinite on the coordinate ring exactly when it is the place at infinity.
• TauCeti.Place.degree_infinity: the place at infinity has degree one.

Roadmap

TauCetiRoadmap/EllipticCurves/README.md, Layer 0, The point--place dictionary: for elliptic W, identify W.toAffine.Point with the degree-one places, taking O to infinityPlace and an affine point to its maximal ideal.

Provenance

Not ported. The proof composes Tau Ceti's generic normalized-place and affine-model APIs with the existing elliptic infinity valuation and affine point--prime dictionary. Mathlib supplies the coordinate ring, its finite F[X]-module structure, and the valuation machinery, but contains no point--place equivalence for Weierstrass function fields.

noncomputable def TauCeti.Place.infinity {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : Place F W.FunctionField

The normalized place induced by W.infinityPlace, with value group ℤᵐ⁰.

Equations

• TauCeti.Place.infinity W = { valuation := W.infinityPlace, valuation_surjective := ⋯, isTrivialOn := ⋯ }

@[simp]

theorem TauCeti.Place.valuation_infinity {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : (infinity W).valuation = W.infinityPlace

theorem TauCeti.Place.exists_eq_ofPrime_iff_valuation_X_le_one {F : Type u_1} [Field F] {W : WeierstrassCurve.Affine F} [IsDedekindDomain W.CoordinateRing] (P : Place F W.FunctionField) : (∃ (𝔭 : IsDedekindDomain.HeightOneSpectrum W.CoordinateRing), ofPrime F W.FunctionField 𝔭 = P) ↔ P.valuation ((algebraMap (Polynomial F) W.FunctionField) Polynomial.X) ≤ 1

A normalized place of F(W) / F lies on the affine chart exactly when x has no pole at that place.

theorem TauCeti.Place.eq_infinity_or_existsUnique_eq_ofPrime {F : Type u_1} [Field F] {W : WeierstrassCurve.Affine F} [IsDedekindDomain W.CoordinateRing] (P : Place F W.FunctionField) : P = infinity W ∨ ∃! 𝔭 : IsDedekindDomain.HeightOneSpectrum W.CoordinateRing, ofPrime F W.FunctionField 𝔭 = P

If the coordinate ring is Dedekind, every normalized place of a Weierstrass function field is either the place at infinity or the place of a unique height-one prime of the coordinate ring.

@[simp]

theorem TauCeti.Place.exists_one_lt_valuation_algebraMap_iff_eq_infinity {F : Type u_1} [Field F] {W : WeierstrassCurve.Affine F} [IsDedekindDomain W.CoordinateRing] (Q : Place F W.FunctionField) : (∃ (r : W.CoordinateRing), 1 < Q.valuation ((algebraMap W.CoordinateRing W.FunctionField) r)) ↔ Q = infinity W

A place is infinite on the coordinate ring exactly when it is the place at infinity.

@[simp]

theorem TauCeti.Place.degree_infinity {F : Type u_1} [Field F] {W : WeierstrassCurve.Affine F} : (infinity W).degree = 1

The place at infinity is rational: its residue field has degree one over the base field.

@[simp]

theorem TauCeti.Place.infinity_ne_ofPrime {F : Type u_1} [Field F] {W : WeierstrassCurve.Affine F} [IsDedekindDomain W.CoordinateRing] (𝔭 : IsDedekindDomain.HeightOneSpectrum W.CoordinateRing) : infinity W ≠ ofPrime F W.FunctionField 𝔭

The place at infinity is different from the place of every prime on the affine chart.

theorem TauCeti.Place.not_isEquiv_infinityPlace_valuation {F : Type u_1} [Field F] {W : WeierstrassCurve.Affine F} [IsDedekindDomain W.CoordinateRing] (𝔭 : IsDedekindDomain.HeightOneSpectrum W.CoordinateRing) : ¬W.infinityPlace.IsEquiv (IsDedekindDomain.HeightOneSpectrum.valuation W.FunctionField 𝔭)

The place at infinity is not equivalent to the place of any prime of the affine chart: the valuation form of infinity_ne_ofPrime, a place being determined by the class of its valuation.

noncomputable def TauCeti.Place.degreeOneAffineOrInfinityEquiv {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [IsDedekindDomain W.CoordinateRing] : WithZero { 𝔭 : IsDedekindDomain.HeightOneSpectrum W.CoordinateRing // Module.finrank F (W.CoordinateRing ⧸ 𝔭.asIdeal) = 1 } ≃ { P : Place F W.FunctionField // P.degree = 1 }

The degree-one normalized places are exactly the place at infinity together with the degree-one height-one primes of the affine coordinate ring.

Equations

• TauCeti.Place.degreeOneAffineOrInfinityEquiv W = Equiv.ofBijective (TauCeti.Place.affineOrInfinityToDegreeOnePlace✝ W) ⋯

@[simp]

theorem TauCeti.Place.coe_degreeOneAffineOrInfinityEquiv_none {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [IsDedekindDomain W.CoordinateRing] : ↑((degreeOneAffineOrInfinityEquiv W) 0) = infinity W

@[simp]

theorem TauCeti.Place.coe_degreeOneAffineOrInfinityEquiv_some {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [IsDedekindDomain W.CoordinateRing] (𝔭 : { 𝔭 : IsDedekindDomain.HeightOneSpectrum W.CoordinateRing // Module.finrank F (W.CoordinateRing ⧸ 𝔭.asIdeal) = 1 }) : ↑((degreeOneAffineOrInfinityEquiv W) ↑𝔭) = ofPrime F W.FunctionField ↑𝔭

theorem WeierstrassCurve.Affine.instIsDedekindDomainCoordinateRing_tauCeti {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] : IsDedekindDomain W.CoordinateRing

noncomputable def WeierstrassCurve.Affine.pointEquivDegreeOnePlace {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] : W.Point ≃ { P : TauCeti.Place F W.FunctionField // P.degree = 1 }

The point--place dictionary for an elliptic curve: rational points correspond to the degree-one normalized places of the function field. The point at infinity goes to Place.infinity W, while (x, y) goes to the adic place of (X - x, Y - y).

Equations

• W.pointEquivDegreeOnePlace = W.pointEquiv.trans ((WeierstrassCurve.Affine.CoordinateRing.equationEquivDegreeOnePlace W).optionCongr.trans (TauCeti.Place.degreeOneAffineOrInfinityEquiv W))

@[simp]

theorem WeierstrassCurve.Affine.coe_pointEquivDegreeOnePlace_zero {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] : ↑(W.pointEquivDegreeOnePlace Point.zero) = TauCeti.Place.infinity W

The point--place dictionary sends the point at infinity to the place at infinity.

@[simp]

theorem WeierstrassCurve.Affine.coe_pointEquivDegreeOnePlace_mk {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {x y : F} (h : W.Equation x y) : ↑(W.pointEquivDegreeOnePlace (Point.mk h)) = TauCeti.Place.ofPrime F W.FunctionField (CoordinateRing.pointPlace h)

The point--place dictionary sends (x, y) to the normalized place of its maximal ideal.

@[simp]

theorem WeierstrassCurve.Affine.coe_pointEquivDegreeOnePlace_some {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {x y : F} (h : W.Nonsingular x y) : ↑(W.pointEquivDegreeOnePlace (Point.some x y h)) = TauCeti.Place.ofPrime F W.FunctionField (CoordinateRing.pointPlace ⋯)

The point--place dictionary sends a nonsingular point (x, y) to the normalized place of its maximal ideal.

@[simp]

theorem WeierstrassCurve.Affine.pointEquivDegreeOnePlace_symm_infinity {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] : W.pointEquivDegreeOnePlace.symm ⟨TauCeti.Place.infinity W, ⋯⟩ = Point.zero

Reading the place at infinity backwards through the dictionary recovers the point at infinity.

@[simp]

theorem WeierstrassCurve.Affine.pointEquivDegreeOnePlace_symm_ofPrime {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {x y : F} (h : W.Equation x y) : W.pointEquivDegreeOnePlace.symm ⟨TauCeti.Place.ofPrime F W.FunctionField (CoordinateRing.pointPlace h), ⋯⟩ = Point.mk h

Reading the place of an affine point backwards through the dictionary recovers that point.