Documentation

Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Change of variables of Weierstrass curves #

This file defines admissible linear change of variables of Weierstrass curves.

Main definitions #

Main statements #

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

    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
      • 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

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

        Equations
        Instances For
          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'')
          Equations
          • WeierstrassCurve.VariableChange.instGroup = Group.mk

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

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

            Equations
            Instances For
              @[reducible, inline]

              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
                Instances For
                  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 φ