Reduction of points modulo a prime of the base ring #
Source: MichaelStollBayreuth/EllipticCurves at commit 3f8c39c0fc4c0fd0a40e693aa2a9bbda08d9ee1f.
Exact-pin changes are documented in PORTING.md.
Let E be an elliptic curve over the fraction field K of a Dedekind domain R, let v be a
maximal ideal (height-one prime) of R, and let W₀ be an integral model of E over R
(hE : W₀.map (algebraMap R K) = E) whose reduction modulo v is again elliptic — good
reduction at v, the instance hypothesis [(redCurve v W₀).IsElliptic]. This file defines the
reduced curve redCurve v W₀ over the residue field R ⧸ v.asIdeal and the reduction
homomorphism redHom v hE : E(K) →+ E_red(R ⧸ v.asIdeal) — a point with v-integral coordinates
maps to their residues (via residueHom v), a point with a pole at v maps to 0 — with no
completions in the definitions or statements.
The completion K_v enters only through proofs: adicRed_pointMap identifies red v hE with
the reduction map adicRed of the base-changed curve over K_v (where the formal-group
machinery of EllipticCurves.WeierstrassFormalGroup lives), and additivity, injectivity on
torsion, and preservation of the order of torsion points are transported back along it.
Main definitions and statements #
WeierstrassCurve.Affine.redCurve: the reductionE_redofW₀modulov, a Weierstrass curve overR ⧸ v.asIdeal.WeierstrassCurve.Affine.red,WeierstrassCurve.Affine.redHom: the reduction mapE(K) →+ E_red(R ⧸ v.asIdeal).WeierstrassCurve.Affine.nsmul_eq_zero_of_red_nsmul_eq_zero: if the reduction of a torsion point ism-torsion, so is the point itself — under the standard ramification condition on the residue characteristicp, namely(p : R) ∈ v.asIdealand(p : R) ∉ v.asIdeal ^ (p - 1)(that is,e ≤ p - 2for the ramification indexe, e.g.podd andvunramified).WeierstrassCurve.Affine.addOrderOf_red: under the same condition, reduction preserves the order of a torsion point.WeierstrassCurve.Affine.addOrderOf_dvd_natCard_red: consequently, the order of a torsion point divides the number of points of the reduction.
The reduction E_red of the integral model W₀ modulo the prime v, a Weierstrass curve over
the residue field R ⧸ v.asIdeal: the base change of W₀ along
algebraMap R (R ⧸ v.asIdeal) = Ideal.Quotient.mk v.asIdeal. Good reduction of W₀ at v
is the instance hypothesis [(redCurve v W₀).IsElliptic].
Equations
- WeierstrassCurve.Affine.redCurve v W₀ = WeierstrassCurve.toAffine (W₀.toAffine.baseChange (R ⧸ v.asIdeal))
Instances For
The reduction map, defined over K #
The definition of red needs three facts about a point of E(K) with v-integral
x-coordinate: its y-coordinate is v-integral, the residues of its coordinates satisfy the
reduced Weierstrass equation, and (under good reduction) they are a nonsingular point of E_red.
The first is transported from the completion (integral_of_not_mem); the others are proved
directly from residueHom.
The base change to 𝒪_v of an integral model of E over R is an integral model of the
base change of E to K_v.
The y-coordinate of a point of E(K) whose x-coordinate is v-integral is itself
v-integral.
The residues of the coordinates of a v-integral point of E(K) satisfy the reduced
Weierstrass equation.
Under good reduction, the residues of the coordinates of a v-integral point of E(K) are
a nonsingular point of the reduced curve.
The reduction map E(K) → E_red(R ⧸ v.asIdeal) at the prime v, for an integral model W₀
of E over R with good reduction at v: a point with v-integral coordinates reduces
coordinatewise (via residueHom v), and a point with a pole at v (the kernel of reduction)
maps to the point at infinity.
Equations
- One or more equations did not get rendered due to their size.
- WeierstrassCurve.Affine.red v hE WeierstrassCurve.Affine.Point.zero = 0
Instances For
Unfolding lemma for red at a v-integral point.
Unfolding lemma for red at a point with a pole at v.
Transport from the completion #
The following identifies red v hE with the reduction map adicRed of the base-changed curve
over the completion K_v, along the base change of points E(K) → E(K_v) and the residue field
isomorphism R ⧸ v.asIdeal ≃+* 𝒪_v ⧸ 𝔪_v. All group-theoretic properties of red follow.
The group structures on the point sets require decidable equality of the base fields
([DecidableEq K], [DecidableEq (R ⧸ v.asIdeal)] in the public statements); the corresponding
instances on the completion and its residue field appear only in private lemmas and are
discharged with classical in the proofs of the public ones.
The R-algebra structure on the residue field of the completed valuation ring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The algebra structure induced by the residue-field equivalence from R ⧸ v.asIdeal.
Equations
Instances For
The reduction homomorphism and its behaviour on torsion #
The reduction map is additive.
The reduction homomorphism E(K) →+ E_red(R ⧸ v.asIdeal) at a prime v of good
reduction.
Equations
Instances For
Reduction is injective on torsion: a torsion point of E(K) reducing to 0 at a prime
v of good reduction is 0, provided the residue characteristic p satisfies
(p : R) ∈ v.asIdeal and (p : R) ∉ v.asIdeal ^ (p - 1) — that is, e ≤ p - 2 for the
ramification index e of v over p (e.g. p odd and v unramified).
If the reduction at a good prime v of a torsion point is annihilated by m, then so is
the point itself (hypotheses on the residue characteristic as in
eq_zero_of_isOfFinAddOrder_of_red_eq_zero).
Reduction preserves the order of a torsion point (hypotheses on the residue
characteristic as in eq_zero_of_isOfFinAddOrder_of_red_eq_zero).
The order of a torsion point of E(K) divides the number of points of the reduction at a
good prime v (hypotheses on the residue characteristic as in
eq_zero_of_isOfFinAddOrder_of_red_eq_zero). This is nontrivial only when the residue field
is finite, which makes E_red(R ⧸ v.asIdeal) a finite group.