The Kummer character of an isogeny

Let φ : W₁ → W₂ be an isogeny of elliptic curves over a field F, and g a nonzero function on W₁ whose n-th power is pulled back along φ. The translations by the points of ker φ fix every pulled-back function, so each of them moves g by an n-th root of unity, and these roots of unity are constants because F is integrally closed in F(W₁). The resulting homomorphism S ↦ τ_S g / g from ker φ to the n-th roots of unity of F is the Kummer character of g.

Main definitions

• TauCeti.Isogeny.kummerCharacter: the character S ↦ τ_S g / g of ker φ.

Main results

• TauCeti.Isogeny.algebraMap_kummerCharacter: its value at S, read in F(W₁), is τ_S g / g.
• TauCeti.Isogeny.kummerCharacter_mul: it is multiplicative in g.
• TauCeti.Isogeny.kummerCharacter_eq_one_iff: it is trivial exactly when g is fixed by the translations by ker φ; in particular it is trivial on a pulled-back function (TauCeti.Isogeny.kummerCharacter_eq_one_of_mem_fieldRange).
• TauCeti.Isogeny.kummerCharacter_eq_of_principal_eq: it depends on g only through its divisor, two functions with the same divisor differing by a constant; so does the condition that gⁿ be a pullback (TauCeti.Isogeny.pow_mem_fieldRange_of_principal_eq).

In Silverman's construction (AEC III.8.1), for T ∈ E[N] one takes g_T with g_T^N = [N]^* f_T, where div f_T = N (T) - N (O), and sets e_N(S, T) = τ_S g_T / g_T. That is this character, at φ = [N], n = N and g = g_T, evaluated at S; its multiplicativity in S is the bilinearity of the pairing in its first variable.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.8.1.

noncomputable def TauCeti.Isogeny.kummerCharacter {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] (φ : Isogeny W₁ W₂) (n : ℕ) [NeZero n] (g : W₁.FunctionFieldˣ) (hg : ↑g ^ n ∈ φ.fieldPullback.fieldRange) : Multiplicative ↥φ.ker →* ↥(rootsOfUnity n F)

The Kummer character of an isogeny: for a unit g of F(W₁) whose n-th power is pulled back along φ, the homomorphism S ↦ τ_S g / g from ker φ to the n-th roots of unity of F.

Equations

• φ.kummerCharacter n g hg = (TauCeti.Isogeny.kerTranslationHom✝ φ).kummerCharacter n g ⋯

@[simp]

theorem TauCeti.Isogeny.algebraMap_kummerCharacter {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] {φ : Isogeny W₁ W₂} {n : ℕ} [NeZero n] {g : W₁.FunctionFieldˣ} (hg : ↑g ^ n ∈ φ.fieldPullback.fieldRange) (S : Multiplicative ↥φ.ker) : (algebraMap F W₁.FunctionField) ↑↑((φ.kummerCharacter n g hg) S) = (W₁.translation ↑(Multiplicative.toAdd S)) ↑g / ↑g

The value of the Kummer character, read in F(W₁): τ_S g / g.

theorem TauCeti.Isogeny.kummerCharacter_mul {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] {φ : Isogeny W₁ W₂} {n : ℕ} [NeZero n] {g h : W₁.FunctionFieldˣ} (hg : ↑g ^ n ∈ φ.fieldPullback.fieldRange) (hh : ↑h ^ n ∈ φ.fieldPullback.fieldRange) : φ.kummerCharacter n (g * h) ⋯ = φ.kummerCharacter n g hg * φ.kummerCharacter n h hh

The Kummer character is multiplicative in g; (g h)ⁿ = gⁿ hⁿ is pulled back when both factors are.

theorem TauCeti.Isogeny.kummerCharacter_eq_one_iff {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] {φ : Isogeny W₁ W₂} {n : ℕ} [NeZero n] {g : W₁.FunctionFieldˣ} (hg : ↑g ^ n ∈ φ.fieldPullback.fieldRange) : φ.kummerCharacter n g hg = 1 ↔ ↑g ∈ W₁.translationFixedField φ.ker

The Kummer character is trivial exactly when the kernel translations fix g.

theorem TauCeti.Isogeny.kummerCharacter_eq_one_of_mem_fieldRange {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] {φ : Isogeny W₁ W₂} {n : ℕ} [NeZero n] {g : W₁.FunctionFieldˣ} (hmem : ↑g ∈ φ.fieldPullback.fieldRange) : φ.kummerCharacter n g ⋯ = 1

The Kummer character of a pulled-back function is trivial: the kernel translations fix every pullback.

theorem TauCeti.Isogeny.pow_mem_fieldRange_of_principal_eq {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] {φ : Isogeny W₁ W₂} {n : ℕ} {g g' : W₁.FunctionFieldˣ} (hg : ↑g ^ n ∈ φ.fieldPullback.fieldRange) (h : Divisor.principal ⋯ g = Divisor.principal ⋯ g') : ↑g' ^ n ∈ φ.fieldPullback.fieldRange

Whether gⁿ is pulled back along φ depends only on the divisor of g: two functions with the same divisor differ by a constant, and the constants are pullbacks.

theorem TauCeti.Isogeny.kummerCharacter_eq_of_principal_eq {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] {φ : Isogeny W₁ W₂} {n : ℕ} [NeZero n] {g g' : W₁.FunctionFieldˣ} (hg : ↑g ^ n ∈ φ.fieldPullback.fieldRange) (h : Divisor.principal ⋯ g = Divisor.principal ⋯ g') : φ.kummerCharacter n g hg = φ.kummerCharacter n g' ⋯

The Kummer character depends on g only through its divisor: two functions with the same divisor differ by a constant, which every translation fixes.