Group law on Weierstrass curves #
This file proves that the nonsingular rational points on a Weierstrass curve form an abelian group
under the geometric group law defined in Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean.
Mathematical background #
Let W be a Weierstrass curve over a field F given by a Weierstrass equation W(X, Y) = 0 in
affine coordinates. As in Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean, the set of
nonsingular rational points W⟮F⟯ of W consist of the unique point at infinity 𝓞 and
nonsingular affine points (x, y). With this description, there is an addition-preserving injection
between W⟮F⟯ and the ideal class group of the affine coordinate ring
F[W] := F[X, Y] / ⟨W(X, Y)⟩ of W. This is given by mapping 𝓞 to the trivial ideal class and a
nonsingular affine point (x, y) to the ideal class of the invertible ideal ⟨X - x, Y - y⟩.
Proving that this is well-defined and preserves addition reduces to equalities of integral ideals
checked in WeierstrassCurve.Affine.CoordinateRing.XYIdeal_neg_mul and in
WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdeal via explicit ideal computations.
Now F[W] is a free rank two F[X]-algebra with basis {1, Y}, so every element of F[W] is of
the form p + qY for some p, q in F[X], and there is an algebra norm N : F[W] → F[X].
Injectivity can then be shown by computing the degree of such a norm N(p + qY) in two different
ways, which is done in WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis and in the
auxiliary lemmas in the proof of WeierstrassCurve.Affine.Point.instAddCommGroup.
Main definitions #
WeierstrassCurve.Affine.CoordinateRing: the coordinate ringF[W]of a Weierstrass curveW.WeierstrassCurve.Affine.CoordinateRing.basis: the power basis ofF[W]overF[X].
Main statements #
WeierstrassCurve.Affine.CoordinateRing.instIsDomainCoordinateRing: the affine coordinate ring of a Weierstrass curve is an integral domain.WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis: the degree of the norm of an element in the affine coordinate ring in terms of its power basis.WeierstrassCurve.Affine.Point.instAddCommGroup: the type of nonsingular pointsW⟮F⟯in affine coordinates forms an abelian group under addition.
References #
Tags #
elliptic curve, group law, class group
Weierstrass curves in affine coordinates #
The affine coordinate ring R[W] := R[X, Y] / ⟨W(X, Y)⟩ of a Weierstrass curve W.
Equations
The function field R(W) := Frac(R[W]) of a Weierstrass curve W.
Equations
The coordinate ring as an R[X]-algebra #
The natural ring homomorphism mapping R[X][Y] to R[W].
The power basis {1, Y} for R[W] over R[X].
Equations
- WeierstrassCurve.Affine.CoordinateRing.basis W = ⋯.by_cases (fun (x : Subsingleton R) => default) fun (x : Nontrivial R) => (AdjoinRoot.powerBasis' ⋯).basis.reindex (finCongr ⋯)
Ideals in the coordinate ring over a ring #
The class of the element X - x in R[W] for some x in R.
The class of the element Y - y(X) in R[W] for some y(X) in R[X].
The ideal ⟨X - x⟩ of R[W] for some x in R.
The ideal ⟨Y - y(X)⟩ of R[W] for some y(X) in R[X].
The ideal ⟨X - x, Y - y(X)⟩ of R[W] for some x in R and y(X) in R[X].
The R-algebra isomorphism from R[W] / ⟨X - x, Y - y(X)⟩ to R obtained by evaluation at
some y(X) in R[X] and at some x in R provided that W(x, y(x)) = 0.
Equations
- One or more equations did not get rendered due to their size.
Ideals in the coordinate ring over a field #
The non-zero fractional ideal ⟨X - x, Y - y⟩ of F(W) for some x and y in F.
Equations
- One or more equations did not get rendered due to their size.
Alias of WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul.
Norms on the coordinate ring #
The axioms for nonsingular rational points on a Weierstrass curve #
The group homomorphism mapping a nonsingular affine point (x, y) of a Weierstrass curve W to
the class of the non-zero fractional ideal ⟨X - x, Y - y⟩ in the ideal class group of F[W].
Equations
- One or more equations did not get rendered due to their size.
Alias of WeierstrassCurve.Affine.Point.toClass.
The group homomorphism mapping a nonsingular affine point (x, y) of a Weierstrass curve W to
the class of the non-zero fractional ideal ⟨X - x, Y - y⟩ in the ideal class group of F[W].
Elliptic curves in affine coordinates #
An affine point on an elliptic curve E over a commutative ring R.