Ideals of points of a Weierstrass curve

For a point (x, y) on an affine Weierstrass curve W over a field, Mathlib's CoordinateRing.XYIdeal W x (C y) is the ideal ⟨X - x, Y - y⟩ of the coordinate ring, and CoordinateRing.quotientXYIdealEquiv identifies the quotient by it with the base field. This file records the consequences: that ideal is maximal, it is nonzero, and it determines the coordinates it was built from. Conversely, every ideal whose quotient has rank one over the base field is the ideal of a point.

The identification of XYIdeal with the kernel of evaluation needs none of that: evaluation kernels identify point ideals over any commutative base ring. Only the maximality results below want a field.

Main results

• WeierstrassCurve.Affine.CoordinateRing.XYIdeal_ne_bot: XYIdeal W x y is nonzero, over any nontrivial commutative base.
• WeierstrassCurve.Affine.CoordinateRing.mk_mem_XYIdeal_iff: a class lies in the ideal of a point exactly when its representative vanishes there.
• WeierstrassCurve.Affine.CoordinateRing.XYIdeal_isMaximal: XYIdeal W x y is maximal for any y : F[X] solving the Weierstrass equation at x, matching the generality of XYIdeal and quotientXYIdealEquiv themselves.
• WeierstrassCurve.Affine.CoordinateRing.XYIdeal_isMaximal_of_equation: the point case, XYIdeal W x (C y) for (x, y) on W.
• WeierstrassCurve.Affine.CoordinateRing.XYIdeal_eq_iff_of_ne_top: two such ideals are equal exactly when x₁ = x₂ and the two Y-polynomials agree at the point, y₁.eval x₁ = y₂.eval x₂, as soon as the first is proper.
• WeierstrassCurve.Affine.CoordinateRing.XYIdeal_eq_iff: the constant-polynomial point case, where the conclusion is equality of the coordinates and properness comes from maximality.
• WeierstrassCurve.Affine.CoordinateRing.finrank_quotient_eq_one_iff: an ideal has a rank-one quotient exactly when it is XYIdeal W x (C y) for a solution (x, y) of the Weierstrass equation.
• WeierstrassCurve.Affine.CoordinateRing.ker_evalAlgHom_eq_XYIdeal: the kernel of evaluation at a point is the ideal of that point.
• WeierstrassCurve.Affine.CoordinateRing.mem_XYIdeal_iff_evalAlgHom_eq_zero: its elementwise form, a function lying in the ideal exactly when it vanishes at the point.

Mathlib has the quotient isomorphism but records nothing about the ideal itself; the many XYIdeal lemmas it does state (XYIdeal_eq₁, XYIdeal_eq₂, XYIdeal_mul_XYIdeal, XYIdeal_neg_mul) are all about products and rewriting, not about the ideal's place in the spectrum. It does record that the two generators are nonzero (XClass_ne_zero, YClass_ne_zero), which is what XYIdeal_ne_bot rests on.

Only the curve equation is needed, not nonsingularity: the quotient is the base field either way.

Evaluation at a point of the curve is an F-algebra map out of the coordinate ring whose kernel is that point's ideal, so a function lies in the ideal exactly when it vanishes at the point. The membership test detects that vanishing and nothing finer — the order of vanishing is a fact about the valuation, not about the ideal — and it is what identifies the residue-degree-one ideals with points below.

This supports TauCetiRoadmap/EllipticCurves/README.md, Layer 0, whose point–place dictionary identifies the affine places of W with the maximal ideals of its coordinate ring — "the affine places are the maximal ideals of the coordinate ring". Maximality of XYIdeal is the direction that sends a point to a place, XYIdeal_eq_iff says that map is injective, and finrank_quotient_eq_one_iff classifies the ideals with residue degree one.

The roadmap's §"What Mathlib already has (consume)" lists Affine.CoordinateRing as consumed infrastructure that "is load-bearing API here, not an implementation detail"; this is a complement to that API, not a reimplementation of it.

Provenance

Ported from the AINTLIB HasseWeil project (github.com/CBirkbeck/AINTLIB, Apache-2.0, pinned by that roadmap at dev/hasse-weil @ 513e83879e2f), HasseWeil/Curves/Basic.lean, declaration maximalIdealAt_isMaximal. The two XYIdeal_eq_iff lemmas are not in the source.

Changes from the source. There the ideal is reached through a SmoothPlaneCurve structure wrapping WeierstrassCurve.Affine and a SmoothPoint structure bundling the coordinates with their nonsingularity proof; the surrounding wrappers are not ported, and the statement is made directly about Mathlib's XYIdeal. The hypothesis is correspondingly weakened from nonsingularity to the curve equation, which is all the quotient isomorphism consumes.

