The fixed field of the coefficient action on a Weierstrass function field

For a Galois extension K/F, the functions on W_K fixed by every coefficient automorphism are exactly the functions defined over F. This applies to infinite Galois extensions, including the separable closure over an imperfect field. Neither ellipticity nor perfectness is required.

The basis {1, y} over K(x) separates a function into two rational functions; coefficient automorphisms act on those two coefficients and fix the basis. This supplies the fixed-field calculation needed to descend equivariant function-field maps.

References

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

@[simp]

theorem WeierstrassCurve.functionFieldGaloisAction_algebraMap_ratFunc {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) (σ : Gal(K/F)) (z : RatFunc K) : (W.functionFieldGaloisAction σ) ((algebraMap (RatFunc K) (W.baseChange K).toAffine.FunctionField) z) = (algebraMap (RatFunc K) (W.baseChange K).toAffine.FunctionField) ((RatFunc.mapRingHom (Polynomial.mapRingHom σ.toRingEquiv.toRingHom) ⋯) z)

The coefficient action on the Weierstrass function field restricts to the coefficient action on its rational-function subfield.

theorem WeierstrassCurve.functionFieldGaloisAction_basis_repr {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.FunctionField) (i : Fin 2) : ((Affine.FunctionField.basis (W.baseChange K).toAffine (RatFunc K)).repr ((W.functionFieldGaloisAction σ) z)) i = (RatFunc.mapRingHom (Polynomial.mapRingHom σ.toRingEquiv.toRingHom) ⋯) (((Affine.FunctionField.basis (W.baseChange K).toAffine (RatFunc K)).repr z) i)

The coefficients of a function in the basis {1, y} transform by the coefficient action on rational functions.

theorem WeierstrassCurve.mem_range_functionFieldMap_iff_fixed {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (W : WeierstrassCurve F) [IsGalois F K] (z : (W.baseChange K).toAffine.FunctionField) : z ∈ Set.range ⇑(Affine.FunctionField.map W.toAffine (algebraMap F K)) ↔ ∀ (σ : Gal(K/F)), (W.functionFieldGaloisAction σ) z = z

The functions fixed by every coefficient automorphism of a Galois extension are exactly the images of ground-field functions. This holds for infinite extensions as well.