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.
• An instance which states that change of variables forms a group.
• An instance which states that change of variables acts on Weierstrass curves.

Main statements

• An instance which states that change of variables preserves elliptic curves.
• 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][silverman2009]

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ˣ 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.

theorem WeierstrassCurve.VariableChange.ext_iff {R : Type u} {inst✝ : CommRing R} {x y : VariableChange R} : x = y ↔ x.u = y.u ∧ x.r = y.r ∧ x.s = y.s ∧ x.t = y.t

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

instance WeierstrassCurve.VariableChange.instOne {R : Type u} [CommRing R] : One (VariableChange R)

theorem WeierstrassCurve.VariableChange.one_def {R : Type u} [CommRing R] : 1 = { u := 1, r := 0, s := 0, t := 0 }

The identity linear change of variables given by the identity matrix.

instance WeierstrassCurve.VariableChange.instMul {R : Type u} [CommRing R] : Mul (VariableChange R)

theorem WeierstrassCurve.VariableChange.mul_def {R : Type u} [CommRing R] (C C' : VariableChange R) : C * 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 }

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

instance WeierstrassCurve.VariableChange.instInv {R : Type u} [CommRing R] : Inv (VariableChange R)

theorem WeierstrassCurve.VariableChange.inv_def {R : Type u} [CommRing R] (C : VariableChange R) : C⁻¹ = { u := C.u⁻¹, r := -C.r * ↑C.u⁻¹ ^ 2, s := -C.s * ↑C.u⁻¹, t := (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 }

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

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

instance WeierstrassCurve.instSMulVariableChange {R : Type u} [CommRing R] : SMul (VariableChange R) (WeierstrassCurve R)

theorem WeierstrassCurve.variableChange_def {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) : C • W = { a₁ := ↑C.u⁻¹ * (W.a₁ + 2 * C.s), a₂ := ↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2), a₃ := ↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t), 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), 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₁) }

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.

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

theorem WeierstrassCurve.variableChange_a₁ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) : (C • W).a₁ = ↑C.u⁻¹ * (W.a₁ + 2 * C.s)

theorem WeierstrassCurve.variableChange_a₂ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) : (C • W).a₂ = ↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)

theorem WeierstrassCurve.variableChange_a₃ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) : (C • W).a₃ = ↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)

theorem WeierstrassCurve.variableChange_a₄ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) : (C • W).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_a₆ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) : (C • W).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₁)

theorem WeierstrassCurve.variableChange_b₂ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) : (C • W).b₂ = ↑C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)

theorem WeierstrassCurve.variableChange_b₄ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) : (C • W).b₄ = ↑C.u⁻¹ ^ 4 * (W.b₄ + C.r * W.b₂ + 6 * C.r ^ 2)

theorem WeierstrassCurve.variableChange_b₆ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) : (C • W).b₆ = ↑C.u⁻¹ ^ 6 * (W.b₆ + 2 * C.r * W.b₄ + C.r ^ 2 * W.b₂ + 4 * C.r ^ 3)

theorem WeierstrassCurve.variableChange_b₈ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) : (C • W).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)

theorem WeierstrassCurve.variableChange_c₄ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) : (C • W).c₄ = ↑C.u⁻¹ ^ 4 * W.c₄

theorem WeierstrassCurve.variableChange_c₆ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) : (C • W).c₆ = ↑C.u⁻¹ ^ 6 * W.c₆

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

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

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

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

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

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

@[simp]

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

Maps and base changes

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

The change of variables mapped over a ring homomorphism φ : R →+* A.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[reducible, inline]

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

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

@[simp]

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

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

@[simp]

theorem WeierstrassCurve.VariableChange.map_baseChange {R : Type u} [CommRing R] (C : 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) : map (↑ψ) (baseChange A C) = 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 (map φ)

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

The map over a ring homomorphism of a change of variables is a group homomorphism.

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