Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.Affine.Point.ToClass

Surjectivity of Point.toClass #

Mathlib builds WeierstrassCurve.Affine.Point.toClass : W.Point →+ Additive (ClassGroup W.CoordinateRing) and proves it injective, realising the points of an affine Weierstrass curve as a subgroup of the affine ideal class group. It does not prove surjectivity; this file proves it by an explicit genus-one Riemann--Roch argument in the affine coordinate ring.

It first records what surjectivity amounts to: every ideal class is trivial or the class of an XYIdeal' at a nonsingular affine point. It then proves that statement.

Main results #

What this is, mathematically #

The right-hand side is stated for an arbitrary affine Weierstrass curve; nothing here assumes smoothness or ellipticity, and no divisor group occurs.

On a smooth genus-1 curve, and under the identification of the affine ideal class group with degree-zero divisor classes, it becomes the familiar divisor-reduction statement — every such class is (P) - (O) for a rational point P. That is the reading which motivates recording the equivalence, since it turns "prove toClass is surjective" into the form the geometric proof takes; but it is an interpretation under extra hypotheses, not the content of the statement.

The formal equivalence and its proof carry no ellipticity hypothesis. In particular, the subsequent proof shows that the required invertible ideals cannot occur at singular equation solutions. No named representability predicate is introduced because Function.Surjective already names the property consumers need.

Provenance #

Ported from the AINTLIB HasseWeil project (github.com/CBirkbeck/AINTLIB, Apache-2.0) at the roadmap's HasseWeil pin dev/hasse-weil @ 513e83879e2f, file HasseWeil/Pic0/ToClassSurjective.lean (by Chris Birkbeck). The source states the equivalence through a named ClassRepresentableByPoints predicate, with the two directions as toClass_surjective_of_classRepresentableByPoints and classRepresentableByPoints_of_toClass_surjective; here they are one iff with the disjunction spelled out, so no name is carried over.

The proof ports the source's concrete Riemann--Roch argument while reusing Tau Ceti's existing CoordinateRing.finrank_quotient_eq_one_iff in place of the source's duplicate codimension-one classification.

The mathematical argument is the affine ideal-class construction of Silverman, The Arithmetic of Elliptic Curves, III.3.4--5.

Point.toClass_surjective and toClassEquiv are also components of D. Angdinata's in-flight upstream CoordinateRing split-out, which TauCetiRoadmap/EllipticCurves/README.md:1095 lists at this same hypothesis strength — that bullet's "no ellipticity hypothesis" phrase describes his split-out, not the AINTLIB source above, whose headline surjectivity theorem is elliptic. ⚠ mathlib-track: dedupe on landing.

The genus-one codimension argument #

Surjectivity and the class-group equivalence #

source
theorem WeierstrassCurve.Affine.Point.toClass_surjective_iff {F : Type u_1} [Field F] {W : Affine F} [DecidableEq F] :
Function.Surjective ⇑toClass ↔ ∀ (g : ClassGroup W.CoordinateRing), g = 1 ∨ ∃ (x : F) (y : F) (h : W.Nonsingular x y), g = (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)

Surjectivity of toClass is exactly representability of every ideal class by a point.

toClass is surjective precisely when each element of ClassGroup W.CoordinateRing is either trivial or the class of XYIdeal' h for a nonsingular affine point (x, y). The right-hand side is proved below in toClass_surjective.

Stated for an arbitrary affine Weierstrass curve: neither smoothness nor ellipticity is assumed, and no divisor group appears. Under the hypotheses that make W a smooth genus-1 curve, and the identification of ClassGroup W.CoordinateRing with degree-zero divisor classes, the right-hand side reads as the familiar statement that every such class is (P) - (O) for a rational point P — but that reading is an interpretation under extra hypotheses, not part of what is stated here.

The disjunction is spelled out rather than named: Function.Surjective already expresses the left-hand side, so a separate predicate would only add an unfolding layer for consumers to cross.

source
theorem WeierstrassCurve.Affine.Point.toClass_surjective {F : Type u_1} [Field F] {W : Affine F} [DecidableEq F] :
Function.Surjective ⇑toClass

The point-to-class map is surjective. Equivalently, every ideal class of its affine coordinate ring is represented by a rational point.

source
noncomputable def WeierstrassCurve.Affine.Point.toClassEquiv {F : Type u_1} [Field F] {W : Affine F} [DecidableEq F] :
W.Point ≃+ Additive (ClassGroup W.CoordinateRing)

The points are their affine ideal class group.

Equations
Instances For
    source
    @[simp]
    theorem WeierstrassCurve.Affine.Point.toClassEquiv_apply {F : Type u_1} [Field F] {W : Affine F} [DecidableEq F] (P : W.Point) :
    toClassEquiv P = toClass P

    The point-to-class equivalence has underlying map Point.toClass.

    The class of an affine point as an integral ideal #

    source
    theorem WeierstrassCurve.Affine.Point.toClass_some_eq_ofMul_mk0 {F : Type u_1} [Field F] {W : Affine F} [DecidableEq F] [IsDedekindDomain W.CoordinateRing] {x y : F} (h : W.Nonsingular x y) :
    toClass (some x y h) = Additive.ofMul (ClassGroup.mk0 ⟨CoordinateRing.XYIdeal W x (Polynomial.C y), ⋯⟩)

    The class of an affine point is the class of its integral ideal ⟨X - x, Y - y⟩, when the coordinate ring is a Dedekind domain. Mathlib's toClass_some states it through the invertible fractional ideal XYIdeal'; this is the form in which class-group maps defined on integral ideals, such as a relative norm, are evaluated.