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.instMulActionVariableChange
: 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^\times$ 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) \mapsto (u^2X + r, u^3Y + u^2sX + 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
The Weierstrass curve over R
induced by an admissible linear change of variables
$(X, Y) \mapsto (u^2X + r, u^3Y + u^2sX + t)$ for some $u \in R^\times$ and some $r, s, t \in R$.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- WeierstrassCurve.instMulActionVariableChange = MulAction.mk ⋯ ⋯
Maps and base changes of variable changes #
The change of variables mapped over a ring homomorphism φ : R →+* A
.
Equations
- WeierstrassCurve.VariableChange.map φ C = { u := (Units.map ↑φ) C.u, r := φ C.r, s := φ C.s, t := φ C.t }
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' := ⋯ }