Admissible changes of Weierstrass coordinates #
An admissible change of variables over the constant field preserves the pole orders two and
three of Weierstrass coordinates, and their regularity away from the chosen place. Consequently
at a degree-one place of a function field, normalizing the equation also gives normalized
generators of the field.
The equation transport uses WeierstrassCurve.Affine.variableChange_equation.
References #
- H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Springer, 2009, Proposition 6.1.2.
- J. H. Silverman, The Arithmetic of Elliptic Curves, 2nd ed., Springer, 2009, Chapter III, Section 1.
theorem
TauCeti.Place.IsWeierstrassCoordinates.variableChange
{k : Type u_1}
{F : Type u_2}
[Field k]
[Field F]
[Algebra k F]
{P : Place k F}
{W : WeierstrassCurve k}
{x y : F}
(h : P.IsWeierstrassCoordinates W x y)
(C : WeierstrassCurve.VariableChange k)
:
P.IsWeierstrassCoordinates (C • W) ((algebraMap k F) ↑C⁻¹.u ^ 2 * x + (algebraMap k F) C⁻¹.r)
((algebraMap k F) ↑C⁻¹.u ^ 3 * y + (algebraMap k F) ↑C⁻¹.u ^ 2 * (algebraMap k F) C⁻¹.s * x + (algebraMap k F) C⁻¹.t)
An admissible change of variables over the constant field preserves Weierstrass
coordinates. The coordinates on C • W are obtained by applying the inverse change.