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: the Weierstrass curve induced by a change of variables.
WeierstrassCurve.instMulActionVariableChange: change of variables act on Weierstrass curves.
EllipticCurve.variableChange: the elliptic curve induced by a change of variables.
EllipticCurve.instMulActionVariableChange: change of variables act on elliptic curves.

Main statements #

EllipticCurve.variableChange_j: the j-invariant of an elliptic curve is invariant under an admissible linear change of variables.

References #

[J Silverman, The Arithmetic of Elliptic Curves][silverman2009]

Tags #

elliptic curve, weierstrass equation, change of variables

Variable changes #

source

structure WeierstrassCurve.VariableChange (R : Type u) [CommRing R] :

Type u

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}$.

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

source

theorem WeierstrassCurve.VariableChange.ext {R : Type u} :

∀ {inst : CommRing R} {x y : WeierstrassCurve.VariableChange R}, x.u = y.u → x.r = y.r → x.s = y.s → x.t = y.t → x = y

source

def WeierstrassCurve.VariableChange.id {R : Type u} [CommRing R] :

WeierstrassCurve.VariableChange R

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

source

def WeierstrassCurve.VariableChange.comp {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) (C' : WeierstrassCurve.VariableChange R) :

WeierstrassCurve.VariableChange R

The composition of two linear changes of variables given by matrix multiplication.

Equations

C.comp C' = { u := C.u * C'.u, r := C.r * ↑C'.u ^ 2 + C'.r, s := ↑C'.u * C.s + C'.s, t := C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t }

Instances For

source

def WeierstrassCurve.VariableChange.inv {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) :

WeierstrassCurve.VariableChange R

The inverse of a linear change of variables given by matrix inversion.

Equations

C.inv = { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }

Instances For

source

theorem WeierstrassCurve.VariableChange.id_comp {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) :

WeierstrassCurve.VariableChange.id.comp C = C

source

theorem WeierstrassCurve.VariableChange.comp_id {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) :

C.comp WeierstrassCurve.VariableChange.id = C

source

theorem WeierstrassCurve.VariableChange.comp_left_inv {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) :

C.inv.comp C = WeierstrassCurve.VariableChange.id

source

theorem WeierstrassCurve.VariableChange.comp_assoc {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) (C' : WeierstrassCurve.VariableChange R) (C'' : WeierstrassCurve.VariableChange R) :

(C.comp C').comp C'' = C.comp (C'.comp C'')

source

instance WeierstrassCurve.VariableChange.instGroup {R : Type u} [CommRing R] :

Group (WeierstrassCurve.VariableChange R)

Equations

WeierstrassCurve.VariableChange.instGroup = Group.mk ⋯

source

def WeierstrassCurve.variableChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) :

WeierstrassCurve R

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

source

@[simp]

theorem WeierstrassCurve.variableChange_a₁ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) :

(W.variableChange C).a₁ = ↑C.u⁻¹ * (W.a₁ + 2 * C.s)

source

@[simp]

theorem WeierstrassCurve.variableChange_a₃ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) :

(W.variableChange C).a₃ = ↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)

source

@[simp]

theorem WeierstrassCurve.variableChange_a₂ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) :

(W.variableChange C).a₂ = ↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)

source

@[simp]

theorem WeierstrassCurve.variableChange_a₆ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) :

(W.variableChange C).a₆ = ↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)

source

@[simp]

theorem WeierstrassCurve.variableChange_a₄ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) :

(W.variableChange C).a₄ = ↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)

source

theorem WeierstrassCurve.variableChange_id {R : Type u} [CommRing R] (W : WeierstrassCurve R) :

W.variableChange WeierstrassCurve.VariableChange.id = W

source

theorem WeierstrassCurve.variableChange_comp {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) (C' : WeierstrassCurve.VariableChange R) (W : WeierstrassCurve R) :

W.variableChange (C.comp C') = (W.variableChange C').variableChange C

source

instance WeierstrassCurve.instMulActionVariableChange {R : Type u} [CommRing R] :

MulAction (WeierstrassCurve.VariableChange R) (WeierstrassCurve R)

Equations

WeierstrassCurve.instMulActionVariableChange = MulAction.mk ⋯ ⋯

source

@[simp]

theorem WeierstrassCurve.variableChange_b₂ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) :

(W.variableChange C).b₂ = ↑C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)

source

@[simp]

theorem WeierstrassCurve.variableChange_b₄ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) :

(W.variableChange C).b₄ = ↑C.u⁻¹ ^ 4 * (W.b₄ + C.r * W.b₂ + 6 * C.r ^ 2)

source

@[simp]

theorem WeierstrassCurve.variableChange_b₆ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) :

(W.variableChange C).b₆ = ↑C.u⁻¹ ^ 6 * (W.b₆ + 2 * C.r * W.b₄ + C.r ^ 2 * W.b₂ + 4 * C.r ^ 3)

