The x - T map of an elliptic curve into its étale algebra #
Let W : y² = f(x) = x³ + a₂x² + a₄x + a₆ be an elliptic curve in characteristic ≠ 2 normal
form over a field K, and let A := K[X]⧸⟨f⟩ be the étale algebra of f. The descent map,
or x - T map, sends a point of W to the square class of x - T in A, where T is the
class of X. It is the engine of the descent computing E(K)/2E(K): its kernel is exactly
2E(K), so E(K)/2E(K) embeds into a group of square classes, which is finite under the
finiteness hypotheses of the weak Mordell-Weil theorem.
The subtlety is at the 2-torsion. If f x ≠ 0 then x - T is already a unit of A, but at a
root x of f the element x - T is a zero divisor, and the map instead returns the class of
the corrected representative x - T + fCofactor x. Adding fCofactor x changes nothing modulo
fCofactor x, where the element still agrees with x - T; at the remaining factor, where
x - T vanishes, it takes the value f' x, which is nonzero because f is separable. That is
what makes the corrected element a unit. Both branches are packaged in μX, and μ₀ extends
μX by sending the point at infinity to 1.
Main definitions #
WeierstrassCurve.Affine.μX,WeierstrassCurve.Affine.μ₀: thex - Tmap, first onx-coordinates and then on points, as a plain function.WeierstrassCurve.Affine.μ: the same map upgraded to a group homomorphismMultiplicative W.Point →* W.M.
Main results #
WeierstrassCurve.Affine.μ₀_mul_mul_eq_one_of_add_add_eq_zero: the square classes of three collinear points multiply to1. This is the substance of the file, and the multiplicativity that makesμa homomorphism; it is proved by exhibiting an explicit square root in each of the ways the three points can meet the2-torsion.WeierstrassCurve.Affine.exists_eq_two_smul_iff: a point is divisible by2exactly when an explicit polynomial identity has a solution. This is the bridge from thex - Tmap to the kernel computation below.WeierstrassCurve.Affine.ker_μ_eq: the kernel ofμis exactly2 • W(K). This is the injectivity half of the descent, and the reasonW(K)/2W(K)embeds intoW.M. A point in the kernel is exhibited as2 • Pby solving the identity ofexists_eq_two_smul_ifffrom a square root ofx - T, in two cases according to whether thex-coordinate is a root off; the point-wise statement isWeierstrassCurve.Affine.eq_two_smul_of_μ_eq_one.WeierstrassCurve.Affine.normM,WeierstrassCurve.Affine.range_μ_le_ker_normM: the norm map on square classes, and the norm condition on the image of the descent map — every square class in the image ofμhas square norm. This is what the2-descent tests a class against.WeierstrassCurve.Affine.norm_mk_C_sub_X_add_fCofactor: at a root off, the corrected representativex - T + fCofactor xhas norm(f' x) ^ 2. This is the value the norm condition on the image of the descent map is read off from at the2-torsion.
WeierstrassCurve.Affine.A is the étale algebra and WeierstrassCurve.Affine.M its group of
square classes of units; M is spelled as a quotient of W.Aˣ by the range of Mathlib's
powMonoidHom 2, which is the same spelling that TauCeti/GroupTheory/Finiteness.lean already
uses for square classes.
Namespace #
These declarations extend Mathlib's own WeierstrassCurve.Affine namespace rather than sitting
under TauCeti. That is forced by dot notation: Affine is a reducible abbreviation for
WeierstrassCurve, so W.f is resolved by a direct lookup on the structure's namespace and a
TauCeti.-prefixed copy is never found. Writing f W throughout instead would diverge from the
source for no gain. TauCeti/RingTheory/AdjoinRoot/Basic.lean sets the same precedent for a file
whose whole content extends a Mathlib namespace.
Provenance #
Adapted, with the author's proofs, from Michael Stoll's EllipticCurves project
(github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, revision 66889eada51a),
EllipticCurves/WeakMordellWeil.lean lines 60-798, which are that file's Steps 2 and 3,
the divisibility criterion opening its Step 4, and Step 4 itself — the kernel computation.
The source is written against Lean v4.32.0; this is a forward port.
Two changes were made against the source. Stoll defines the square classes through a local
abbreviation Units.modPow; here they are the quotient by (powMonoidHom 2).range directly, so
that TauCeti carries a single spelling of square classes. In the kernel proofs this replaces the
source's Units.modPow.unit_eq_one_iff step by
TauCeti.powMonoidHom_range_mk_eq_one_iff_exists_pow, which says
the same thing about this spelling, for any commutative monoid. norm_mk_C_sub_X_add_fCofactor
is the source's Step 5 opening, WeakMordellWeil.lean lines 284-313, specialised here from the
general AdjoinRoot.norm_mk_C_sub_X_add, which carries that attribution. The rest of that step —
the induced norm map on square classes and the containment of the image of μ in its kernel — is
WeakMordellWeil.lean lines 873-919. It is adapted rather than copied: Stoll builds the map as
Units.modPow.map (Algebra.norm K) 2 through his local square-class abbreviation, and the single
spelling this repo carries makes it a QuotientGroup.map into Kˣ ⧸ (powMonoidHom 2).range
instead.
Commutative-ring and polynomial identities #
These encode the multiplicativity of the x - T map on the level of coordinates, and are used
only in the proof that μ is a homomorphism. The polynomial ones are sign normalisations: the
representatives are naturally written C x - X, while f factors into X - C x, and each
rewriting step below turns one into the other.
The polynomial on the right hand side of a Weierstrass equation with a₁ = a₃ = 0.
Defined over a commutative ring: it is a polynomial in the coefficients and uses nothing about
R beyond its ring structure. The descent constructions below specialise it to a field.
Equations
- W.f = Polynomial.X ^ 3 + Polynomial.C W.a₂ * Polynomial.X ^ 2 + Polynomial.C W.a₄ * Polynomial.X + Polynomial.C W.a₆
Instances For
The synthetic cofactor of f at x, defined for every x by the coefficients of synthetic
division: it satisfies fCofactor x * (X - C x) = f - C (f.eval x) (fCofactor_mul_eq). It is
the quotient of f by X - x exactly when x is a root of f, which is the case
f_eq_mul_of_eval_eq_zero records.
Equations
- W.fCofactor x = Polynomial.X ^ 2 + Polynomial.C (x + W.a₂) * Polynomial.X + Polynomial.C (x ^ 2 + W.a₂ * x + W.a₄)
Instances For
The derivative of f. Its values at the roots of f are what makes the corrected
representative a unit; see deriv_f_ne_zero.
In a normal form for characteristic ≠ 2, the negation involution on y-coordinates is
y ↦ -y.
Not a simp lemma: the default simp set already reduces negY through the normal-form
values of a₁ and a₃.
At a point of W, a nonzero value of f x forces the y-coordinate to be nonzero.
The norm at the 2-torsion #
At a root x of f the descent map uses the corrected representative x - T + fCofactor x, and
the norm condition on the image of the map is read off from its norm, which is a square. The
computation is AdjoinRoot.norm_mk_C_sub_X_add, stated there for any monic polynomial split off
a linear factor; here it is specialised to f = fCofactor x * (X - C x). The other value the
condition needs, the norm of x - T itself on the branch where that is already a unit, is
AdjoinRoot.norm_algebraMap_sub_root W.monic_f x.
At a root of f, the corrected representative x - T + fCofactor x has norm
(f' x) ^ 2, where f' x = 3 * x ^ 2 + 2 * a₂ * x + a₄. This coefficient identity holds
without a normal-form or ellipticity hypothesis. Over a field, deriv_f_ne_zero supplies the
nonvanishing needed to read the norm as a square class of units.
Any factorization of f by X - C x has fCofactor x as its other factor.
The cubic quotient algebra R[X]/(f). It is étale when W is elliptic and in
characteristic ≠ 2 normal form, by separable_f.
Equations
- W.A = AdjoinRoot W.f
Instances For
The Chinese Remainder Theorem isomorphism R[X]⧸f ≃ R × R[X]⧸cf, where cf is the cofactor
f / (X - x).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Two classes in W.A agree exactly when they agree in both factors of the Chinese Remainder
decomposition at a root of f. This is not a corollary of AdjoinRoot.mk_eq_mk, which reads the
equality as a divisibility by f: here the point is that the divisibility is detected by the two
factors separately.
A polynomial of degree at most 2 has degree less than that of f, which has degree 3.
Supplies the degree side conditions of AdjoinRoot.mk_eq_mk_iff_of_degree_lt for the relator
f.
A polynomial of degree at most 1 has degree less than that of fCofactor x, which has
degree 2. Supplies the degree side conditions of AdjoinRoot.mk_eq_mk_iff_of_degree_lt for the
relator fCofactor x.
At a root of f, its derivative does not vanish.
The point (x, 0) at a root of f lies on the curve.
Every class in W.A is represented by a polynomial of degree at most 2. The bound is
natDegree f - 1 = 2; this is the normal form the kernel computation reduces to before
multiplying by a linear class.
Every class in W.A' x is represented by a polynomial of degree at most 1. This is
exists_mk_quadratic_eq for the cofactor, where the bound is natDegree (fCofactor x) - 1 = 1.
Multiplying a quadratic representative with a nonzero leading coefficient by a suitable
linear class lowers its degree to 1. This is the reduction step of the kernel computation: it
trades the quadratic normal form of exists_mk_quadratic_eq for a linear one, at the cost of a
factor X - C ξ whose ξ the statement produces.
The group of square classes of units of W.A.
Equations
- WeierstrassCurve.Affine.M = (W.Aˣ ⧸ (powMonoidHom 2).range)
Instances For
The square classes of W.A form a commutative group. This is the target of the descent
map: μ lands in W.M, and M.sq_eq_one says every element squares to 1 (equivalently
M.inv_eq_self: every element is its own inverse), so W.M is an elementary abelian 2-group.
The instance is stated rather than left to inferInstance: the latter succeeds on the spot, but
instance search does not find it at the use sites below (e.g. for mul_right_comm in
μX_mul_mul_eq_one) unless it is declared here.
The product of the classes of three units of W.A is trivial exactly when their product is a
square in W.A. This is the shape in which multiplicativity of the x - T map is proved: each
case exhibits an explicit square root of the product of the three representatives.
The descent or x - T map on x-coordinates: it sends x to the square class of x - T
if f x ≠ 0, and otherwise to the square class of the corrected representative
x - T + fCofactor x, which is a unit even though x - T is not.
Classical decidability is used for the branch: μX is noncomputable regardless, so requiring
DecidableEq K here would buy nothing.
Equations
- WeierstrassCurve.Affine.μX x = if hx : Polynomial.eval x W.f = 0 then ↑⋯.unit else ↑⋯.unit
Instances For
The value of μX on the branch where x is a root of f, namely the square class of the
corrected representative x - T + fCofactor x.
Not a simp lemma: the right-hand side mentions the hypothesis proof hx, so it cannot serve
as a rewrite rule. Every use site names it explicitly.
The value of μX on the branch where x is not a root of f, namely the square class of
x - T.
Not a simp lemma, for the same reason as μX_of_eval_f_eq_zero.
The descent or x - T map μ₀ on the group of points of an affine Weierstrass curve.
This is a plain map; it is upgraded to a group homomorphism μ below.
Equations
Instances For
The descent map sends the point at infinity to the trivial square class.
On an affine point the descent map is the coordinate-level map μX applied to the
x-coordinate: it does not see y.
Step 3: μ is a homomorphism #
Multiplicativity is the statement that the square classes of three collinear points multiply to
1. The proof splits on how many of the three x-coordinates are roots of f, i.e. on how many
of the points are 2-torsion, and in each case exhibits an explicit square root of the product of
the three representatives.
Three collinear points cut f down to a square. If three affine points sum to 0, the
product of the three linear factors X - C x is f minus the square of a polynomial of degree
at most 1, namely the line through them.
The descent map takes negation to inversion. Since μ₀ P and μ₀ (-P) are computed from
the same x-coordinate, this is the statement that each square class is its own inverse.
Multiplicativity at the level of x-coordinates. If three affine points sum to 0, the
product of the three square classes is trivial. This is the coordinate-level heart of the proof
that μ is a homomorphism; the case split is on how many of the three points are 2-torsion.
Multiplicativity of the descent map on collinear triples. μX_mul_mul_eq_one lifted from
x-coordinates to points, including the degenerate cases where one of the three is 0. This is
exactly the hypothesis MonoidHom.ofMapMulMulEqOne needs to build μ.
The descent, or x - T, map as a group homomorphism.
Equations
Instances For
The homomorphism μ agrees with the underlying map μ₀. This is the characteristic lemma
for μ, and the simp normal form: use sites rewrite with it rather than unfolding the
MonoidHom.ofMapMulMulEqOne that defines μ.
The descent map kills doubled points. Consequently μ factors through the quotient of
W.Point by its doubled points, which is what makes it a descent map: the image of μ can only
detect a point up to adding 2 • Q.
The divisibility criterion #
What belongs here is the criterion the kernel computation runs on, namely that divisibility by
2 is equivalent to an explicit polynomial identity. exists_eq_two_smul_iff' restates it inside
W.A, which is the form the square-class argument consumes; the section below runs that argument
and concludes in ker_μ_eq.
A nonsingular affine point is divisible by 2 exactly when an explicit polynomial identity
has a solution.
The criterion of exists_eq_two_smul_iff restated as an identity in W.A.
The kernel of the x - T map #
Both inclusions of ker_μ_eq. That 2 • P is killed is μ₀_two_nsmul; the converse is trivial at
the point at infinity and, at an affine point, splits on whether f vanishes at the x-coordinate.
Each affine branch feeds the criterion of the previous section a square root extracted from
μ (some x y h) = 1.
A nonsingular affine point killed by the x - T map is divisible by 2.
The kernel of the x - T map is exactly 2 • W(K). This is the injectivity half of the
descent: it is what makes W(K)/2W(K) embed into the group of square classes W.M.
The norm map on square classes #
Algebra.norm K : W.A →* K carries units to units and squares to squares, so it descends to the
square classes: normM sends the class of u : W.Aˣ to the class of its norm in
Kˣ ⧸ (powMonoidHom 2).range, the ambient of Mathlib's Selmer group. Both branches of μX have
square norm — off the 2-torsion the norm of x - T is f x, which the curve equation makes
y ^ 2, and at a root of f the norm of the corrected representative is (f' x) ^ 2 — so the
image of μ lies in the kernel of normM. That containment is the norm condition the 2-descent
reads off the image of the descent map.
The norm map on square classes, induced by Algebra.norm K : W.A →* K. It is well defined
because the norm carries a square of W.Aˣ to a square of Kˣ.
Equations
Instances For
Every value of μX has trivial norm class. On the branch where f x ≠ 0 the norm of
x - T is f x, a square by the curve equation; at a root of f the norm of the corrected
representative is (f' x) ^ 2.
The image of μ lies in the kernel of the norm map on square classes. This is the norm
condition on im μ: every square class in the image of the descent map has square norm.