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 #

theorem WeierstrassCurve.VariableChange.ext_iff {R : Type u} :
∀ {inst : CommRing R} {x y : WeierstrassCurve.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 : WeierstrassCurve.VariableChange R}, x.u = y.ux.r = y.rx.s = y.sx.t = y.tx = y

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

    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
          Equations
          • WeierstrassCurve.VariableChange.instGroup = Group.mk
          @[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⁻¹ * (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⁻¹ ^ 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)
          @[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₁)

          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
            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 : WeierstrassCurve.VariableChange R) (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

            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 φ

                  Variable changes of elliptic curves #

                  @[simp]
                  theorem EllipticCurve.variableChange_a₃ {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) :
                  (E.variableChange C).a₃ = C.u⁻¹ ^ 3 * (E.a₃ + C.r * E.a₁ + 2 * C.t)
                  @[simp]
                  theorem EllipticCurve.variableChange_a₄ {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) :
                  (E.variableChange C).a₄ = C.u⁻¹ ^ 4 * (E.a₄ - C.s * E.a₃ + 2 * C.r * E.a₂ - (C.t + C.r * C.s) * E.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)
                  @[simp]
                  theorem EllipticCurve.variableChange_a₂ {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) :
                  (E.variableChange C).a₂ = C.u⁻¹ ^ 2 * (E.a₂ - C.s * E.a₁ + 3 * C.r - C.s ^ 2)
                  @[simp]
                  theorem EllipticCurve.variableChange_Δ' {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) :
                  (E.variableChange C).Δ' = C.u⁻¹ ^ 12 * E.Δ'
                  @[simp]
                  theorem EllipticCurve.variableChange_a₆ {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) :
                  (E.variableChange C).a₆ = C.u⁻¹ ^ 6 * (E.a₆ + C.r * E.a₄ + C.r ^ 2 * E.a₂ + C.r ^ 3 - C.t * E.a₃ - C.t ^ 2 - C.r * C.t * E.a₁)
                  @[simp]
                  theorem EllipticCurve.variableChange_a₁ {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) :
                  (E.variableChange C).a₁ = C.u⁻¹ * (E.a₁ + 2 * C.s)
                  @[simp]
                  theorem EllipticCurve.variableChange_toWeierstrassCurve {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) :
                  (E.variableChange C).toWeierstrassCurve = E.variableChange C

                  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
                  • E.variableChange C = { toWeierstrassCurve := E.variableChange C, Δ' := C.u⁻¹ ^ 12 * E.Δ', coe_Δ' := }
                  Instances For
                    theorem EllipticCurve.variableChange_id {R : Type u} [CommRing R] (E : EllipticCurve R) :
                    E.variableChange WeierstrassCurve.VariableChange.id = E
                    theorem EllipticCurve.variableChange_comp {R : Type u} [CommRing R] (C : WeierstrassCurve.VariableChange R) (C' : WeierstrassCurve.VariableChange R) (E : EllipticCurve R) :
                    E.variableChange (C.comp C') = (E.variableChange C').variableChange C
                    Equations
                    theorem EllipticCurve.coe_variableChange_Δ' {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) :
                    (E.variableChange C).Δ' = C.u⁻¹ ^ 12 * E.Δ'
                    theorem EllipticCurve.coe_inv_variableChange_Δ' {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) :
                    (E.variableChange C).Δ'⁻¹ = C.u ^ 12 * E.Δ'⁻¹
                    @[simp]
                    theorem EllipticCurve.variableChange_j {R : Type u} [CommRing R] (E : EllipticCurve R) (C : WeierstrassCurve.VariableChange R) :
                    (E.variableChange C).j = E.j