The basis of a Weierstrass function field over its rational parameter

The coordinate-ring basis {1, y} remains a basis of the function field over any fraction field of the polynomial ring in x. Thus every function has a unique expression a(x) + b(x)y. The explicit basis is useful when transporting functions along a change of coefficients.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.2.

noncomputable def WeierstrassCurve.Affine.FunctionField.basis {R : Type u_1} [CommRing R] [IsDomain R] (W : Affine R) (L : Type u_2) [Field L] [Algebra (Polynomial R) L] [IsFractionRing (Polynomial R) L] [Algebra L W.FunctionField] [IsScalarTower (Polynomial R) L W.FunctionField] : Module.Basis (Fin 2) L W.FunctionField

The basis {1, y} of the function field over a fraction field of R[X].

Equations

• WeierstrassCurve.Affine.FunctionField.basis W L = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯

theorem WeierstrassCurve.Affine.FunctionField.basis_apply {R : Type u_1} [CommRing R] [IsDomain R] (W : Affine R) (L : Type u_2) [Field L] [Algebra (Polynomial R) L] [IsFractionRing (Polynomial R) L] [Algebra L W.FunctionField] [IsScalarTower (Polynomial R) L W.FunctionField] (i : Fin 2) : (basis W L) i = (algebraMap W.CoordinateRing W.FunctionField) ((CoordinateRing.basis W) i)

The function-field basis is the image of the coordinate-ring basis.

@[simp]

theorem WeierstrassCurve.Affine.FunctionField.basis_zero {R : Type u_1} [CommRing R] [IsDomain R] (W : Affine R) (L : Type u_2) [Field L] [Algebra (Polynomial R) L] [IsFractionRing (Polynomial R) L] [Algebra L W.FunctionField] [IsScalarTower (Polynomial R) L W.FunctionField] : (basis W L) 0 = 1

@[simp]

theorem WeierstrassCurve.Affine.FunctionField.basis_one {R : Type u_1} [CommRing R] [IsDomain R] (W : Affine R) (L : Type u_2) [Field L] [Algebra (Polynomial R) L] [IsFractionRing (Polynomial R) L] [Algebra L W.FunctionField] [IsScalarTower (Polynomial R) L W.FunctionField] : (basis W L) 1 = W.genericY