Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_CycSubRootBridgeN.lean

definition module

Roots of the modular polynomial versus cyclic subgroups

Throughout, \bar{\mathbf Q} denotes an algebraic closure of \mathbf Q and H the field of Hahn series over \bar{\mathbf Q} with value group \mathbf Q. For a Weierstrass curve W over a field with decidable equality, a point Q of its affine model and N \in \mathbf N, the curve W.fullKernelQuotient Q N is the Vélu-type curve with the same a_1,a_2,a_3 and with a_4 and a_6 corrected by t = \sum_P G_x(P) and w = \sum_P (x_P G_x(P) - y_P G_y(P)), the sums running over the coordinates of Q, 2Q, \dots, (N-1)Q.

Three propositions in the level N alone are introduced as hypotheses. FullKernelIsRootAt N says: for every elliptic Weierstrass curve W over H and every point Q of exact additive order N with \Delta of the full-kernel quotient nonzero, and every datum data : ModularPolynomialData N (a monic \Phi \in \mathbf Z[X][Y] of degree \psi(N) vanishing on the pair (j(q), j(q^N))), the j-invariant of the quotient is a root of \Phi(j(W), Y) \in H[Y]. FullKernelInjAt N says: if moreover j(W) is transcendental over \mathbf Q, two points Q, Q' of exact order N with nondegenerate quotients of equal j-invariant satisfy \mathbf Z Q = \mathbf Z Q'. FullKernelDiscAt N says: over any algebraically closed field with 2 \ne 0, the full-kernel quotient at any point of exact order N has nonzero discriminant.

Granting these, cycSubRootN sends a subgroup G of E(H) admitting a generator of exact order N to the j-invariant of the full-kernel quotient of E by a chosen such generator, viewed as a root of \Phi(j(E), Y); it is injective when j(E) is transcendental over \bar{\mathbf Q}, and bijective because the source has exactly \psi(N) elements while the root set has at most \deg_Y \Phi = \psi(N). rootsEquivCycSubHN is the inverse equivalence, and dictN is its instance at the curve \mathrm{ofJ}(j_0 + s), whose j-invariant is transcendental for every j_0 \in \bar{\mathbf Q}. Further lemmas record the underlying value of cycSubRootN and the characterisation of the equivalence by e(r) = G \iff r = cycSubRootN G.

Relation to Mathlib

Mathlib supplies Weierstrass curves, the j-invariant, IsElliptic and Hahn series; the full-kernel Vélu quotient, the type of cyclic N-subgroups, the type of roots of a modular polynomial datum and the datum itself (monic \Phi of Y-degree \psi(N) with the q-expansion relation) are the project's own notions.

Where it is used

These definitions provide the moduli dictionary at level N: over the Hahn-series field the roots of \Phi_N(j(E), Y) correspond bijectively to the cyclic subgroups of order N of E, which is the form in which the modular interpretation of X_0(N) is used in the argument. For odd N the three hypotheses are available from the identification of the full-kernel quotient with the Vélu quotient over a half-system of the kernel.

References

  1. J. Vélu, Isogénies entre courbes elliptiques, Comptes Rendus de l'Académie des Sciences Paris, Série A 273 (1971), 238–241
  2. J. H. Silverman, Advanced Topics in the Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 151, Springer, 1994, Chapter II
  3. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_ModularCurve_CycSubRootBridge
import Definitions.Def_WeierstrassCurve_FullKernelQuotient

set_option autoImplicit false

noncomputable section

open ModularCurve WeierstrassCurve Polynomial
open scoped Classical

namespace ModularCurve.TatePoint

abbrev FullKernelIsRootAt (N : ℕ) [NeZero N] : Prop :=
  ∀ [DecidableEq (HahnSeries ℚ (AlgebraicClosure ℚ))]
    (W : WeierstrassCurve (HahnSeries ℚ (AlgebraicClosure ℚ))) [W.IsElliptic]
    (Q : W.toAffine.Point) (_ : addOrderOf Q = N)
    (hΔ : (W.fullKernelQuotient Q N).Δ ≠ 0)
    (data : ModularCurve.ModularPolynomialData N),
    haveI : (W.fullKernelQuotient Q N).IsElliptic := ⟨isUnit_iff_ne_zero.mpr hΔ⟩
    (data.Φ.map (Polynomial.eval₂RingHom
      (Int.castRingHom (HahnSeries ℚ (AlgebraicClosure ℚ))) W.j)).IsRoot
      (W.fullKernelQuotient Q N).j

