The degree of an isogeny is invariant under base change

Let φ : W₁ → W₂ be an isogeny over a field F and f : F →+* K a homomorphism of fields. This file proves deg (φ.map f) = deg φ: base change along any field extension, algebraic or not, preserves the degree, and so does transport along an automorphism of F.

Write M = φ^* F(W₂) ⊆ F(W₁) and M' = φ_K^* K(W₂) ⊆ K(W₁), so that deg φ = [F(W₁) : M] and deg (φ.map f) = [K(W₁) : M']. The embedding F(W₁) → K(W₁) carries M into M', and the proof shows that it carries a basis of F(W₁) over M to a basis of K(W₁) over M'.

• Spanning. The M'-span of the image of the basis contains the image of F(W₁), and is closed under multiplication. It is therefore a subalgebra of K(W₁), finite over the field M' and so itself a field. It contains K and the generic point, hence the coordinate ring of W₁⁄K, and hence every fraction.
• Independence. An M'-linear relation among the images becomes, once the coefficients are written over a common denominator and expanded in the monomial basis of K[W₂], a K-linear relation among the images of the products φ^*(xⁱyʲ) · bₖ. These products are F-linearly independent in F(W₁), and F(W₁) is linearly disjoint from K over F (WeierstrassCurve.Affine.FunctionField.linearIndependent_map), so the relation is trivial.

Linear disjointness of F(W₁) and K is where the curve enters. The coordinate ring K[W₁⁄K] is the scalar extension K ⊗_F F[W₁], the monomials xⁱyʲ forming a basis of both, so F-linearly independent elements of F[W₁] stay K-linearly independent; clearing denominators passes this to the function fields. For a separable algebraic extension of constants of an arbitrary field in which the constants are relatively algebraically closed, this persistence of linear independence is TauCeti.linearIndependent_algebraMap_comp_of_isIntegrallyClosedIn_of_isSeparable; the Weierstrass argument needs no hypothesis on K at all, so it also covers inseparable and transcendental extensions, such as an algebraic closure of an imperfect field.

Main results

• TauCeti.Isogeny.degree_map: deg (φ.map f) = deg φ.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.2.
• H. Stichtenoth, Algebraic Function Fields and Codes, III.6, the case of an algebraic extension of constants.

@[simp]

theorem TauCeti.Isogeny.degree_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (f : F →+* K) : (φ.map f).degree = φ.degree

Base change preserves the degree of an isogeny: deg (φ.map f) = deg φ for every homomorphism of fields f, in particular along every field extension.