The tower K⟮g⟯ ⊆ K(x) ⊆ K(W) over an arbitrary generator

For a rational function g, the subfield K⟮g⟯ of K(x) has a copy inside the function field K(W) of a Weierstrass curve. This file computes the two degrees of the resulting tower in terms of the single input [K(x) : K⟮g⟯]: the inner storey contributes that degree, the outer storey contributes two, and an embedding of function fields carrying the affine coordinate to g has image of index exactly [K(x) : K⟮g⟯].

Everything here is generator-agnostic. A caller supplies g together with a theorem computing Module.finrank K⟮g⟯ (RatFunc K), and gets the whole tower back; PowerTower.lean does this for g = X ^ n, where that degree is n.

The copy of K⟮g⟯ inside K(W) is Mathlib's IntermediateField.extendRight, written (IntermediateField.adjoin K {g}).extendRight W.FunctionField; this file adds the degree lemmas for it in this tower and no new object. Its membership and order API is generic and lives in TauCeti.FieldTheory.IntermediateField.ExtendRight.

Main results

• WeierstrassCurve.Affine.relfinrank_extendRight: [K(x) : F], read inside K(W).
• WeierstrassCurve.Affine.finrank_extendRight: [K(W) : F] = 2 · [K(x) : F].
• WeierstrassCurve.Affine.extendRight_adjoin_eq_map_ratFuncRange and WeierstrassCurve.Affine.finrank_fieldRange_of_apply_X_eq: for any embedding f : K(W') → K(W) of function fields sending the affine coordinate of W' to g, the copy of K⟮g⟯ is the image of K(x'), and [K(W) : f(K(W'))] = [K(x) : K⟮g⟯].

No result needs W to be elliptic: the Weierstrass equation alone gives the power basis, through finrank_ratFuncRange.

The Frobenius degree computation is a specialisation of this tower, through PowerTower.lean.

Provenance

The argument, naming scheme and proof shapes are Affine/FunctionField/PowerTower.lean's, stated here for an arbitrary generator instead of X ^ n. The finite-field ancestor of both is the AINTLIB HasseWeil project (github.com/CBirkbeck/AINTLIB, Apache-2.0, pinned at 513e83879e2f8cbc626eb9e04d660e92be16ccba), HasseWeil/FrobeniusIsogeny.lean, private declarations frobFracRange, frobFracRange_le_frobRange, finrank_frobFracRange_functionField and finrank_over_frobenius_image, where the exponent is the cardinality of a finite field.

theorem WeierstrassCurve.Affine.extendRight_le_ratFuncRange {K : Type u_1} [Field K] (W : Affine K) (F : IntermediateField K (RatFunc K)) : F.extendRight W.FunctionField ≤ W.ratFuncRange

Any subfield of K(x) sits inside K(x), both read inside K(W).

@[simp]

theorem WeierstrassCurve.Affine.relfinrank_extendRight {K : Type u_1} [Field K] (W : Affine K) (F : IntermediateField K (RatFunc K)) : (F.extendRight W.FunctionField).relfinrank W.ratFuncRange = Module.finrank (↥F) (RatFunc K)

[K(x) : F], read inside K(W), is the degree it has inside K(x) itself.

@[simp]

theorem WeierstrassCurve.Affine.finrank_extendRight {K : Type u_1} [Field K] (W : Affine K) (F : IntermediateField K (RatFunc K)) : Module.finrank (↥(F.extendRight W.FunctionField)) W.FunctionField = 2 * Module.finrank (↥F) (RatFunc K)

[K(W) : F] = 2 · [K(x) : F]: the inner storey contributes the degree of F and the outer one contributes two. When K(x) is infinite-dimensional over F both sides are 0, Module.finrank's value there.

theorem WeierstrassCurve.Affine.extendRight_adjoin_eq_map_ratFuncRange {K : Type u_1} [Field K] (W : Affine K) {W' : Affine K} {g : RatFunc K} (f : W'.FunctionField →ₐ[K] W.FunctionField) (hf : f ((algebraMap (Polynomial K) W'.FunctionField) Polynomial.X) = (algebraMap (RatFunc K) W.FunctionField) g) : K⟮g⟯.extendRight W.FunctionField = IntermediateField.map f W'.ratFuncRange

The copy of K⟮g⟯ inside K(W) is the image of the rational function field of W', for any embedding f : K(W') → K(W) of function fields carrying the affine coordinate of W' to g. This is the field the degree tower below is anchored at, in its two descriptions.

theorem WeierstrassCurve.Affine.finrank_fieldRange_of_apply_X_eq {K : Type u_1} [Field K] (W : Affine K) {W' : Affine K} {g : RatFunc K} (f : W'.FunctionField →ₐ[K] W.FunctionField) (hf : f ((algebraMap (Polynomial K) W'.FunctionField) Polynomial.X) = (algebraMap (RatFunc K) W.FunctionField) g) : Module.finrank (↥f.fieldRange) W.FunctionField = Module.finrank (↥K⟮g⟯) (RatFunc K)

[K(W) : f(K(W'))] = [K(x) : K⟮g⟯] for an embedding f : K(W') → K(W) of function fields carrying the affine coordinate of W' to g. Both K(x) and the image of K(W') lie between K⟮g⟯ and K(W), of relative degrees [K(x) : K⟮g⟯] and 2 over it; since [K(W) : K(x)] = 2 as well, the two towers give 2 · [K(W) : f(K(W'))] = 2 · [K(x) : K⟮g⟯].