The points of a Weierstrass curve are the degree-zero divisor classes of its function field

The coordinate ring of an affine Weierstrass curve is an affine model of its function field whose only place at infinity is TauCeti.Place.infinity, and that place is rational. The general affine-model bridge therefore identifies the ideal class group of the coordinate ring with the degree-zero divisor class group of the function field. Composing with the identification of the points with that ideal class group gives the points as degree-zero divisor classes.

Main results

• WeierstrassCurve.Affine.setOf_exists_notMem_integers_eq_singleton_infinity: the same fact as an equality of sets, which is the shape Divisor.degreeZeroClassGroupEquiv consumes.
• WeierstrassCurve.Affine.pointEquivDegreeZeroDivisorClass: the points of W are the degree-zero divisor classes of F(W).
• WeierstrassCurve.Affine.val_pointEquivDegreeZeroDivisorClass_some: that equivalence sends an affine point P to the class of (P) - (O).

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.3.4.
• H. Stichtenoth, Algebraic Function Fields and Codes, I.4.

theorem WeierstrassCurve.Affine.setOf_exists_notMem_integers_eq_singleton_infinity {F : Type u_1} [Field F] (W : Affine F) [IsDedekindDomain W.CoordinateRing] : {Q : TauCeti.Place F W.FunctionField | ∃ (r : W.CoordinateRing), (algebraMap W.CoordinateRing W.FunctionField) r ∉ Q.integers} = {TauCeti.Place.infinity W}

The place at infinity is the only place infinite on the coordinate ring, as an equality of sets.

@[simp]

theorem WeierstrassCurve.Affine.classGroupMk_pointPlace {F : Type u_1} [Field F] (W : Affine F) [IsDedekindDomain W.CoordinateRing] {x y : F} (h : W.Nonsingular x y) : (CoordinateRing.pointPlace ⋯).classGroupMk = (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)

The ideal class of a point's place is the class Mathlib's toClass takes. The place of a point has the point's ideal ⟨X - x, Y - y⟩ underneath it, and XYIdeal' is that ideal as an invertible fractional ideal.

theorem WeierstrassCurve.Affine.degreeClass_divisorClass_pointPlace_sub_infinity {F : Type u_1} [Field F] (W : Affine F) [IsDedekindDomain W.CoordinateRing] {x y : F} (h : W.Equation x y) : (TauCeti.Divisor.degreeClass ⋯) ((TauCeti.Place.orderSystem ⋯).divisorClass (TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint (TauCeti.Place.ofPrime F W.FunctionField (CoordinateRing.pointPlace h)) - TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint (TauCeti.Place.infinity W))) = 0

The class of (P) - (O) has degree zero: both places are rational.

noncomputable def WeierstrassCurve.Affine.pointEquivDegreeZeroDivisorClass {F : Type u_1} [Field F] (W : Affine F) [IsDedekindDomain W.CoordinateRing] [DecidableEq F] : W.Point ≃+ ↥(TauCeti.Divisor.degreeClass ⋯).ker

The points of W are the degree-zero divisor classes of F(W). The point at infinity is the trivial class and an affine point P is the class of (P) - (O).

Equations

• W.pointEquivDegreeZeroDivisorClass = WeierstrassCurve.Affine.Point.toClassEquiv.trans (TauCeti.Divisor.degreeZeroClassGroupEquiv W.CoordinateRing ⋯ ⋯ ⋯).symm

@[simp]

theorem WeierstrassCurve.Affine.val_pointEquivDegreeZeroDivisorClass_some {F : Type u_1} [Field F] (W : Affine F) [IsDedekindDomain W.CoordinateRing] [DecidableEq F] {x y : F} (h : W.Nonsingular x y) : ↑(W.pointEquivDegreeZeroDivisorClass (Point.some x y h)) = (TauCeti.Place.orderSystem ⋯).divisorClass (TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint (TauCeti.Place.ofPrime F W.FunctionField (CoordinateRing.pointPlace ⋯)) - TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint (TauCeti.Place.infinity W))

An affine point goes to the class of (P) - (O). This is the computation rule for pointEquivDegreeZeroDivisorClass, whose value is otherwise opaque.