The reduction of the generic point

Let W be an elliptic curve over a field F. The generic point (genericX, genericY) is a point of W over its own function field F(W), and every point P of W has a place of F(W), of degree one (WeierstrassCurve.Affine.pointEquivDegreeOnePlace). At that place the generic point reduces to P.

In the language of Affine/Point/DegreeOneReduction.lean, this is the statement that reductionOfDegreeEqOne of the generic point at the place of P is P (WeierstrassCurve.Affine.reductionOfDegreeEqOne_genericPoint). Any F-algebra map τ out of F(W) carries the generic point to the tautological point of τ, and this identity is what the reduction of such points is computed from: an isogeny's action on points in particular.

Transporting a point along a homomorphism of fields f : F →+* K is compatible with places: the place of the transported point restricts along FunctionField.map W f to the place of the point (WeierstrassCurve.Affine.isEquiv_comap_pointPlace_map), so reduction at the two places can be compared.

Main results

• WeierstrassCurve.Affine.valuation_pointPlace_genericX_sub_lt_one and WeierstrassCurve.Affine.valuation_pointPlace_genericY_sub_lt_one: x - a and y - b vanish at the place of (a, b).
• WeierstrassCurve.Affine.reductionOfDegreeEqOne_genericPoint: the generic point reduces to P at the place of P.
• WeierstrassCurve.Affine.isEquiv_comap_pointPlace_map: the place of a point transported along a field homomorphism f restricts along FunctionField.map W f to the place of the point.
• WeierstrassCurve.Affine.map_mem_polePoints_smul_iff and WeierstrassCurve.Affine.reductionOfDegreeEqOne_smul_map: reduction commutes with field automorphisms and their action on places.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.1, VII.2.1.

theorem WeierstrassCurve.Affine.isDedekindDomain_coordinateRing_of_isElliptic {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] : IsDedekindDomain W.CoordinateRing

The coordinate ring of an elliptic curve is a Dedekind domain.

theorem WeierstrassCurve.Affine.valuation_pointPlace_genericX_sub_lt_one {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {x y : F} (h : W.Equation x y) : (TauCeti.Place.ofPrime F W.FunctionField (CoordinateRing.pointPlace h)).valuation (W.genericX - (algebraMap F W.FunctionField) x) < 1

x - a vanishes at the place of (a, b): the class of X - a lies in the point ideal.

theorem WeierstrassCurve.Affine.valuation_pointPlace_genericY_sub_lt_one {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {x y : F} (h : W.Equation x y) : (TauCeti.Place.ofPrime F W.FunctionField (CoordinateRing.pointPlace h)).valuation (W.genericY - (algebraMap F W.FunctionField) y) < 1

y - b vanishes at the place of (a, b): the class of Y - b lies in the point ideal.

theorem WeierstrassCurve.Affine.isEquiv_comap_pointPlace_map {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {K : Type u_2} [Field K] (f : F →+* K) {x y : F} (h : W.Equation x y) : (Valuation.comap (FunctionField.map W f) (TauCeti.Place.ofPrime K (W.map f).FunctionField (CoordinateRing.pointPlace ⋯)).valuation).IsEquiv (TauCeti.Place.ofPrime F W.FunctionField (CoordinateRing.pointPlace h)).valuation

The place of a transported point restricts to the place of the point: along the embedding FunctionField.map W f : F(W) → K(W), the valuation of the place of (f a, f b) restricts to one equivalent to the valuation of the place of (a, b). The restriction is bounded by 1 on the coordinate ring of W and vanishes on x - a and y - b, so its centre is the ideal of (a, b).

theorem WeierstrassCurve.Affine.map_mem_polePoints_smul_iff {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {K : Type u_2} [Field K] [Algebra F K] [DecidableEq K] (σ : Gal(K/F)) (w : TauCeti.Place F K) (A : (toAffine (W.baseChange K)).Point) : (Point.map ↑σ) A ∈ W.polePoints (σ • w) ↔ A ∈ W.polePoints w

An automorphism carries the kernel of reduction at w onto that at σ • w: the x-coordinate of σ A has a pole at σ • w exactly when that of A has one at w.

@[simp]

theorem WeierstrassCurve.Affine.reductionOfDegreeEqOne_smul_map {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {K : Type u_2} [Field K] [Algebra F K] [DecidableEq K] [DecidableEq F] (σ : Gal(K/F)) {w : TauCeti.Place F K} (hw : w.degree = 1) (A : (toAffine (W.baseChange K)).Point) : (W.reductionOfDegreeEqOne ⋯) ((Point.map ↑σ) A) = (W.reductionOfDegreeEqOne hw) A

Reduction commutes with automorphisms: reducing σ A at σ • w is reducing A at w, for a place w of degree one and an automorphism σ of K / F.

@[simp]

theorem WeierstrassCurve.Affine.reductionOfDegreeEqOne_genericPoint {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] [DecidableEq F] (P : W.Point) : (W.reductionOfDegreeEqOne ⋯) W.genericPoint = (Point.equivBaseChangeSelf W) P

The generic point reduces to P at the place of P.