Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_JWidth.lean

definition module

The width of a -invariant: , , else

For a field K with decidable equality and an element j \in K, ModularCurve.jWidth j is the natural number defined by the three-way case distinction \mathrm{jWidth}(j)=\begin{cases}3,& j=0,\\ 2,& j=1728,\\ 1,&\text{otherwise,}\end{cases} where the tests are performed in the order shown, so that the value at j=0 is 3 even in a field in which 0 and 1728 happen to coincide. The remaining declarations are the elementary facts about this function. The three defining clauses are recorded separately: jWidth_of_eq_zero gives the value 3 when j=0; jWidth_of_eq_1728 gives the value 2 from the hypotheses j=1728 and j \neq 0 (the second hypothesis being what makes the clause correct when 1728=0 in K); and jWidth_of_ne gives the value 1 when j is neither 0 nor 1728. The unfolding jWidth_eq_ite states that jWidth j equals the nested conditional itself. The numerical range is described by jWidth_pos (0 < \mathrm{jWidth}(j)), by jWidth_eq_one_or (the value is 1, 2 or 3) and by jWidth_dvd_six (the value divides 6). Finally, jWidth_map asserts invariance under change of field: for any ring homomorphism f : K \to L of fields and any j \in K one has \mathrm{jWidth}(f(j)) = \mathrm{jWidth}(j), which uses that such an f is injective and carries the numeral 1728 to 1728.

Relation to Mathlib

Mathlib has no such function; it is the project's own numerical bookkeeping device, a bare case distinction on an element of a field with decidable equality.

Where it is used

The function records, for a j-invariant in characteristic 0 or \geq 5, the weight \tfrac12\,\#\mathrm{Aut}(E) of an elliptic curve E with j(E)=j over an algebraically closed field, the quantity that also measures the thickness of the corresponding supersingular point on a modular curve in characteristic p. It is used throughout the project as the numerical weight attached to a j-invariant in such statements.

References

  1. J. H. Silverman, The Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 106, Springer, 1986, III.10.1
  2. B. Mazur, Modular curves and the Eisenstein ideal, Publications Mathématiques de l'IHÉS 47 (1977), 33–186, appendix with M. Rapoport
  3. P. Deligne and M. Rapoport, Les schémas de modules de courbes elliptiques, in: Modular Functions of One Variable II, Lecture Notes in Mathematics 349, Springer, 1973, 143–316

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

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

set_option autoImplicit false

namespace ModularCurve

def jWidth {K : Type*} [Field K] [DecidableEq K] (j : K) : ℕ :=
  if j = 0 then 3 else if j = 1728 then 2 else 1

variable {K : Type*} [Field K] [DecidableEq K]

theorem jWidth_of_eq_zero {j : K} (h : j = 0) : jWidth j = 3 := by simp [jWidth, h]

theorem jWidth_of_eq_1728 {j : K} (h : j = 1728) (h0 : j ≠ 0) : jWidth j = 2 := by
  subst h; simp [jWidth, h0]

theorem jWidth_of_ne {j : K} (h0 : j ≠ 0) (h1728 : j ≠ 1728) : jWidth j = 1 := by
  simp [jWidth, h0, h1728]

theorem jWidth_eq_ite (j : K) :
    jWidth j = (if j = 0 then 3 else if j = 1728 then 2 else 1) := rfl

theorem jWidth_pos (j : K) : 0 < jWidth j := by
  unfold jWidth; split_ifs <;> decide

theorem jWidth_eq_one_or (j : K) : jWidth j = 1 ∨ jWidth j = 2 ∨ jWidth j = 3 := by
  unfold jWidth; split_ifs <;> simp

theorem jWidth_dvd_six (j : K) : jWidth j ∣ 6 := by
  unfold jWidth; split_ifs <;> decide

theorem jWidth_map {L : Type*} [Field L] [DecidableEq L] (f : K →+* L) (j : K) :
    jWidth (f j) = jWidth j := by
  have h1728 : f 1728 = (1728 : L) := map_ofNat f 1728
  unfold jWidth
  by_cases hj0 : j = 0
  · subst hj0; simp
  · have hne : f j ≠ 0 := (map_ne_zero_iff f f.injective).mpr hj0
    rw [if_neg hj0, if_neg hne]
    by_cases hj : j = 1728
    · have hfj : f j = 1728 := by rw [hj, h1728]
      rw [if_pos hj, if_pos hfj]
    · have hfj : f j ≠ 1728 := fun h => hj (f.injective (h.trans h1728.symm))
      rw [if_neg hj, if_neg hfj]

end ModularCurve

Statements phrased using this module (107)