Power subfields of the function field of a Weierstrass curve

For any field K, exponent n, and Weierstrass curve W, this file packages the tower K(x^n) ⊆ K(x) ⊆ K(W) and computes [K(W) : K(x^n)] = 2n.

It is the generator X ^ n case of AdjoinTower.lean, which proves the same tower for an arbitrary rational function; the single input this file supplies is TauCeti.RatFunc.finrank_adjoin_X_pow, that [K(x) : K⟮X ^ n⟯] = n.

At n = 0, the displayed degree formulas use Module.finrank's value 0 for an infinite-dimensional extension: K(x^0) = K, so both sides of each formula read 0.

Main results

• WeierstrassCurve.Affine.ratFuncAdjoinXPowRange: the copy of K(x^n) inside K(W), with algebraMap_X_pow_mem_ratFuncAdjoinXPowRange for its generator.
• WeierstrassCurve.Affine.finrank_ratFuncAdjoinXPowRange: [K(W) : K(x^n)] = 2 * n.
• WeierstrassCurve.Affine.ratFuncAdjoinXPowRange_eq_map_ratFuncRange and WeierstrassCurve.Affine.finrank_fieldRange_of_apply_X_eq_pow: for any embedding f : K(W') → K(W) of function fields sending the affine coordinate of W' to x ^ n, the copy of K(x^n) is the image of K(x'), and [K(W) : f(K(W'))] = n. This is the whole tower comparison behind a degree of an inseparable isogeny; the absolute and the relative Frobenius each supply their own hf and read off their degree.

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

The finite-field Frobenius and relative Frobenius degree computations both use this tower.

Provenance

The tower argument lives in Affine/FunctionField/AdjoinTower.lean, stated for an arbitrary generator; this file holds the X ^ n specialisation. Its finite-field ancestor is the AINTLIB HasseWeil project (github.com/CBirkbeck/AINTLIB, Apache-2.0, pinned at 513e83879e2f8cbc626eb9e04d660e92be16ccba), HasseWeil/FrobeniusIsogeny.lean, where the exponent is the cardinality of a finite field and the embedding is the q-power map. The rational-function input TauCeti.RatFunc.finrank_adjoin_X_pow is recorded in TauCeti/FieldTheory/RatFunc/PowerTower.lean; the finite-field specialisation stays in Affine/FunctionField/FrobeniusTower.lean.

noncomputable def WeierstrassCurve.Affine.ratFuncAdjoinXPowRange {K : Type u_1} [Field K] (W : Affine K) (n : ℕ) : IntermediateField K W.FunctionField

The image of the field generated by X ^ n inside K(W). This is IntermediateField.extendRight at the generator X ^ n; everything below is AdjoinTower.lean's tower read through TauCeti.RatFunc.finrank_adjoin_X_pow, which supplies [K(x) : K⟮X ^ n⟯] = n.

Equations

• W.ratFuncAdjoinXPowRange n = K⟮RatFunc.X ^ n⟯.extendRight W.FunctionField

theorem WeierstrassCurve.Affine.algebraMap_X_pow_mem_ratFuncAdjoinXPowRange {K : Type u_1} [Field K] (W : Affine K) (n : ℕ) : (algebraMap (Polynomial K) W.FunctionField) Polynomial.X ^ n ∈ W.ratFuncAdjoinXPowRange n

The generator: x ^ n lies in the copy of K(x^n).

@[simp]

theorem WeierstrassCurve.Affine.ratFuncAdjoinXPowRange_le_iff {K : Type u_1} [Field K] (W : Affine K) {n : ℕ} {L : IntermediateField K W.FunctionField} : W.ratFuncAdjoinXPowRange n ≤ L ↔ (algebraMap (Polynomial K) W.FunctionField) Polynomial.X ^ n ∈ L

The universal property: the copy of K(x^n) lies inside an intermediate field exactly when that field contains x ^ n.

@[simp]

theorem WeierstrassCurve.Affine.relfinrank_ratFuncAdjoinXPowRange {K : Type u_1} [Field K] (W : Affine K) (n : ℕ) : (W.ratFuncAdjoinXPowRange n).relfinrank W.ratFuncRange = n

[K(x) : K(x^n)] = n, read inside K(W). At n = 0, this is the finrank value 0 for the infinite-dimensional extension K(x) / K.

@[simp]

theorem WeierstrassCurve.Affine.finrank_ratFuncAdjoinXPowRange {K : Type u_1} [Field K] (W : Affine K) (n : ℕ) : Module.finrank (↥(W.ratFuncAdjoinXPowRange n)) W.FunctionField = 2 * n

[K(W) : K(x^n)] = 2n. At n = 0, both sides are 0: the extension over K(x^0) = K is infinite-dimensional, and Module.finrank reports 0.

theorem WeierstrassCurve.Affine.ratFuncAdjoinXPowRange_eq_map_ratFuncRange {K : Type u_1} [Field K] (W : Affine K) {W' : Affine K} {n : ℕ} (f : W'.FunctionField →ₐ[K] W.FunctionField) (hf : f ((algebraMap (Polynomial K) W'.FunctionField) Polynomial.X) = (algebraMap (Polynomial K) W.FunctionField) Polynomial.X ^ n) : W.ratFuncAdjoinXPowRange n = IntermediateField.map f W'.ratFuncRange

The copy of K(x^n) 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 x ^ n. This is the field the degree tower below is anchored at, in its two descriptions.

theorem WeierstrassCurve.Affine.finrank_fieldRange_of_apply_X_eq_pow {K : Type u_1} [Field K] (W : Affine K) {W' : Affine K} {n : ℕ} (f : W'.FunctionField →ₐ[K] W.FunctionField) (hf : f ((algebraMap (Polynomial K) W'.FunctionField) Polynomial.X) = (algebraMap (Polynomial K) W.FunctionField) Polynomial.X ^ n) : Module.finrank (↥f.fieldRange) W.FunctionField = n

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