Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_LambdaModularPolynomialData.lean

definition module

Level-two modular polynomial data for the lambda series

This module introduces the structure ModularCurve.LambdaModularPolynomialData q, for a natural number q with NeZero q, which bundles a presentation of the modular equation relating the \lambda-series in the variable \mathfrak q to the same series in \mathfrak q^{q}. An element of the structure consists of a bivariate integral polynomial \Psi, formalised as an element \Psi \in (\mathbb Z[X])[Y], together with three fields that are themselves theorems about it: \Psi is monic (in Y), its degree in Y equals q+1, and it vanishes on the pair of \lambda-expansions.

The vanishing condition is stated as an identity in the Laurent series field \mathbb Q((\mathfrak q)) (Hahn series over \mathbb Z with rational coefficients). The outer variable Y is sent to lambdaNModC ℚ q, that is to the image of the integral series lambdaInt in \mathbb Q((\mathfrak q)) followed by the substitution \mathfrak q \mapsto \mathfrak q^{q} given by qExpand; the coefficients, elements of \mathbb Z[X], are evaluated by the ring homomorphism evalAtLambdaInt, which substitutes X \mapsto lambdaInt in \mathbb Z((\mathfrak q)), followed by the coefficientwise map \mathbb Z \to \mathbb Q. Here lambdaInt is the integral Laurent series \mathfrak q \prod_{n \ge 1} (1-\mathfrak q^{n})^{8}\,(1-\mathfrak q^{4n})^{16}\,(1-\mathfrak q^{2n})^{-24}, the eta quotient \eta(\tau)^{8}\eta(4\tau)^{16}\eta(2\tau)^{-24}, the normalised Hauptmodul \lambda/16 for the level-two structure.

Thus the structure is a predicate-carrying datum on a chosen polynomial, not an existence assertion: nothing here produces such a \Psi, and no symmetry or congruence property is imposed. It is the level-two counterpart of ModularPolynomialData N, in which j replaces \lambda and the degree q+1 is replaced by the Dedekind \psi-function.

Relation to Mathlib

Mathlib has no notion of modular polynomial or of the \lambda (or j) q-expansion; the structure is the project's own, built on Mathlib's Hahn/Laurent series and polynomial API. It is parallel in shape to the project's ModularPolynomialData for the j-series.

Where it is used

Data of this kind record, in purely formal q-expansion terms, that the \lambda-expansion at level q is integral of degree q+1 over the one at level 1; together with the associated congruence modulo q (of Kronecker type, as for the j-series packets) they are the input used to study the function fields generated by such expansions in the modular-curve part of the development.

References

  1. S. Lang, Elliptic Functions, 2nd ed., Graduate Texts in Mathematics 112, Springer, 1987
  2. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Publications of the Mathematical Society of Japan 11, Princeton University Press, 1971

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_LambdaSeries

set_option autoImplicit false

noncomputable section

namespace ModularCurve

structure LambdaModularPolynomialData (q : ℕ) [NeZero q] : Type where

  Ψ : Polynomial (Polynomial ℤ)
  monic : Ψ.Monic
  natDegree_eq : Ψ.natDegree = q + 1

  eval_eq_zero : Ψ.eval₂ ((laurentMap (Int.castRingHom ℚ)).comp evalAtLambdaInt) (lambdaNModC ℚ q) = 0

end ModularCurve

end

Statements phrased using this module (16)