Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_CycSubRootBridge.lean

definition module

Cyclic -subgroups versus roots of the modular polynomial

Throughout, H = \mathrm{HahnSeries}\,\mathbb{Q}\,\overline{\mathbb{Q}} is the Hahn-series field with rational exponents and coefficients in an algebraic closure of \mathbb{Q}; isAlgClosed_H and charZero_H record that it is algebraically closed of characteristic zero, and transcendental_rat_of_transcendental_qbar transfers transcendence over \overline{\mathbb{Q}} to transcendence over \mathbb{Q}. For a Weierstrass curve E over H and N \in \mathbb{N}, an element of CycSubH E N is a subgroup G of E(H) together with the existence of g \in E(H) of additive order N with G = \mathbb{Z}g; cycSubGen chooses such a generator, addOrderOf_cycSubGen and coe_eq_zmultiples_cycSubGen state its two defining properties, and CycSubH.ext says such data are determined by the underlying subgroup. For a prime p \neq 2, cycSubSummingSet E G is the finite set of affine coordinate pairs of g, 2g, \dots, \frac{p-1}{2}g (Vélu summing set of odd order), and isElliptic_veluQuotient_cycSubSummingSet shows the associated Vélu quotient E/G has invertible discriminant. Given \Phi of level p (a ModularPolynomialData p: a monic \Phi \in \mathbb{Z}[X][Y] of degree \psi(p) vanishing on the pair (j(q), j(q^p))), cycSubRoot E hp2 data G is the element j(E/G) of RootsAt data E.j, the subtype of y \in H with \Phi(j(E), y) = 0 after mapping coefficients into H via X \mapsto j(E). If j(E) is transcendental over \overline{\mathbb{Q}} this map is injective (cycSubRoot_injective). The counting part establishes \#\,CycSubH E p\, = \psi(p) = \sum_{d \mid p,\ d \text{ squarefree}} p/d (natCard_cycSubH, via a characterisation of the cyclic-subgroup condition as IsAddCyclic together with cardinality p), finiteness of both sides, and \#\,RootsAt data E.j\, \le \psi(p) from \deg_Y \Phi = \psi(p). Hence cycSubRoot is bijective, and rootsEquivCycSubH is its inverse equivalence \mathrm{RootsAt}(\Phi, j(E)) \simeq \mathrm{CycSubH}(E,p), with the two computation rules e^{-1}(G) = j(E/G) and e(r) = G \iff r = j(E/G).

Relation to Mathlib

Mathlib supplies the ambient objects — HahnSeries, AlgebraicClosure, WeierstrassCurve with its affine points and AddSubgroup.zmultiples — while the cyclic-subgroup type CycSubH, the root subtype RootsAt, the Vélu quotient and its odd summing sets, the modular-polynomial datum and the Dedekind \psi function are the project's own definitions.

Where it is used

The equivalence constructed here is exactly the data required by the predicate ModuliDictionary at prime level: over the Hahn-series field it identifies the roots of the level-p modular polynomial at j(E) with the order-p cyclic subgroups of E, each root being the j-invariant of the corresponding Vélu quotient. This is part of the construction of modular curves and their modular equations used in the modularity route to Fermat's Last Theorem.

References

  1. J. Vélu, Isogénies entre courbes elliptiques, C. R. Acad. Sci. Paris Sér. A 273 (1971), 238–241
  2. J. H. Silverman, Advanced Topics in the Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 151, Springer, 1994

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

Imports

Theorems imported by this definition module

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_TatePoint
import Definitions.Def_WeierstrassCurve_OddOrderSummingSet
import Theorems.Thm_HahnSeries_isAlgClosed_rat
import Theorems.Thm_WeierstrassCurve_veluQuotient_oddOrderSummingSet_discriminant_ne_zero
import Theorems.Thm_ModularCurve_ModularPolynomialData_isRoot_map_j_veluQuotient_j_of_addOrderOf_eq
import Theorems.Thm_WeierstrassCurve_zmultiples_eq_of_veluQuotient_j_eq_of_transcendental
import Theorems.Thm_WeierstrassCurve_natCard_addSubgroup_isAddCyclic_card_eq_dedekindPsi_of_isAlgClosed

