Reduction of points at a place of degree one #
Let W be an elliptic curve over F, let K be a field extension of F and let w be a place
of K / F. The points of W over K with a pole of x at w, together with the point at
infinity, form the subgroup polePoints W w (Affine/Point/PolePoints.lean), the kernel of
reduction at w. This file identifies that kernel in coordinates, and uses it to build the
reduction map when w has degree one.
The coordinate criterion is some_sub_baseChange_mem_polePoints_iff: for an affine point
A = (x₁, y₁) of W over K and an affine point (a, b) of W over F, the difference
A - (a, b) lies in the kernel of reduction exactly when x₁ ≡ a and y₁ ≡ b modulo w. The
subtraction is computed by the chord through A and -(a, b), whose x-coordinate is
λ² + a₁λ - a₂ - x₁ - a; this has a pole exactly when the slope λ does, and the chord identity
(y₁ - b') (y₁ + b' + a₁ x₁ + a₃) = (x₁ - a) M (Affine/Formula/Chord.lean), with b' the
y-coordinate of -(a, b) and M integral, shows that λ has a pole exactly when A is
congruent to (a, b).
The residues (a, b) of the coordinates of an integral point of W over K satisfy the equation
of W, the defect of that equation at (a, b) being a constant congruent to 0
(nonsingular_of_valuation_sub_lt_one). When w has degree one its residue field is F, so
every integral point of W over K is congruent to a point of W over F
(exists_sub_mem_polePoints). That point is unique, since a nonzero constant affine point has
no pole (eq_of_sub_mem_polePoints, in Affine/Point/PolePoints.lean). So every point A has
a unique reduction Q ∈ W(F) with A - Q ∈ polePoints W w, and A ↦ Q is additive because
polePoints W w is a subgroup.
This is the reduction map W(K) → W(F) of Silverman VII.2.1, at a place whose residue field is
the base field. WeierstrassCurve.Affine.Point.reduction (Affine/Point/Reduction.lean) reduces
modulo an arbitrary valuation into the projective plane over the residue field; at a place of
degree one it sends A to the projective class of the reduction here, read through
TauCeti.Place.residueFieldEquivOfDegreeEqOne.
Main definitions #
WeierstrassCurve.Affine.reductionOfDegreeEqOne: the reductionW(K) →+ W(F)at a place of degree one.
Main results #
WeierstrassCurve.Affine.nonsingular_of_valuation_sub_lt_one: the residues of the coordinates of a point ofWoverKform a point ofWoverF.WeierstrassCurve.Affine.some_sub_baseChange_mem_polePoints_iff:A - (a, b)lies in the kernel of reduction exactly when both coordinates ofAare congruent to those of(a, b).WeierstrassCurve.Affine.exists_sub_mem_polePoints: at a place of degree one, every point ofWoverKis congruent to a point ofWoverF.WeierstrassCurve.Affine.reductionOfDegreeEqOne_eq_iff: the reduction ofAis the unique pointQofWoverFwithA - Qin the kernel of reduction.WeierstrassCurve.Affine.reductionOfDegreeEqOne_some: an integral affine point reduces to the residues of its coordinates.WeierstrassCurve.Affine.ker_reductionOfDegreeEqOne: the kernel of the reduction map ispolePoints W w.
References #
- J. Silverman, The Arithmetic of Elliptic Curves, VII.2.1, VII.2.2.
The residues of the coordinates of a point of W over K form a point of W over F.
If (x, y) lies on W over K and x ≡ a, y ≡ b modulo w for constants a, b : F, then
(a, b) is a nonsingular point of W: the defect of the equation of W at (a, b) is a
constant congruent to 0, hence 0.
A point minus a point of W over F lies in the kernel of reduction exactly when it reduces
to that point. For a place w of K / F, an affine point (x₁, y₁) of W over K and an
affine point (a, b) of W over F, the difference (x₁, y₁) - (a, b) is the point at infinity
or has x-coordinate with a pole at w exactly when x₁ ≡ a and y₁ ≡ b modulo w.
Every point reduces to a point of W over F at a place of degree one. For a place w of
K / F with residue field F, every point of W over K differs from a point of W over F by
an element of the kernel of reduction.
The reduction of points at a place of degree one: each point of W over K goes to the
unique point of W over F it is congruent to modulo the kernel of reduction. It is additive
because that kernel is a subgroup.
Equations
- W.reductionOfDegreeEqOne hw = { toFun := fun (A : (WeierstrassCurve.toAffine (W.baseChange K)).Point) => ⋯.choose, map_zero' := ⋯, map_add' := ⋯ }
Instances For
A point is congruent to its reduction modulo the kernel of reduction.
The reduction of A is the unique point Q of W over F with A - Q in the kernel of
reduction.
An integral affine point reduces to the residues of its coordinates: if x ≡ a and
y ≡ b modulo w, then (x, y) reduces to (a, b).
Reduction fixes the points of W over F.
The kernel of the reduction map is the kernel of reduction polePoints W w.