Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_LegendreJ.lean

definition module

The -invariant of the Legendre curve as a rational function

This module introduces a single total function. For a field K and an element t \in K, ModularCurve.legendreJ t is the element 2^{8}\,\frac{(t^{2}-t+1)^{3}}{t^{2}\,(t-1)^{2}} \in K, written exactly as that quotient of polynomial expressions in t. Classically this is the j-invariant of the Legendre curve E_t : y^{2} = x(x-1)(x-t), equivalently of the Weierstrass model y^{2} = x^{3} - (1+t)x^{2} + t x, so that t \mapsto legendreJ t is the degree-six map from the \lambda-line to the j-line, invariant under the six substitutions t,\ 1-t,\ 1/t,\ 1/(1-t),\ t/(t-1),\ (t-1)/t.

The definition is made for an arbitrary field, with no hypothesis on t and no hypothesis on the characteristic; it is a formula, not an assertion about a curve. Since division in a Lean field is total with x/0 = 0, the value at the two points t = 0 and t = 1, where the cubic x(x-1)(x-t) acquires a double root and the Legendre curve degenerates, is 0 by that convention and carries no geometric meaning. Accordingly, results about legendreJ elsewhere in the development are stated under the hypotheses t \neq 0 and t \neq 1, which also make the denominator invertible.

Relation to Mathlib

Mathlib provides the j-invariant of a Weierstrass curve, but no dedicated function for the Legendre family; ModularCurve.legendreJ is the project's own abbreviation for the rational expression in the parameter.

Where it is used

The \lambda-to-j map is used to parametrise j-invariants of elliptic curves together with a chosen 2-torsion structure, in particular to identify the supersingular j-invariants in characteristic p as the images under legendreJ of the roots of the Deuring polynomial, which in turn feeds the mass formula for supersingular points.

References

  1. J. H. Silverman, The Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 106, Springer, 1986, III.1
  2. R. Hartshorne, Algebraic Geometry, Graduate Texts in Mathematics 52, Springer, 1977, IV.4
  3. M. Deuring, Die Typen der Multiplikatorenringe elliptischer Funktionenkörper, Abh. Math. Sem. Univ. Hamburg 14 (1941), 197–272

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

Declarations

Source

import Mathlib

set_option autoImplicit false

namespace ModularCurve

def legendreJ {K : Type*} [Field K] (t : K) : K :=
  2 ^ 8 * (t ^ 2 - t + 1) ^ 3 / (t ^ 2 * (t - 1) ^ 2)

end ModularCurve

Statements phrased using this module (14)