Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.Isogeny.MulByInt.WeilPairing.Basic

The Weil pairing #

Let W be an elliptic curve over a separably closed field F and N a positive integer invertible in F. For T ∈ E[N] the divisor [N]^* (T) - [N]^* (O) is principal (TauCeti.Isogeny.exists_principal_eq_weilPairingDivisor); let g_T be a function with that divisor. Its N-th power has divisor [N]^* (N (T) - N (O)), the pullback of a principal divisor, so g_T ^ N is itself a pullback along [N]. The translations by the N-torsion fix every pullback, so they move g_T by N-th roots of unity, and these are constants: the Kummer character of g_T (TauCeti.Isogeny.kummerCharacter). The Weil pairing is

e_N(S, T) = τ_S g_T / g_T,

independent of the choice of g_T, since two choices differ by a constant. It is additive in S because the Kummer character is a homomorphism, and additive in T because g_{T₁} g_{T₂} [N]^* h, with h a function of divisor (T₁ + T₂) - (T₁) - (T₂) + (O), is a choice of g_{T₁ + T₂} and the Kummer character of the pullback [N]^* h is trivial. It is nondegenerate in T: if e_N(·, T) is trivial then g_T is fixed by the N-torsion translations, hence a pullback [N]^* h, and div h = (T) - (O) forces T = O.

It is alternating: e_N(T, T) = 1. Together with bilinearity, this gives skew-symmetry and, using nondegeneracy in T, nondegeneracy in S.

This is the construction of Silverman III.8.1, with the proofs of its parts (a)–(c). It is a divisor construction, and its inputs are the divisor calculus of the function field and the fibre of [N]; it does not use Weil reciprocity, which the alternative construction through evaluation of functions on divisors requires.

Main definitions #

Main results #

References #

source
theorem TauCeti.Isogeny.instIsDedekindDomainCoordinateRingToAffine_2 {F : Type u_1} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] :
IsDedekindDomain W.toAffine.CoordinateRing

The coordinate ring of an elliptic curve is a Dedekind domain.

source
theorem TauCeti.Isogeny.zpow_mem_fieldRange_mulByIntIsogeny {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) [W.IsElliptic] {n : ℤ} (hn : psiFunctionField W n ≠ 0) {T : W.toAffine.Point} (hT : n • T = 0) {g : W.toAffine.FunctionFieldˣ} (hg : Divisor.principal ⋯ g = weilPairingDivisor W hn T) :
↑g ^ n ∈ (mulByIntIsogeny W hn).fieldPullback.fieldRange

A function with divisor [n]^* (T) - [n]^* (O) has its n-th power pulled back along [n], at an n-torsion point T: that power has divisor [n]^* (n (T) - n (O)), the pullback of a principal divisor.

source
noncomputable def TauCeti.Isogeny.weilPairing {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) [W.IsElliptic] [IsSepClosed F] (N : ℕ) [NeZero N] (hN : ↑N ≠ 0) :
↥(Submodule.torsionBy ℤ W.toAffine.Point ↑N) →+ ↥(Submodule.torsionBy ℤ W.toAffine.Point ↑N) →+ Additive ↥(rootsOfUnity N F)

The Weil pairing e_N(S, T) = τ_S g_T / g_T (Silverman III.8.1), over a separably closed field in which N is invertible, additive in both variables.

Equations
Instances For
    source
    theorem TauCeti.Isogeny.algebraMap_weilPairing {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) [W.IsElliptic] [IsSepClosed F] (N : ℕ) [NeZero N] (hN : ↑N ≠ 0) {S T : ↥(Submodule.torsionBy ℤ W.toAffine.Point ↑N)} {g : W.toAffine.FunctionFieldˣ} {hψ : psiFunctionField W ↑N ≠ 0} (hg : Divisor.principal ⋯ g = weilPairingDivisor W hψ ↑T) :
    (algebraMap F W.toAffine.FunctionField) ↑↑(Additive.toMul (((weilPairing W N hN) S) T)) = (W.toAffine.translation ((WeierstrassCurve.Affine.Point.equivBaseChangeSelf W.toAffine) ↑S)) ↑g / ↑g

    The value of the Weil pairing: e_N(S, T) = τ_S g / g for every function g with divisor [N]^* (T) - [N]^* (O).

    source
    theorem TauCeti.Isogeny.weilPairing_eq_zero_iff {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) [W.IsElliptic] [IsSepClosed F] (N : ℕ) [NeZero N] (hN : ↑N ≠ 0) {S T : ↥(Submodule.torsionBy ℤ W.toAffine.Point ↑N)} {g : W.toAffine.FunctionFieldˣ} {hψ : psiFunctionField W ↑N ≠ 0} (hg : Divisor.principal ⋯ g = weilPairingDivisor W hψ ↑T) :
    ((weilPairing W N hN) S) T = 0 ↔ (W.toAffine.translation ((WeierstrassCurve.Affine.Point.equivBaseChangeSelf W.toAffine) ↑S)) ↑g = ↑g

    The vanishing criterion for the Weil pairing: e_N(S, T) = 1 exactly when translation by S fixes a function g with divisor [N]^* (T) - [N]^* (O).

    source
    theorem TauCeti.Isogeny.eq_zero_of_forall_weilPairing_eq_zero {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) [W.IsElliptic] [IsSepClosed F] (N : ℕ) [NeZero N] (hN : ↑N ≠ 0) {T : ↥(Submodule.torsionBy ℤ W.toAffine.Point ↑N)} (hT : ∀ (S : ↥(Submodule.torsionBy ℤ W.toAffine.Point ↑N)), ((weilPairing W N hN) S) T = 0) :
    T = 0

    The Weil pairing is nondegenerate in its second variable: if e_N(S, T) = 1 for every S, then T = O.

    source
    @[simp]
    theorem TauCeti.Isogeny.weilPairing_self {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) [W.IsElliptic] [IsSepClosed F] (N : ℕ) [NeZero N] (hN : ↑N ≠ 0) (T : ↥(Submodule.torsionBy ℤ W.toAffine.Point ↑N)) :
    ((weilPairing W N hN) T) T = 0

    The Weil pairing is alternating: e_N(T, T) = 1 (Silverman III.8.1(b)).

    source
    theorem TauCeti.Isogeny.neg_weilPairing {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) [W.IsElliptic] [IsSepClosed F] (N : ℕ) [NeZero N] (hN : ↑N ≠ 0) (S T : ↥(Submodule.torsionBy ℤ W.toAffine.Point ↑N)) :
    -((weilPairing W N hN) S) T = ((weilPairing W N hN) T) S

    The Weil pairing is skew-symmetric: e_N(S, T)⁻¹ = e_N(T, S).

    source
    theorem TauCeti.Isogeny.weilPairing_nondegenerate {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) [W.IsElliptic] [IsSepClosed F] (N : ℕ) [NeZero N] (hN : ↑N ≠ 0) {S : ↥(Submodule.torsionBy ℤ W.toAffine.Point ↑N)} (hS : ∀ (T : ↥(Submodule.torsionBy ℤ W.toAffine.Point ↑N)), ((weilPairing W N hN) S) T = 0) :
    S = 0

    The Weil pairing is nondegenerate in its first variable: if e_N(S, T) = 1 for every T, then S = O.