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

• J Silverman, The Arithmetic of Elliptic Curves

Tags

elliptic curve, weierstrass equation, change of variables

Variable changes

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

theorem WeierstrassCurve.VariableChange.ext {R : Type u} {inst✝ : CommRing R} {x y : WeierstrassCurve.VariableChange R} (u : x.u = y.u) (r : x.r = y.r) (s : x.s = y.s) (t : x.t = y.t) : x = y

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 }

def WeierstrassCurve.VariableChange.comp {R : Type u} [CommRing R] (C 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 }

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 }

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

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

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

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

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

Equations

• WeierstrassCurve.VariableChange.instGroup = Group.mk ⋯

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.

@[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)

@[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)

@[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)

@[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₁)

@[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)

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

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

instance WeierstrassCurve.instMulActionVariableChange {R : Type u} [CommRing R] : MulAction (WeierstrassCurve.VariableChange R) (WeierstrassCurve R)

Equations

• WeierstrassCurve.instMulActionVariableChange = MulAction.mk ⋯ ⋯

@[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)

@[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)

@[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)

@[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)

@[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₄

@[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₆

@[simp]

theorem WeierstrassCurve.variableChange_Δ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) : (W.variableChange C).Δ = ↑C.u⁻¹ ^ 12 * W.Δ

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

@[simp]

theorem WeierstrassCurve.variableChange_Δ' {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) [W.IsElliptic] : (W.variableChange C).Δ' = C.u⁻¹ ^ 12 * W.Δ'

theorem WeierstrassCurve.coe_variableChange_Δ' {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) [W.IsElliptic] : ↑(W.variableChange C).Δ' = ↑C.u⁻¹ ^ 12 * ↑W.Δ'

theorem WeierstrassCurve.inv_variableChange_Δ' {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) [W.IsElliptic] : (W.variableChange C).Δ'⁻¹ = C.u ^ 12 * W.Δ'⁻¹

theorem WeierstrassCurve.coe_inv_variableChange_Δ' {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) [W.IsElliptic] : ↑(W.variableChange C).Δ'⁻¹ = ↑C.u ^ 12 * ↑W.Δ'⁻¹

@[simp]

theorem WeierstrassCurve.variableChange_j {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) [W.IsElliptic] : (W.variableChange C).j = W.j

Maps and base changes of variable changes

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 }

@[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

@[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

@[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

@[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

@[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

@[simp]

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

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

@[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

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 φ)

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

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 φ