Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_Isogeny_ConditionalCurrency.lean

definition module

Pic⁰ pushforward along function-field maps; isogeny data on points

The first part descends the divisor pushforward along an integral K-algebra map \varphi : F \to F' of fields to divisor classes. AlgebraicCurve.Pic0.pushforwardAlongDegZero restricts Divisor.pushforwardAlong φ hφ (on places: w \mapsto f(w)\,[w|_F], where w|_F is the restriction of the valuation subring and f(w) the residue-extension degree) to the degree-zero subgroups, which is legitimate because pushforward preserves degree; pushforwardAlongHom then quotients by principal divisors, using two extra explicit hypotheses: hfin : FiniteAlong K φ, i.e. F' is a finite F-module via \varphi, and hN : NormFormulaAlong K φ hfin, the project's predicate asserting that for every f \in F'^\times the pushforward of \mathrm{div}(f) is \mathrm{div}(N_{F'/F}f) — a hypothesis, not a theorem. Place.deg_restrictAlong_mul_inertiaDegAlong records \deg(w|_F)\cdot f(w) = \deg(w).

The second part fixes an algebraically closed field F of characteristic zero, elliptic V,W in affine Weierstrass form carrying the classes GenusOnePlaceGate (data: a bijection W(F) \simeq places of F(W), all residue degrees 1) and AbelTheorem (a degree-zero divisor is principal iff its image under divisorSum vanishes), and an integral F-algebra map \iota : F(V) \to F(W). Since all residue degrees are 1, all inertia degrees are 1 and pushforward carries n[w] to n[w|_{F(V)}]. Conjugating pushforwardAlongHom by the Abel–Jacobi isomorphisms genusOnePic0Equiv gives pointMapOfPushforward : W.Point →+ V.Point. A group of three lemmas in a common shape says that any map g of point sets with g(0)=0 which matches \iota on places, (\mathrm{place}\,P)|_{F(V)} = \mathrm{place}\,g(P), equals this homomorphism, hence is additive, and that g(P)=0 exactly when the class of (P)-(0) pushes forward to zero. Finally IsogenyEndDatum W and IsogenyHomDatum V₀ V₁ bundle (\iota,\ \text{integrality},\ \text{finiteness}) — note the contravariance: the latter has \iota : F(V_1) \to F(V_0) and yields pointHom : V₀.Point →+ V₁.Point; isogenyEndSubring is the subring of AddMonoid.End W.Point generated by all pointEnd, given norm-formula witnesses for every datum.

Relation to Mathlib

Places, divisors, principal divisors and \mathrm{Pic}^0 of a function field in this valuation-subring formulation are the project's own; Mathlib supplies the ambient algebra (Finsupp, QuotientAddGroup, AddMonoid.End, Subring.closure, Algebra.norm, residue fields of local rings) and WeierstrassCurve.Affine with its group of points, but no divisor-class theory for curves and no isogeny-induced maps of this kind.

Where it is used

This is the mechanism by which an inclusion of function fields of elliptic curves is turned into an additive map of point groups, so that endomorphism rings and isogeny-induced homomorphisms can be manipulated group-theoretically. The GenusOnePlaceGate datum is an arbitrary point–place bijection with all residue degrees one, so statements identifying these maps with named geometric maps require further hypotheses pinning the dictionary.

References

  1. J. H. Silverman, The Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 106, Springer, 1986, Chapters II–III
  2. H. Stichtenoth, Algebraic Function Fields and Codes, Springer, 1993, Chapter III

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_AlgebraicCurve_Correspondence
import Definitions.Def_WeierstrassCurve_GenusOnePic0

set_option autoImplicit false

noncomputable section IsogenyCurrency

section Delta

namespace AlgebraicCurve

variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']

namespace Pic0

variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
variable (hfin : FiniteAlong K φ) (hN : NormFormulaAlong K φ hfin)

def pushforwardAlongDegZero :
    Divisor.degZero (K := K) (F := F') →+ Divisor.degZero (K := K) (F := F) :=
  ((Divisor.pushforwardAlong φ hφ).domRestrict
    (Divisor.degZero (K := K) (F := F'))).codRestrict _
    (fun D => Divisor.pushforwardAlong_mem_degZero φ hφ D.2)

@[simp]
theorem coe_pushforwardAlongDegZero (D : Divisor.degZero (K := K) (F := F')) :
    (pushforwardAlongDegZero φ hφ D : Divisor K F) =
      Divisor.pushforwardAlong φ hφ (D : Divisor K F') :=
  rfl

def pushforwardAlongHom : Pic0 K F' →+ Pic0 K F :=
  QuotientAddGroup.map _ _ (pushforwardAlongDegZero φ hφ) (by
    rintro ⟨D, hD0⟩ hD
    simp only [AddSubgroup.mem_addSubgroupOf] at hD ⊢
    exact Divisor.isPrincipal_pushforwardAlong φ hφ hfin hN hD)

theorem pushforwardAlongHom_mk (D : Divisor.degZero (K := K) (F := F')) :
    pushforwardAlongHom φ hφ hfin hN (mk D) = mk (pushforwardAlongDegZero φ hφ D) :=
  rfl

end Pic0

end AlgebraicCurve

end Delta

open AlgebraicCurve

namespace AlgebraicCurve

variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']

theorem Place.deg_restrictAlong_mul_inertiaDegAlong (φ : F →ₐ[K] F')
    (hφ : φ.toRingHom.IsIntegral) (w : Place K F') :
    (w.restrictAlong φ hφ).deg * w.inertiaDegAlong φ hφ = w.deg := by
  letI := algebraAlong φ
  haveI := isScalarTower_along φ
  haveI := isIntegral_along φ hφ
  exact w.deg_restrict_mul_inertiaDeg

end AlgebraicCurve

namespace WeierstrassCurve.Affine

universe u

variable {F : Type u} [Field F] [DecidableEq F] [IsAlgClosed F] [CharZero F]
variable {V W : Affine F} [V.IsElliptic] [W.IsElliptic]
variable [GenusOnePlaceGate V] [AbelTheorem V] [GenusOnePlaceGate W] [AbelTheorem W]
variable (ι : V.FunctionField →ₐ[F] W.FunctionField) (hι : ι.toRingHom.IsIntegral)

theorem inertiaDegAlong_eq_one (w : AlgebraicCurve.Place F W.FunctionField) :
    w.inertiaDegAlong ι hι = 1 := by
  have h := AlgebraicCurve.Place.deg_restrictAlong_mul_inertiaDegAlong ι hι w
  rw [deg_eq_one (W := V) (w.restrictAlong ι hι), deg_eq_one (W := W) w, one_mul] at h
  exact h

theorem pushforwardAlong_single_eq (w : AlgebraicCurve.Place F W.FunctionField) (n : ℤ) :
    Divisor.pushforwardAlong ι hι (Finsupp.single w n)
      = Finsupp.single (w.restrictAlong ι hι) n := by
  rw [Divisor.pushforwardAlong_single, inertiaDegAlong_eq_one ι hι w, Nat.cast_one, mul_one]

variable (hfin : FiniteAlong F ι) (hN : NormFormulaAlong F ι hfin)

theorem pushforwardAlongDegZero_pointDivisor {P : W.Point} {Q : V.Point}
    (hP : (placeOfPoint P).restrictAlong ι hι = placeOfPoint Q)
    (h0 : (placeOfPoint (0 : W.Point)).restrictAlong ι hι = placeOfPoint (0 : V.Point)) :
    Pic0.pushforwardAlongDegZero ι hι (pointDivisor P) = pointDivisor Q := by
  refine Subtype.ext ?_
  rw [Pic0.coe_pushforwardAlongDegZero, coe_pointDivisor, coe_pointDivisor, map_sub,
    pushforwardAlong_single_eq ι hι, pushforwardAlong_single_eq ι hι, hP, h0]

theorem pushforwardAlongHom_pointClass {P : W.Point} {Q : V.Point}
    (hP : (placeOfPoint P).restrictAlong ι hι = placeOfPoint Q)
    (h0 : (placeOfPoint (0 : W.Point)).restrictAlong ι hι = placeOfPoint (0 : V.Point)) :
    Pic0.pushforwardAlongHom ι hι hfin hN (pointClass P) = pointClass Q := by
  show Pic0.pushforwardAlongHom ι hι hfin hN (Pic0.mk (pointDivisor P))
      = Pic0.mk (pointDivisor Q)
  rw [Pic0.pushforwardAlongHom_mk, pushforwardAlongDegZero_pointDivisor ι hι hP h0]

def pointMapOfPushforward : W.Point →+ V.Point :=
  ((genusOnePic0Equiv V).toAddMonoidHom.comp
      (Pic0.pushforwardAlongHom ι hι hfin hN)).comp
    (genusOnePic0Equiv W).symm.toAddMonoidHom

@[simp]
theorem pointMapOfPushforward_apply (P : W.Point) :
    pointMapOfPushforward ι hι hfin hN P
      = genusOnePic0Equiv V (Pic0.pushforwardAlongHom ι hι hfin hN (pointClass P)) := by
  rw [← genusOnePic0Equiv_symm_apply]
  rfl

theorem pointMapOfPushforward_eq_of_seam (g : W.Point → V.Point) (hg0 : g 0 = 0)
    (hg : ∀ P, (placeOfPoint P).restrictAlong ι hι = placeOfPoint (g P)) (P : W.Point) :
    pointMapOfPushforward ι hι hfin hN P = g P := by
  rw [pointMapOfPushforward_apply,
    pushforwardAlongHom_pointClass ι hι hfin hN (hg P) ((hg 0).trans (by rw [hg0])),
    genusOnePic0Equiv_apply, pic0ToPoint_pointClass]

include hfin hN in

theorem map_add_of_seam (g : W.Point → V.Point) (hg0 : g 0 = 0)
    (hg : ∀ P, (placeOfPoint P).restrictAlong ι hι = placeOfPoint (g P)) (P Q : W.Point) :
    g (P + Q) = g P + g Q := by
  rw [← pointMapOfPushforward_eq_of_seam ι hι hfin hN g hg0 hg (P + Q),
    ← pointMapOfPushforward_eq_of_seam ι hι hfin hN g hg0 hg P,
    ← pointMapOfPushforward_eq_of_seam ι hι hfin hN g hg0 hg Q, map_add]

theorem eq_zero_iff_of_seam (g : W.Point → V.Point) (hg0 : g 0 = 0)
    (hg : ∀ P, (placeOfPoint P).restrictAlong ι hι = placeOfPoint (g P)) (P : W.Point) :
    g P = 0 ↔ Pic0.pushforwardAlongHom ι hι hfin hN (pointClass P) = 0 := by
  rw [← pointMapOfPushforward_eq_of_seam ι hι hfin hN g hg0 hg P, pointMapOfPushforward_apply]
  constructor
  · intro h
    exact (genusOnePic0Equiv V).injective (by rw [h, map_zero])
  · intro h
    rw [h, map_zero]

end WeierstrassCurve.Affine

namespace WeierstrassCurve.Affine

universe u

variable {F : Type u} [Field F] [DecidableEq F] [IsAlgClosed F] [CharZero F]
variable (W : Affine F) [W.IsElliptic] [GenusOnePlaceGate W] [AbelTheorem W]

structure IsogenyEndDatum where

  ι : W.FunctionField →ₐ[F] W.FunctionField

  hι : ι.toRingHom.IsIntegral

  hfin : FiniteAlong F ι

namespace IsogenyEndDatum

variable {W}

def pointEnd (D : IsogenyEndDatum W) (hN : NormFormulaAlong F D.ι D.hfin) :
    AddMonoid.End W.Point :=
  pointMapOfPushforward D.ι D.hι D.hfin hN

theorem pointEnd_apply (D : IsogenyEndDatum W) (hN : NormFormulaAlong F D.ι D.hfin)
    (P : W.Point) :
    D.pointEnd hN P
      = genusOnePic0Equiv W
          (Pic0.pushforwardAlongHom D.ι D.hι D.hfin hN (pointClass P)) :=
  pointMapOfPushforward_apply D.ι D.hι D.hfin hN P

theorem pointEnd_eq_of_seam (D : IsogenyEndDatum W) (hN : NormFormulaAlong F D.ι D.hfin)
    (g : W.Point → W.Point) (hg0 : g 0 = 0)
    (hg : ∀ P, (placeOfPoint P).restrictAlong D.ι D.hι = placeOfPoint (g P)) (P : W.Point) :
    D.pointEnd hN P = g P :=
  pointMapOfPushforward_eq_of_seam D.ι D.hι D.hfin hN g hg0 hg P

end IsogenyEndDatum

def isogenyEndSubring (hNs : ∀ D : IsogenyEndDatum W, NormFormulaAlong F D.ι D.hfin) :
    Subring (AddMonoid.End W.Point) :=
  Subring.closure (Set.range (fun D => IsogenyEndDatum.pointEnd D (hNs D)))

theorem IsogenyEndDatum.pointEnd_mem_isogenyEndSubring
    (hNs : ∀ D : IsogenyEndDatum W, NormFormulaAlong F D.ι D.hfin) (D : IsogenyEndDatum W) :
    D.pointEnd (hNs D) ∈ isogenyEndSubring W hNs :=
  Subring.subset_closure ⟨D, rfl⟩

structure IsogenyHomDatum (V₀ V₁ : Affine F) where
  ι : V₁.FunctionField →ₐ[F] V₀.FunctionField
  hι : ι.toRingHom.IsIntegral
  hfin : FiniteAlong F ι

namespace IsogenyHomDatum

variable {V₀ V₁ : Affine F} [V₀.IsElliptic] [V₁.IsElliptic]
variable [GenusOnePlaceGate V₀] [AbelTheorem V₀] [GenusOnePlaceGate V₁] [AbelTheorem V₁]

def pointHom (D : IsogenyHomDatum V₀ V₁) (hN : NormFormulaAlong F D.ι D.hfin) :
    V₀.Point →+ V₁.Point :=
  pointMapOfPushforward D.ι D.hι D.hfin hN

theorem pointHom_apply (D : IsogenyHomDatum V₀ V₁) (hN : NormFormulaAlong F D.ι D.hfin)
    (P : V₀.Point) :
    D.pointHom hN P = genusOnePic0Equiv V₁
      (Pic0.pushforwardAlongHom D.ι D.hι D.hfin hN (pointClass P)) :=
  pointMapOfPushforward_apply D.ι D.hι D.hfin hN P

theorem pointHom_eq_of_seam (D : IsogenyHomDatum V₀ V₁) (hN : NormFormulaAlong F D.ι D.hfin)
    (g : V₀.Point → V₁.Point) (hg0 : g 0 = 0)
    (hg : ∀ P, (placeOfPoint P).restrictAlong D.ι D.hι = placeOfPoint (g P))
    (P : V₀.Point) :
    D.pointHom hN P = g P :=
  pointMapOfPushforward_eq_of_seam D.ι D.hι D.hfin hN g hg0 hg P

def ofEndDatum {W' : Affine F} (D : IsogenyEndDatum W') : IsogenyHomDatum W' W' where
  ι := D.ι
  hι := D.hι
  hfin := D.hfin

end IsogenyHomDatum

end WeierstrassCurve.Affine

end IsogenyCurrency

Statements phrased using this module (66)