The ideal of a point in the intermediate ring of an isogeny

Let φ : W₁ → W₂ be an isogeny, and P = (x, y) an affine point of W₁, with ideal ⟨X - x, Y - y⟩ of W₁.CoordinateRing. The intermediate ring of φ sits between that coordinate ring and W₁.FunctionField; geometrically it is the ring of functions regular away from the fibre φ⁻¹(O₂). Extending the ideal of P into it therefore depends only on whether P lies in that fibre:

• if P lies over O₂ — the pulled-back coordinate φ^* x₂ has a pole at P — the extended ideal is the unit ideal, since the intermediate ring contains φ^* x₂;
• otherwise the whole intermediate ring lies in the valuation ring of P, so the valuation of P is that of a height one prime of the intermediate ring, and the extended ideal is that prime.

These are the two cases of the ideal extension that TauCeti.Isogeny.pushClass performs before taking the relative norm down to W₂.CoordinateRing, which is how the class-group point map TauCeti.Isogeny.toPointHom evaluates at P.

Main results

• TauCeti.Isogeny.map_XYIdeal_eq_top_of_one_lt_valuation: the ideal of a point over O₂ extends to the unit ideal.
• TauCeti.Isogeny.valuation_le_one_of_valuation_pullback_X_le_one: the intermediate ring lies in the valuation ring of any other point.
• TauCeti.Isogeny.map_XYIdeal_eq_asIdeal_of_valuation_eq: the ideal of such a point extends to the prime of the intermediate ring carrying its valuation.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.2 and III.3.

theorem TauCeti.Isogeny.instIsDedekindDomainCoordinateRing {F : Type u_1} [Field F] {W₁ : WeierstrassCurve.Affine F} [IsIntegrallyClosed W₁.CoordinateRing] : IsDedekindDomain W₁.CoordinateRing

theorem TauCeti.Isogeny.map_XYIdeal_eq_top_of_one_lt_valuation {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) [IsIntegrallyClosed W₁.CoordinateRing] {x y : F} (h : W₁.Equation x y) (hP : 1 < (IsDedekindDomain.HeightOneSpectrum.valuation W₁.FunctionField (WeierstrassCurve.Affine.CoordinateRing.pointPlace h)) (φ.pullback ((algebraMap (Polynomial F) W₂.CoordinateRing) Polynomial.X))) : Ideal.map φ.toIntermediateRing (WeierstrassCurve.Affine.CoordinateRing.XYIdeal W₁ x (Polynomial.C y)) = ⊤

The ideal of a point over O₂ extends to the unit ideal of the intermediate ring. If the pulled-back coordinate φ^* x₂ has a pole at the affine point (x, y) of W₁, that is, if the point lies in the fibre of φ over the point at infinity of W₂, then ⟨X - x, Y - y⟩ generates the unit ideal, the intermediate ring containing φ^* x₂.

theorem TauCeti.Isogeny.valuation_le_one_of_valuation_pullback_X_le_one {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) [IsIntegrallyClosed W₁.CoordinateRing] {x y : F} (h : W₁.Equation x y) (hP : (IsDedekindDomain.HeightOneSpectrum.valuation W₁.FunctionField (WeierstrassCurve.Affine.CoordinateRing.pointPlace h)) (φ.pullback ((algebraMap (Polynomial F) W₂.CoordinateRing) Polynomial.X)) ≤ 1) (b : ↥φ.intermediateRing) : (IsDedekindDomain.HeightOneSpectrum.valuation W₁.FunctionField (WeierstrassCurve.Affine.CoordinateRing.pointPlace h)) ((algebraMap (↥φ.intermediateRing) W₁.FunctionField) b) ≤ 1

The intermediate ring lies in the valuation ring of a point off the fibre over O₂. If φ^* x₂ has no pole at the affine point (x, y) of W₁, then neither has any function pulled back from W₂, the coordinate ring of W₂ being integral over F[x₂]; nor, by integrality, has any element of the intermediate ring.

theorem TauCeti.Isogeny.map_XYIdeal_eq_asIdeal_of_valuation_eq {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) [IsIntegrallyClosed W₁.CoordinateRing] [IsDedekindDomain ↥φ.intermediateRing] {x y : F} (h : W₁.Equation x y) (𝔓 : IsDedekindDomain.HeightOneSpectrum ↥φ.intermediateRing) (h𝔓 : IsDedekindDomain.HeightOneSpectrum.valuation W₁.FunctionField 𝔓 = IsDedekindDomain.HeightOneSpectrum.valuation W₁.FunctionField (WeierstrassCurve.Affine.CoordinateRing.pointPlace h)) : Ideal.map φ.toIntermediateRing (WeierstrassCurve.Affine.CoordinateRing.XYIdeal W₁ x (Polynomial.C y)) = 𝔓.asIdeal

The ideal of a point extends to the prime of the intermediate ring at that point. If the height one prime 𝔓 of the intermediate ring has the valuation of the affine point (x, y) of W₁ — so the point does not lie over O₂ — then ⟨X - x, Y - y⟩ extends to 𝔓 exactly, with no ramification. Every point off the fibre over O₂ has such a prime, by valuation_le_one_of_valuation_pullback_X_le_one and Valuation.existsUnique_heightOneSpectrum_valuation_eq.