source

@[simp]

theorem WeierstrassCurve.variableChange_b₈ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) :

(W.variableChange C).b₈ = ↑C.u⁻¹ ^ 8 * (W.b₈ + 3 * C.r * W.b₆ + 3 * C.r ^ 2 * W.b₄ + C.r ^ 3 * W.b₂ + 3 * C.r ^ 4)

source

@[simp]

theorem WeierstrassCurve.variableChange_c₄ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) :

(W.variableChange C).c₄ = ↑C.u⁻¹ ^ 4 * W.c₄

source

@[simp]

theorem WeierstrassCurve.variableChange_c₆ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) :

(W.variableChange C).c₆ = ↑C.u⁻¹ ^ 6 * W.c₆

source

@[simp]

theorem WeierstrassCurve.variableChange_Δ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) :

(W.variableChange C).Δ = ↑C.u⁻¹ ^ 12 * W.Δ

Maps and base changes of variable changes #

source

def WeierstrassCurve.VariableChange.map {R : Type u} [CommRing R] {A : Type v} [CommRing A] (φ : R →+* A) (C : WeierstrassCurve.VariableChange R) :

WeierstrassCurve.VariableChange A

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

source

@[simp]

theorem WeierstrassCurve.VariableChange.map_s {R : Type u} [CommRing R] {A : Type v} [CommRing A] (φ : R →+* A) (C : WeierstrassCurve.VariableChange R) :

(WeierstrassCurve.VariableChange.map φ C).s = φ C.s

source

@[simp]

theorem WeierstrassCurve.VariableChange.map_r {R : Type u} [CommRing R] {A : Type v} [CommRing A] (φ : R →+* A) (C : WeierstrassCurve.VariableChange R) :

(WeierstrassCurve.VariableChange.map φ C).r = φ C.r

source

@[simp]

theorem WeierstrassCurve.VariableChange.map_u {R : Type u} [CommRing R] {A : Type v} [CommRing A] (φ : R →+* A) (C : WeierstrassCurve.VariableChange R) :

(WeierstrassCurve.VariableChange.map φ C).u = (Units.map ↑φ) C.u

source

@[simp]

theorem WeierstrassCurve.VariableChange.map_t {R : Type u} [CommRing R] {A : Type v} [CommRing A] (φ : R →+* A) (C : WeierstrassCurve.VariableChange R) :

(WeierstrassCurve.VariableChange.map φ C).t = φ C.t

source

@[reducible, inline]

abbrev WeierstrassCurve.VariableChange.baseChange {R : Type u} [CommRing R] (A : Type v) [CommRing A] (C : WeierstrassCurve.VariableChange R) [Algebra R A] :

WeierstrassCurve.VariableChange A

The change of variables base changed to an algebra A over R.

Equations

WeierstrassCurve.VariableChange.baseChange A C = WeierstrassCurve.VariableChange.map (algebraMap R A) C

Instances For

source

@[simp]

theorem WeierstrassCurve.VariableChange.map_id {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) :

WeierstrassCurve.VariableChange.map (RingHom.id R) C = C

source

theorem WeierstrassCurve.VariableChange.map_map {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) {A : Type v} [CommRing A] (φ : R →+* A) {B : Type w} [CommRing B] (ψ : A →+* B) :

WeierstrassCurve.VariableChange.map ψ (WeierstrassCurve.VariableChange.map φ C) = WeierstrassCurve.VariableChange.map (ψ.comp φ) C

source

@[simp]

theorem WeierstrassCurve.VariableChange.map_baseChange {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) {S : Type s} [CommRing S] [Algebra R S] {A : Type v} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type w} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (ψ : A →ₐ[S] B) :

WeierstrassCurve.VariableChange.map (↑ψ) (WeierstrassCurve.VariableChange.baseChange A C) = WeierstrassCurve.VariableChange.baseChange B C

source

theorem WeierstrassCurve.VariableChange.map_injective {R : Type u} [CommRing R] {A : Type v} [CommRing A] {φ : R →+* A} (hφ : Function.Injective ⇑φ) :

Function.Injective (WeierstrassCurve.VariableChange.map φ)

source

def WeierstrassCurve.VariableChange.mapHom {R : Type u} [CommRing R] {A : Type v} [CommRing A] (φ : R →+* A) :

WeierstrassCurve.VariableChange R →* WeierstrassCurve.VariableChange A

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' := ⋯ }

Instances For

source

theorem WeierstrassCurve.map_variableChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (φ : R →+* A) (C : WeierstrassCurve.VariableChange R) :

(W.map φ).variableChange (WeierstrassCurve.VariableChange.map φ C) = (W.variableChange C).map φ

Variable changes of elliptic curves #

source

def EllipticCurve.variableChange {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) :

EllipticCurve R

The elliptic 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$. When R is a field, any two Weierstrass equations isomorphic to E are related by this.

Equations