set_option autoImplicit false
set_option maxHeartbeats 800000
set_option synthInstance.maxHeartbeats 400000

noncomputable section

open ModularCurve WeierstrassCurve Polynomial
open scoped Classical

namespace ModularCurve.TatePoint

theorem isAlgClosed_H : IsAlgClosed H := HahnSeries.isAlgClosed_rat

theorem charZero_H : CharZero H :=
  (RingHom.charZero_iff (HahnSeries.C (R := Qbar) (Γ := ℚ)).injective).mp inferInstance

attribute [local instance] isAlgClosed_H charZero_H

theorem transcendental_rat_of_transcendental_qbar {_ : Algebra ℚ H} {x : H}
    (hx : Transcendental Qbar x) : Transcendental ℚ x := by
  haveI := IsScalarTower.of_algebraMap_eq' (R := ℚ) (S := Qbar) (A := H) (Subsingleton.elim _ _)
  exact hx.of_tower_top ℚ

theorem two_mul_pred_div_two_add_one {p : ℕ} [Fact p.Prime] (hp2 : p ≠ 2) :
    2 * ((p - 1) / 2) + 1 = p := by
  rcases (Fact.out : p.Prime).eq_two_or_odd' with h | h
  · exact absurd h hp2
  · obtain ⟨m, rfl⟩ := h; omega

section Gen

variable (E : WeierstrassCurve H) {p : ℕ}

def cycSubGen (G : CycSubH E p) : E.toAffine.Point := Classical.choose G.2

theorem addOrderOf_cycSubGen (G : CycSubH E p) : addOrderOf (cycSubGen E G) = p :=
  (Classical.choose_spec G.2).1

theorem coe_eq_zmultiples_cycSubGen (G : CycSubH E p) :
    G.1 = AddSubgroup.zmultiples (cycSubGen E G) :=
  (Classical.choose_spec G.2).2

theorem CycSubH.ext {G G' : CycSubH E p} (h : G.1 = G'.1) : G = G' := Subtype.ext h

def cycSubSummingSet (G : CycSubH E p) : Finset (H × H) :=
  E.oddOrderSummingSet (cycSubGen E G) ((p - 1) / 2)

theorem cycSubSummingSet_def (G : CycSubH E p) :
    cycSubSummingSet E G = E.oddOrderSummingSet (cycSubGen E G) ((p - 1) / 2) := rfl

end Gen

section Root

variable (E : WeierstrassCurve H) [E.IsElliptic] {p : ℕ} [Fact p.Prime]

theorem isElliptic_veluQuotient_cycSubSummingSet (hp2 : p ≠ 2) (G : CycSubH E p) :
    (E.veluQuotient (cycSubSummingSet E G)).IsElliptic :=
  ⟨isUnit_iff_ne_zero.mpr
    (WeierstrassCurve.veluQuotient_oddOrderSummingSet_discriminant_ne_zero (L := H) two_ne_zero E
      ((p - 1) / 2) (cycSubGen E G)
      (by rw [addOrderOf_cycSubGen, two_mul_pred_div_two_add_one hp2]))⟩

theorem isRoot_map_j_veluQuotient_j_of_eq {N : ℕ} [NeZero N] (n : ℕ) (hN : 2 * n + 1 = N)
    (data : ModularPolynomialData N) (Q : E.toAffine.Point) (hQ : addOrderOf Q = N)
    (hΔ : (E.veluQuotient (E.oddOrderSummingSet Q n)).Δ ≠ 0) :
    haveI : (E.veluQuotient (E.oddOrderSummingSet Q n)).IsElliptic := ⟨isUnit_iff_ne_zero.mpr hΔ⟩
    (data.Φ.map (Polynomial.eval₂RingHom (Int.castRingHom H) E.j)).IsRoot
      (E.veluQuotient (E.oddOrderSummingSet Q n)).j := by
  subst hN
  exact ModularPolynomialData.isRoot_map_j_veluQuotient_j_of_addOrderOf_eq E n Q hQ hΔ data

