Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_PeriodPair_Uniformization.lean

definition module

Weierstrass curve, ℘-parametrisation and j-invariant of a lattice

The context is Mathlib's PeriodPair L, i.e. a pair of complex numbers \omega_1,\omega_2 that are linearly independent over \mathbb R, with its lattice \Lambda = \mathbb Z\omega_1 + \mathbb Z\omega_2, its Weierstrass function \wp and derivative \wp', and its invariants g_2, g_3. PeriodPair.weierstrassCurve is the Weierstrass curve over \mathbb C with a_1=a_2=a_3=0, a_4=-g_2/4, a_6=-g_3/4, that is y^2 = x^3 - (g_2/4)x - (g_3/4); the accompanying computations give \Delta = g_2^3 - 27g_3^2 and c_4 = 12 g_2, and equation_weierstrassP says that for z \notin \Lambda the point (\wp(z), \wp'(z)/2) satisfies the affine equation of this curve (the normalisation y = \wp'/2 is what produces these unscaled formulae for \Delta and c_4). DiscriminantNeZero is the predicate g_2^3 - 27g_3^2 \neq 0, equivalently \Delta \neq 0 for this model. Given that predicate, toPoint sends z \in \Lambda to the point at infinity and z \notin \Lambda to the affine point (\wp(z), \wp'(z)/2), which is nonsingular because \Delta \neq 0; IsUniformization is the conjunction of three assertions about this map: it is additive, it is surjective onto the points of the curve, and any z with toPoint z = 0 lies in \Lambda. jLattice is 1728\,g_2^3/(g_2^3 - 27g_3^2), shown to equal c_4^3/\Delta of the above model (both sides being 0 when the denominator vanishes), and JSurjective asserts that every complex number is j(\Lambda) for some period pair with nonvanishing discriminant. Finally, ofTau is the normalised pair (\tau,1) for \tau in the upper half-plane, with lattice the \mathbb Z-span of \{\tau,1\}; scale is the homothety (\alpha\omega_1,\alpha\omega_2) by a unit \alpha; and sublatticeIndex L L', sublatticeQuotient L L' are the index and the quotient of \Lambda by the subgroup \Lambda' \cap \Lambda of \Lambda.

Relation to Mathlib

The structure PeriodPair itself, its lattice, \wp, \wp', g_2, g_3 and the differential equation for \wp'^2 are Mathlib's, as are WeierstrassCurve with its invariants \Delta, c_4 and the affine point group; what is added here is the passage from a period pair to a concrete Weierstrass model, the ℘-parametrisation of its points, the lattice j-invariant, and the predicates recording nonvanishing of the discriminant, the uniformization property and surjectivity of j.

Where it is used

These definitions provide the analytic side of the theory of elliptic curves over \mathbb C: the dictionary between lattices up to homothety and complex elliptic curves via j, and between sublattices of finite index and isogenies, as used in the treatment of modular curves and modular forms in the modularity part of the argument.

References

  1. J. H. Silverman, The Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 106, Springer, 1986, Chapter VI
  2. J. H. Silverman, Advanced Topics in the Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 151, Springer, 1994, Chapter I

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

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

set_option autoImplicit false

noncomputable section

open scoped PeriodPair UpperHalfPlane

namespace PeriodPair

variable (L : PeriodPair)

def weierstrassCurve : WeierstrassCurve ℂ where
  a₁ := 0
  a₂ := 0
  a₃ := 0
  a₄ := -L.g₂ / 4
  a₆ := -L.g₃ / 4

@[simp] theorem weierstrassCurve_a₁ : L.weierstrassCurve.a₁ = 0 := rfl
@[simp] theorem weierstrassCurve_a₂ : L.weierstrassCurve.a₂ = 0 := rfl
@[simp] theorem weierstrassCurve_a₃ : L.weierstrassCurve.a₃ = 0 := rfl
@[simp] theorem weierstrassCurve_a₄ : L.weierstrassCurve.a₄ = -L.g₂ / 4 := rfl
@[simp] theorem weierstrassCurve_a₆ : L.weierstrassCurve.a₆ = -L.g₃ / 4 := rfl

theorem weierstrassCurve_Δ : L.weierstrassCurve.Δ = L.g₂ ^ 3 - 27 * L.g₃ ^ 2 := by
  simp only [WeierstrassCurve.Δ, WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.b₆,
    WeierstrassCurve.b₈, weierstrassCurve_a₁, weierstrassCurve_a₂, weierstrassCurve_a₃,
    weierstrassCurve_a₄, weierstrassCurve_a₆]
  ring

theorem weierstrassCurve_c₄ : L.weierstrassCurve.c₄ = 12 * L.g₂ := by
  simp only [WeierstrassCurve.c₄, WeierstrassCurve.b₂, WeierstrassCurve.b₄, weierstrassCurve_a₁,
    weierstrassCurve_a₂, weierstrassCurve_a₃, weierstrassCurve_a₄]
  ring

theorem equation_weierstrassP {z : ℂ} (hz : z ∉ L.lattice) :
    L.weierstrassCurve.toAffine.Equation (℘[L] z) (℘'[L] z / 2) := by
  rw [WeierstrassCurve.Affine.equation_iff]
  have h := L.derivWeierstrassP_sq z hz
  show (℘'[L] z / 2) ^ 2 + L.weierstrassCurve.a₁ * ℘[L] z * (℘'[L] z / 2) +
      L.weierstrassCurve.a₃ * (℘'[L] z / 2) = ℘[L] z ^ 3 + L.weierstrassCurve.a₂ * ℘[L] z ^ 2 +
      L.weierstrassCurve.a₄ * ℘[L] z + L.weierstrassCurve.a₆
  rw [weierstrassCurve_a₁, weierstrassCurve_a₂, weierstrassCurve_a₃, weierstrassCurve_a₄,
    weierstrassCurve_a₆]
  linear_combination (1 / 4 : ℂ) * h

def DiscriminantNeZero : Prop :=
  L.g₂ ^ 3 - 27 * L.g₃ ^ 2 ≠ 0

theorem DiscriminantNeZero.weierstrassCurve_Δ_ne_zero {L : PeriodPair}
    (h : L.DiscriminantNeZero) : L.weierstrassCurve.Δ ≠ 0 := by
  rwa [L.weierstrassCurve_Δ]

open Classical in

def toPoint (h : L.DiscriminantNeZero) (z : ℂ) : L.weierstrassCurve.toAffine.Point :=
  if hz : z ∈ L.lattice then 0
  else .some _ _ ((WeierstrassCurve.Affine.equation_iff_nonsingular_of_Δ_ne_zero
    h.weierstrassCurve_Δ_ne_zero).mp (L.equation_weierstrassP hz))

@[simp]
theorem toPoint_of_mem (h : L.DiscriminantNeZero) {z : ℂ} (hz : z ∈ L.lattice) :
    L.toPoint h z = 0 := by simp [toPoint, hz]

@[simp]
theorem toPoint_zero (h : L.DiscriminantNeZero) : L.toPoint h 0 = 0 :=
  L.toPoint_of_mem h (zero_mem _)

theorem toPoint_of_notMem (h : L.DiscriminantNeZero) {z : ℂ} (hz : z ∉ L.lattice) :
    L.toPoint h z = .some _ _ ((WeierstrassCurve.Affine.equation_iff_nonsingular_of_Δ_ne_zero
      h.weierstrassCurve_Δ_ne_zero).mp (L.equation_weierstrassP hz)) := by
  simp [toPoint, hz]

def IsUniformization (h : L.DiscriminantNeZero) : Prop :=
  (∀ z w, L.toPoint h (z + w) = L.toPoint h z + L.toPoint h w) ∧
    Function.Surjective (L.toPoint h) ∧
      ∀ z, L.toPoint h z = 0 → z ∈ L.lattice

def jLattice : ℂ := 1728 * L.g₂ ^ 3 / (L.g₂ ^ 3 - 27 * L.g₃ ^ 2)

theorem jLattice_eq_c₄_pow_three_div_Δ :
    L.jLattice = L.weierstrassCurve.c₄ ^ 3 / L.weierstrassCurve.Δ := by
  rw [jLattice, weierstrassCurve_c₄, weierstrassCurve_Δ]
  by_cases h : L.g₂ ^ 3 - 27 * L.g₃ ^ 2 = 0
  · rw [h, div_zero, div_zero]
  · rw [div_eq_div_iff h h]
    ring

def JSurjective : Prop :=
  ∀ c : ℂ, ∃ L : PeriodPair, L.DiscriminantNeZero ∧ L.jLattice = c

theorem linearIndependent_coe_upperHalfPlane_one (τ : ℍ) :
    LinearIndependent ℝ ![(τ : ℂ), (1 : ℂ)] := by
  rw [LinearIndependent.pair_iff]
  intro a b h
  have him : (a • (τ : ℂ) + b • (1 : ℂ)).im = 0 := by rw [h]; simp
  simp only [Complex.add_im, Complex.smul_im, Complex.one_im, smul_zero, add_zero] at him
  have ha : a = 0 := (mul_eq_zero.mp him).resolve_right (ne_of_gt τ.im_pos)
  subst ha
  simp only [zero_smul, zero_add, smul_eq_zero, one_ne_zero, or_false] at h
  exact ⟨rfl, h⟩

def ofTau (τ : ℍ) : PeriodPair where
  ω₁ := (τ : ℂ)
  ω₂ := 1
  indep := linearIndependent_coe_upperHalfPlane_one τ

@[simp] theorem ofTau_ω₁ (τ : ℍ) : (ofTau τ).ω₁ = (τ : ℂ) := rfl
@[simp] theorem ofTau_ω₂ (τ : ℍ) : (ofTau τ).ω₂ = 1 := rfl

@[simp] theorem ofTau_lattice (τ : ℍ) :
    (ofTau τ).lattice = Submodule.span ℤ {(τ : ℂ), 1} := rfl

section Scale

variable (α : ℂˣ)

theorem scale_indep : LinearIndependent ℝ ![(α : ℂ) * L.ω₁, (α : ℂ) * L.ω₂] := by
  have h : ![(α : ℂ) * L.ω₁, (α : ℂ) * L.ω₂] = (LinearMap.mulLeft ℝ (α : ℂ)) ∘ ![L.ω₁, L.ω₂] := by
    funext i; fin_cases i <;> simp
  rw [h]
  exact L.indep.map' (LinearMap.mulLeft ℝ (α : ℂ))
    (LinearMap.ker_eq_bot_of_injective (mul_right_injective₀ α.ne_zero))

def scale : PeriodPair where
  ω₁ := (α : ℂ) * L.ω₁
  ω₂ := (α : ℂ) * L.ω₂
  indep := L.scale_indep α

@[simp] theorem scale_ω₁ : (L.scale α).ω₁ = (α : ℂ) * L.ω₁ := rfl
@[simp] theorem scale_ω₂ : (L.scale α).ω₂ = (α : ℂ) * L.ω₂ := rfl

end Scale

def sublatticeIndex (L L' : PeriodPair) : ℕ :=
  (L'.lattice.toAddSubgroup.addSubgroupOf L.lattice.toAddSubgroup).index

abbrev sublatticeQuotient (L L' : PeriodPair) :=
  L.lattice.toAddSubgroup ⧸ L'.lattice.toAddSubgroup.addSubgroupOf L.lattice.toAddSubgroup

end PeriodPair

end

Statements phrased using this module (16)