The degree of an isogeny

The degree of an isogeny φ : W₁ → W₂ of affine Weierstrass curves over a field F is the dimension of W₁.FunctionField over the image of the function-field pullback φ.fieldPullback — the pulled-back copy of W₂.FunctionField, which that pullback embeds isomorphically. No properness, smoothness or separability input is involved: the degree is field theory.

That reading is only honest once the extension is known to be finite, since Module.finrank of an infinite extension reads 0. Finiteness holds for every isogeny, and this file proves it: the pullback of the affine coordinate is transcendental over F (TauCeti.Isogeny.transcendental_pullback_X), so the pulled-back function field already contains a transcendental element t, and F(W₁) is finite over F(t) because it is finite over the rational function field. Positivity of the degree follows at once, and degree one reads as an isomorphism on function fields.

Multiplicativity under composition is the finrank tower formula, applied to F(W₃) → F(W₂) → F(W₁). The pulled-back copies of F(W₂) and F(W₃) are subfields of F(W₁), so the tower is stated through TauCeti.Isogeny.degree_eq_finrank, which reads a degree off any algebra structure whose structure map is the pullback.

Main definitions

• TauCeti.Isogeny.degree: the degree of an isogeny, with TauCeti.Isogeny.degree_def the equation lemma the module boundary makes necessary.

Main results

• TauCeti.Isogeny.finiteDimensional: automatic finiteness — the extension a degree measures is finite, the inseparable case included.
• TauCeti.Isogeny.degree_eq_finrank: the degree read off an arbitrary algebra structure induced by the pullback.
• TauCeti.Isogeny.finiteDimensional_functionField: the function-field extension is finite, for any algebra structure whose structure map is the pullback.
• TauCeti.Isogeny.degree_pos: an isogeny has positive degree.
• TauCeti.Isogeny.degree_eq_one_iff: degree one means the function-field pullback is onto; TauCeti.Isogeny.degree_id is the identity's case, and is the @[simp] normal form of a degree.
• TauCeti.Isogeny.finrank_map_ratFuncRange_fieldPullback: the pulled-back coordinate subfield sits 2 · deg φ below the function field.
• TauCeti.Isogeny.degree_comp: the tower formula deg (ψ ∘ φ) = deg ψ * deg φ.

The mathematics is Silverman, The Arithmetic of Elliptic Curves, II.2.4(a) and II.2.4(c), where finiteness of the extension is exactly what makes a nonconstant map of curves finite.

degree is the coordinate-ring form of D. Angdinata's function-field definition, as the Isogeny structure itself is. The finiteness result also follows that development's function-field formulation.

Provenance

degree and finiteDimensional are as described above. Separately, finrank_map_ratFuncRange_fieldPullback is an identity the AINTLIB HasseWeil project (Chris Birkbeck, Apache 2.0, commit 513e83879e2f8cbc626eb9e04d660e92be16ccba) needs for its point count and assumes rather than proves: it is the hypothesis h_tower_witness of bridgeA_intermediateField_finrank_eq_two_mul_degree_of_witness in Hasse/SepDegreeEqPointCount.lean.

References

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

