The subfield of F(W) generated by Φₙ / ΨSqₙ

RatFuncDegree.lean shows that adjoining Φₙ / ΨSqₙ to F inside F(x) leaves an extension of dimension n². This file carries that up the tower F(Φₙ/ΨSqₙ) ⊆ F(x) ⊆ F(W) and computes [F(W) : F(Φₙ/ΨSqₙ)] = 2n², then divides the outer degree two back out: an embedding of function fields carrying the affine coordinate to Φₙ / ΨSqₙ has image of index exactly n².

That last statement is the geometric half of deg [n] = n². The degree of an isogeny is the degree of the extension of function fields it induces, and multiplication by n pulls the affine coordinate x back to Φₙ / ΨSqₙ. So an isogeny with that pullback has image of index n² in F(W), which is its degree: the result below is stated for an arbitrary embedding precisely so that identifying the pullback is all that remains.

Main definitions

• WeierstrassCurve.ratFuncAdjoinΦDivΨSqRange: the copy of F(Φₙ/ΨSqₙ) inside F(W), with algebraMap_Φ_div_ΨSq_mem_ratFuncAdjoinΦDivΨSqRange for its generator and ratFuncAdjoinΦDivΨSqRange_le_iff for its universal property.

Main results

• WeierstrassCurve.relfinrank_ratFuncAdjoinΦDivΨSqRange: [F(x) : F(Φₙ/ΨSqₙ)] = n², read inside F(W).
• WeierstrassCurve.finrank_ratFuncAdjoinΦDivΨSqRange: [F(W) : F(Φₙ/ΨSqₙ)] = 2n².
• WeierstrassCurve.finrank_fieldRange_of_apply_X_eq_Φ_div_ΨSq: [F(W) : f(F(W'))] = n² for any embedding f of function fields sending the affine coordinate of W' to Φₙ / ΨSqₙ. The copy of F(Φₙ/ΨSqₙ) is then the image of F(x'), by Affine.extendRight_adjoin_eq_map_ratFuncRange.

Nonsingularity is assumed as n ≠ 0 → W.Δ ≠ 0, the form finrank_adjoin_Φ_div_ΨSq takes: at n = 0 every displayed degree is 0 by Module.finrank's value on an infinite extension, and that holds for a singular W too.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.6.4(a).

noncomputable def WeierstrassCurve.ratFuncAdjoinΦDivΨSqRange {F : Type u_1} [Field F] (W : WeierstrassCurve F) (n : ℤ) : IntermediateField F W.toAffine.FunctionField

The image of the field generated by Φₙ / ΨSqₙ inside F(W).

Equations

• W.ratFuncAdjoinΦDivΨSqRange n = F⟮(algebraMap (Polynomial F) (RatFunc F)) (W.Φ n) / (algebraMap (Polynomial F) (RatFunc F)) (W.ΨSq n)⟯.extendRight W.toAffine.FunctionField

@[simp]

theorem WeierstrassCurve.ratFuncAdjoinΦDivΨSqRange_le_iff {F : Type u_1} [Field F] (W : WeierstrassCurve F) {n : ℤ} {L : IntermediateField F W.toAffine.FunctionField} : W.ratFuncAdjoinΦDivΨSqRange n ≤ L ↔ (algebraMap (RatFunc F) W.toAffine.FunctionField) ((algebraMap (Polynomial F) (RatFunc F)) (W.Φ n) / (algebraMap (Polynomial F) (RatFunc F)) (W.ΨSq n)) ∈ L

The universal property: the copy of F(Φₙ/ΨSqₙ) lies inside an intermediate field exactly when that field contains Φₙ / ΨSqₙ.

theorem WeierstrassCurve.algebraMap_Φ_div_ΨSq_mem_ratFuncAdjoinΦDivΨSqRange {F : Type u_1} [Field F] (W : WeierstrassCurve F) (n : ℤ) : (algebraMap (RatFunc F) W.toAffine.FunctionField) ((algebraMap (Polynomial F) (RatFunc F)) (W.Φ n) / (algebraMap (Polynomial F) (RatFunc F)) (W.ΨSq n)) ∈ W.ratFuncAdjoinΦDivΨSqRange n

The generator: Φₙ / ΨSqₙ lies in the copy of F(Φₙ/ΨSqₙ).

@[simp]

theorem WeierstrassCurve.relfinrank_ratFuncAdjoinΦDivΨSqRange {F : Type u_1} [Field F] (W : WeierstrassCurve F) (n : ℤ) (hΔ : n ≠ 0 → W.Δ ≠ 0) : (W.ratFuncAdjoinΦDivΨSqRange n).relfinrank W.toAffine.ratFuncRange = n.natAbs ^ 2

[F(x) : F(Φₙ/ΨSqₙ)] = n², read inside F(W).

@[simp]

theorem WeierstrassCurve.finrank_ratFuncAdjoinΦDivΨSqRange {F : Type u_1} [Field F] (W : WeierstrassCurve F) (n : ℤ) (hΔ : n ≠ 0 → W.Δ ≠ 0) : Module.finrank (↥(W.ratFuncAdjoinΦDivΨSqRange n)) W.toAffine.FunctionField = 2 * n.natAbs ^ 2

[F(W) : F(Φₙ/ΨSqₙ)] = 2n². At n = 0 both sides are 0.

theorem WeierstrassCurve.finrank_fieldRange_of_apply_X_eq_Φ_div_ΨSq {F : Type u_1} [Field F] (W : WeierstrassCurve F) {W' : Affine F} {n : ℤ} (hΔ : n ≠ 0 → W.Δ ≠ 0) (f : W'.FunctionField →ₐ[F] W.toAffine.FunctionField) (hf : f ((algebraMap (Polynomial F) W'.FunctionField) Polynomial.X) = (algebraMap (RatFunc F) W.toAffine.FunctionField) ((algebraMap (Polynomial F) (RatFunc F)) (W.Φ n) / (algebraMap (Polynomial F) (RatFunc F)) (W.ΨSq n))) : Module.finrank (↥f.fieldRange) W.toAffine.FunctionField = n.natAbs ^ 2

[F(W) : f(F(W'))] = n² for an embedding f : F(W') → F(W) of function fields carrying the affine coordinate of W' to Φₙ / ΨSqₙ.

This is the geometric half of deg [n] = n².