The classification has a counterpart in the same project, in projects/HasseWeil/HasseWeil/Foundation/Curves/Valuation/NormValuation.lean at github.com/CBirkbeck/AINTLIB @ 1c1c74664e40 (Apache-2.0 per that file's header; Authors: Chris Birkbeck): exists_coordinates_of_isMaximal_of_surjective, equation_of_coordinates_of_field and exists_smoothPoint_of_isMaximal_of_surjective, packaged in Valuation/SmoothPointPrime.lean as smoothPointEquivHeightOneSpectrum. That statement is about a maximal ideal of the coordinate ring of a SmoothPlaneCurve, hypothesises surjectivity of algebraMap F (F[C] ⧸ M), and assumes ellipticity throughout. The classification below is written directly against Mathlib's XYIdeal: its hypothesis is the residue degree and it uses no ellipticity or Dedekind assumption.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_ne_bot {R : Type u_1} [CommRing R] [Nontrivial R] {W : Affine R} (x : R) (y : Polynomial R) : XYIdeal W x y ≠ ⊥

The ideal ⟨X - x, Y - y(X)⟩ of the coordinate ring is nonzero over a nontrivial base.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.ker_evalAlgHom_eq_XYIdeal {R : Type u_2} [CommRing R] {W : Affine R} {x y : R} (h : (toAffine (W.baseChange R)).Equation x y) : RingHom.ker ↑(evalAlgHom h) = XYIdeal W x (Polynomial.C y)

The kernel of evaluation at a point is the ideal of that point. The evaluation map W.CoordinateRing →ₐ[R] R at a solution (x, y) of the Weierstrass equation has kernel ⟨X - x, Y - y⟩.

theorem WeierstrassCurve.Affine.CoordinateRing.mem_XYIdeal_iff_evalAlgHom_eq_zero {R : Type u_2} [CommRing R] {W : Affine R} {x y : R} (h : (toAffine (W.baseChange R)).Equation x y) {f : W.CoordinateRing} : f ∈ XYIdeal W x (Polynomial.C y) ↔ (evalAlgHom h) f = 0

A function lies in the ideal of a point exactly when it vanishes there, the elementwise form of ker_evalAlgHom_eq_XYIdeal.

Not @[simp]: AlgHom.toRingHom_eq_coe rewrites the left-hand side of the kernel equality this rests on, and simpNF rejects the pair.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.mk_mem_XYIdeal_iff {R : Type u_1} [CommRing R] {W : Affine R} {x y : R} (h : W.Equation x y) (p : Polynomial (Polynomial R)) : (mk W) p ∈ XYIdeal W x (Polynomial.C y) ↔ Polynomial.evalEval x y p = 0

A class lies in the ideal of a point exactly when its representative vanishes there. The ideal ⟨X - x, Y - y⟩ collects the classes of the polynomials that vanish at (x, y).

theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_isMaximal {F : Type u_1} [Field F] {W : Affine F} {x : F} {y : Polynomial F} (h : Polynomial.eval x (Polynomial.eval y W.polynomial) = 0) : (XYIdeal W x y).IsMaximal

The ideal ⟨X - x, Y - y(X)⟩ of the coordinate ring is maximal whenever y is a polynomial solving the Weierstrass equation at x. Equivalently, the quotient by it is the base field.

theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_isMaximal_of_equation {F : Type u_1} [Field F] {W : Affine F} {x y : F} (h : W.Equation x y) : (XYIdeal W x (Polynomial.C y)).IsMaximal

The ideal of a point of a Weierstrass curve is maximal, the constant-polynomial case of XYIdeal_isMaximal.

theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_eq_iff_of_ne_top {F : Type u_1} [Field F] {W : Affine F} {x₁ x₂ : F} {y₁ y₂ : Polynomial F} (hI : XYIdeal W x₁ y₁ ≠ ⊤) : XYIdeal W x₁ y₁ = XYIdeal W x₂ y₂ ↔ x₁ = x₂ ∧ Polynomial.eval x₁ y₁ = Polynomial.eval x₂ y₂

Two such ideals are equal exactly when their data agree at the point, given only that the first is proper: the X-coordinates must coincide, and the two Y-polynomials must take the same value there. Stated for polynomial y, matching XYIdeal and XYIdeal_isMaximal; no curve equation is needed. Use XYIdeal_eq_iff for points, whose properness is automatic.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_eq_iff {F : Type u_1} [Field F] {W : Affine F} {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) : XYIdeal W x₁ (Polynomial.C y₁) = XYIdeal W x₂ (Polynomial.C y₂) ↔ x₁ = x₂ ∧ y₁ = y₂

The ideal of a point determines the point: for points of the curve, equality of the ideals ⟨X - x, Y - y⟩ is equality of the coordinates, so fun (x, y) ↦ XYIdeal W x (C y) is injective on points. The point case of XYIdeal_eq_iff_of_ne_top, whose properness comes from XYIdeal_isMaximal_of_equation.

theorem WeierstrassCurve.Affine.CoordinateRing.finrank_quotient_eq_one_iff {F : Type u_1} [Field F] {W : Affine F} {I : Ideal W.CoordinateRing} : Module.finrank F (W.CoordinateRing ⧸ I) = 1 ↔ ∃ (x : F) (y : F), W.Equation x y ∧ I = XYIdeal W x (Polynomial.C y)

The ideals of residue degree one are exactly the ideals of points. An ideal I has a rank-one quotient over F if and only if it is XYIdeal W x (C y) for some solution (x, y) of the Weierstrass equation. No ellipticity or Dedekind hypothesis is involved.