noncomputable def TauCeti.Isogeny.degree {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : ℕ

The degree of an isogeny: the dimension of the source function field W₁.FunctionField over the image of fieldPullback — the pulled-back copy of the target's function field W₂.FunctionField, which fieldPullback embeds isomorphically.

This is Silverman, The Arithmetic of Elliptic Curves, II.2.4(a). The extension is finite (finiteDimensional below), so the dimension is honest and positive.

Equations

• φ.degree = Module.finrank (↥φ.fieldPullback.fieldRange) W₁.FunctionField

theorem TauCeti.Isogeny.degree_def {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : φ.degree = Module.finrank (↥φ.fieldPullback.fieldRange) W₁.FunctionField

The defining formula for degree. The definition's body is not exposed across the module boundary, so this is how downstream modules compute with it.

Not @[simp]: degree_id is the simp-normal form of a degree, and this lemma rewrites its left-hand side, so tagging both fails simpNF.

instance TauCeti.Isogeny.finiteDimensional {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : FiniteDimensional (↥φ.fieldPullback.fieldRange) W₁.FunctionField

An isogeny has finite degree (Silverman II.2.4(a)): the extension of W₁.FunctionField over the pulled-back copy of W₂.FunctionField is finite, with no separability hypothesis — purely inseparable isogenies such as Frobenius are covered.

The pulled-back copy contains the pullback t of the target's affine coordinate, transcendental over F by transcendental_pullback_X, and W₁.FunctionField is finite over F(t), because it is a function field over F: finite over the rational function field, by WeierstrassCurve.Affine.finiteDimensional_functionField. Enlarging the base field from F(t) to the whole pulled-back copy keeps it finite. This is where the isogeny hypotheses are spent — a merely arbitrary subfield of W₁.FunctionField need not sit under a finite extension.

theorem TauCeti.Isogeny.degree_eq_finrank {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) [Algebra W₂.FunctionField W₁.FunctionField] (h : ∀ (z : W₂.FunctionField), (algebraMap W₂.FunctionField W₁.FunctionField) z = φ.fieldPullback z) : φ.degree = Module.finrank W₂.FunctionField W₁.FunctionField

The degree read off any algebra structure induced by the pullback. The function-field pullback identifies W₂.FunctionField with the subfield of W₁.FunctionField that degree measures against, so the two dimensions agree. Stated for an arbitrary algebra structure whose structure map is the pullback, rather than for one fixed choice: registering such a structure globally would create a diamond, since different isogenies induce different ones.

theorem TauCeti.Isogeny.degree_pos {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : 0 < φ.degree

The degree of an isogeny is positive. The extension is finite and the source function field is nontrivial.

theorem TauCeti.Isogeny.finiteDimensional_functionField {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) [Algebra W₂.FunctionField W₁.FunctionField] (h : ∀ (z : W₂.FunctionField), (algebraMap W₂.FunctionField W₁.FunctionField) z = φ.fieldPullback z) : FiniteDimensional W₂.FunctionField W₁.FunctionField

An isogeny's function-field extension is finite.

Isogeny.finiteDimensional gives this over φ.fieldPullback.fieldRange; this is the same fact for any algebra structure whose structure map is the pullback, which is the form consumers hold. It takes the same hypothesis as degree_eq_finrank, and needs nothing beyond it: every isogeny has positive degree, and the degree is the relevant finrank.

@[simp]

theorem TauCeti.Isogeny.degree_ne_zero {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : φ.degree ≠ 0

The degree of an isogeny is nonzero, the ≠ form of degree_pos.

theorem TauCeti.Isogeny.degree_eq_one_iff {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : φ.degree = 1 ↔ Function.Surjective ⇑φ.fieldPullback

Degree one means an isomorphism of function fields. The degree measures W₁.FunctionField over the image of fieldPullback, so it is one exactly when that image is everything.

@[simp]

theorem TauCeti.Isogeny.degree_id {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : (id W).degree = 1

The identity isogeny has degree one: its function-field pullback is the identity, so the extension it measures is trivial.

@[simp]

theorem TauCeti.Isogeny.degree_comp {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} (ψ : Isogeny W₂ W₃) (φ : Isogeny W₁ W₂) : (ψ.comp φ).degree = ψ.degree * φ.degree

The degree is multiplicative under composition (Silverman II.2.4(c)): the tower formula for F(W₃) ⊆ F(W₂) ⊆ F(W₁), the inclusions being the pullbacks.

@[simp]

theorem TauCeti.Isogeny.finrank_map_ratFuncRange_fieldPullback {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : Module.finrank (↥(IntermediateField.map φ.fieldPullback W₂.ratFuncRange)) W₁.FunctionField = 2 * φ.degree

The pulled-back coordinate subfield sits 2 · deg φ below the function field, converting the isogeny's degree into a degree over a rational subfield. Over a finite base that is what a point count is read through, but nothing here is restricted to one and no count is proved.

theorem TauCeti.Isogeny.degree_eq_one_of_comp_eq_id {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} {ψ : Isogeny W₂ W₁} {φ : Isogeny W₁ W₂} (h : ψ.comp φ = id W₁) : ψ.degree = 1 ∧ φ.degree = 1

Both factors of an identity composite have degree one. Degree is multiplicative and the identity has degree one, and 1 factors in ℕ only as 1 * 1.