Descent of rational functions under coefficient automorphisms

For a Galois extension K/F, a rational function in K(X) comes from F(X) exactly when it is fixed by every coefficient automorphism in Gal(K/F). The extension may be infinite. In particular, the result applies to the separable closure of an arbitrary field.

The normalized numerator and monic denominator turn descent of a rational function into descent of their coefficients. This is the rational-function input to descent of functions on curves.

References

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

theorem RatFunc.mem_range_mapRingHom_iff_fixed {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] [IsGalois F K] (z : RatFunc K) : z ∈ Set.range ⇑(mapRingHom (Polynomial.mapRingHom (algebraMap F K)) ⋯) ↔ ∀ (σ : Gal(K/F)), (mapRingHom (Polynomial.mapRingHom σ.toRingEquiv.toRingHom) ⋯) z = z

A rational function over a Galois extension comes from the ground field exactly when all coefficient automorphisms fix it. No finite-dimensionality assumption is needed.