The pullback of a point along [n]

Let W be an elliptic curve over a field F and n an integer invertible in F. The coefficient of [n]^* D at the place of a point R is the coefficient of D at the place of n • R. Over a separably closed field, pulling the divisor (T) of a point back along multiplication by n gives the points R with n • R = T, each with multiplicity one.

At an n-torsion point T, the divisor [n]^* (T) - [n]^* (O) is principal. This is the second input to the divisor construction of the Weil pairing (Silverman III.8.1), after WeierstrassCurve.Affine.exists_principal_eq_zsmul_ofPoint_sub_infinity: the pairing is built from a function with this divisor.

Main definitions

• TauCeti.Isogeny.weilPairingDivisor: the divisor [n]^* (T) - [n]^* (O).

Main results

• TauCeti.Isogeny.coeff_divisorPullback_mulByIntIsogeny: the coefficient of [n]^* D at the place of R is the coefficient of D at the place of n • R.
• TauCeti.Isogeny.divisorPullback_mulByIntIsogeny_ofPoint: over a separably closed field, [n]^* (T) = ∑_{n • R = T} (R).
• TauCeti.Isogeny.weilPairingDivisor_eq_sum: with n • R₀ = T, the divisor [n]^* (T) - [n]^* (O) is ∑_{n • S = O} ((R₀ + S) - (S)).
• TauCeti.Isogeny.exists_principal_eq_weilPairingDivisor: at an n-torsion point T, [n]^* (T) - [n]^* (O) is the divisor of a function.

The place-level inputs are in Isogeny/MulByInt/PointPlace.lean (isEquiv_comap_valuation_pointEquivDegreeOnePlace_iff, finite_setOf_zsmul_eq, restrict_eq_pointEquivDegreeOnePlace_iff), and the torsion counts on the points of W in Isogeny/MulByInt/IsSepClosed.lean.

References

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

Prior art

AINTLIB (github.com/CBirkbeck/AINTLIB @ f622f4aa0bd7b9d8b8cb931b5f8cb709f1d179e2, Apache-2.0) proves both results in its own divisor framework, in projects/HasseWeil/HasseWeil/HasseBound/WeilPairing/: Pullback.lean defines the fibre divisor pullbackDiv combinatorially, DivisorPullback.lean's projectiveDivisorOf_pullback_eq_pullbackDivisor identifies it with the divisor of k ∘ φ by per-place order transport over an algebraically closed field, and WeilFunction.lean's pullbackDiv_sub_isPrincipal (used by Pairing.lean's weilFunction_isPrincipal) proves the fibre difference principal. Nothing is ported: here the pullback is the conorm TauCeti.Isogeny.divisorPullback, read off places.

theorem TauCeti.Isogeny.instIsDedekindDomainCoordinateRingToAffine_1 {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.

@[simp]

theorem TauCeti.Isogeny.coeff_divisorPullback_mulByIntIsogeny {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) [W.IsElliptic] {n : ℤ} (hchar : ↑n ≠ 0) (D : Divisor F W.toAffine.FunctionField) (R : W.toAffine.Point) : AlgebraicGeometry.WeilDivisor.coeff (((mulByIntIsogeny W ⋯).divisorPullback ⋯) D) ↑(W.toAffine.pointEquivDegreeOnePlace R) = AlgebraicGeometry.WeilDivisor.coeff D ↑(W.toAffine.pointEquivDegreeOnePlace (n • R))

The coefficient of [n]^* D at the place of R is the coefficient of D at the place of n • R, for n invertible in F: the place of R lies over that of n • R, and [n] is unramified, being separable.

noncomputable def TauCeti.Isogeny.weilPairingDivisor {F : Type u_1} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] {n : ℤ} (hn : psiFunctionField W n ≠ 0) (T : W.toAffine.Point) : Divisor F W.toAffine.FunctionField

The divisor [n]^* (T) - [n]^* (O), the pullback along [n] of (T) - (O). The Weil pairing is built from a function with this divisor (Silverman III.8.1).

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Isogeny.weilPairingDivisor_def {F : Type u_1} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] {n : ℤ} (hn : psiFunctionField W n ≠ 0) (T : W.toAffine.Point) : weilPairingDivisor W hn T = ((mulByIntIsogeny W hn).divisorPullback ⋯) (AlgebraicGeometry.WeilDivisor.ofPoint ↑(W.toAffine.pointEquivDegreeOnePlace T)) - ((mulByIntIsogeny W hn).divisorPullback ⋯) (AlgebraicGeometry.WeilDivisor.ofPoint (Place.infinity W.toAffine))

The defining equation of weilPairingDivisor.

@[simp]

theorem TauCeti.Isogeny.divisorPullback_mulByIntIsogeny_ofPoint {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) [W.IsElliptic] [IsSepClosed F] {n : ℤ} (hchar : ↑n ≠ 0) (T : W.toAffine.Point) : ((mulByIntIsogeny W ⋯).divisorPullback ⋯) (AlgebraicGeometry.WeilDivisor.ofPoint ↑(W.toAffine.pointEquivDegreeOnePlace T)) = ∑ R ∈ ⋯.toFinset, AlgebraicGeometry.WeilDivisor.ofPoint ↑(W.toAffine.pointEquivDegreeOnePlace R)

The pullback of a point along [n] is its fibre: over a separably closed field in which n is invertible, [n]^* (T) = ∑_{n • R = T} (R).

The divisor [n]^* (T) - [n]^* (O)

theorem TauCeti.Isogeny.weilPairingDivisor_eq_sum {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) [W.IsElliptic] [IsSepClosed F] {n : ℤ} (hchar : ↑n ≠ 0) {T R₀ : W.toAffine.Point} (hR₀ : n • R₀ = T) : weilPairingDivisor W ⋯ T = ∑ S ∈ ⋯.toFinset, (AlgebraicGeometry.WeilDivisor.ofPoint ↑(W.toAffine.pointEquivDegreeOnePlace (R₀ + S)) - AlgebraicGeometry.WeilDivisor.ofPoint ↑(W.toAffine.pointEquivDegreeOnePlace S))

[n]^* (T) - [n]^* (O) is the translate of the fibre over O minus that fibre: for any R₀ with n • R₀ = T, it is ∑_{n • S = O} ((R₀ + S) - (S)), over a separably closed field in which n is invertible.

theorem TauCeti.Isogeny.exists_principal_eq_weilPairingDivisor {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) [W.IsElliptic] [IsSepClosed F] {n : ℤ} (hchar : ↑n ≠ 0) {T : W.toAffine.Point} (hT : n • T = 0) : ∃ (z : W.toAffine.FunctionFieldˣ), Divisor.principal ⋯ z = weilPairingDivisor W ⋯ T

[n]^* (T) - [n]^* (O) is principal at an n-torsion point T, over a separably closed field in which n is invertible (Silverman III.8.1). A function with this divisor is the function g_T from which the Weil pairing is built.