Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_WeierstrassCurve_GenusOnePic0.lean

definition module

Abel–Jacobi gate: degree-zero divisor classes versus Weierstrass points

Fix a field F (with decidable equality) and an affine Weierstrass curve W over F, and work with the function field W.FunctionField and with the places, divisors, degree, principal divisors and degree-zero class group AlgebraicCurve.Pic0 supplied by the project's divisor-class-group module (those notions are the project's own). Two assumptions are packaged as typeclasses carrying data or a theorem as fields. GenusOnePlaceGate W carries an explicit bijection pointEquivPlace : W.Point ≃ AlgebraicCurve.Place F W.FunctionField between the points of W (with its Mathlib group structure) and the places of the function field, together with the field deg_eq_one asserting that every place has degree 1; placeOfPoint is the forward map of this bijection, and the place attached to the origin plays the role of the place at infinity. AbelTheorem W is a Prop-valued class whose single field is Abel's theorem in the form: for every divisor D of degree 0, D is principal if and only if divisorSum D = 0.

The remaining declarations are consequences. degree_eq_sum says that, all residue degrees being 1, the degree of a divisor is the plain sum of its coefficients. divisorSum is the additive homomorphism from divisors to W.Point sending a single place v with multiplicity n to n \cdot \mathrm{pointEquivPlace}^{-1}(v), i.e. the Abel–Jacobi sum \sum_v n_v P_v computed in the group law of W. For a point P, pointDivisor P is the degree-zero divisor (P) - (O) and pointClass P its class in Pic0. Given both gates, divisorSum descends along the quotient to pic0ToPoint : Pic0 →+ W.Point, which is shown surjective (using pointClass) and injective (using the converse direction of Abel's theorem), yielding the additive isomorphism genusOnePic0Equiv : Pic0 F W.FunctionField ≃+ W.Point with inverse P \mapsto [(P) - (O)]; pointClass_add records that P \mapsto [(P)-(O)] is additive.

Relation to Mathlib

WeierstrassCurve.Affine, its point group W.Point and W.FunctionField are Mathlib's; the places, divisors, degree, principality and Pic0 used here come from the project's own algebraic-curve divisor module. Mathlib has no Abel–Jacobi identification of this kind, and neither the point–place dictionary nor Abel's theorem is proved here: both are hypotheses, stated as fields of the classes GenusOnePlaceGate and AbelTheorem.

Where it is used

The isomorphism \operatorname{Pic}^0(F(W)/F) \simeq W(F) provides the dictionary between divisor classes on a genus-one curve and points of the associated Weierstrass model, used in the parts of the development that compare Jacobians of modular curves with elliptic curves and that count points on reductions via the action on degree-zero divisor classes.

References

  1. J. H. Silverman, The Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 106, Springer, 1986 (Chapter III)
  2. H. Stichtenoth, Algebraic Function Fields and Codes, Springer, 2nd edition, 2009

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_WeierstrassCurve_GenusOnePic0.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_AlgebraicCurve_DivisorClassGroup

set_option autoImplicit false

noncomputable section

open AlgebraicCurve

namespace WeierstrassCurve.Affine

universe u

variable {F : Type u} [Field F] [DecidableEq F]

variable (W : Affine F) in

class GenusOnePlaceGate : Type u where

  pointEquivPlace : W.Point ≃ AlgebraicCurve.Place F W.FunctionField

  deg_eq_one : ∀ v : AlgebraicCurve.Place F W.FunctionField, v.deg = 1

variable {W : Affine F} [GenusOnePlaceGate W]

abbrev pointEquivPlace : W.Point ≃ AlgebraicCurve.Place F W.FunctionField :=
  GenusOnePlaceGate.pointEquivPlace (W := W)

def placeOfPoint : W.Point → AlgebraicCurve.Place F W.FunctionField :=
  pointEquivPlace (W := W)

@[simp]
theorem pointEquivPlace_apply (P : W.Point) :
    (pointEquivPlace (W := W)) P = placeOfPoint P := rfl

@[simp]
theorem pointEquivPlace_symm_placeOfPoint (P : W.Point) :
    (pointEquivPlace (W := W)).symm (placeOfPoint P) = P :=
  (pointEquivPlace (W := W)).symm_apply_apply P

theorem deg_eq_one (v : AlgebraicCurve.Place F W.FunctionField) : v.deg = 1 :=
  GenusOnePlaceGate.deg_eq_one v

@[simp]
theorem deg_placeOfPoint (P : W.Point) : (placeOfPoint (W := W) P).deg = 1 :=
  deg_eq_one _

theorem degree_eq_sum (D : AlgebraicCurve.Divisor F W.FunctionField) :
    Divisor.degree D = D.sum fun _ n => n := by
  rw [Divisor.degree, Finsupp.liftAddHom_apply]
  exact Finsupp.sum_congr fun v _ => by
    rw [AddMonoidHom.mulRight_apply, deg_eq_one v, Nat.cast_one, mul_one]

def divisorSum : AlgebraicCurve.Divisor F W.FunctionField →+ W.Point :=
  Finsupp.liftAddHom fun v => zmultiplesHom W.Point ((pointEquivPlace (W := W)).symm v)

@[simp]
theorem divisorSum_single (v : AlgebraicCurve.Place F W.FunctionField) (n : ℤ) :
    divisorSum (Finsupp.single v n) = n • (pointEquivPlace (W := W)).symm v :=
  Finsupp.liftAddHom_apply_single _ v n

theorem divisorSum_single_placeOfPoint (P : W.Point) (n : ℤ) :
    divisorSum (Finsupp.single (placeOfPoint P) n) = n • P := by
  rw [divisorSum_single, pointEquivPlace_symm_placeOfPoint]

def pointDivisor (P : W.Point) : Divisor.degZero (K := F) (F := W.FunctionField) :=
  ⟨Finsupp.single (placeOfPoint P) 1 - Finsupp.single (placeOfPoint (0 : W.Point)) 1, by
    rw [Divisor.mem_degZero, map_sub, Divisor.degree_single, Divisor.degree_single,
      deg_placeOfPoint, deg_placeOfPoint, sub_self]⟩

@[simp]
theorem coe_pointDivisor (P : W.Point) :
    (pointDivisor P : AlgebraicCurve.Divisor F W.FunctionField)
      = Finsupp.single (placeOfPoint P) 1 - Finsupp.single (placeOfPoint (0 : W.Point)) 1 :=
  rfl

@[simp]
theorem pointDivisor_zero : pointDivisor (0 : W.Point) = 0 :=
  Subtype.ext (sub_self _)

theorem divisorSum_pointDivisor (P : W.Point) :
    divisorSum (pointDivisor P : AlgebraicCurve.Divisor F W.FunctionField) = P := by
  rw [coe_pointDivisor, map_sub, divisorSum_single_placeOfPoint, divisorSum_single_placeOfPoint,
    one_smul, one_smul, sub_zero]

def pointClass (P : W.Point) : AlgebraicCurve.Pic0 F W.FunctionField :=
  Pic0.mk (pointDivisor P)

@[simp]
theorem pointClass_zero : pointClass (0 : W.Point) = 0 := by
  rw [pointClass, pointDivisor_zero, Pic0.mk_zero]

variable (W) in

class AbelTheorem : Prop where

  isPrincipal_iff_divisorSum_eq_zero :
    ∀ D : AlgebraicCurve.Divisor F W.FunctionField, Divisor.degree D = 0 →
      (Divisor.IsPrincipal D ↔ divisorSum D = 0)

section AbelTheorem

variable [AbelTheorem W]

theorem divisorSum_eq_zero_of_isPrincipal {D : AlgebraicCurve.Divisor F W.FunctionField}
    (h0 : Divisor.degree D = 0) (hD : Divisor.IsPrincipal D) : divisorSum D = 0 :=
  (AbelTheorem.isPrincipal_iff_divisorSum_eq_zero D h0).mp hD

theorem isPrincipal_of_divisorSum_eq_zero {D : AlgebraicCurve.Divisor F W.FunctionField}
    (h0 : Divisor.degree D = 0) (hD : divisorSum D = 0) : Divisor.IsPrincipal D :=
  (AbelTheorem.isPrincipal_iff_divisorSum_eq_zero D h0).mpr hD

def pic0ToPoint : AlgebraicCurve.Pic0 F W.FunctionField →+ W.Point :=
  QuotientAddGroup.lift _
    (divisorSum.comp (Divisor.degZero (K := F) (F := W.FunctionField)).subtype)
    (by
      rintro ⟨D, hD0⟩ hD
      rw [AddSubgroup.mem_addSubgroupOf] at hD
      rw [AddMonoidHom.mem_ker, AddMonoidHom.comp_apply, AddSubgroup.coe_subtype]
      exact divisorSum_eq_zero_of_isPrincipal (Divisor.mem_degZero.mp hD0)
        (Divisor.mem_principal.mp hD))

@[simp]
theorem pic0ToPoint_mk (D : Divisor.degZero (K := F) (F := W.FunctionField)) :
    pic0ToPoint (Pic0.mk D) = divisorSum (D : AlgebraicCurve.Divisor F W.FunctionField) :=
  rfl

@[simp]
theorem pic0ToPoint_pointClass (P : W.Point) : pic0ToPoint (pointClass P) = P := by
  rw [pointClass, pic0ToPoint_mk, divisorSum_pointDivisor]

theorem pic0ToPoint_surjective : Function.Surjective (pic0ToPoint (W := W)) := fun P =>
  ⟨pointClass P, pic0ToPoint_pointClass P⟩

theorem pic0ToPoint_injective : Function.Injective (pic0ToPoint (W := W)) := by
  rw [injective_iff_map_eq_zero]
  intro c
  induction c using QuotientAddGroup.induction_on with
  | H D =>
    intro hD
    obtain ⟨D, hD0⟩ := D
    replace hD : divisorSum D = 0 := hD
    rw [QuotientAddGroup.eq_zero_iff, AddSubgroup.mem_addSubgroupOf]
    exact Divisor.mem_principal.mpr
      (isPrincipal_of_divisorSum_eq_zero (Divisor.mem_degZero.mp hD0) hD)

variable (W) in

def genusOnePic0Equiv : AlgebraicCurve.Pic0 F W.FunctionField ≃+ W.Point :=
  AddEquiv.ofBijective pic0ToPoint ⟨pic0ToPoint_injective, pic0ToPoint_surjective⟩

@[simp]
theorem genusOnePic0Equiv_apply (c : AlgebraicCurve.Pic0 F W.FunctionField) :
    genusOnePic0Equiv W c = pic0ToPoint c := rfl

@[simp]
theorem genusOnePic0Equiv_symm_apply (P : W.Point) :
    (genusOnePic0Equiv W).symm P = pointClass P :=
  (genusOnePic0Equiv W).injective (by
    rw [AddEquiv.apply_symm_apply, genusOnePic0Equiv_apply, pic0ToPoint_pointClass])

theorem pointClass_add (P Q : W.Point) :
    pointClass (P + Q) = pointClass P + pointClass Q := by
  rw [← genusOnePic0Equiv_symm_apply, ← genusOnePic0Equiv_symm_apply,
    ← genusOnePic0Equiv_symm_apply, ← map_add]

end AbelTheorem

end WeierstrassCurve.Affine

end

Statements phrased using this module (3)