def cycSubRoot (hp2 : p ≠ 2) (data : ModularPolynomialData p) (G : CycSubH E p) : RootsAt data E.j :=
  ⟨@WeierstrassCurve.j H _ (E.veluQuotient (cycSubSummingSet E G))
      (isElliptic_veluQuotient_cycSubSummingSet E hp2 G),
    isRoot_map_j_veluQuotient_j_of_eq E ((p - 1) / 2) (two_mul_pred_div_two_add_one hp2) data
      (cycSubGen E G) (addOrderOf_cycSubGen E G)
      (isElliptic_veluQuotient_cycSubSummingSet E hp2 G).isUnit.ne_zero⟩

theorem cycSubRoot_coe (hp2 : p ≠ 2) (data : ModularPolynomialData p) (G : CycSubH E p) :
    (cycSubRoot E hp2 data G).1 =
      @WeierstrassCurve.j H _ (E.veluQuotient (cycSubSummingSet E G))
        (isElliptic_veluQuotient_cycSubSummingSet E hp2 G) := rfl

theorem cycSubRoot_injective (hp2 : p ≠ 2) (data : ModularPolynomialData p)
    (hj : Transcendental Qbar E.j) : Function.Injective (cycSubRoot E hp2 data) := by
  intro G G' h
  have hjj := congrArg Subtype.val h
  simp only [cycSubRoot_coe] at hjj
  apply CycSubH.ext
  rw [coe_eq_zmultiples_cycSubGen, coe_eq_zmultiples_cycSubGen]
  exact WeierstrassCurve.zmultiples_eq_of_veluQuotient_j_eq_of_transcendental E
    (transcendental_rat_of_transcendental_qbar hj) ((p - 1) / 2) (cycSubGen E G) (cycSubGen E G')
    (by rw [addOrderOf_cycSubGen, two_mul_pred_div_two_add_one hp2])
    (by rw [addOrderOf_cycSubGen, two_mul_pred_div_two_add_one hp2])
    (isElliptic_veluQuotient_cycSubSummingSet E hp2 G).isUnit.ne_zero
    (isElliptic_veluQuotient_cycSubSummingSet E hp2 G').isUnit.ne_zero hjj

end Root

section Count

variable (E : WeierstrassCurve H) {p : ℕ}

theorem exists_addOrderOf_eq_and_eq_zmultiples_iff {A : Type*} [AddCommGroup A] {N : ℕ}
    (G : AddSubgroup A) :
    (∃ g : A, addOrderOf g = N ∧ G = AddSubgroup.zmultiples g) ↔ (IsAddCyclic G ∧ Nat.card G = N) := by
  constructor
  · rintro ⟨g, hg, rfl⟩
    exact ⟨inferInstance, by rw [Nat.card_zmultiples, hg]⟩
  · rintro ⟨hc, hcard⟩
    obtain ⟨g, hg⟩ := (AddSubgroup.isAddCyclic_iff_exists_zmultiples_eq_top G).mp hc
    exact ⟨g, by rw [← Nat.card_zmultiples, hg, hcard], hg.symm⟩

theorem natCard_cycSubH [E.IsElliptic] [NeZero p] : Nat.card (CycSubH E p) = dedekindPsi p := by
  have h := WeierstrassCurve.natCard_addSubgroup_isAddCyclic_card_eq_dedekindPsi_of_isAlgClosed
    (K := H) E (n := p) (by exact_mod_cast NeZero.ne p)
  have hW : WeierstrassCurve.Affine.baseChange E H = E.toAffine := by
    rw [WeierstrassCurve.Affine.baseChange, WeierstrassCurve.baseChange, Algebra.algebraMap_self,
      WeierstrassCurve.map_id]
  rw [hW] at h
  rw [← h]
  unfold CycSubH
  exact Nat.card_congr (Equiv.subtypeEquivRight fun G =>
    exists_addOrderOf_eq_and_eq_zmultiples_iff G)

theorem le_dedekindPsi (N : ℕ) (hN : N ≠ 0) : N ≤ dedekindPsi N := by
  unfold dedekindPsi
  have h1 : (1 : ℕ) ∈ N.divisors.filter Squarefree :=
    Finset.mem_filter.mpr ⟨Nat.one_mem_divisors.mpr hN, squarefree_one⟩
  simpa using Finset.single_le_sum (f := fun d => N / d) (fun _ _ => Nat.zero_le _) h1

theorem finite_cycSubH [E.IsElliptic] [NeZero p] : Finite (CycSubH E p) :=
  Nat.finite_of_card_ne_zero (by
    rw [natCard_cycSubH]
    exact (Nat.lt_of_lt_of_le (Nat.pos_of_ne_zero (NeZero.ne p)) (le_dedekindPsi p (NeZero.ne p))).ne')

def rootsAtEquivMemRootsToFinset [NeZero p] (data : ModularPolynomialData p) (jv : H) :
    RootsAt data jv ≃
      {y : H // y ∈ (data.Φ.map (Polynomial.eval₂RingHom (Int.castRingHom H) jv)).roots.toFinset} := by
  unfold RootsAt
  exact Equiv.subtypeEquivRight fun y => by
    rw [Multiset.mem_toFinset, Polynomial.mem_roots ((data.monic.map _).ne_zero)]

theorem finite_rootsAt [NeZero p] (data : ModularPolynomialData p) (jv : H) :
    Finite (RootsAt data jv) :=
  Finite.of_equiv _ (rootsAtEquivMemRootsToFinset data jv).symm

theorem natCard_rootsAt_le [NeZero p] (data : ModularPolynomialData p) (jv : H) :
    Nat.card (RootsAt data jv) ≤ dedekindPsi p := by
  rw [Nat.card_congr (rootsAtEquivMemRootsToFinset data jv), Nat.card_eq_finsetCard]
  set f := data.Φ.map (Polynomial.eval₂RingHom (Int.castRingHom H) jv) with hf
  calc f.roots.toFinset.card ≤ Multiset.card f.roots := Multiset.toFinset_card_le _
    _ ≤ f.natDegree := Polynomial.card_roots' f
    _ = dedekindPsi p := by rw [hf, data.monic.natDegree_map, data.natDegree_eq]

end Count

section Equiv

variable (E : WeierstrassCurve H) [E.IsElliptic] {p : ℕ} [Fact p.Prime]

theorem cycSubRoot_bijective (hp2 : p ≠ 2) (data : ModularPolynomialData p)
    (hj : Transcendental Qbar E.j) : Function.Bijective (cycSubRoot E hp2 data) := by
  haveI := finite_rootsAt data E.j
  refine (cycSubRoot_injective E hp2 data hj).bijective_of_nat_card_le ?_
  rw [natCard_cycSubH]
  exact natCard_rootsAt_le data E.j

def rootsEquivCycSubH (hp2 : p ≠ 2) (data : ModularPolynomialData p)
    (hj : Transcendental Qbar E.j) : RootsAt data E.j ≃ CycSubH E p :=
  (Equiv.ofBijective (cycSubRoot E hp2 data) (cycSubRoot_bijective E hp2 data hj)).symm

theorem rootsEquivCycSubH_symm_apply (hp2 : p ≠ 2) (data : ModularPolynomialData p)
    (hj : Transcendental Qbar E.j) (G : CycSubH E p) :
    (rootsEquivCycSubH E hp2 data hj).symm G = cycSubRoot E hp2 data G := rfl

theorem rootsEquivCycSubH_apply_eq_iff (hp2 : p ≠ 2) (data : ModularPolynomialData p)
    (hj : Transcendental Qbar E.j) (r : RootsAt data E.j) (G : CycSubH E p) :
    rootsEquivCycSubH E hp2 data hj r = G ↔ r = cycSubRoot E hp2 data G := by
  rw [← rootsEquivCycSubH_symm_apply E hp2 data hj G, Equiv.eq_symm_apply]

end Equiv

end ModularCurve.TatePoint

end

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).