abbrev FullKernelInjAt (N : ℕ) [NeZero N] : Prop :=
  ∀ [DecidableEq (HahnSeries ℚ (AlgebraicClosure ℚ))]
    (W : WeierstrassCurve (HahnSeries ℚ (AlgebraicClosure ℚ))) [W.IsElliptic]
    (_ : Transcendental ℚ W.j) (Q Q' : W.toAffine.Point)
    (_ : addOrderOf Q = N) (_ : addOrderOf Q' = N)
    (hΔ : (W.fullKernelQuotient Q N).Δ ≠ 0)
    (hΔ' : (W.fullKernelQuotient Q' N).Δ ≠ 0)
    (_ : haveI : (W.fullKernelQuotient Q N).IsElliptic := ⟨isUnit_iff_ne_zero.mpr hΔ⟩
      haveI : (W.fullKernelQuotient Q' N).IsElliptic := ⟨isUnit_iff_ne_zero.mpr hΔ'⟩
      (W.fullKernelQuotient Q N).j = (W.fullKernelQuotient Q' N).j),
    AddSubgroup.zmultiples Q = AddSubgroup.zmultiples Q'

abbrev FullKernelDiscAt (N : ℕ) [NeZero N] : Prop :=
  ∀ {L : Type} [Field L] [DecidableEq L] [IsAlgClosed L], (2 : L) ≠ 0 →
    ∀ (W : WeierstrassCurve L) [W.IsElliptic] (Q : W.toAffine.Point),
      addOrderOf Q = N → (W.fullKernelQuotient Q N).Δ ≠ 0

attribute [local instance] isAlgClosed_H charZero_H

theorem isElliptic_fullKernelQuotient_cycSubGen (E : WeierstrassCurve H) [E.IsElliptic] {N : ℕ} [NeZero N]
    (hW3 : FullKernelDiscAt N) (G : CycSubH E N) :
    (E.fullKernelQuotient (cycSubGen E G) N).IsElliptic :=
  ⟨isUnit_iff_ne_zero.mpr (hW3 two_ne_zero E (cycSubGen E G) (addOrderOf_cycSubGen E G))⟩

def cycSubRootN (E : WeierstrassCurve H) [E.IsElliptic] {N : ℕ} [NeZero N] (hW1 : FullKernelIsRootAt N)
    (hW3 : FullKernelDiscAt N) (data : ModularPolynomialData N) (G : CycSubH E N) : RootsAt data E.j :=
  ⟨@WeierstrassCurve.j H _ (E.fullKernelQuotient (cycSubGen E G) N)
      (isElliptic_fullKernelQuotient_cycSubGen E hW3 G),
    hW1 E (cycSubGen E G) (addOrderOf_cycSubGen E G)
      (isElliptic_fullKernelQuotient_cycSubGen E hW3 G).isUnit.ne_zero data⟩

theorem cycSubRootN_coe (E : WeierstrassCurve H) [E.IsElliptic] {N : ℕ} [NeZero N]
    (hW1 : FullKernelIsRootAt N) (hW3 : FullKernelDiscAt N) (data : ModularPolynomialData N)
    (G : CycSubH E N) :
    (cycSubRootN E hW1 hW3 data G).1 =
      @WeierstrassCurve.j H _ (E.fullKernelQuotient (cycSubGen E G) N)
        (isElliptic_fullKernelQuotient_cycSubGen E hW3 G) := rfl

theorem cycSubRootN_injective (E : WeierstrassCurve H) [E.IsElliptic] {N : ℕ} [NeZero N]
    (hW1 : FullKernelIsRootAt N) (hW2 : FullKernelInjAt N) (hW3 : FullKernelDiscAt N)
    (data : ModularPolynomialData N) (hj : Transcendental Qbar E.j) :
    Function.Injective (cycSubRootN E hW1 hW3 data) := by
  intro G G' h
  have hjj := congrArg Subtype.val h
  simp only [cycSubRootN_coe] at hjj
  apply CycSubH.ext
  rw [coe_eq_zmultiples_cycSubGen, coe_eq_zmultiples_cycSubGen]
  exact hW2 E (transcendental_rat_of_transcendental_qbar hj) (cycSubGen E G) (cycSubGen E G')
    (addOrderOf_cycSubGen E G) (addOrderOf_cycSubGen E G')
    (isElliptic_fullKernelQuotient_cycSubGen E hW3 G).isUnit.ne_zero
    (isElliptic_fullKernelQuotient_cycSubGen E hW3 G').isUnit.ne_zero hjj

theorem cycSubRootN_bijective (E : WeierstrassCurve H) [E.IsElliptic] {N : ℕ} [NeZero N]
    (hW1 : FullKernelIsRootAt N) (hW2 : FullKernelInjAt N) (hW3 : FullKernelDiscAt N)
    (data : ModularPolynomialData N) (hj : Transcendental Qbar E.j) :
    Function.Bijective (cycSubRootN E hW1 hW3 data) := by
  haveI := finite_rootsAt data E.j
  refine (cycSubRootN_injective E hW1 hW2 hW3 data hj).bijective_of_nat_card_le ?_
  rw [natCard_cycSubH]
  exact natCard_rootsAt_le data E.j

def rootsEquivCycSubHN (E : WeierstrassCurve H) [E.IsElliptic] {N : ℕ} [NeZero N]
    (hW1 : FullKernelIsRootAt N) (hW2 : FullKernelInjAt N) (hW3 : FullKernelDiscAt N)
    (data : ModularPolynomialData N) (hj : Transcendental Qbar E.j) : RootsAt data E.j ≃ CycSubH E N :=
  (Equiv.ofBijective (cycSubRootN E hW1 hW3 data) (cycSubRootN_bijective E hW1 hW2 hW3 data hj)).symm

theorem rootsEquivCycSubHN_symm_apply (E : WeierstrassCurve H) [E.IsElliptic] {N : ℕ} [NeZero N]
    (hW1 : FullKernelIsRootAt N) (hW2 : FullKernelInjAt N) (hW3 : FullKernelDiscAt N)
    (data : ModularPolynomialData N) (hj : Transcendental Qbar E.j) (G : CycSubH E N) :
    (rootsEquivCycSubHN E hW1 hW2 hW3 data hj).symm G = cycSubRootN E hW1 hW3 data G := rfl

theorem rootsEquivCycSubHN_apply_eq_iff (E : WeierstrassCurve H) [E.IsElliptic] {N : ℕ} [NeZero N]
    (hW1 : FullKernelIsRootAt N) (hW2 : FullKernelInjAt N) (hW3 : FullKernelDiscAt N)
    (data : ModularPolynomialData N) (hj : Transcendental Qbar E.j) (r : RootsAt data E.j)
    (G : CycSubH E N) :
    rootsEquivCycSubHN E hW1 hW2 hW3 data hj r = G ↔ r = cycSubRootN E hW1 hW3 data G := by
  rw [← rootsEquivCycSubHN_symm_apply E hW1 hW2 hW3 data hj G, Equiv.eq_symm_apply]

def dictN (N : ℕ) [NeZero N] (data : ModularPolynomialData N) (j₀ : Qbar) (hW1 : FullKernelIsRootAt N)
    (hW2 : FullKernelInjAt N) (hW3 : FullKernelDiscAt N) :
    RootsAt data (nearCurve j₀).j ≃ CycSubH (nearCurve j₀) N :=
  rootsEquivCycSubHN (nearCurve j₀) hW1 hW2 hW3 data (nearCurve_j_transcendental j₀)

theorem dictN_symm_apply_coe (N : ℕ) [NeZero N] (data : ModularPolynomialData N) (j₀ : Qbar)
    (hW1 : FullKernelIsRootAt N) (hW2 : FullKernelInjAt N) (hW3 : FullKernelDiscAt N)
    (G : CycSubH (nearCurve j₀) N) :
    ((dictN N data j₀ hW1 hW2 hW3).symm G).1 =
      @WeierstrassCurve.j H _ ((nearCurve j₀).fullKernelQuotient (cycSubGen (nearCurve j₀) G) N)
        (isElliptic_fullKernelQuotient_cycSubGen (nearCurve j₀) hW3 G) := rfl

theorem dictN_apply_eq_iff (N : ℕ) [NeZero N] (data : ModularPolynomialData N) (j₀ : Qbar)
    (hW1 : FullKernelIsRootAt N) (hW2 : FullKernelInjAt N) (hW3 : FullKernelDiscAt N)
    (r : RootsAt data (nearCurve j₀).j) (G : CycSubH (nearCurve j₀) N) :
    dictN N data j₀ hW1 hW2 hW3 r = G ↔ r = cycSubRootN (nearCurve j₀) hW1 hW3 data G :=
  rootsEquivCycSubHN_apply_eq_iff (nearCurve j₀) hW1 hW2 hW3 data (nearCurve_j_transcendental j₀) r G

end ModularCurve.TatePoint

end

example (N : ℕ) [NeZero N] (h : ∀ [DecidableEq (HahnSeries ℚ (AlgebraicClosure ℚ))]
    (W : WeierstrassCurve (HahnSeries ℚ (AlgebraicClosure ℚ))) [W.IsElliptic]
    (Q : W.toAffine.Point) (_ : addOrderOf Q = N)
    (hΔ : (W.fullKernelQuotient Q N).Δ ≠ 0)
    (data : ModularCurve.ModularPolynomialData N),
    haveI : (W.fullKernelQuotient Q N).IsElliptic := ⟨isUnit_iff_ne_zero.mpr hΔ⟩
    (data.Φ.map (Polynomial.eval₂RingHom
      (Int.castRingHom (HahnSeries ℚ (AlgebraicClosure ℚ))) W.j)).IsRoot
      (W.fullKernelQuotient Q N).j) : ModularCurve.TatePoint.FullKernelIsRootAt N := h
example (N : ℕ) [NeZero N] (h : ModularCurve.TatePoint.FullKernelIsRootAt N)
    [DecidableEq (HahnSeries ℚ (AlgebraicClosure ℚ))]
    (W : WeierstrassCurve (HahnSeries ℚ (AlgebraicClosure ℚ))) [W.IsElliptic]
    (Q : W.toAffine.Point) (hQ : addOrderOf Q = N) (hΔ : (W.fullKernelQuotient Q N).Δ ≠ 0)
    (data : ModularCurve.ModularPolynomialData N) :
    haveI : (W.fullKernelQuotient Q N).IsElliptic := ⟨isUnit_iff_ne_zero.mpr hΔ⟩
    (data.Φ.map (Polynomial.eval₂RingHom
      (Int.castRingHom (HahnSeries ℚ (AlgebraicClosure ℚ))) W.j)).IsRoot
      (W.fullKernelQuotient Q N).j := h W Q hQ hΔ data
example (N : ℕ) [NeZero N] (h : ∀ [DecidableEq (HahnSeries ℚ (AlgebraicClosure ℚ))]
    (W : WeierstrassCurve (HahnSeries ℚ (AlgebraicClosure ℚ))) [W.IsElliptic]
    (_ : Transcendental ℚ W.j) (Q Q' : W.toAffine.Point)
    (_ : addOrderOf Q = N) (_ : addOrderOf Q' = N)
    (hΔ : (W.fullKernelQuotient Q N).Δ ≠ 0)
    (hΔ' : (W.fullKernelQuotient Q' N).Δ ≠ 0)
    (_ : haveI : (W.fullKernelQuotient Q N).IsElliptic := ⟨isUnit_iff_ne_zero.mpr hΔ⟩
      haveI : (W.fullKernelQuotient Q' N).IsElliptic := ⟨isUnit_iff_ne_zero.mpr hΔ'⟩
      (W.fullKernelQuotient Q N).j = (W.fullKernelQuotient Q' N).j),
    AddSubgroup.zmultiples Q = AddSubgroup.zmultiples Q') : ModularCurve.TatePoint.FullKernelInjAt N := h
example (N : ℕ) [NeZero N] (h : ModularCurve.TatePoint.FullKernelInjAt N)
    [DecidableEq (HahnSeries ℚ (AlgebraicClosure ℚ))]
    (W : WeierstrassCurve (HahnSeries ℚ (AlgebraicClosure ℚ))) [W.IsElliptic]
    (ht : Transcendental ℚ W.j) (Q Q' : W.toAffine.Point)
    (hQ : addOrderOf Q = N) (hQ' : addOrderOf Q' = N)
    (hΔ : (W.fullKernelQuotient Q N).Δ ≠ 0) (hΔ' : (W.fullKernelQuotient Q' N).Δ ≠ 0)
    (hj : haveI : (W.fullKernelQuotient Q N).IsElliptic := ⟨isUnit_iff_ne_zero.mpr hΔ⟩
      haveI : (W.fullKernelQuotient Q' N).IsElliptic := ⟨isUnit_iff_ne_zero.mpr hΔ'⟩
      (W.fullKernelQuotient Q N).j = (W.fullKernelQuotient Q' N).j) :
    AddSubgroup.zmultiples Q = AddSubgroup.zmultiples Q' := h W ht Q Q' hQ hQ' hΔ hΔ' hj
example (N : ℕ) [NeZero N] (h : ∀ {L : Type} [Field L] [DecidableEq L] [IsAlgClosed L], (2 : L) ≠ 0 →
    ∀ (W : WeierstrassCurve L) [W.IsElliptic] (Q : W.toAffine.Point),
      addOrderOf Q = N → (W.fullKernelQuotient Q N).Δ ≠ 0) : ModularCurve.TatePoint.FullKernelDiscAt N := h
example (N : ℕ) [NeZero N] (h : ModularCurve.TatePoint.FullKernelDiscAt N)
    {L : Type} [Field L] [DecidableEq L] [IsAlgClosed L]
    (h2 : (2 : L) ≠ 0) (W : WeierstrassCurve L) [W.IsElliptic] (Q : W.toAffine.Point) (hQ : addOrderOf Q = N) :
    (W.fullKernelQuotient Q N).Δ ≠ 0 := h h2 W Q hQ

Statements phrased using this module (8)