Change of variables of Weierstrass curves #
This file defines admissible linear change of variables of Weierstrass curves.
Main definitions #
WeierstrassCurve.VariableChange
: a change of variables of Weierstrass curves.WeierstrassCurve.VariableChange.instGroup
: change of variables form a group.WeierstrassCurve.variableChange
: the Weierstrass curve induced by a change of variables.WeierstrassCurve.instIsEllipticVariableChange
: change of variables act on Weierstrass curves.
Main statements #
WeierstrassCurve.variableChange_j
: the j-invariant of an elliptic curve is invariant under an admissible linear change of variables.
References #
Tags #
elliptic curve, weierstrass equation, change of variables
Variable changes #
An admissible linear change of variables of Weierstrass curves defined over a ring R
given by
a tuple (u, r, s, t)
for some u
in Rˣ
and some r, s, t
in R
. As a matrix, it is
$$\begin{pmatrix} u^2 & 0 & r \cr u^2s & u^3 & t \cr 0 & 0 & 1 \end{pmatrix}.$$
In other words, this is the change of variables (X, Y) ↦ (u²X + r, u³Y + u²sX + t)
.
When R
is a field, any two isomorphic Weierstrass equations are related by this.
- u : Rˣ
The
u
coefficient of an admissible linear change of variables, which must be a unit. - r : R
The
r
coefficient of an admissible linear change of variables. - s : R
The
s
coefficient of an admissible linear change of variables. - t : R
The
t
coefficient of an admissible linear change of variables.
Instances For
The identity linear change of variables given by the identity matrix.
Equations
- WeierstrassCurve.VariableChange.id = { u := 1, r := 0, s := 0, t := 0 }
Instances For
The composition of two linear changes of variables given by matrix multiplication.
Equations
Instances For
The inverse of a linear change of variables given by matrix inversion.
Equations
Instances For
Equations
The Weierstrass curve over R
induced by an admissible linear change of variables
(X, Y) ↦ (u²X + r, u³Y + u²sX + t)
for some u
in Rˣ
and some r, s, t
in R
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Maps and base changes #
The change of variables mapped over a ring homomorphism φ : R →+* A
.
Equations
Instances For
The change of variables base changed to an algebra A
over R
.
Equations
Instances For
The map over a ring homomorphism of a change of variables is a group homomorphism.
Equations
- WeierstrassCurve.VariableChange.mapHom φ = { toFun := WeierstrassCurve.VariableChange.map φ, map_one' := ⋯, map_mul' := ⋯ }