Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.Affine.Point.VariableChange

The isomorphism of point groups induced by a change of variables #

An admissible change of variables C : VariableChange R over a commutative ring induces a bijection (C • W).toAffine.Point ≃ W.toAffine.Point of nonsingular points, sending (x, y) to (u²x + r, u³y + u²sx + t) and fixing the point at infinity, with inverse induced by C⁻¹. Over a field it is a group isomorphism. No ellipticity hypothesis is needed, so this applies to the nonsingular points of singular Weierstrass curves as well.

Main definitions and results #

These maps identify the point groups of different Weierstrass models and, in particular, a quadratic twist with its original curve over a splitting field.

References #

Adapted from the FLT project (ImperialCollegeLondon/FLT, FLT/Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean at commit bc2fe8ff7396, FLT PR #1088, Apache 2.0), by Michael Stoll and Claude.

source
def WeierstrassCurve.Affine.Point.equivVariableChange {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) :
(C • W).toAffine.Point ≃ W.toAffine.Point

The bijection (C • W).Point ≃ W.Point of nonsingular points induced by the admissible change of variables (x, y) ↦ (u²x + r, u³y + u²sx + t), with inverse coming from C⁻¹.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem WeierstrassCurve.Affine.Point.equivVariableChange_some {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) {x y : R} (h : (C • W).toAffine.Nonsingular x y) :
    (equivVariableChange W C) (some x y h) = some (↑C.u ^ 2 * x + C.r) (↑C.u ^ 3 * y + ↑C.u ^ 2 * C.s * x + C.t) ⋯

    The forward coordinate formula for the change-of-variables bijection.

    source
    @[simp]
    theorem WeierstrassCurve.Affine.Point.equivVariableChange_zero {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) :
    (equivVariableChange W C) 0 = 0

    The change-of-variables bijection fixes the point at infinity.

    source
    @[simp]
    theorem WeierstrassCurve.Affine.Point.equivVariableChange_symm_zero {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) :
    (equivVariableChange W C).symm 0 = 0

    The inverse of the change-of-variables bijection fixes the point at infinity.

    source
    @[simp]
    theorem WeierstrassCurve.Affine.Point.equivVariableChange_symm_some {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) {x y : R} (h : W.toAffine.Nonsingular x y) :
    (equivVariableChange W C).symm (some x y h) = some (↑C⁻¹.u ^ 2 * x + C⁻¹.r) (↑C⁻¹.u ^ 3 * y + ↑C⁻¹.u ^ 2 * C⁻¹.s * x + C⁻¹.t) ⋯

    The inverse coordinate formula, given by the inverse change of variables.

    source
    def WeierstrassCurve.Affine.Point.addEquivVariableChange {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) (C : VariableChange F) :
    (C • W).toAffine.Point ≃+ W.toAffine.Point

    The group isomorphism (C • W).Point ≃+ W.Point induced by the admissible change of variables; its underlying bijection is equivVariableChange.

    Equations
    Instances For
      source
      @[simp]
      theorem WeierstrassCurve.Affine.Point.coe_addEquivVariableChange {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) (C : VariableChange F) :
      ⇑(addEquivVariableChange W C) = ⇑(equivVariableChange W C)

      The group isomorphism addEquivVariableChange has underlying function equivVariableChange.

      source
      @[simp]
      theorem WeierstrassCurve.Affine.Point.coe_addEquivVariableChange_symm {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) (C : VariableChange F) :
      ⇑(addEquivVariableChange W C).symm = ⇑(equivVariableChange W C).symm

      The inverse of the group isomorphism addEquivVariableChange has underlying function the inverse of equivVariableChange.

      Curves over a ring and their points over a field #

      source
      def WeierstrassCurve.pointEquivVariableChange {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (L : Type u_2) [Field L] [DecidableEq L] [Algebra R L] (C : VariableChange R) :
      ((C • W).baseChange L).toAffine.Point ≃+ (W.baseChange L).toAffine.Point

      The points over L of C • W and of W are identified by a change of variables C over R: the group isomorphism (x, y) ↦ (u²x + r, u³y + u²sx + t) between the points of their base changes to a field L. It is WeierstrassCurve.Affine.Point.addEquivVariableChange for the base change of C to L, read on the base change of C • W.

      Equations
      Instances For
        source
        @[simp]
        theorem WeierstrassCurve.pointEquivVariableChange_some {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (L : Type u_2) [Field L] [DecidableEq L] [Algebra R L] (C : VariableChange R) {x y : L} (h : ((C • W).baseChange L).toAffine.Nonsingular x y) :
        (W.pointEquivVariableChange L C) (Affine.Point.some x y h) = Affine.Point.some (↑(C.baseChange L).u ^ 2 * x + (C.baseChange L).r) (↑(C.baseChange L).u ^ 3 * y + ↑(C.baseChange L).u ^ 2 * (C.baseChange L).s * x + (C.baseChange L).t) ⋯

        What the identification pointEquivVariableChange does to a point given by coordinates: it is the change of variables C, base changed to L.

        source
        @[simp]
        theorem WeierstrassCurve.pointEquivVariableChange_symm_some {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (L : Type u_2) [Field L] [DecidableEq L] [Algebra R L] (C : VariableChange R) {x y : L} (h : (W.baseChange L).toAffine.Nonsingular x y) :
        (W.pointEquivVariableChange L C).symm (Affine.Point.some x y h) = Affine.Point.some (↑(C.baseChange L)⁻¹.u ^ 2 * x + (C.baseChange L)⁻¹.r) (↑(C.baseChange L)⁻¹.u ^ 3 * y + ↑(C.baseChange L)⁻¹.u ^ 2 * (C.baseChange L)⁻¹.s * x + (C.baseChange L)⁻¹.t) ⋯

        What the inverse of the identification pointEquivVariableChange does to a point given by coordinates: it is the change of variables C⁻¹, base changed to L.