Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_EllipticCurve_WeilPairingFun.lean

definition module

Weil functions and a point-level Weil pairing constant

Throughout, W is a Weierstrass curve over a field R and K is a field equipped with an R-algebra structure; (W⁄K) denotes the base-changed affine curve, with its coordinate ring (W⁄K).CoordinateRing, its function field (W⁄K).FunctionField and its group of points (W⁄K).Point. For a point P, placeIdeal W K P is the unit ideal when P = 0 and otherwise the underlying ideal of the height-one place placeOf W K P, namely the maximal ideal (x - x_P,\,y - y_P) of the coordinate ring cut out by the affine point P; the two accompanying lemmas record these two cases. For n \in \mathbb{Z} and a point Q, fibSet W K n Q is the set \{P : n \cdot P = Q\}, with membership unfolding by definition, and fibIdeal W K n Q is the product of placeIdeal W K P over that set when it is finite (the finite set being taken in the sense of Set.Finite.toFinset), and the unit ideal otherwise. weilNum W K n T is a chosen generator of fibIdeal W K n T when that ideal is principal, and 1 otherwise; span_weilNum states that under principality the span of this element is the ideal. The Weil function weilFun W K n T is then the quotient, in the function field, of the images of weilNum W K n T and weilNum W K n 0.

Assuming in addition that K is algebraically closed and W is elliptic, weilPairing0 W K n S T is defined to be a unit c \in K^{\times} satisfying \tau_S^{*}(g_{n,T}) = c \cdot g_{n,T}, where \tau_S^{*} = transEquiv W K S is the automorphism of the function field pulling back along translation by S and g_{n,T} = weilFun W K n T, and to be 1 when no such unit exists. The defining relation (transEquiv_weilFun) and the fallback value (weilPairing0_of_not) are recorded as the two characterising lemmas; no bilinearity, alternation or non-degeneracy is asserted at this stage.

Relation to Mathlib

Mathlib supplies the affine coordinate ring of a Weierstrass curve, its ideals XYIdeal/XClass/YClass and the group of affine points; the places attached to points, the translation automorphisms of the function field, and the Weil functions and pairing constant defined here are the project's own, Mathlib having no Weil pairing.

Where it is used

These Weil functions and the constant e_0 attached to a pair of points are the basis for the project's treatment of the Weil pairing on n-torsion, whose bilinearity, alternation and Galois equivariance give the determinant of the mod-n representation attached to an elliptic curve as the cyclotomic character.

References

  1. J. H. Silverman, The Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 106, Springer, 1986, III.8

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_EllipticCurve_WeilPairingFun.lean

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_EllipticCurve_FunctionFieldPullback

namespace WeierstrassCurve.Affine

section WeilPairingDefs

variable {R : Type*} [Field R] (W : WeierstrassCurve R) (K : Type*) [Field K] [Algebra R K]
  [DecidableEq K]

open Classical in

noncomputable def placeIdeal (P : (W⁄K).Point) : Ideal (W⁄K).CoordinateRing :=
  if hP : P = 0 then ⊤ else (placeOf W K P hP).asIdeal

theorem placeIdeal_zero : placeIdeal W K 0 = ⊤ := dif_pos rfl

theorem placeIdeal_of_ne_zero {P : (W⁄K).Point} (hP : P ≠ 0) :
    placeIdeal W K P = (placeOf W K P hP).asIdeal := dif_neg hP

def fibSet (n : ℤ) (Q : (W⁄K).Point) : Set (W⁄K).Point := {P | n • P = Q}

@[simp] theorem mem_fibSet {n : ℤ} {Q P : (W⁄K).Point} : P ∈ fibSet W K n Q ↔ n • P = Q := Iff.rfl

open Classical in

noncomputable def fibIdeal (n : ℤ) (Q : (W⁄K).Point) : Ideal (W⁄K).CoordinateRing :=
  if h : (fibSet W K n Q).Finite then ∏ P ∈ h.toFinset, placeIdeal W K P else ⊤

theorem fibIdeal_eq {n : ℤ} {Q : (W⁄K).Point} (h : (fibSet W K n Q).Finite) :
    fibIdeal W K n Q = ∏ P ∈ h.toFinset, placeIdeal W K P := by
  rw [fibIdeal, dif_pos h]

open Classical in

noncomputable def weilNum (n : ℤ) (T : (W⁄K).Point) : (W⁄K).CoordinateRing :=
  if h : (fibIdeal W K n T).IsPrincipal then @Submodule.IsPrincipal.generator _ _ _ _ _ _ h else 1

theorem span_weilNum {n : ℤ} {T : (W⁄K).Point} (h : (fibIdeal W K n T).IsPrincipal) :
    Ideal.span {weilNum W K n T} = fibIdeal W K n T := by
  rw [weilNum, dif_pos h]
  exact @Ideal.span_singleton_generator _ _ _ h

noncomputable def weilFun (n : ℤ) (T : (W⁄K).Point) : (W⁄K).FunctionField :=
  algebraMap _ (W⁄K).FunctionField (weilNum W K n T) / algebraMap _ (W⁄K).FunctionField (weilNum W K n 0)

open Classical in

noncomputable def weilPairing0 [IsAlgClosed K] [W.IsElliptic] (n : ℤ) (S T : (W⁄K).Point) : Kˣ :=
  if h : ∃ c : Kˣ, transEquiv W K S (weilFun W K n T) =
      algebraMap K (W⁄K).FunctionField (c : K) * weilFun W K n T
  then h.choose else 1

theorem transEquiv_weilFun [IsAlgClosed K] [W.IsElliptic] {n : ℤ} {S T : (W⁄K).Point}
    (h : ∃ c : Kˣ, transEquiv W K S (weilFun W K n T) =
      algebraMap K (W⁄K).FunctionField (c : K) * weilFun W K n T) :
    transEquiv W K S (weilFun W K n T) =
      algebraMap K (W⁄K).FunctionField (weilPairing0 W K n S T : K) * weilFun W K n T := by
  rw [weilPairing0, dif_pos h]
  exact h.choose_spec

theorem weilPairing0_of_not [IsAlgClosed K] [W.IsElliptic] {n : ℤ} {S T : (W⁄K).Point}
    (h : ¬ ∃ c : Kˣ, transEquiv W K S (weilFun W K n T) =
      algebraMap K (W⁄K).FunctionField (c : K) * weilFun W K n T) :
    weilPairing0 W K n S T = 1 := by
  rw [weilPairing0, dif_neg h]

end WeilPairingDefs

end WeierstrassCurve.Affine

Statements phrased using this module (100)