A separable isogeny is unramified

A separable isogeny φ : W₁ → W₂ of elliptic curves makes F(W₁) a finite separable extension of the pulled-back function field F(W₂), and both fields have genus one. The Hurwitz genus formula

2g₁ - 2 = n · (2g₂ - 2) + deg Diff(F(W₁)/F(W₂))

therefore reads 0 = 0 + deg Diff. The different divisor is effective, so a vanishing degree forces it to vanish, and a vanishing different exponent forces the ramification index to be 1: every place of F(W₁) is unramified over F(W₂), with no exceptional locus.

Ramification is what separates the fundamental identity ∑_{P' ∣ P} e(P' ∣ P) · f(P' ∣ P) = deg φ from a count of the fibre of P. With e ≡ 1 the identity becomes ∑_{P' ∣ P} f(P' ∣ P) = deg φ at every place. Over a separably closed field of constants, the vanishing different also makes each relative residue extension separable, hence trivial, so P has exactly deg φ places above it.

Main results

• TauCeti.Isogeny.different_eq_zero: the different divisor of a separable isogeny vanishes.
• TauCeti.Isogeny.ramificationIdx_eq_one: a separable isogeny is unramified — e(P' ∣ P) = 1 at every place P' of F(W₁).
• TauCeti.Isogeny.sum_relativeDegree_eq_degree: the fundamental identity with the ramification indices removed, ∑_{P' ∣ P} f(P' ∣ P) = deg φ.
• TauCeti.Isogeny.isSplitCompletely and TauCeti.Isogeny.ncard_setOf_restrict_eq_degree: over a separably closed field of constants every place splits completely, so it has exactly deg φ places above it.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.5.9 and III.4.10.
• H. Stichtenoth, Algebraic Function Fields and Codes, Theorem 3.1.11, Remark 3.4.4 and Theorem 3.4.13.

theorem TauCeti.Isogeny.different_eq_zero {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) [Algebra W₂.FunctionField W₁.FunctionField] (h : ∀ (z : W₂.FunctionField), (algebraMap W₂.FunctionField W₁.FunctionField) z = φ.fieldPullback z) [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] : Divisor.different F W₁.FunctionField ⋯ = 0

The different divisor of a separable isogeny vanishes.

theorem TauCeti.Isogeny.ramificationIdx_eq_one {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) [Algebra W₂.FunctionField W₁.FunctionField] (h : ∀ (z : W₂.FunctionField), (algebraMap W₂.FunctionField W₁.FunctionField) z = φ.fieldPullback z) [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] (P' : Place F W₁.FunctionField) : Place.ramificationIdx W₂.FunctionField P' = 1

A separable isogeny is unramified: every place of F(W₁) has ramification index 1 over the place of F(W₂) below it (Silverman III.4.10(c)).

theorem TauCeti.Isogeny.sum_relativeDegree_eq_degree {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) [Algebra W₂.FunctionField W₁.FunctionField] (h : ∀ (z : W₂.FunctionField), (algebraMap W₂.FunctionField W₁.FunctionField) z = φ.fieldPullback z) [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] (P : Place F W₂.FunctionField) : ∑ P' ∈ ⋯.toFinset, Place.relativeDegree F W₂.FunctionField P' = φ.degree

The fundamental identity for a separable isogeny: the relative degrees of the places above a place P of F(W₂) sum to deg φ, the ramification indices of ∑ e · f = deg φ having all been removed by ramificationIdx_eq_one.

The fibre of P is its finite set of places, TauCeti.Place.finite_setOf_restrict_eq.

theorem TauCeti.Isogeny.isSplitCompletely {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) [Algebra W₂.FunctionField W₁.FunctionField] (h : ∀ (z : W₂.FunctionField), (algebraMap W₂.FunctionField W₁.FunctionField) z = φ.fieldPullback z) [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] [IsSepClosed F] (P : Place F W₂.FunctionField) : P.IsSplitCompletely

Over a separably closed field of constants every place splits completely in a separable isogeny (Silverman III.4.10(a) in its place-theoretic form).

theorem TauCeti.Isogeny.ncard_setOf_restrict_eq_degree {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) [Algebra W₂.FunctionField W₁.FunctionField] (h : ∀ (z : W₂.FunctionField), (algebraMap W₂.FunctionField W₁.FunctionField) z = φ.fieldPullback z) [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] [IsSepClosed F] (P : Place F W₂.FunctionField) : {P' : Place F W₁.FunctionField | Place.restrict F W₂.FunctionField P' = P}.ncard = φ.degree

A separable isogeny over a separably closed field of constants has exactly deg φ places above every place, the count form of Isogeny.isSplitCompletely read against the degree of the isogeny rather than against the degree of the field extension.