The points with a pole at a place form a subgroup

Let W be an elliptic curve over F, let K be a field extension of F and let P be a place of K / F. A point of W over K either has both coordinates in the valuation ring of P or has a pole of x there (Affine/ValuationIntegrality.lean). This file shows that the points with a pole, together with the point at infinity, form a subgroup of W(K). These are the K-points lying in the kernel E₁(K_P) of reduction at P on the completion K_P (Silverman VII.2.2); no reduction map is constructed here, the subgroup being cut out by the valuation of the x-coordinate alone (at a place of degree one, Affine/Point/DegreeOneReduction.lean builds one from it).

The group law on the points of an affine Weierstrass curve depends definitionally on the chosen DecidableEq K, so that instance is a parameter of every declaration here rather than being fixed classically: the statements apply to the point operations of whatever instance is in context, in particular to the function field of a curve with its own.

Main definitions

• WeierstrassCurve.Affine.polePoints: the subgroup of W(K) of points whose x-coordinate has a pole at P, together with the point at infinity.

Main results

• WeierstrassCurve.Affine.one_lt_valuation_xCoord_add: a pole of x at P is preserved by addition of points, as long as the sum is not the point at infinity.
• WeierstrassCurve.Affine.mem_polePoints_iff: membership in polePoints.
• WeierstrassCurve.Affine.baseChange_mem_polePoints_iff: a point of W over F lies in polePoints only if it is the point at infinity, so a point of W over K is congruent to at most one point of W over F modulo polePoints (eq_of_sub_mem_polePoints).

References

• J. Silverman, The Arithmetic of Elliptic Curves, VII.2.2.

Provenance

Built on WeierstrassCurve.range_formalPointHomAdicCompletion (FormalGroup/Point/Range.lean, adapted there from Michael Stoll's EllipticCurves development) and TauCeti.Place.center (FieldTheory/FunctionField/AffineModel/Place.lean).

theorem WeierstrassCurve.Affine.one_lt_valuation_xCoord_add {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] [DecidableEq K] (W : Affine F) [WeierstrassCurve.IsElliptic W] (P : TauCeti.Place F K) {Q₁ Q₂ : (toAffine (W.baseChange K)).Point} (h₁ : 1 < P.valuation Q₁.xCoord) (h₂ : 1 < P.valuation Q₂.xCoord) (h : Q₁ + Q₂ ≠ 0) : 1 < P.valuation (Q₁ + Q₂).xCoord

A pole of x at a place is preserved by addition of points. If the x-coordinates of two points of W over K both have a pole at the place P, and the points do not cancel, then the x-coordinate of their sum has a pole at P too.

def WeierstrassCurve.Affine.polePoints {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] [DecidableEq K] (W : Affine F) [WeierstrassCurve.IsElliptic W] (P : TauCeti.Place F K) : AddSubgroup (toAffine (W.baseChange K)).Point

The points with a pole at P, together with the point at infinity, as a subgroup of W(K): the K-points lying in the kernel E₁(K_P) of reduction at P on the completion.

Equations

• W.polePoints P = { carrier := {Q : (WeierstrassCurve.toAffine (W.baseChange K)).Point | Q = 0 ∨ 1 < P.valuation Q.xCoord}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem WeierstrassCurve.Affine.mem_polePoints_iff {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] [DecidableEq K] (W : Affine F) [WeierstrassCurve.IsElliptic W] (P : TauCeti.Place F K) (Q : (toAffine (W.baseChange K)).Point) : Q ∈ W.polePoints P ↔ Q = 0 ∨ 1 < P.valuation Q.xCoord

A point lies in polePoints when it is the point at infinity or its x-coordinate has a pole at P.

theorem WeierstrassCurve.Affine.baseChange_mem_polePoints_iff {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] [DecidableEq K] (W : Affine F) [WeierstrassCurve.IsElliptic W] [DecidableEq F] (P : TauCeti.Place F K) (Q : (toAffine (W.baseChange F)).Point) : (Point.baseChange F K) Q ∈ W.polePoints P ↔ Q = 0

A point of W over F lies in the kernel of reduction only if it is the point at infinity: the x-coordinate of a constant point has no pole.

theorem WeierstrassCurve.Affine.eq_of_sub_mem_polePoints {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] [DecidableEq K] (W : Affine F) [WeierstrassCurve.IsElliptic W] [DecidableEq F] (P : TauCeti.Place F K) {A : (toAffine (W.baseChange K)).Point} {Q Q' : (toAffine (W.baseChange F)).Point} (hQ : A - (Point.baseChange F K) Q ∈ W.polePoints P) (hQ' : A - (Point.baseChange F K) Q' ∈ W.polePoints P) : Q = Q'

A point is congruent to at most one point of W over F modulo the kernel of reduction.