Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.Projective.VariableChange

Variable changes on the homogeneous coordinate ring of a Weierstrass curve #

An admissible change of variables C = (u, r, s, t) carries a point (x, y) of C • W to the point (u²x + r, u³y + u²sx + t) of W. In homogeneous coordinates this is the linear map [X : Y : Z] ↦ [u²X + rZ : u²sX + u³Y + tZ : Z] with matrix C.toMatrix. Substituting it into the homogeneous Weierstrass polynomial of W gives u⁶ times that of C • W, so it induces an R-algebra isomorphism of homogeneous coordinate rings variableChangeEquiv W C : R[X, Y, Z] ⧸ (W) ≃ₐ[R] R[X, Y, Z] ⧸ (C • W) which preserves the grading by total degree. Its Proj is the isomorphism between the projective Weierstrass models of C • W and W.

Main definitions #

Main results #

References #

source
def WeierstrassCurve.VariableChange.toMatrix {R : Type u_1} [CommRing R] (C : VariableChange R) :
Matrix (Fin 3) (Fin 3) R

The matrix of the change of variables C = (u, r, s, t) acting on homogeneous coordinates: [X : Y : Z] ↦ [u²X + rZ : u²sX + u³Y + tZ : Z], the homogenisation of (x, y) ↦ (u²x + r, u³y + u²sx + t).

Equations
Instances For
    source
    @[simp]
    theorem WeierstrassCurve.VariableChange.toMatrix_one {R : Type u_1} [CommRing R] :
    toMatrix 1 = 1
    source
    @[simp]
    theorem WeierstrassCurve.VariableChange.toMatrix_mul {R : Type u_1} [CommRing R] (C C' : VariableChange R) :
    (C * C').toMatrix = C'.toMatrix * C.toMatrix

    toMatrix reverses products: a point of (C * C') • W = C • C' • W is first carried to C' • W by C, and then to W by C'.

    source
    theorem WeierstrassCurve.VariableChange.toMatrix_mul_toMatrix_inv {R : Type u_1} [CommRing R] (C : VariableChange R) :
    C.toMatrix * C⁻¹.toMatrix = 1
    source
    theorem WeierstrassCurve.VariableChange.toMatrix_inv_mul_toMatrix {R : Type u_1} [CommRing R] (C : VariableChange R) :
    C⁻¹.toMatrix * C.toMatrix = 1
    source
    theorem WeierstrassCurve.Projective.linearSubst_polynomial {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) :
    (MvPolynomial.linearSubst C.toMatrix) W.toProjective.polynomial = MvPolynomial.C (↑C.u ^ 6) * (C • W).toProjective.polynomial

    The change of variables multiplies the homogeneous Weierstrass polynomial by u⁶: W(u²X + rZ, u²sX + u³Y + tZ, Z) = u⁶ (C • W)(X, Y, Z).

    source
    noncomputable def WeierstrassCurve.Projective.variableChangeEquiv {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) :
    W.toProjective.CoordinateRing ≃ₐ[R] (C • W).toProjective.CoordinateRing

    The isomorphism of homogeneous coordinate rings R[X, Y, Z] ⧸ (W) ≃ₐ[R] R[X, Y, Z] ⧸ (C • W) induced by the change of variables C: the class of p(X, Y, Z) goes to the class of p(u²X + rZ, u²sX + u³Y + tZ, Z).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem WeierstrassCurve.Projective.variableChangeEquiv_mk {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) (p : MvPolynomial (Fin 3) R) :
      (variableChangeEquiv W C) ((Ideal.Quotient.mk (Ideal.span {W.toProjective.polynomial})) p) = (Ideal.Quotient.mk (Ideal.span {(C • W).toProjective.polynomial})) ((MvPolynomial.linearSubst C.toMatrix) p)
      source
      @[simp]
      theorem WeierstrassCurve.Projective.variableChangeEquiv_symm_mk {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) (p : MvPolynomial (Fin 3) R) :
      (variableChangeEquiv W C).symm ((Ideal.Quotient.mk (Ideal.span {(C • W).toProjective.polynomial})) p) = (Ideal.Quotient.mk (Ideal.span {W.toProjective.polynomial})) ((MvPolynomial.linearSubst C⁻¹.toMatrix) p)
      source
      @[simp]
      theorem WeierstrassCurve.Projective.variableChangeEquiv_one {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) :
      variableChangeEquiv W 1 = Ideal.quotientEquivAlgOfEq R ⋯

      The identity change of variables induces the canonical isomorphism R[X, Y, Z] ⧸ (W) ≃ₐ[R] R[X, Y, Z] ⧸ (1 • W) coming from 1 • W = W.

      source
      @[simp]
      theorem WeierstrassCurve.Projective.variableChangeEquiv_mul {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (C C' : VariableChange R) :
      variableChangeEquiv W (C * C') = ((variableChangeEquiv W C').trans (variableChangeEquiv (C' • W) C)).trans (Ideal.quotientEquivAlgOfEq R ⋯)

      The isomorphism induced by a product C * C' is the isomorphism induced by C' followed by the one induced by C, up to the canonical isomorphism coming from C • C' • W = (C * C') • W.

      source
      theorem WeierstrassCurve.Projective.variableChangeEquiv_mem_grading {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) {n : ℕ} {x : W.toProjective.CoordinateRing} (hx : x ∈ W.toProjective.grading n) :
      (variableChangeEquiv W C) x ∈ (C • W).toProjective.grading n

      The isomorphism of homogeneous coordinate rings preserves the grading by total degree.

      source
      theorem WeierstrassCurve.Projective.variableChangeEquiv_symm_mem_grading {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) {n : ℕ} {x : (C • W).toProjective.CoordinateRing} (hx : x ∈ (C • W).toProjective.grading n) :
      (variableChangeEquiv W C).symm x ∈ W.toProjective.grading n

      The inverse isomorphism of homogeneous coordinate rings preserves the grading by total degree.

      source
      theorem WeierstrassCurve.Projective.evalZero_variableChangeEquiv {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) {n : ℕ} {x : W.toProjective.CoordinateRing} (hx : x ∈ W.toProjective.grading n) :
      (C • W).toProjective.evalZero ((variableChangeEquiv W C) x) = (↑C.u ^ 3) ^ n * W.toProjective.evalZero x

      Evaluating at [0 : 1 : 0] after the change of variables is evaluating at [0 : u³ : 0]: on the degree-n part it multiplies the value at [0 : 1 : 0] by (u³)ⁿ.