Galois actions on function fields of Weierstrass curves

Let W be a Weierstrass curve over a field F, and let K/F be a field extension. Every F-automorphism of K acts semilinearly on the function field of W_K: it applies the automorphism to coefficients and fixes the coordinate functions x and y. This file extends the coordinate-ring action WeierstrassCurve.coordinateRingGaloisAction to the function field and proves its identity and composition laws.

The action on functions, together with the action on points, enters the proof of Galois equivariance of the Weil pairing; the compatibility with translation proved here, conjugating translation by P to translation by the conjugate point, is the function-side half of that argument.

Main definitions

• WeierstrassCurve.functionFieldGaloisAction: the action on the function field.

Main results

• WeierstrassCurve.functionFieldGaloisAction_algebraMap: the action is semilinear on constants.
• WeierstrassCurve.functionFieldGaloisAction_genericX and WeierstrassCurve.functionFieldGaloisAction_genericY: the two coordinate functions are fixed.
• WeierstrassCurve.functionFieldGaloisAction_map_algebraMap: every function defined over the ground field is fixed.
• WeierstrassCurve.functionFieldGaloisAction_translation: on an elliptic curve, the action intertwines translation by a point with translation by its Galois conjugate.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.8.

noncomputable def WeierstrassCurve.functionFieldGaloisAction {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) : Gal(K/F) →* (W.baseChange K).toAffine.FunctionField ≃+* (W.baseChange K).toAffine.FunctionField

The Galois action on the function field of a base-changed Weierstrass curve. It is the unique extension of coordinateRingGaloisAction to the fraction field.

Equations

• W.functionFieldGaloisAction = (IsFractionRing.ringEquivOfRingEquivHom (W.baseChange K).toAffine.CoordinateRing (W.baseChange K).toAffine.FunctionField).comp W.coordinateRingGaloisAction

@[simp]

theorem WeierstrassCurve.functionFieldGaloisAction_symm {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) (σ : Gal(K/F)) : (W.functionFieldGaloisAction σ).symm = W.functionFieldGaloisAction σ.symm

The inverse function-field action is the action of the inverse coefficient automorphism.

@[simp]

theorem WeierstrassCurve.functionFieldGaloisAction_algebraMap_coordinateRing {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) (σ : Gal(K/F)) (z : (W.baseChange K).toAffine.CoordinateRing) : (W.functionFieldGaloisAction σ) ((algebraMap (W.baseChange K).toAffine.CoordinateRing (W.baseChange K).toAffine.FunctionField) z) = (algebraMap (W.baseChange K).toAffine.CoordinateRing (W.baseChange K).toAffine.FunctionField) ((W.coordinateRingGaloisAction σ) z)

The function-field action restricts to the coordinate-ring action.

theorem WeierstrassCurve.functionFieldGaloisAction_algebraMap_mk {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) (σ : Gal(K/F)) (p : Polynomial (Polynomial K)) : (W.functionFieldGaloisAction σ) ((algebraMap (W.baseChange K).toAffine.CoordinateRing (W.baseChange K).toAffine.FunctionField) ((Affine.CoordinateRing.mk (W.baseChange K).toAffine) p)) = (algebraMap (W.baseChange K).toAffine.CoordinateRing (W.baseChange K).toAffine.FunctionField) ((Affine.CoordinateRing.mk (W.baseChange K).toAffine) (Polynomial.map (Polynomial.mapRingHom ↑σ) p))

The function-field action on the class of a polynomial applies the automorphism to its coefficients.

@[simp]

theorem WeierstrassCurve.functionFieldGaloisAction_algebraMap {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) (σ : Gal(K/F)) (a : K) : (W.functionFieldGaloisAction σ) ((algebraMap K (W.baseChange K).toAffine.FunctionField) a) = (algebraMap K (W.baseChange K).toAffine.FunctionField) (σ a)

The function-field action applies the field automorphism to constants.

@[simp]

theorem WeierstrassCurve.functionFieldGaloisAction_genericX {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) (σ : Gal(K/F)) : (W.functionFieldGaloisAction σ) (W.baseChange K).toAffine.genericX = (W.baseChange K).toAffine.genericX

The function-field action fixes the generic x-coordinate.

@[simp]

theorem WeierstrassCurve.functionFieldGaloisAction_genericY {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) (σ : Gal(K/F)) : (W.functionFieldGaloisAction σ) (W.baseChange K).toAffine.genericY = (W.baseChange K).toAffine.genericY

The function-field action fixes the generic y-coordinate.

@[simp]

theorem WeierstrassCurve.functionFieldGaloisAction_map_algebraMap {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) (σ : Gal(K/F)) (z : W.toAffine.FunctionField) : (W.functionFieldGaloisAction σ) ((Affine.FunctionField.map W.toAffine (algebraMap F K)) z) = (Affine.FunctionField.map W.toAffine (algebraMap F K)) z

The Galois action fixes the function field defined over the ground field.

@[simp]

theorem WeierstrassCurve.functionFieldGaloisAction_translation {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) [DecidableEq K] [W.IsElliptic] (σ : Gal(K/F)) (P : (W.baseChange K).toAffine.Point) (z : (W.baseChange K).toAffine.FunctionField) : (W.functionFieldGaloisAction σ) (((W.baseChange K).toAffine.translation ((Affine.Point.equivBaseChangeSelf (W.baseChange K).toAffine) P)) z) = ((W.baseChange K).toAffine.translation ((Affine.Point.equivBaseChangeSelf (W.baseChange K).toAffine) ((Multiplicative.toAdd (W.pointGaloisAction σ)) P))) ((W.functionFieldGaloisAction σ) z)

Galois conjugation intertwines translation by P with translation by the conjugate point. Equivalently, the pullback squares formed by the two translations and the Galois action commute.